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

--===============1785519127843295146==
Content-Type: multipart/alternative; boundary="0000000000005761af05c9697202"

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

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 wi=
ll
> 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 the=
m.
>> We have fixed it but still in the process of publishing it)
>>
>> In our model, we did not use the happens-before approach anymore. Instea=
d
>> 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 coherence
>> rules. The release-acquire mode accesses preserves program orders but no=
t
>> 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 beca=
use
>> 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-goin=
g
>> 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 emul=
ating 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 convention=
al
>> definition for happens before, which is (po | sw)+ (the transitive closu=
re
>> of the union of program order and synchronizes-with), where sw is define=
d
>> 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-a=
ir
>> 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 othe=
r,
>>> 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 will or=
der
>>>> 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 =
that
>>>> 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-=
store
>>>> will prevent any older load/store to be reordered with the release-sto=
re
>>>> and acquire-load will prevent any later load/store to be reordered wit=
h 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 f=
rom
>>>> 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
>>
>>

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

<div dir=3D"ltr"><div>Thanks Shuyang,</div><div><br></div><div>I&#39;ll che=
ck out the paper. <br></div><div><br></div><div>Is the plan that this new m=
odel is going to replace the happens-before model?<br><br></div><div>Regard=
s,<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 &lt;<a href=3D"mailto:[email protected]">[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"><a class=3D"gmail_plusreply" id=3D"gmail-m_-85375443087552=
43141plusReplyChip-0" href=3D"mailto:[email protected]" target=3D"=
_blank">@Alex Otenko</a><div><br></div><div> I think there is a problem wit=
h the approach.</div><div><br></div><div>The SO is a total order over all s=
ynchronization actions that is consistent with PO. So it shouldn&#39;t happ=
en that e.g. in the PO you have A-&gt;B and in the SO you have B-&gt;A.<br>=
<br></div><div>Let&#39;s assume the following program:<br><br></div><div>CP=
U1:<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-&gt;B, but in the synchronization order A is not ordered before B bec=
ause 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 w=
ith PO.<br><br><br></div></div><br><div class=3D"gmail_quote"><div dir=3D"l=
tr" class=3D"gmail_attr">On Thu, Aug 12, 2021 at 11:43 AM Shuyang Liu &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:0p=
x 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><d=
iv dir=3D"auto"><div dir=3D"ltr">Our group had a paper in 2019 formalizing =
the access modes in Java:=C2=A0<a href=3D"https://dl.acm.org/doi/10.1145/33=
60568" target=3D"_blank">https://dl.acm.org/doi/10.1145/3360568</a><div>(No=
te that there was a small problem on the semantics of volatile. In particul=
ar, one should use either leading or trailing fence insertion scheme consis=
tently 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><d=
iv>In our model, we did not use the happens-before approach anymore. Instea=
d we formalized it in terms of visibility order. (Details can be found in t=
he paper).</div><div><br></div><div>In general, opaque mode accesses do not=
 preserve program orders for accesses to different locations. They do, howe=
ver, follows the coherence rules. The release-acquire mode accesses preserv=
es program orders but not necessarily global orders. This has to do with th=
e non-MCA nature of the Power architecture that it compiles to. You might f=
ind it strange that there is no sw order for release-acquire mode in our mo=
del. This is because we simplified the cumulative effect of lwsync and hwsy=
nc using rf while not considering fr (we have proved the compilation is cor=
rect 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 order thou=
gh: a pair of accesses is said to form a race if they are 1) conflicting, a=
nd 2) not ordered by happens-before. We use the conventional definition for=
 happens before, which is (po | sw)+ (the transitive closure of the union o=
f program order and synchronizes-with), where sw is defined as the reads-fr=
om 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-thin-air=
 results. As a consequence, this requires the compiler to yield a =E2=80=9C=
fake=E2=80=9D dependency after each read instruction, which is not true in =
practice.=C2=A0</div><div><br></div><div>Hope this helps!</div><div><br><di=
v 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 V=
eentjer via Concurrency-interest &lt;<a href=3D"mailto:concurrency-interest=
@cs.oswego.edu" target=3D"_blank">[email protected]</a>&gt=
; wrote:<br><br></blockquote></div><blockquote type=3D"cite"><div dir=3D"lt=
r">=EF=BB=BF<div dir=3D"ltr"><div>Hi Alex,</div><div><br></div><div>Thanks =
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></div><di=
v>Peter.<br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" cla=
ss=3D"gmail_attr">On Thu, Aug 12, 2021 at 11:14 AM Alex Otenko &lt;<a href=
=3D"mailto:[email protected]" target=3D"_blank">oleksandr.otenko@g=
mail.com</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-le=
ft:1ex"><div dir=3D"auto">I treat opaque read/write as part of SO, but whic=
h 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"aut=
o"><br></div><div dir=3D"auto">Then acquire/ release introduce correspondin=
g parts of transitive closure. In the end volatile load/store are just that=
.<br><div dir=3D"auto"><br></div><div dir=3D"auto">Alex</div></div></div><b=
r><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, =
12 Aug 2021, 08:52 Peter Veentjer via Concurrency-interest, &lt;<a href=3D"=
mailto:[email protected]" target=3D"_blank">concurrency-in=
[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quo=
te" 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><di=
v><div><div>The happens-before (HB) order is defined using:<br><br></div>Sy=
nchronization order (SO): total order over all synchronization actions.<br>=
<br></div>Synchronizes with order (SW): a sub order of the SO that only ord=
ers 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></div>My q=
uestion is how do relaxed access modes like opaque and acquire/release fit =
into the HB?<br><br></div>Let&#39;s start with opaque; is an opaque write/r=
ead part of the SO? If so, then it will be part of the SW and HB. And becau=
se 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 read/wri=
te is not part of the SO and hence we don&#39;t get this problem.=C2=A0 How=
ever now we have the problem that an opaque read/write is not ordered by th=
e HB and we have a data race (read will still be hb-consistent).<br></div><=
br></div>I&#39;m running into a similar problem with the acquire/release. T=
raditionally they are called synchronization actions since a release-store =
will prevent any older load/store to be reordered with the release-store an=
d acquire-load will prevent any later load/store to be reordered with the a=
cquire-load. So they provide some level of=C2=A0 &#39;synchronization&#39;;=
 but is this sufficient for them to be part of the SO order? Or are they ex=
cluded 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><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>

--0000000000005761af05c9697202--

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

--===============1785519127843295146==--