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

Marko Topolnik marko at hazelcast.com
Thu Mar 19 15:34:06 EDT 2015


Your fallacy is in assuming total sync order as a part of the
happens-before consistency. It is not. JLS 17.4.5:

"A set of actions A is happens-before consistent if for all reads r in A,
where W(r) is the write action seen by r, it is not the case that either
hb(r, W(r)) or that there exists a write w in A such that w.v = r.v and
hb(W(r), w) and hb(w, r)."

"In a happens-before consistent set of actions, each read sees a write that
it is allowed to see by the happens-before ordering."

That's all there is to it, and my diagram clearly satisfies this
definition. Now, you may argue that the happens-before order is itself
constrained by the total sync order, but before you do that I urge you to
consider lazySet(). This method's semantics are exactly that of a volatile
write which is exempted from the total sync order. In its presence the
incidental correspondence between sync order and happens-before order
breaks.

---
Marko

On Thu, Mar 19, 2015 at 7:32 PM, Oleksandr Otenko <
oleksandr.otenko at oracle.com> wrote:
>
> 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> 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/055d8e16/attachment.html>


More information about the Concurrency-interest mailing list