[concurrency-interest] Enforcing total sync order on modern hardware
Oleksandr Otenko
oleksandr.otenko at oracle.com
Thu Mar 19 14:32:09 EDT 2015
Looking from another angle, you have claimed it is "happens-before
consistent" without showing that you have found */all/* happens-before
edges.
I have explained why there definitely is another happens-before edge. I
can provide another constructive proof, if it will look easier:
Suppose, Rwt6 observed T6 and not T9. Suppose, Wv1 appears after Rv0 in
synchronization order, so Rv0 sees the write of Wv0, and does not see
Wv1. Then Rwt6 appears after Rrt9 and T9 in synchronization order, and
Rwt6 must observe T9, not T6 - contradiction. Thus by contradiction the
two assumptions cannot exist together. Placing Rwt6 after T9 or Wv1
before Rv0 exposes existence of one more happens-before edge, which is
not on the diagram. Therefore, if we assume Rwt6 sees T6 and not T9,
then Rv0 sees Wv1.
Alex
On 19/03/2015 18:14, Oleksandr Otenko wrote:
> No, you don't need Rv1'.
>
> No, happens-before consistency is not the only rule for correctness of
> the outcome. The "read must see the last write it synchronizes-with"
> is also part of the rule set. You must either show the proof that Wv1
> appears after Rv0, or accept Wv1 appears before Rv0 in synchronization
> order.
>
> Alex
>
> On 19/03/2015 18:02, Marko Topolnik wrote:
>>
>>
>> On Thu, Mar 19, 2015 at 6:07 PM, Oleksandr Otenko
>> <oleksandr.otenko at oracle.com <mailto:oleksandr.otenko at oracle.com>> wrote:
>>
>> Your scenario is exactly IRIW.
>>
>> T9 is x=1
>> Wv1 is y=1
>> Rrt9 is r0=x
>> Rv0 is r1=y
>>
>> T6 is initial x=0
>>
>> Rwt6 is a constraint that you want to consider only total orders
>> with y=1 preceding x=1
>> It is equivalent to the independent reader thread doing r2=y,
>> then r3=x, and observing r2==1, r3==0. That is, you have
>> reformulated IRIW in such a way so that we consider only one
>> specific outcome, not all possible outcomes.
>>
>>
>> No, for a correct analogy to IRIW you need to introduce an Rv1'
>> between Wv1 and Rwt6.
>>
>> Now,
>>
>> T9 is x=1
>> Wv1 is y=1
>> Rrt9 is r0=x
>> Rv0 is r1=y
>> Rv1' is r2=y
>> Rwt6 is r3=x
>>
>> Now we can clearly see that the JMM does not allow (r0,r1,r2,r3) =
>> (1,0,1,0) even though this is a happens before-consistent result. In
>> other words, JMM gives this the exact same treatment as in IRIW.
>> However, on a low level there is a key difference in that it involves
>> the store buffers in the timing, and does it asymetrically, just for
>> one of the two reading threads. This variation is potentially more
>> interesting because it is specifically excluded from the guarantees
>> of the Intel specification. Therefore it is harder to meet by the JIT
>> compiler.
>>
>> T1:
>> x=1
>>
>> T2:
>> y=1
>>
>> T3:
>> r0=x;
>> r1=y;
>>
>> T4:
>> r2=y;
>> r3=x;
>>
>> JMM forbids the outcome (r0,r1,r2,r3) = (1,0,1,0) - ie one thread
>> thinking x=1 happened before y=1, the other thread thinking y=1
>> happened before x=1.
>>
>>
>> ---
>> Marko
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20150319/ea8fe9d4/attachment-0001.html>
More information about the Concurrency-interest
mailing list