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

--===============6602269216354690753==
Content-Type: multipart/alternative; boundary="0000000000006854b105c96c4327"

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

Ok, re-reading it today it is clear those were counterexamples.

But what is trace order? The definition says a total order of all memory
accesses. Does this include plain accesses? Or is it all accesses
considered thus far - opaque, ra, volatile?

Alex

On Fri, 13 Aug 2021, 08:02 Alex Otenko, <[email protected]> wrote:

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

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

<div dir=3D"auto">Ok, re-reading it today it is clear those were counterexa=
mples.<div dir=3D"auto"><br></div><div dir=3D"auto">But what is trace order=
? The definition says a total order of all memory accesses. Does this inclu=
de plain accesses? Or is it all accesses considered thus far - opaque, ra, =
volatile?<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 Fri, 13 Aug 2021, 08:02 Alex Otenko, &lt;<a href=3D"mailto:oleksandr.ote=
[email protected]">[email protected]</a>&gt; wrote:<br></div><blockquo=
te class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px #ccc so=
lid;padding-left:1ex"><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 g=
oing in opposite directions in the diagrams, but the text claims co_0 are t=
reated just like other co. Doesn&#39;t that introduce cycles?..</div><div d=
ir=3D"auto"><br></div><div dir=3D"auto">Alex</div></div><br><div class=3D"g=
mail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, 12 Aug 2021, 09:4=
3 Shuyang Liu, &lt;<a href=3D"mailto:[email protected]" target=3D"_blank" =
rel=3D"noreferrer">[email protected]</a>&gt; wrote:<br></div><blockquote c=
lass=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left: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 href=3D"https://dl.ac=
m.org/doi/10.1145/3360568" rel=3D"noreferrer noreferrer" target=3D"_blank">=
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 volatile reads=
 and writes, instead of mixing them. We have fixed it but still in the proc=
ess of publishing it)=C2=A0</div><div><br></div><div>In our model, we did n=
ot use the happens-before approach anymore. Instead we formalized it in ter=
ms of visibility order. (Details can be found in the paper).</div><div><br>=
</div><div>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 not=
 necessarily global orders. This has to do with the non-MCA nature of the P=
ower 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 because we s=
implified the cumulative effect of lwsync and hwsync using rf while not con=
sidering fr (we have proved the compilation is correct in our on-going pape=
r) and x86 and ARMv8 are MCA. Finally, there is a total order among volatil=
e 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 though: a pair of accesses is=
 said to form a race if they are 1) conflicting, and 2) not ordered by happ=
ens-before. We use the conventional definition for happens before, which is=
 (po | sw)+ (the transitive closure of the union of program order and synch=
ronizes-with), where sw is defined as the reads-from order from a release w=
rite 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 consequenc=
e, this requires the compiler to yield a =E2=80=9Cfake=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><div dir=3D"ltr">Best Regard=
s,<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-i=
nterest &lt;<a href=3D"mailto:[email protected]" rel=3D"no=
referrer noreferrer" target=3D"_blank">[email protected]</=
a>&gt; 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 &lt;<a=
 href=3D"mailto:[email protected]" rel=3D"noreferrer noreferrer" t=
arget=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockq=
uote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1p=
x solid 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 transit=
ive closure of program orders. They observe each other, because SO specifie=
s who is before who.<div dir=3D"auto"><br></div><div dir=3D"auto">Then acqu=
ire/ release introduce corresponding parts of transitive closure. In the en=
d volatile load/store are just that.<br><div dir=3D"auto"><br></div><div di=
r=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 Co=
ncurrency-interest, &lt;<a href=3D"mailto:[email protected]=
u" rel=3D"noreferrer noreferrer" target=3D"_blank">concurrency-interest@cs.=
oswego.edu</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><div><div><div><div><div><div><div><div><d=
iv>The happens-before (HB) order is defined using:<br><br></div>Synchroniza=
tion 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 all subsequent volatile reads of X.<br><br></div=
>Program Order (PO): a partial order that=C2=A0 orders all memory actions i=
ssued by a single CPU.<br><br></div>And the HB relation is defined as the t=
ransitive closure of the union of the SW and PO.<br><br></div>My question i=
s 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/read part =
of the SO? If so, then it will be part of the SW and HB. And because of thi=
s, it will 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&#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 will still be hb-consistent).<br></div><br></div>=
I&#39;m running into a similar problem with the acquire/release. Traditiona=
lly they are called synchronization actions since a release-store will prev=
ent 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-lo=
ad. So they provide some level of=C2=A0 &#39;synchronization&#39;; but is t=
his 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?</div><div><br></div><div>Or could=
 it be that the happens-before model isn&#39;t a suitable model to deal wit=
h 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 noreferrer" target=3D"_blank">[email protected]</a=
><br>
<a href=3D"http://cs.oswego.edu/mailman/listinfo/concurrency-interest" rel=
=3D"noreferrer noreferrer noreferrer noreferrer" target=3D"_blank">http://c=
s.oswego.edu/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]" rel=3D"noreferrer noreferrer" target=3D"_blank">Con=
[email protected]</a></span><br><span><a href=3D"http://cs.os=
wego.edu/mailman/listinfo/concurrency-interest" rel=3D"noreferrer noreferre=
r" target=3D"_blank">http://cs.oswego.edu/mailman/listinfo/concurrency-inte=
rest</a></span><br></div></blockquote></div></blockquote></div>
</blockquote></div>

--0000000000006854b105c96c4327--

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

--===============6602269216354690753==--