Hi, all I read a test named SB+rfionceonce-poonceonces in tools/memory-model/litmus-tests like this
P0(int *x, int *y) { int r1; int r2;
WRITE_ONCE(*x, 1); r1 = READ_ONCE(*x); r2 = READ_ONCE(*y); }
P1(int *x, int *y) { int r3; int r4;
WRITE_ONCE(*y, 1); r3 = READ_ONCE(*y); r4 = READ_ONCE(*x); }
locations [0:r1; 1:r3; x; y] (* Debug aid: Print things not in "exists". *) exists (0:r2=0 /\ 1:r4=0)
The comment says
This litmus test demonstrates that LKMM is not fully multicopy atomic.
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
in a multiprocessing system, if one observer observes a write to memory because of a store-release operation, then all observers observe it.
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. Given that "All store-release operations are multi-copy atomic" in Arm, I designed a assembly code version of this litmus test, like this
{ 0:X1=x; 0:X4=y; 1:X1=y; 1:X4=x; } P0 | P1 ; MOV W0,#1 | MOV W0,#1 ; STLR W0,[X1] | STLR W0,[X1] ; LDR W2,[X1] | LDR W2,[X1] ; LDR W3,[X4] | LDR W3,[X4] ; locations [0:X2; 1:X2; x; y] exists (0:X3=0 /\ 1:X3=0)
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. So, why this test can "demonstrates that LKMM is not fully multicopy atomic"? And did I misunderstand something? Thanks in advance. Zhang Zeren