Re: How do relaxed access modes like opaque/acquire/release fit into the happens-before order.

--===============8796474791128817217==
Content-Type: multipart/alternative; boundary="000000000000ad9d2305c968ea7b"

--000000000000ad9d2305c968ea7b
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

@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 will
not order loads/stores of different addresses. So if opaque would be part
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 them=
.
> 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 t=
he
> paper).
>
> In general, opaque mode accesses do not preserve program orders for
> accesses to different locations. They do, however, follows the coherence
> rules. The release-acquire mode accesses preserves program orders but not
> necessarily global orders. This has to do with the non-MCA nature of the
> 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 becau=
se
> we simplified the cumulative effect of lwsync and hwsync using rf while n=
ot
> considering fr (we have proved the compilation is 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 emula=
ting 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 conventional definition for
> happens before, which is (po | sw)+ (the transitive closure of the union =
of
> program order and synchronizes-with), where sw is defined as the reads-fr=
om
> 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-ai=
r
> 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]>
> 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 other=
,
>> 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 action=
s.
>>>
>>> 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 o=
f
>>> 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 will ord=
er
>>> 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 the problem t=
hat
>>> an opaque read/write is not ordered by the HB and we have 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-s=
tore
>>> will prevent any older load/store to be reordered with the release-stor=
e
>>> and acquire-load will prevent any later load/store to be reordered with=
 the
>>> acquire-load. So they provide some level of  'synchronization'; but is =
this
>>> sufficient for them to be part of the SO order? Or are they excluded fr=
om
>>> the SO and we end up with a data-race?
>>>
>>> Or could it be that the happens-before model isn't a suitable model to
>>> 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
>
>

--000000000000ad9d2305c968ea7b
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><a class=3D"gmail_plusreply" id=3D"plusReplyChip-0" href=
=3D"mailto:[email protected]" tabindex=3D"-1">@Alex Otenko</a><div=
><br></div><div> I think there is a problem with the approach.</div><div><b=
r></div><div>The SO is a total order over all synchronization actions that =
is consistent with PO. So it shouldn&#39;t happen that e.g. in the PO you h=
ave A-&gt;B and in the SO you have B-&gt;A.<br><br></div><div>Let&#39;s ass=
ume the following program:<br><br></div><div>CPU1:<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>An=
d these to writes are opaque writes, than in the PO A-&gt;B, but in the syn=
chronization order A is not ordered before B because opaque creates a total=
 order over the loads/stores if a single address (coherence), but will not =
order loads/stores of different addresses. So if opaque would be part of th=
e SO, it could violate the SO being consistent 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 &lt;<a href=3D"mailto:sliu44@cs.=
ucla.edu">[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"g=
mail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204=
,204,204);padding-left:1ex"><div dir=3D"auto"><div dir=3D"ltr">Our group ha=
d a paper in 2019 formalizing the access modes in Java:=C2=A0<a href=3D"htt=
ps://dl.acm.org/doi/10.1145/3360568" target=3D"_blank">https://dl.acm.org/d=
oi/10.1145/3360568</a><div>(Note that there was a small problem on the sema=
ntics of volatile. In particular, one should use either leading or trailing=
 fence insertion scheme consistently 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></div><div>In our model, we did not use the happens-b=
efore approach anymore. Instead we formalized it in terms of visibility ord=
er. (Details can be found in the paper).</div><div><br></div><div>In genera=
l, opaque mode accesses do not preserve program orders for accesses to diff=
erent locations. They do, however, follows the coherence rules. The release=
-acquire mode accesses preserves program orders but not necessarily global =
orders. This has to do with the non-MCA nature of the Power architecture th=
at it compiles to. You might find it strange that there is no sw order for =
release-acquire mode in our model. This is because we simplified the cumula=
tive effect of lwsync and hwsync using rf while not considering fr (we have=
 proved the compilation is 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 fence=
s.=C2=A0</div><div><br></div><div>The formal definition of data race is def=
ined 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 t=
he conventional definition for happens before, which is (po | sw)+ (the tra=
nsitive closure of the union of program order and synchronizes-with), where=
 sw is defined as the reads-from order from a release write to an acquire r=
ead.=C2=A0</div><div><br></div><div>One last thing, in our formal model, op=
aque reads preserves the local program order. But this is purely a work-aro=
und 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 inst=
ruction, which is not true 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><div dir=3D"ltr"><br><blockquote type=3D"cite">On Aug=
 12, 2021, at 1:18 AM, Peter Veentjer via Concurrency-interest &lt;<a href=
=3D"mailto:[email protected]" target=3D"_blank">concurrenc=
[email protected]</a>&gt; wrote:<br><br></blockquote></div><blockquo=
te type=3D"cite"><div dir=3D"ltr">=EF=BB=BF<div dir=3D"ltr"><div>Hi Alex,</=
div><div><br></div><div>Thanks for your answer. That sounds like a very sen=
sible approach. <br><br></div><div>I need to think about this.<br><br></div=
><div>Regards,<br><br></div><div>Peter.<br></div></div><br><div class=3D"gm=
ail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, Aug 12, 2021 at 11=
:14 AM Alex Otenko &lt;<a href=3D"mailto:[email protected]" target=
=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquote =
class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px sol=
id rgb(204,204,204);padding-left:1ex"><div dir=3D"auto">I treat opaque read=
/write as part of SO, but which do not introduce SW edges - no transitive c=
losure 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 corresponding parts of transitive closure. In the end vol=
atile load/store are just 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">On Thu, 12 Aug 2021, 08:52 Peter Veentjer via Concurr=
ency-interest, &lt;<a href=3D"mailto:[email protected]" ta=
rget=3D"_blank">[email protected]</a>&gt; wrote:<br></div>=
<blockquote class=3D"gmail_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><di=
v><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 al=
l synchronization actions.<br><br></div>Synchronizes with order (SW): a sub=
 order of the SO that only orders e.g. a volatile write of X with all subse=
quent 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 th=
e SW and PO.<br><br></div>My question is how do relaxed access modes like o=
paque and acquire/release fit into the HB?<br><br></div>Let&#39;s start wit=
h opaque; is an opaque write/read part of the SO? If so, then it will be pa=
rt of the SW and HB. And because of this, it will order loads/stores to dif=
ferent addresses which is not desirable. So I guess the logical solution wo=
uld be that an opaque read/write is not part of the SO and hence we don&#39=
;t get this problem.=C2=A0 However now we have the problem that an opaque r=
ead/write is not ordered by the HB and we have a data race (read will still=
 be hb-consistent).<br></div><br></div>I&#39;m running into a similar probl=
em with the acquire/release. Traditionally they are called synchronization =
actions since a release-store will prevent any older load/store to be reord=
ered with the release-store and acquire-load will prevent any later load/st=
ore to be reordered with the acquire-load. So they provide some level of=C2=
=A0 &#39;synchronization&#39;; but is this sufficient for them to be part o=
f the SO order? Or are they excluded from the SO and we end up with a data-=
race?</div><div><br></div><div>Or could it be that the happens-before model=
 isn&#39;t a suitable model to deal with relaxed access modes?<br></div><di=
v><br></div>Regards,<br><br></div>Peter.<br><div><div><br><br><div><div><di=
v><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>

--000000000000ad9d2305c968ea7b--

--===============8796474791128817217==
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

--===============8796474791128817217==--