[concurrency-interest] What can an incorrectly synchronized read see?

Alex Otenko oleksandr.otenko at gmail.com
Thu Sep 29 08:16:00 EDT 2016


Sure. I do mean “statements that got executed”.

The “enumerate all possible outcomes” approach can work for other cases - CAS succeeded or not; lock acquired or not; pointer set or not (even then you’d need a method to model ABA). But integer counters are more complex than that, and need a sound method of extending the enumeration of a few outcomes to all integers.


> On 29 Sep 2016, at 09:05, Aleksey Shipilev <shade at redhat.com> wrote:
> 
> 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.

Sure, in the end it will have to rely on the same postulates to extend the conclusion to all integers - that’s all the postulates we can use, no magic there. I am just pointing out that the method does not tell us how we can jump from “this works for 0 and 1” to “this works for all integers”.

“pattern” is not part of JMM, so something else is needed.

Say, is (3,1) allowed? Now you need to look at R->W->W->W, W->R->W->W, W->W->R->W, W->W->W->R, provide a method of determining these are the only cases we need to consider (say, why W->W->W->R->W is irrelevant), and provide a method of reducing them to the previously considered cases before we can conclude that “everything else is the extension”.


I am not trying to say there is no way to do that (although I wouldn’t approach the problem that way), or that “enumerate all possible outcomes” is not practical - after all, that’s the only automated validation we have - I am merely pointing out that it is not a rigorous proof for the general question posed, and sweeps important details under the carpet.


Alex


> 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:
> 
> Thread 1:
>  if (false) // more complicated predicate in real-life case, of course
>    y = 1
>  sync(this) {
>    w = 1
>  }
> 
> Thread 2:
>  sync(this) {
>    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 [1],
> and it does not help that we keep perpetuating it with inaccurate claims
> on public lists.
> 
> Thanks,
> -Aleksey
> 
> [1]
> https://shipilev.net/blog/2016/close-encounters-of-jmm-kind/#wishful-all-my-hb
> 



More information about the Concurrency-interest mailing list