Re: How do relaxed access modes like opaque/acquire/release fit into the happens-before order.
SHUYANG LIU via Concurrency-interest <[email protected]> Thu, 12 Aug 2021 21:48:13 -0700
| Newsgroups | gmane.comp.java.jsr.166-concurrency |
|---|---|
| Message-ID | <CABsauHMQWEjN315Lth3YkfVGi8+TWErBmyR_kNpZZ_mu7K-dwg@mail.gmail.com> |
--===============1092842955889695454== Content-Type: multipart/alternative; boundary="000000000000cadac305c9698f8a" --000000000000cadac305c9698f8a Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable We are certainly working toward that goal :) Best, Shuyang On Thu, Aug 12, 2021 at 9:40 PM Peter Veentjer <[email protected]> wrote: > Thanks Shuyang, > > I'll check out the paper. > > Is the plan that this new model is going to replace the happens-before > model? > > Regards, > > Peter. > > On Fri, Aug 13, 2021 at 7:02 AM Peter Veentjer <[email protected]> > wrote: > >> @Alex Otenko <[email protected]> >> >> I think there is a problem with the approach. >> >> The SO is a total order over all synchronization actions that is >> consistent with PO. So it shouldn't happen that e.g. in the PO you have >> A->B and in the SO you have B->A. >> >> Let's assume the following program: >> >> CPU1: >> A=3D1 >> B=3D1 >> >> And these to writes are opaque writes, than in the PO A->B, but in the >> synchronization order A is not ordered before B because opaque creates a >> total order over the loads/stores if a single address (coherence), but w= ill >> not order loads/stores of different addresses. So if opaque would be par= t >> of the SO, it could violate the SO being consistent with PO. >> >> >> >> On Thu, Aug 12, 2021 at 11:43 AM Shuyang Liu <[email protected]> wrote: >> >>> Our group had a paper in 2019 formalizing the access modes in Java: >>> https://dl.acm.org/doi/10.1145/3360568 >>> (Note that there was a small problem on the semantics of volatile. In >>> particular, one should use either leading or trailing fence insertion >>> scheme consistently for volatile reads and writes, instead of mixing th= em. >>> We have fixed it but still in the process of publishing it) >>> >>> In our model, we did not use the happens-before approach anymore. >>> Instead we formalized it in terms of visibility order. (Details can be >>> found in the paper). >>> >>> In general, opaque mode accesses do not preserve program orders for >>> accesses to different locations. They do, however, follows the coherenc= e >>> rules. The release-acquire mode accesses preserves program orders but n= ot >>> necessarily global orders. This has to do with the non-MCA nature of th= e >>> Power architecture that it compiles to. You might find it strange that >>> there is no sw order for release-acquire mode in our model. This is bec= ause >>> we simplified the cumulative effect of lwsync and hwsync using rf while= not >>> considering fr (we have proved the compilation is correct in our on-goi= ng >>> paper) and x86 and ARMv8 are MCA. Finally, there is a total order among >>> volatile accesses when they carry out =E2=80=9Cpush=E2=80=9D orders emu= lating the effect of >>> full fences. >>> >>> The formal definition of data race is defined in terms of sw order >>> though: a pair of accesses is said to form a race if they are 1) >>> conflicting, and 2) not ordered by happens-before. We use the conventio= nal >>> definition for happens before, which is (po | sw)+ (the transitive clos= ure >>> of the union of program order and synchronizes-with), where sw is defin= ed >>> as the reads-from order from a release write to an acquire read. >>> >>> One last thing, in our formal model, opaque reads preserves the local >>> program order. But this is purely a work-around to prevent out-of-thin-= air >>> results. As a consequence, this requires the compiler to yield a =E2=80= =9Cfake=E2=80=9D >>> dependency after each read instruction, which is not true in practice. >>> >>> Hope this helps! >>> >>> Best Regards, >>> Shuyang >>> >>> On Aug 12, 2021, at 1:18 AM, Peter Veentjer via Concurrency-interest < >>> [email protected]> wrote: >>> >>> =EF=BB=BF >>> Hi Alex, >>> >>> Thanks for your answer. That sounds like a very sensible approach. >>> >>> I need to think about this. >>> >>> Regards, >>> >>> Peter. >>> >>> On Thu, Aug 12, 2021 at 11:14 AM Alex Otenko <[email protected]= m> >>> wrote: >>> >>>> I treat opaque read/write as part of SO, but which do not introduce SW >>>> edges - no transitive closure of program orders. They observe each oth= er, >>>> because SO specifies who is before who. >>>> >>>> Then acquire/ release introduce corresponding parts of transitive >>>> closure. In the end volatile load/store are just that. >>>> >>>> Alex >>>> >>>> On Thu, 12 Aug 2021, 08:52 Peter Veentjer via Concurrency-interest, < >>>> [email protected]> wrote: >>>> >>>>> The happens-before (HB) order is defined using: >>>>> >>>>> Synchronization order (SO): total order over all synchronization >>>>> actions. >>>>> >>>>> Synchronizes with order (SW): a sub order of the SO that only orders >>>>> e.g. a volatile write of X with all subsequent volatile reads of X. >>>>> >>>>> Program Order (PO): a partial order that orders all memory actions >>>>> issued by a single CPU. >>>>> >>>>> And the HB relation is defined as the transitive closure of the union >>>>> of the SW and PO. >>>>> >>>>> My question is how do relaxed access modes like opaque and >>>>> acquire/release fit into the HB? >>>>> >>>>> Let's start with opaque; is an opaque write/read part of the SO? If >>>>> so, then it will be part of the SW and HB. And because of this, it wi= ll >>>>> order loads/stores to different addresses which is not desirable. So = I >>>>> guess the logical solution would be that an opaque read/write is not = part >>>>> of the SO and hence we don't get this problem. However now we have t= he >>>>> problem that an opaque read/write is not ordered by the HB and we hav= e a >>>>> data race (read will still be hb-consistent). >>>>> >>>>> I'm running into a similar problem with the acquire/release. >>>>> Traditionally they are called synchronization actions since a release= -store >>>>> will prevent any older load/store to be reordered with the release-st= ore >>>>> and acquire-load will prevent any later load/store to be reordered wi= th the >>>>> acquire-load. So they provide some level of 'synchronization'; but i= s this >>>>> sufficient for them to be part of the SO order? Or are they excluded = from >>>>> the SO and we end up with a data-race? >>>>> >>>>> Or could it be that the happens-before model isn't a suitable model t= o >>>>> deal with relaxed access modes? >>>>> >>>>> Regards, >>>>> >>>>> Peter. >>>>> >>>>> >>>>> >>>>> >>>>> _______________________________________________ >>>>> Concurrency-interest mailing list >>>>> [email protected] >>>>> http://cs.oswego.edu/mailman/listinfo/concurrency-interest >>>>> >>>> _______________________________________________ >>> Concurrency-interest mailing list >>> [email protected] >>> http://cs.oswego.edu/mailman/listinfo/concurrency-interest >>> >>> --000000000000cadac305c9698f8a Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"auto">We are certainly working toward that goal :)=C2=A0</div><= div dir=3D"auto"><br></div><div dir=3D"auto">Best,</div><div dir=3D"auto">S= huyang=C2=A0</div><div><br><div class=3D"gmail_quote"><div dir=3D"ltr" clas= s=3D"gmail_attr">On Thu, Aug 12, 2021 at 9:40 PM Peter Veentjer <<a href= =3D"mailto:[email protected]">[email protected]</a>> wrote:<br><= /div><blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-le= ft:1px #ccc solid;padding-left:1ex"><div dir=3D"ltr"><div>Thanks Shuyang,</= div><div><br></div><div>I'll check out the paper. <br></div><div><br></= div><div>Is the plan that this new model is going to replace the happens-be= fore model?<br><br></div><div>Regards,<br><br></div><div>Peter.<br></div></= div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On= Fri, Aug 13, 2021 at 7:02 AM Peter Veentjer <<a href=3D"mailto:alarmnum= [email protected]" target=3D"_blank">[email protected]</a>> wrote:<br></= div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;bor= der-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><a c= lass=3D"gmail_plusreply" id=3D"m_-1601774322362320366gmail-m_-8537544308755= 243141plusReplyChip-0" href=3D"mailto:[email protected]" target=3D= "_blank">@Alex Otenko</a><div><br></div><div> I think there is a problem wi= th the approach.</div><div><br></div><div>The SO is a total order over all = synchronization actions that is consistent with PO. So it shouldn't hap= pen that e.g. in the PO you have A->B and in the SO you have B->A.<br= ><br></div><div>Let's assume the following program:<br><br></div><div>C= PU1:<br></div><div>=C2=A0=C2=A0=C2=A0 A=3D1<br></div><div>=C2=A0=C2=A0=C2= =A0 B=3D1<br><br></div><div>And these to writes are opaque writes, than in = the PO A->B, but in the synchronization order A is not ordered before B = because opaque creates a total order over the loads/stores if a single addr= ess (coherence), but will not order loads/stores of different addresses. So= if opaque would be part of the SO, it could violate the SO being consisten= t with PO.<br><br><br></div></div><br><div class=3D"gmail_quote"><div dir= =3D"ltr" class=3D"gmail_attr">On Thu, Aug 12, 2021 at 11:43 AM Shuyang Liu = <<a href=3D"mailto:[email protected]" target=3D"_blank">[email protected].= edu</a>> wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"marg= in:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1e= x"><div dir=3D"auto"><div dir=3D"ltr">Our group had a paper in 2019 formali= zing the access modes in Java:=C2=A0<a href=3D"https://dl.acm.org/doi/10.11= 45/3360568" target=3D"_blank">https://dl.acm.org/doi/10.1145/3360568</a><di= v>(Note that there was a small problem on the semantics of volatile. In par= ticular, one should use either leading or trailing fence insertion scheme c= onsistently for volatile reads and writes, instead of mixing them. We have = fixed it but still in the process of publishing it)=C2=A0</div><div><br></d= iv><div>In our model, we did not use the happens-before approach anymore. I= nstead we formalized it in terms of visibility order. (Details can be found= in the paper).</div><div><br></div><div>In general, opaque mode accesses d= o not preserve program orders for accesses to different locations. They do,= however, follows the coherence rules. The release-acquire mode accesses pr= eserves program orders but not necessarily global orders. This has to do wi= th the non-MCA nature of the Power architecture that it compiles to. You mi= ght find it strange that there is no sw order for release-acquire mode in o= ur model. This is because we simplified the cumulative effect of lwsync and= hwsync using rf while not considering fr (we have proved the compilation i= s correct in our on-going paper) and x86 and ARMv8 are MCA. Finally, there = is a total order among volatile accesses when they carry out =E2=80=9Cpush= =E2=80=9D orders emulating the effect of full fences.=C2=A0</div><div><br><= /div><div>The formal definition of data race is defined in terms of sw orde= r though: a pair of accesses is said to form a race if they are 1) conflict= ing, and 2) not ordered by happens-before. We use the conventional definiti= on for happens before, which is (po | sw)+ (the transitive closure of the u= nion of program order and synchronizes-with), where sw is defined as the re= ads-from order from a release write to an acquire read.=C2=A0</div><div><br= ></div><div>One last thing, in our formal model, opaque reads preserves the= local program order. But this is purely a work-around to prevent out-of-th= in-air results. As a consequence, this requires the compiler to yield a =E2= =80=9Cfake=E2=80=9D dependency after each read instruction, which is not tr= ue in practice.=C2=A0</div><div><br></div><div>Hope this helps!</div><div><= br><div dir=3D"ltr">Best Regards,<br><div>Shuyang</div></div></div></div><d= iv dir=3D"ltr"><br><blockquote type=3D"cite">On Aug 12, 2021, at 1:18 AM, P= eter Veentjer via Concurrency-interest <<a href=3D"mailto:concurrency-in= [email protected]" target=3D"_blank">[email protected]<= /a>> wrote:<br><br></blockquote></div><blockquote type=3D"cite"><div dir= =3D"ltr">=EF=BB=BF<div dir=3D"ltr"><div>Hi Alex,</div><div><br></div><div>T= hanks for your answer. That sounds like a very sensible approach. <br><br><= /div><div>I need to think about this.<br><br></div><div>Regards,<br><br></d= iv><div>Peter.<br></div></div><br><div class=3D"gmail_quote"><div dir=3D"lt= r" class=3D"gmail_attr">On Thu, Aug 12, 2021 at 11:14 AM Alex Otenko <<a= href=3D"mailto:[email protected]" target=3D"_blank">oleksandr.ote= [email protected]</a>> wrote:<br></div><blockquote class=3D"gmail_quote" sty= le=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);paddi= ng-left:1ex"><div dir=3D"auto">I treat opaque read/write as part of SO, but= which do not introduce SW edges - no transitive closure of program orders.= They observe each other, because SO specifies who is before who.<div dir= =3D"auto"><br></div><div dir=3D"auto">Then acquire/ release introduce corre= sponding parts of transitive closure. In the end volatile load/store are ju= st that.<br><div dir=3D"auto"><br></div><div dir=3D"auto">Alex</div></div><= /div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">O= n Thu, 12 Aug 2021, 08:52 Peter Veentjer via Concurrency-interest, <<a h= ref=3D"mailto:[email protected]" target=3D"_blank">concurr= [email protected]</a>> wrote:<br></div><blockquote class=3D"gm= ail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,= 204,204);padding-left:1ex"><div dir=3D"ltr"><div><div><div><div><div><div><= div><div><div><div>The happens-before (HB) order is defined using:<br><br><= /div>Synchronization order (SO): total order over all synchronization actio= ns.<br><br></div>Synchronizes with order (SW): a sub order of the SO that o= nly orders e.g. a volatile write of X with all subsequent volatile reads of= X.<br><br></div>Program Order (PO): a partial order that=C2=A0 orders all = memory actions issued by a single CPU.<br><br></div>And the HB relation is = defined as the transitive closure of the union of the SW and PO.<br><br></d= iv>My question is how do relaxed access modes like opaque and acquire/relea= se fit into the HB?<br><br></div>Let's start with opaque; is an opaque = write/read part of the SO? If so, then it will be part of the SW and HB. An= d because of this, it will order loads/stores to different addresses which = is not desirable. So I guess the logical solution would be that an opaque r= ead/write is not part of the SO and hence we don't get this problem.=C2= =A0 However now we have the problem that an opaque read/write is not ordere= d by the HB and we have a data race (read will still be hb-consistent).<br>= </div><br></div>I'm running into a similar problem with the acquire/rel= ease. Traditionally they are called synchronization actions since a release= -store will prevent any older load/store to be reordered with the release-s= tore and acquire-load will prevent any later load/store to be reordered wit= h the acquire-load. So they provide some level of=C2=A0 'synchronizatio= n'; but is this sufficient for them to be part of the SO order? Or are = they excluded from the SO and we end up with a data-race?</div><div><br></d= iv><div>Or could it be that the happens-before model isn't a suitable m= odel to deal with relaxed access modes?<br></div><div><br></div>Regards,<br= ><br></div>Peter.<br><div><div><br><br><div><div><div><br><br></div></div><= /div></div></div></div> _______________________________________________<br> Concurrency-interest mailing list<br> <a href=3D"mailto:[email protected]" rel=3D"noreferrer" ta= rget=3D"_blank">[email protected]</a><br> <a href=3D"http://cs.oswego.edu/mailman/listinfo/concurrency-interest" rel= =3D"noreferrer noreferrer" target=3D"_blank">http://cs.oswego.edu/mailman/l= istinfo/concurrency-interest</a><br> </blockquote></div> </blockquote></div> <span>_______________________________________________</span><br><span>Concu= rrency-interest mailing list</span><br><span><a href=3D"mailto:Concurrency-= [email protected]" target=3D"_blank">[email protected]= u</a></span><br><span><a href=3D"http://cs.oswego.edu/mailman/listinfo/conc= urrency-interest" target=3D"_blank">http://cs.oswego.edu/mailman/listinfo/c= oncurrency-interest</a></span><br></div></blockquote></div></blockquote></d= iv> </blockquote></div> </blockquote></div></div> --000000000000cadac305c9698f8a-- --===============1092842955889695454== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline _______________________________________________ Concurrency-interest mailing list [email protected] http://cs.oswego.edu/mailman/listinfo/concurrency-interest --===============1092842955889695454==--