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

--===============3614634901970939246==
Content-Type: multipart/alternative; boundary="0000000000003256db05c96b71c9"

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

Hi Shuyang,

Is it ok to ask for clarifications here?

I am confused by co_0 and co going in opposite directions in the diagrams,
but the text claims co_0 are treated just like other co. Doesn't that
introduce cycles?..

Alex

On Thu, 12 Aug 2021, 09:43 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
>
>

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

<div dir=3D"auto">Hi Shuyang,=C2=A0<div dir=3D"auto"><br></div><div dir=3D"=
auto">Is it ok to ask for clarifications here?</div><div dir=3D"auto"><br><=
/div><div dir=3D"auto">I am confused by co_0 and co going in opposite direc=
tions in the diagrams, but the text claims co_0 are treated just like other=
 co. Doesn&#39;t that introduce cycles?..</div><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"gmail_attr">On Thu, 12 Aug 2021, 09:43 Shuyang Liu, &lt;<=
a href=3D"mailto:[email protected]">[email protected]</a>&gt; 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"auto"><div dir=3D"ltr">Our =
group had a paper in 2019 formalizing the access modes in Java:=C2=A0<a hre=
f=3D"https://dl.acm.org/doi/10.1145/3360568" target=3D"_blank" rel=3D"noref=
errer">https://dl.acm.org/doi/10.1145/3360568</a><div>(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 volatil=
e reads and writes, instead of mixing them. We have fixed it but still in t=
he process of publishing it)=C2=A0</div><div><br></div><div>In our model, w=
e did not use the happens-before approach anymore. Instead we formalized it=
 in terms of visibility order. (Details can be found in the paper).</div><d=
iv><br></div><div>In general, opaque mode accesses do not preserve program =
orders for accesses to different locations. They do, however, follows the c=
oherence rules. The release-acquire mode accesses preserves program orders =
but not necessarily global orders. This has to do with the non-MCA nature o=
f the Power architecture that it compiles to. You might find it strange tha=
t 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 =
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 emulati=
ng the effect of full fences.=C2=A0</div><div><br></div><div>The formal def=
inition of data race is defined in terms of sw order though: a pair of acce=
sses 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, w=
hich is (po | sw)+ (the transitive closure of the union of program order an=
d synchronizes-with), where sw is defined as the reads-from order from a re=
lease write to an acquire read.=C2=A0</div><div><br></div><div>One last thi=
ng, in our formal model, opaque reads preserves the local program order. Bu=
t this is purely a work-around to prevent out-of-thin-air results. As a con=
sequence, this requires the compiler to yield a =E2=80=9Cfake=E2=80=9D depe=
ndency after each read instruction, which is not true in practice.=C2=A0</d=
iv><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><bloc=
kquote type=3D"cite">On Aug 12, 2021, at 1:18 AM, Peter Veentjer via Concur=
rency-interest &lt;<a href=3D"mailto:[email protected]" ta=
rget=3D"_blank" rel=3D"noreferrer">[email protected]</a>&g=
t; wrote:<br><br></blockquote></div><blockquote type=3D"cite"><div dir=3D"l=
tr">=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><d=
iv>Peter.<br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" cl=
ass=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><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"auto">I treat opaque read/write as p=
art of SO, but which do not introduce SW edges - no transitive closure of p=
rogram 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 int=
roduce 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"g=
mail_attr">On Thu, 12 Aug 2021, 08:52 Peter Veentjer via Concurrency-intere=
st, &lt;<a href=3D"mailto:[email protected]" target=3D"_bl=
ank" rel=3D"noreferrer">[email protected]</a>&gt; wrote:<b=
r></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><div><div><div><div><div><div><div><div><div>The happens-before (HB) o=
rder is defined using:<br><br></div>Synchronization order (SO): total order=
 over all 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 a=
ll subsequent volatile reads of X.<br><br></div>Program Order (PO): a parti=
al order that=C2=A0 orders all memory actions issued by a single CPU.<br><b=
r></div>And the HB relation is defined as the transitive closure of the uni=
on of the SW and PO.<br><br></div>My question is how do relaxed access mode=
s like opaque and acquire/release fit into the HB?<br><br></div>Let&#39;s s=
tart with opaque; is an opaque write/read part of the SO? If so, then it wi=
ll be part of the SW and HB. And because of this, it will order loads/store=
s to different addresses which is not desirable. So I guess the logical sol=
ution 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 the problem that an =
opaque read/write is not ordered by the HB and we have a data race (read wi=
ll still be hb-consistent).<br></div><br></div>I&#39;m running into a simil=
ar problem with the acquire/release. Traditionally they are called synchron=
ization actions since a release-store will prevent any older load/store to =
be reordered with the release-store and acquire-load will prevent any later=
 load/store to be reordered with the acquire-load. So they provide some lev=
el of=C2=A0 &#39;synchronization&#39;; but is this sufficient for them to b=
e 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 that the happens-befo=
re 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>

--0000000000003256db05c96b71c9--

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

--===============3614634901970939246==--