path: root/tools/memory-model/litmus-tests
diff options
authorPaul E. McKenney <paulmck@linux.vnet.ibm.com>2018-07-16 11:05:52 -0700
committerIngo Molnar <mingo@kernel.org>2018-07-17 09:29:29 +0200
commitb464818978d45cd4d78c8f13207891142c68bea9 (patch)
tree5749db3d8c9387f9698fdbb6ef67aa6b9546f6ee /tools/memory-model/litmus-tests
parent52b544bd386688177c41d53e748111c29d0ccc98 (diff)
tools/memory-model: Add litmus test for full multicopy atomicity
This commit adds a litmus test suggested by Alan Stern that is forbidden on fully multicopy atomic systems, but allowed on other-multicopy and on non-multicopy atomic systems. For reference, s390 is fully multicopy atomic, x86 and ARMv8 are other-multicopy atomic, and ARMv7 and powerpc are non-multicopy atomic. Suggested-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Acked-by: Andrea Parri <andrea.parri@amarulasolutions.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180716180605.16115-1-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
Diffstat (limited to 'tools/memory-model/litmus-tests')
2 files changed, 41 insertions, 0 deletions
diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 17eb9a8c222d..00140aaf58b7 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -111,6 +111,15 @@ SB+mbonceonces.litmus
As above, but without the smp_mb() invocations.
+ This litmus test demonstrates that LKMM is not fully multicopy
+ atomic. (Neither is it other multicopy atomic.) This litmus test
+ also demonstrates the "locations" debugging aid, which designates
+ additional registers and locations to be printed out in the dump
+ of final states in the herd7 output. Without the "locations"
+ statement, only those registers and locations mentioned in the
+ "exists" clause will be printed.
As below, but without the smp_wmb() and acquire load.
diff --git a/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
new file mode 100644
index 000000000000..04a16603660b
--- /dev/null
+++ b/tools/memory-model/litmus-tests/SB+rfionceonce-poonceonces.litmus
@@ -0,0 +1,32 @@
+C SB+rfionceonce-poonceonces
+ * Result: Sometimes
+ *
+ * This litmus test demonstrates that LKMM is not fully 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);
+locations [0:r1; 1:r3; x; y] (* Debug aid: Print things not in "exists". *)
+exists (0:r2=0 /\ 1:r4=0)