<div dir="ltr"><div>Hi, all</div>I read a test named SB+rfionceonce-poonceonces in tools/memory-model/litmus-tests like this<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">P0(int *x, int *y)<br>{<br>        int r1;<br>        int r2;<br><br>        WRITE_ONCE(*x, 1);<br>        r1 = READ_ONCE(*x);<br>        r2 = READ_ONCE(*y);<br>}<br><br>P1(int *x, int *y)<br>{<br>        int r3;<br>        int r4;<br><br>        WRITE_ONCE(*y, 1);<br>        r3 = READ_ONCE(*y);<br>        r4 = READ_ONCE(*x);<br>}<br><br>locations [0:r1; 1:r3; x; y] (* Debug aid: Print things not in "exists". *)<br>exists (0:r2=0 /\ 1:r4=0)<br></blockquote><div>The comment says </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">This litmus test demonstrates that LKMM is not fully multicopy atomic.</blockquote><div> I understand why 0:r2=0 /\ 1:r4=0 is possible:  r2 = READ_ONCE(*y); executes before WRITE_ONCE(*x, 1); in P0 and r4 = READ_ONCE(*x); executes before WRITE_ONCE(*y, 1); in P1. But I don't understand why this test is suffice to "demonstrates that LKMM is not fully multicopy atomic". I got the definition of multicopy atomic in ARM's documentation, which says </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">in a multiprocessing system, if one observer observes a write to memory because of a store-release operation, then all observers observe it.<br></blockquote><div>As far as I understand it, this litmus test wants to know if P0 and P1 can observe the value change of x and y at the same time. More specifically, after P1 executed WRITE_ONCE(*x, 1) and r1 got new value 1, we want to know if P1 can also observe the new value of x. But there is no guarantee that r4 = READ_ONCE(*x); has been executed.</div><div><br></div><div>Given that "All store-release operations are multi-copy atomic" in Arm, I designed a assembly code version of this litmus test, like this</div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">{<br>0:X1=x; 0:X4=y;<br>1:X1=y; 1:X4=x;<br>}<br> P0           | P1           ;<br> MOV W0,#1    | MOV W0,#1    ;<br> STLR W0,[X1] | STLR W0,[X1] ;<br> LDR W2,[X1]  | LDR W2,[X1]  ;<br> LDR W3,[X4]  | LDR W3,[X4]  ;<br>locations [0:X2; 1:X2; x; y]<br>exists (0:X3=0 /\ 1:X3=0)<br></blockquote><div>If STLR provide multicopy atomic, and this test can confirm it, we should't get the (0:X3=0 /\ 1:X3=0)  and the test result show that (0:X3=0 /\ 1:X3=0) do exists. </div><div><br></div><div>So, why this test can "demonstrates that LKMM is not fully multicopy atomic"? And did I misunderstand something?</div><div><br></div><div>Thanks in advance.</div><div>Zhang Zeren</div></div>