[concurrency-interest] What can an incorrectly synchronized read see?
shade at redhat.com
Thu Sep 29 04:05:10 EDT 2016
On 09/29/2016 09:13 AM, Alex Otenko wrote:
> You need to be careful about using a “proof by example” as a proof. It
> is ok to use it to demonstrate what happens to two reads of two writes,
> but it is not a proof about *all* reads and *all* writes.
> It is not as formal as it looks. How do you conclude it is sufficient to
> consider just two diagrams? How do you conclude it is sufficient to
> consider just four outcomes?
If you look closely, my proof basically shows the same properties you
picked: actions that happened-before lock acquisition in one thread
cannot see the updates happening in after lock acquisition in another
thread. For the same reason your interpretation uses -- the total
ordering of locks/unlocks, plus transitivity -- we are free to only look
for two cases of relative sequencing of Reader and Writer, either R->W,
or W->R, and everything else is the extension of these two basic patterns.
But I would be very, very careful with interpretations that talk about
statements, and not the program actions with the actual values observed.
Because this is subtly broken: "All statements in program order before a
lock release happen-before any statements that are in program order
after the lock acquires following that lock release"
Statements do not form a program order. Program order is total, and
statements are not forming total order (easy example: control flow split
at conditionals). As stated, in this example:
if (false) // more complicated predicate in real-life case, of course
y = 1
w = 1
r1 = w;
r2 = y;
...your interpretation says the "statement" y=1 happens-before r2=y,
which mandates seeing (r1, r2) = (1, 1), which is obviously incorrect.
This is an easy mistake that everyone makes when talking about JMM ,
and it does not help that we keep perpetuating it with inaccurate claims
on public lists.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the Concurrency-interest