Nice to @Share?

[Neal Gafter]

On Tue, Feb 23, 2010 at 4:11 PM, Doug Lea <dl at cs.oswego.edu> wrote:
> The only way we know to phrase a usable memory ordering spec
> entails distinguishing variables that CANNOT be shared
> across threads from those that happen not to be
> shared in a given program execution. There is nothing
> especially Java-ish about this. Specs for other languages
> and processors take the same form -- we must be able to
> describe states strictly from the point of view of
> a given processor/thread, unconditionally with respect
> to possible multithreaded program executions.

You keep saying that you only know how to do it with an extra axiom,
and that others do it that way too, but in fact (1) The Java spec does
not have the axiom you require, and (2) The guarantees for other
"shared" variables serve precisely the purpose you need for local
variables.  There, now you know how to do it.

>>>> Final variables have guarantees in the memory model too.
>>>
>>> Weaker and messier ones.
>>
>> Weaker and messier than what?
>
> Than those for local variables. For example, if
> "this" leaks in a constructor, a reader might see
> pre-initialized values of a final field. So to
> verify some property of a use of a final field
> of some object, you must know something about
> its constructor. In contrast, properties of
> local variables are unconditional.

Right, because local variables cannot leak before they are
initialized; the definite assignment rules ensure that, and so you
don't need to know anything more about the code that initializes them.
 The stronger property for local variables that you require falls out
of the general rules for shared variables coupled with the definite
assignment rules for locals.  No separate axioms are required, nor are
any stronger guarantees currently in the spec.

Cheers,
Neal