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

--===============0633839133676993129==
Content-Type: multipart/alternative; boundary="000000000000c47ef905c96a15fd"

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

Yes, you are right, it's more nuanced. I didn't use this intuition in
earnest.

Alex

On Fri, 13 Aug 2021, 05:02 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
>>
>>

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

<div dir=3D"auto">Yes, you are right, it&#39;s more nuanced. I didn&#39;t u=
se this intuition in earnest.<div dir=3D"auto"><br></div><div dir=3D"auto">=
Alex</div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gm=
ail_attr">On Fri, 13 Aug 2021, 05:02 Peter Veentjer, &lt;<a href=3D"mailto:=
[email protected]">[email protected]</a>&gt; wrote:<br></div><block=
quote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px #ccc=
 solid;padding-left:1ex"><div dir=3D"ltr"><a class=3D"gmail_plusreply" id=
=3D"m_48113149820028421plusReplyChip-0" href=3D"mailto:oleksandr.otenko@gma=
il.com" target=3D"_blank" rel=3D"noreferrer">@Alex Otenko</a><div><br></div=
><div> I think there is a problem with the approach.</div><div><br></div><d=
iv>The SO is a total order over all synchronization actions that is consist=
ent with PO. So it shouldn&#39;t happen 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 fo=
llowing 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>And these to =
writes are opaque writes, than in the PO A-&gt;B, but in the synchronizatio=
n 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 co=
uld violate the SO being consistent with PO.<br><br><br></div></div><br><di=
v class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, Aug 1=
2, 2021 at 11:43 AM Shuyang Liu &lt;<a href=3D"mailto:[email protected]" t=
arget=3D"_blank" rel=3D"noreferrer">[email protected]</a>&gt; 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"auto"><di=
v 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/3360568" target=3D"_b=
lank" rel=3D"noreferrer">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" rel=3D"noreferrer">concurrency-interest@c=
s.oswego.edu</a>&gt; wrote:<br><br></blockquote></div><blockquote type=3D"c=
ite"><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 sensible approa=
ch. <br><br></div><div>I need to think about this.<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 Thu, Aug 12, 2021 at 11:14 AM Alex =
Otenko &lt;<a href=3D"mailto:[email protected]" target=3D"_blank" =
rel=3D"noreferrer">[email protected]</a>&gt; wrote:<br></div><bloc=
kquote 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"auto">I treat opaq=
ue read/write as part of SO, but which do not introduce SW edges - no trans=
itive closure of program orders. They observe each other, because SO specif=
ies who is before who.<div dir=3D"auto"><br></div><div dir=3D"auto">Then ac=
quire/ release introduce corresponding 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><br><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]=
.edu" target=3D"_blank" rel=3D"noreferrer">[email protected]=
du</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margi=
n: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 ha=
ppens-before (HB) order is defined using:<br><br></div>Synchronization orde=
r (SO): total order over all synchronization actions.<br><br></div>Synchron=
izes with order (SW): a sub order of the SO that only orders e.g. a volatil=
e 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 question is how do =
relaxed access modes like opaque and acquire/release fit into the HB?<br><b=
r></div>Let&#39;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 wil=
l order loads/stores to different addresses which is not desirable. So I gu=
ess the logical solution would 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 t=
he problem that an opaque read/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 r=
unning into a similar problem with the acquire/release. Traditionally they =
are called synchronization actions since a release-store will prevent any o=
lder load/store to be reordered with the release-store and acquire-load wil=
l prevent any later load/store to be reordered with the acquire-load. So th=
ey provide some level of=C2=A0 &#39;synchronization&#39;; but is this suffi=
cient 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></div><div>Or could it be th=
at 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 nor=
eferrer" target=3D"_blank">[email protected]</a><br>
<a href=3D"http://cs.oswego.edu/mailman/listinfo/concurrency-interest" rel=
=3D"noreferrer noreferrer noreferrer" target=3D"_blank">http://cs.oswego.ed=
u/mailman/listinfo/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" rel=3D"noreferrer">Concurrency-in=
[email protected]</a></span><br><span><a href=3D"http://cs.oswego.edu/ma=
ilman/listinfo/concurrency-interest" target=3D"_blank" rel=3D"noreferrer">h=
ttp://cs.oswego.edu/mailman/listinfo/concurrency-interest</a></span><br></d=
iv></blockquote></div></blockquote></div>
</blockquote></div>

--000000000000c47ef905c96a15fd--

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

--===============0633839133676993129==--