RFR(M): 8029101: PPC64 (part 211): ordering of Independent Reads of Independent Writes

[Aleksey Shipilev]

TL;DR: Finals are special, we all get that. But there are other possible
scenarios to achieve the same effect, which is the direct consequence of
the usual JMM rules. You need to subsume the entire JMM along with
happens-before and commit order to understand the issue. I have posted
the more rigorous explanation to c-i@ here:

http://cs.oswego.edu/pipermail/concurrency-interest/2013-November/011951.html

I will just make a few remarks here, where it belongs:

On 11/27/2013 02:56 AM, David Holmes wrote:
> A fundamental abstraction in the JMM is the happens-before relation.
> There is nothing in the JMM that requires that #2 happens-before #3.

Yeah, you can call happens-before the fundamental abstraction in JMM,
but happens-before is not the only thing that defines valid executions.
Another thing is commit order and causality, and there are provisions
beyond happens-before which are in play here. If I to cite the spec,
there is a huge paragraph describing how happens-before is not enough to
gain the causality guarantees JMM is after.

The specific part that defines how to commit the trace to check if it is
valid is at play here. The complete semantics of JMM lie within JLS
17.4.{6-8}, which *use* happens-before as the important part in figuring
whether the execution is well-formed or not.

The proof sketch follows exactly the JMM *as spec-ed*: we construct the
possible traces and show that one is committable (the one which yields
42), and another one is not (the one which yields 0). Please, please try
to understand that reasoning instead of ballooning up to the comfortable
but useless-here abstractions like reorderings and happens-before.

>> I think further discussion about this should be held at c-i@, if you
> 
> No it should be on javamemorymodel-discussion at cs.umd.edu

That's a haunted list. I'm going to use c-i at .

> The JMM is quite clear on the special treatment of only final fields

The JMM is clear on the "special treatment of final fields". It is a
logical error to add "only" there, because it is "denying the
antecedent" in disguise: "If P, then Q; Not P. Therefore, not Q". If
field is final (P) then there is a construction safety (Q). The field is
not final, but volatile (Not P). Therefore, the construction safety is
not gainable (Not Q).

>> Please stop saying "reordering" if you want to answer the advanced JMM
>> question. In JMM terms, you have to ask if there are valid executions
>> which yield the default value for the non-volatile field. It's hard for
>> me to answer this question at this point (sigh).
> 
> Show me a happens-before relation that prohibits the reordering.

(sigh)

We need to talk about the *executions*, not the happens-before orders
alone! There is obviously a race, but the point of my sketch is that the
*only* *committable* execution in the presence of that race is the one
which yields final-field-like semantics! That is *because*
happens-before ordering in another execution is inconsistent with
causality. You can't explain that by happens-before alone, you need to
look into the executions!

>>> If volatile gets same treatment as final, then may as well update
>>> spec/Doug's cookbook to dispel the misconception.
>>
>> I don't think spec needs updating. Cookbook might need the update, but
> 
> Of course the spec would need updating if volatiles are to get the same
> special treatment as final fields!

Same logical mistake, see above. The volatile-in-constructor effect we
are discussing here is the direct consequence of JMM rules as stated. It
is not explicit like with finals, but it is there implicitly in rules.

What really needs adjusting is the people mindset which is locked on the
idea finals are not only special in their effects, but SUPER-special by
disallowing any other means to achieve the same effect.

That's hard to subsume, I know that's hard, because I've been there.
This is not the spec problem. This is arguably the cookbook problem
which is supposed to explain some of the non-trivial things in spec.

-Aleksey.