Hi, all
I read a test named SB+rfionceonce-poonceonces in tools/memory-model/litmus-tests like thisP0(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
_______________________________________________ Kernelnewbies mailing list Kernelnewbies@xxxxxxxxxxxxxxxxx https://lists.kernelnewbies.org/mailman/listinfo/kernelnewbies
