summaryrefslogtreecommitdiffstats
path: root/tools/memory-model
diff options
context:
space:
mode:
authorAndrea Parri <andrea.parri@amarulasolutions.com>2018-07-16 14:06:05 -0400
committerIngo Molnar <mingo@kernel.org>2018-07-17 03:30:36 -0400
commit71b7ff5ebc9b1d5aa95eb48d6388234f1304fd19 (patch)
treea4fa218053573b0e3e3fc1801340f77478f916ff /tools/memory-model
parent0fcff1715bec7593a0ba86f3fef46cd89af37a8b (diff)
tools/memory-model: Rename litmus tests to comply to norm7
norm7 produces the 'normalized' name of a litmus test, when the test can be generated from a single cycle that passes through each process exactly once. The commit renames such tests in order to comply to the naming scheme implemented by this tool. Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: Will Deacon <will.deacon@arm.com> Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/20180716180605.16115-14-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
Diffstat (limited to 'tools/memory-model')
-rw-r--r--tools/memory-model/Documentation/recipes.txt8
-rw-r--r--tools/memory-model/README20
-rw-r--r--tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus (renamed from tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus)2
-rw-r--r--tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus (renamed from tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus)2
-rw-r--r--tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus (renamed from tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus)2
-rw-r--r--tools/memory-model/litmus-tests/R+fencembonceonces.litmus (renamed from tools/memory-model/litmus-tests/R+mbonceonces.litmus)2
-rw-r--r--tools/memory-model/litmus-tests/README16
-rw-r--r--tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus (renamed from tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus)2
-rw-r--r--tools/memory-model/litmus-tests/SB+fencembonceonces.litmus (renamed from tools/memory-model/litmus-tests/SB+mbonceonces.litmus)2
-rw-r--r--tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus (renamed from tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus)2
-rw-r--r--tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus (renamed from tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus)2
11 files changed, 30 insertions, 30 deletions
diff --git a/tools/memory-model/Documentation/recipes.txt b/tools/memory-model/Documentation/recipes.txt
index 1fea8ef2b184..af72700cc20a 100644
--- a/tools/memory-model/Documentation/recipes.txt
+++ b/tools/memory-model/Documentation/recipes.txt
@@ -126,7 +126,7 @@ However, it is not necessarily the case that accesses ordered by
126locking will be seen as ordered by CPUs not holding that lock. 126locking will be seen as ordered by CPUs not holding that lock.
127Consider this example: 127Consider this example:
128 128
129 /* See Z6.0+pooncelock+pooncelock+pombonce.litmus. */ 129 /* See Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus. */
130 void CPU0(void) 130 void CPU0(void)
131 { 131 {
132 spin_lock(&mylock); 132 spin_lock(&mylock);
@@ -292,7 +292,7 @@ and to use smp_load_acquire() instead of smp_rmb(). However, the older
292smp_wmb() and smp_rmb() APIs are still heavily used, so it is important 292smp_wmb() and smp_rmb() APIs are still heavily used, so it is important
293to understand their use cases. The general approach is shown below: 293to understand their use cases. The general approach is shown below:
294 294
295 /* See MP+wmbonceonce+rmbonceonce.litmus. */ 295 /* See MP+fencewmbonceonce+fencermbonceonce.litmus. */
296 void CPU0(void) 296 void CPU0(void)
297 { 297 {
298 WRITE_ONCE(x, 1); 298 WRITE_ONCE(x, 1);
@@ -360,7 +360,7 @@ can be seen in the LB+poonceonces.litmus litmus test.
360One way of avoiding the counter-intuitive outcome is through the use of a 360One way of avoiding the counter-intuitive outcome is through the use of a
361control dependency paired with a full memory barrier: 361control dependency paired with a full memory barrier:
362 362
363 /* See LB+ctrlonceonce+mbonceonce.litmus. */ 363 /* See LB+fencembonceonce+ctrlonceonce.litmus. */
364 void CPU0(void) 364 void CPU0(void)
365 { 365 {
366 r0 = READ_ONCE(x); 366 r0 = READ_ONCE(x);
@@ -476,7 +476,7 @@ that one CPU first stores to one variable and then loads from a second,
476while another CPU stores to the second variable and then loads from the 476while another CPU stores to the second variable and then loads from the
477first. Preserving order requires nothing less than full barriers: 477first. Preserving order requires nothing less than full barriers:
478 478
479 /* See SB+mbonceonces.litmus. */ 479 /* See SB+fencembonceonces.litmus. */
480 void CPU0(void) 480 void CPU0(void)
481 { 481 {
482 WRITE_ONCE(x, 1); 482 WRITE_ONCE(x, 1);
diff --git a/tools/memory-model/README b/tools/memory-model/README
index 734f7feaa5dc..ee987ce20aae 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -35,13 +35,13 @@ BASIC USAGE: HERD7
35The memory model is used, in conjunction with "herd7", to exhaustively 35The memory model is used, in conjunction with "herd7", to exhaustively
36explore the state space of small litmus tests. 36explore the state space of small litmus tests.
37 37
38For example, to run SB+mbonceonces.litmus against the memory model: 38For example, to run SB+fencembonceonces.litmus against the memory model:
39 39
40 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+mbonceonces.litmus 40 $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
41 41
42Here is the corresponding output: 42Here is the corresponding output:
43 43
44 Test SB+mbonceonces Allowed 44 Test SB+fencembonceonces Allowed
45 States 3 45 States 3
46 0:r0=0; 1:r0=1; 46 0:r0=0; 1:r0=1;
47 0:r0=1; 1:r0=0; 47 0:r0=1; 1:r0=0;
@@ -50,8 +50,8 @@ Here is the corresponding output:
50 Witnesses 50 Witnesses
51 Positive: 0 Negative: 3 51 Positive: 0 Negative: 3
52 Condition exists (0:r0=0 /\ 1:r0=0) 52 Condition exists (0:r0=0 /\ 1:r0=0)
53 Observation SB+mbonceonces Never 0 3 53 Observation SB+fencembonceonces Never 0 3
54 Time SB+mbonceonces 0.01 54 Time SB+fencembonceonces 0.01
55 Hash=d66d99523e2cac6b06e66f4c995ebb48 55 Hash=d66d99523e2cac6b06e66f4c995ebb48
56 56
57The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that 57The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
@@ -67,16 +67,16 @@ BASIC USAGE: KLITMUS7
67The "klitmus7" tool converts a litmus test into a Linux kernel module, 67The "klitmus7" tool converts a litmus test into a Linux kernel module,
68which may then be loaded and run. 68which may then be loaded and run.
69 69
70For example, to run SB+mbonceonces.litmus against hardware: 70For example, to run SB+fencembonceonces.litmus against hardware:
71 71
72 $ mkdir mymodules 72 $ mkdir mymodules
73 $ klitmus7 -o mymodules litmus-tests/SB+mbonceonces.litmus 73 $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus
74 $ cd mymodules ; make 74 $ cd mymodules ; make
75 $ sudo sh run.sh 75 $ sudo sh run.sh
76 76
77The corresponding output includes: 77The corresponding output includes:
78 78
79 Test SB+mbonceonces Allowed 79 Test SB+fencembonceonces Allowed
80 Histogram (3 states) 80 Histogram (3 states)
81 644580 :>0:r0=1; 1:r0=0; 81 644580 :>0:r0=1; 1:r0=0;
82 644328 :>0:r0=0; 1:r0=1; 82 644328 :>0:r0=0; 1:r0=1;
@@ -86,8 +86,8 @@ The corresponding output includes:
86 Positive: 0, Negative: 2000000 86 Positive: 0, Negative: 2000000
87 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated 87 Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
88 Hash=d66d99523e2cac6b06e66f4c995ebb48 88 Hash=d66d99523e2cac6b06e66f4c995ebb48
89 Observation SB+mbonceonces Never 0 2000000 89 Observation SB+fencembonceonces Never 0 2000000
90 Time SB+mbonceonces 0.16 90 Time SB+fencembonceonces 0.16
91 91
92The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate 92The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate
93that during two million trials, the state specified in this litmus 93that during two million trials, the state specified in this litmus
diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
index 98a3716efa37..e729d2776e89 100644
--- a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus
@@ -1,4 +1,4 @@
1C IRIW+mbonceonces+OnceOnce 1C IRIW+fencembonceonces+OnceOnce
2 2
3(* 3(*
4 * Result: Never 4 * Result: Never
diff --git a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
index de6708229dd1..4727f5aaf03b 100644
--- a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus
@@ -1,4 +1,4 @@
1C LB+ctrlonceonce+mbonceonce 1C LB+fencembonceonce+ctrlonceonce
2 2
3(* 3(*
4 * Result: Never 4 * Result: Never
diff --git a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
index c078f38ff27a..a273da9faa6d 100644
--- a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
@@ -1,4 +1,4 @@
1C MP+wmbonceonce+rmbonceonce 1C MP+fencewmbonceonce+fencermbonceonce
2 2
3(* 3(*
4 * Result: Never 4 * Result: Never
diff --git a/tools/memory-model/litmus-tests/R+mbonceonces.litmus b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
index a0e884ad2132..222a0b850b4a 100644
--- a/tools/memory-model/litmus-tests/R+mbonceonces.litmus
+++ b/tools/memory-model/litmus-tests/R+fencembonceonces.litmus
@@ -1,4 +1,4 @@
1C R+mbonceonces 1C R+fencembonceonces
2 2
3(* 3(*
4 * Result: Never 4 * Result: Never
diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 00140aaf58b7..4581ec2d3c57 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -18,7 +18,7 @@ CoWW+poonceonce.litmus
18 Test of write-write coherence, that is, whether or not two 18 Test of write-write coherence, that is, whether or not two
19 successive writes to the same variable are ordered. 19 successive writes to the same variable are ordered.
20 20
21IRIW+mbonceonces+OnceOnce.litmus 21IRIW+fencembonceonces+OnceOnce.litmus
22 Test of independent reads from independent writes with smp_mb() 22 Test of independent reads from independent writes with smp_mb()
23 between each pairs of reads. In other words, is smp_mb() 23 between each pairs of reads. In other words, is smp_mb()
24 sufficient to cause two different reading processes to agree on 24 sufficient to cause two different reading processes to agree on
@@ -47,7 +47,7 @@ ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus
47 Can a release-acquire chain order a prior store against 47 Can a release-acquire chain order a prior store against
48 a later load? 48 a later load?
49 49
50LB+ctrlonceonce+mbonceonce.litmus 50LB+fencembonceonce+ctrlonceonce.litmus
51 Does a control dependency and an smp_mb() suffice for the 51 Does a control dependency and an smp_mb() suffice for the
52 load-buffering litmus test, where each process reads from one 52 load-buffering litmus test, where each process reads from one
53 of two variables then writes to the other? 53 of two variables then writes to the other?
@@ -88,14 +88,14 @@ MP+porevlocks.litmus
88 As below, but with the first access of the writer process 88 As below, but with the first access of the writer process
89 and the second access of reader process protected by a lock. 89 and the second access of reader process protected by a lock.
90 90
91MP+wmbonceonce+rmbonceonce.litmus 91MP+fencewmbonceonce+fencermbonceonce.litmus
92 Does a smp_wmb() (between the stores) and an smp_rmb() (between 92 Does a smp_wmb() (between the stores) and an smp_rmb() (between
93 the loads) suffice for the message-passing litmus test, where one 93 the loads) suffice for the message-passing litmus test, where one
94 process writes data and then a flag, and the other process reads 94 process writes data and then a flag, and the other process reads
95 the flag and then the data. (This is similar to the ISA2 tests, 95 the flag and then the data. (This is similar to the ISA2 tests,
96 but with two processes instead of three.) 96 but with two processes instead of three.)
97 97
98R+mbonceonces.litmus 98R+fencembonceonces.litmus
99 This is the fully ordered (via smp_mb()) version of one of 99 This is the fully ordered (via smp_mb()) version of one of
100 the classic counterintuitive litmus tests that illustrates the 100 the classic counterintuitive litmus tests that illustrates the
101 effects of store propagation delays. 101 effects of store propagation delays.
@@ -103,7 +103,7 @@ R+mbonceonces.litmus
103R+poonceonces.litmus 103R+poonceonces.litmus
104 As above, but without the smp_mb() invocations. 104 As above, but without the smp_mb() invocations.
105 105
106SB+mbonceonces.litmus 106SB+fencembonceonces.litmus
107 This is the fully ordered (again, via smp_mb() version of store 107 This is the fully ordered (again, via smp_mb() version of store
108 buffering, which forms the core of Dekker's mutual-exclusion 108 buffering, which forms the core of Dekker's mutual-exclusion
109 algorithm. 109 algorithm.
@@ -123,12 +123,12 @@ SB+rfionceonce-poonceonces.litmus
123S+poonceonces.litmus 123S+poonceonces.litmus
124 As below, but without the smp_wmb() and acquire load. 124 As below, but without the smp_wmb() and acquire load.
125 125
126S+wmbonceonce+poacquireonce.litmus 126S+fencewmbonceonce+poacquireonce.litmus
127 Can a smp_wmb(), instead of a release, and an acquire order 127 Can a smp_wmb(), instead of a release, and an acquire order
128 a prior store against a subsequent store? 128 a prior store against a subsequent store?
129 129
130WRC+poonceonces+Once.litmus 130WRC+poonceonces+Once.litmus
131WRC+pooncerelease+rmbonceonce+Once.litmus 131WRC+pooncerelease+fencermbonceonce+Once.litmus
132 These two are members of an extension of the MP litmus-test 132 These two are members of an extension of the MP litmus-test
133 class in which the first write is moved to a separate process. 133 class in which the first write is moved to a separate process.
134 The second is forbidden because smp_store_release() is 134 The second is forbidden because smp_store_release() is
@@ -143,7 +143,7 @@ Z6.0+pooncelock+poonceLock+pombonce.litmus
143 As above, but with smp_mb__after_spinlock() immediately 143 As above, but with smp_mb__after_spinlock() immediately
144 following the spin_lock(). 144 following the spin_lock().
145 145
146Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus 146Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
147 Is the ordering provided by a release-acquire chain sufficient 147 Is the ordering provided by a release-acquire chain sufficient
148 to make ordering apparent to accesses by a process that does 148 to make ordering apparent to accesses by a process that does
149 not participate in that release-acquire chain? 149 not participate in that release-acquire chain?
diff --git a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
index c53350205d28..18479823cd6c 100644
--- a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus
+++ b/tools/memory-model/litmus-tests/S+fencewmbonceonce+poacquireonce.litmus
@@ -1,4 +1,4 @@
1C S+wmbonceonce+poacquireonce 1C S+fencewmbonceonce+poacquireonce
2 2
3(* 3(*
4 * Result: Never 4 * Result: Never
diff --git a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
index 74b874ffa8da..ed5fff18d223 100644
--- a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus
+++ b/tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
@@ -1,4 +1,4 @@
1C SB+mbonceonces 1C SB+fencembonceonces
2 2
3(* 3(*
4 * Result: Never 4 * Result: Never
diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
index ad3448b941e6..e9947250d7de 100644
--- a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+fencermbonceonce+Once.litmus
@@ -1,4 +1,4 @@
1C WRC+pooncerelease+rmbonceonce+Once 1C WRC+pooncerelease+fencermbonceonce+Once
2 2
3(* 3(*
4 * Result: Never 4 * Result: Never
diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
index a20fc3fafb53..88e70b87a683 100644
--- a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus
+++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus
@@ -1,4 +1,4 @@
1C Z6.0+pooncerelease+poacquirerelease+mbonceonce 1C Z6.0+pooncerelease+poacquirerelease+fencembonceonce
2 2
3(* 3(*
4 * Result: Sometimes 4 * Result: Sometimes