[concurrency-interest] Enforcing total sync order on modern hardware

Oleksandr Otenko oleksandr.otenko at oracle.com
Thu Mar 19 14:14:58 EDT 2015


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/4bc819e5/attachment.html>


More information about the Concurrency-interest mailing list