litmus test for multicopy atomic

[Zhang Zeren]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.kernelnewbies.org/pipermail/kernelnewbies/attachments/20211105/5cfd67f3/attachment.html>