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

Marko Topolnik marko at hazelcast.com
Fri Mar 20 04:54:40 EDT 2015


You have correctly identified the regulations I had in mind with the
previous post; but perhaps I should spend some more time explaining its
point. The current JMM has the following property:

An action can participate in a synchronizes-with relation if and only if it
occurs in the total synchronization order.

In the new revision of JMM the above property will no longer hold: there
will be actions which participate in synchronizes-with without occurring in
the sync order (lazySet) and actions which occur in the sync order without
participating in synchronizes-with (weakCompareAndSet). These changes will
not, however, change anything in the definition of the happens-before
consistency. Under such a revised model there will be scenarios, such as
the one under discussion here, which preserve happens-before consistency,
but are not accountable for in terms of a total sync order.

So in the post above I referred to the essence of happens-before
consistency without tying it to the additional constraints which the JMM
currently imposes. Leslie Lamport's original idea did not include a total
sync order; in fact, its main point was the absence of such order. An
analogy can be set up where the current JMM is Newtonian (global time
exists) whereas Lamport's model is relativistic (each frame of reference
has its own time). The revised model will allow for some of the original
relativism.

---
Marko

On Thu, Mar 19, 2015 at 9:58 PM, Oleksandr Otenko <
oleksandr.otenko at oracle.com> wrote:

>  No.
>
> 17.4.5. In plain words, happens-before order is a combination of program
> order and synchronizes-with. Then 17.4.4. In plain words, synchronizes-with
> comes from synchronization order: a volatile write synchronizes-with all
> volatile reads (of the same variable) appearing subsequently in
> synchronization order.
>
> So you can't construct a happens-before by ignoring synchronization order.
>
> Alex
>
>
> On 19/03/2015 19:34, Marko Topolnik wrote:
>
> 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/20150320/0f96a728/attachment.html>


More information about the Concurrency-interest mailing list