Jean-Philippe>is a write to value but no read of this value inside the same
thread, so the write is free to be reordered
It ("reordering") does not really matter.
For instance,
17.4.5. Happens-before Order> If the reordering produces results consistent
with a legal execution, it is not illegal.
What matters is the set of possible "writes" that given "read" is allowed
to observe.
In this case, simple transitivity is enough to establish hb.
As Gil highlights, "negations" are a bit hard to deal with, and Mr.Alexey
converts the negations to a positive clauses:
https://shipilev.net/blog/2014/jmm-pragmatics/#_happens_before
Shipilёv> Therefore, in the absence of races, we can only see the latest
write in HB.
Note: we (as programmers) do not really care HOW the runtime and/or CPU
would make that possible. We have guarantees from JVM that "in the absence
of races, we can only see the latest write in HB".
CPU can reorder things and/or execute multiple instructions in parallel. I
don't really need to know the way it is implemented in order to prove that
"CHM is fine to share objects across threads".
Just in case: there are two writes for w.value field.
"write1" is "the write of default value" which "synchronizes-with the first
action in every thread" (see 17.4.4.) + "If an action x synchronizes-with a
following action y, then we also have hb(x, y)." (see 17.4.5)
"write2" is "w.value=42"
"value=0" (write1) happens-before "w.value=42" (write2) by definition
(17.4.4+17.4.5)
w.value=42 happens-before map.put (program order implies happens-before)
read of u.value happens-before map.put (CHM guarantees that)
In other words, "w.value=42" is the latest write in hb order for u.value
read, so u.value must observe 42.
JRE must ensure that the only possible outcome for the program in question
is 42.
Vladimir
--
You received this message because you are subscribed to the Google Groups
"mechanical-sympathy" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
For more options, visit https://groups.google.com/d/optout.
