local refs

[Stephen Weeks]

> > 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.  

OK.  I'll try again.  I'm still not making myself clear.  I intend to
quantify over all uses u, where the label of the block is determined
by the use.  Suppose I write it this way:

multiThreaded: Label.t -> Bool.t
labelOfBlockContaining: Use.t -> Label.t

(forall uses u of x, 
   multiThreaded(labelOfBlockContaining(u)) ==> u is Ref_assign)
or (forall uses u of x
      multiThreaded(labelOfBlockContaining(u)) ==> u is Ref_deref)

That is, all uses of a particular variable in multithreaded blocks are
of the same flavor (Ref_assign or Ref_deref).

This means the same thing to me as what you wrote in

> all uses of x in _all_ blocks with multi-threaded labels are
> Ref_assigns or all are Ref_derefs.

which still seems like a reasonable interpretation of what I
originally wrote

> all uses of x in a block with a multi-threaded label are Ref_assigns
> or all are Ref_derefs.

This does not mean the same thing to me as what you wrote in

> 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}))

this would seem to let different multiThreaded blocks have different
flavors.  I think you want the or outside of two foralls, not the
forall outside of the or.