local refs

[Matthew Fluet]

> > > Ref-flattening rule:
> > > You can flatten a local ref (x = Ref_ref y) if every use is of the
> > > form Ref_assign (x, z) or Ref_deref x and all uses of x in a block
> > > with a multi-threaded label are Ref_assigns or all are Ref_derefs.
> > 
> > I don't buy this at all.
> > 
> > L_A ()
> >   y = Ref_deref x
> >   case x of true => L_A | false => L_C
> > L_B ()
> >   Ref_assign(x, true)
> >   L_B ()
> > 
> > Assume all lables are are multi-threaded.  This satisfies your criteria,
> > but if one thread executes L_A and another thread executes L_B, then we
> > won't get the desired semantics (i.e., L_A busy-waits until L_B releases
> > it).
> 
> This does not satisfy my criteria as I intended them.  There are both
> Ref_derefs and a Ref_assigns in multi-threaded labels.  To be clear,
> the last bit of my condition is
> 
> either forall uses u in block with label l of x, 
>             if l is multi-threaded, then u is Ref_assign
> or forall uses u in block with label l of x, 
>             if l is multi-threaded, then u is Ref_deref
> 
> I hope this is clear.

It's not.  I want some quantification over all blocks -- otherwise, the
above example trivially satisfies your condition: instantiate l with L_A
and choose the second clause.  

If we define

refUses(r,l) : Var.t x Label.t -> 2^Prim.t
multiThreaded: Label.t -> Bool.t

and you mean

forall l in Label.t.
 ((multiThreaded(l) ==> refUses(r, l) = {Ref_deref}) \/
  (multiThreaded(l) ==> refUses(r, l) = {Ref_assign}))

then I agree that the above example does not satisfy the criteria.  I also
think this is in agreement with the later portion of my email.