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

Oleksandr Otenko oleksandr.otenko at oracle.com
Fri Mar 20 12:45:12 EDT 2015


No, that doesn't answer the question. You need to modify how 
happens-before is built - because happens-before in JMM and in some 
other model are two different happens-befores. If you get rid of 
synchronization order, then you need to explain which reads the write 
will or will not synchronize-with.

I am only involved in this discussion because you said it isn't IRIW, 
but I see all signs that it is. I remember the discussion here doubting 
that IRIW should be supported, and I appreciate the arguments, but 
without the specification it is difficult to continue a meaningful 
discussion.


Alex


On 20/03/2015 15:53, Marko Topolnik wrote:
> Exactly, sequential consistency is at the heart of this matter. In 
> Lamport's model it is a non-goal, being replaced by happens-before 
> consistency. This provides a partial order based on causality, as 
> opposed to a total order based on global time. For many practical 
> concerns SC is an overkill and HBC is all you really need to rely on. 
> SC is also associated with a performance cost which is getting ever 
> larger as CPU architectures become more distributed. A reflection of 
> that within Java is the growing need for things like lazySet() which 
> give you happens-before without a strict SC requirement.
>
> So, to directly respond to your remark: my model of consistency is 
> happens-before.
>
> ---
> Marko
>
> On Fri, Mar 20, 2015 at 12:42 PM, Oleksandr Otenko 
> <oleksandr.otenko at oracle.com <mailto:oleksandr.otenko at oracle.com>> wrote:
>
>     Before discussing whether it is an expected result, you'd also
>     need to come up with a model of consistency - if you get rid of
>     all total orders, do you still have a notion of sequential
>     consistency?
>
>     Alex
>
>
>     On 20/03/2015 08:54, Marko Topolnik wrote:
>>     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
>>     <mailto: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
>>>         <mailto: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
>>>         <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/20150320/6f9001fd/attachment-0001.html>


More information about the Concurrency-interest mailing list