This commit adds a litmus test suggested by Alan Stern that is forbidden on multicopy atomic systems, but allowed on non-multicopy atomic systems. Note that other-multicopy atomic systems are examples of non-multicopy atomic systems. Suggested-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx> Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx> --- .../litmus-tests/SB+poonceoncescoh.litmus | 31 ++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus diff --git a/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus b/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus new file mode 100644 index 000000000000..991a2d6dec63 --- /dev/null +++ b/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus @@ -0,0 +1,31 @@ +C SB+poonceoncescoh + +(* + * Result: Sometimes + * + * This litmus test demonstrates that LKMM is not multicopy atomic. + *) + +{} + +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); +} + +exists (0:r2=0 /\ 1:r4=0 /\ 0:r1=1 /\ 1:r3=1) -- 2.5.2