litmus test for multicopy atomic
zhangzr23 at gmail.com
Fri Nov 5 03:25:23 EDT 2021
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Kernelnewbies