Nice to @Share?

[Neal Gafter]

On Tue, Feb 23, 2010 at 12:20 PM, Doug Lea <dl at cs.oswego.edu> wrote:
>>> One cannot define a processor- or language-level memory
>>> model without reference to a category of variables that are
>>> intrinsically local to a processor/thread.
>>
>> Why not?
>
> Axiomatic locality is needed for the sake of modular
> specification and reasoning. Otherwise memory properties
> could only be validated in the presence of global program
> analyses proving that a variable is only accessed in one
> thread. And given dynamic loading, one cannot in general
> perform global analysis.

In the case of local variables that are *not* accessed within inner
classes or lambdas, or which are declared final, no axioms are
required.  Neither is global analysis required.  Nor is the reasoning
undermined by dynamic loading.  So neither modular specification nor
modular reasoning is undermined by treating locals the same as fields
in the memory model.  The specification would be simpler, and so
reasoning would be simpler.

>>> Of course, the absolute knowledge that a local is in fact
>>> thread-private is critical in implementing many concurrent
>>> algorithms. It is frightening to contemplate how to
>>> program  without this.
>>
>> None of those concurrent algorithms would be undermined in any way by
>> allowing lambdas, or anonymous inner classes, to share local variables
>> from enclosing scopes.
>
> But rarely verifiably or provably so.

Not rarely - always!  Fields that are not used in lambdas or inner
classes are verifiably and provably not shared between threads.  Final
variables have guarantees in the memory model too.  These properties
are locally verifiable and provable always.