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

Oleksandr Otenko oleksandr.otenko at oracle.com
Fri Mar 20 07:42:21 EDT 2015


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/9539873d/attachment-0001.html>


More information about the Concurrency-interest mailing list