diff options
author | Andrea Parri <andrea.parri@amarulasolutions.com> | 2018-07-16 14:06:05 -0400 |
---|---|---|
committer | Ingo Molnar <mingo@kernel.org> | 2018-07-17 03:30:36 -0400 |
commit | 71b7ff5ebc9b1d5aa95eb48d6388234f1304fd19 (patch) | |
tree | a4fa218053573b0e3e3fc1801340f77478f916ff /tools/memory-model | |
parent | 0fcff1715bec7593a0ba86f3fef46cd89af37a8b (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.txt | 8 | ||||
-rw-r--r-- | tools/memory-model/README | 20 | ||||
-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/README | 16 | ||||
-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 | |||
126 | locking will be seen as ordered by CPUs not holding that lock. | 126 | locking will be seen as ordered by CPUs not holding that lock. |
127 | Consider this example: | 127 | Consider 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 | |||
292 | smp_wmb() and smp_rmb() APIs are still heavily used, so it is important | 292 | smp_wmb() and smp_rmb() APIs are still heavily used, so it is important |
293 | to understand their use cases. The general approach is shown below: | 293 | to 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. | |||
360 | One way of avoiding the counter-intuitive outcome is through the use of a | 360 | One way of avoiding the counter-intuitive outcome is through the use of a |
361 | control dependency paired with a full memory barrier: | 361 | control 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, | |||
476 | while another CPU stores to the second variable and then loads from the | 476 | while another CPU stores to the second variable and then loads from the |
477 | first. Preserving order requires nothing less than full barriers: | 477 | first. 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 | |||
35 | The memory model is used, in conjunction with "herd7", to exhaustively | 35 | The memory model is used, in conjunction with "herd7", to exhaustively |
36 | explore the state space of small litmus tests. | 36 | explore the state space of small litmus tests. |
37 | 37 | ||
38 | For example, to run SB+mbonceonces.litmus against the memory model: | 38 | For 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 | ||
42 | Here is the corresponding output: | 42 | Here 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 | ||
57 | The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that | 57 | The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that |
@@ -67,16 +67,16 @@ BASIC USAGE: KLITMUS7 | |||
67 | The "klitmus7" tool converts a litmus test into a Linux kernel module, | 67 | The "klitmus7" tool converts a litmus test into a Linux kernel module, |
68 | which may then be loaded and run. | 68 | which may then be loaded and run. |
69 | 69 | ||
70 | For example, to run SB+mbonceonces.litmus against hardware: | 70 | For 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 | ||
77 | The corresponding output includes: | 77 | The 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 | ||
92 | The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate | 92 | The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate |
93 | that during two million trials, the state specified in this litmus | 93 | that 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 @@ | |||
1 | C IRIW+mbonceonces+OnceOnce | 1 | C 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 @@ | |||
1 | C LB+ctrlonceonce+mbonceonce | 1 | C 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 @@ | |||
1 | C MP+wmbonceonce+rmbonceonce | 1 | C 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 @@ | |||
1 | C R+mbonceonces | 1 | C 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 | ||
21 | IRIW+mbonceonces+OnceOnce.litmus | 21 | IRIW+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 | ||
50 | LB+ctrlonceonce+mbonceonce.litmus | 50 | LB+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 | ||
91 | MP+wmbonceonce+rmbonceonce.litmus | 91 | MP+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 | ||
98 | R+mbonceonces.litmus | 98 | R+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 | |||
103 | R+poonceonces.litmus | 103 | R+poonceonces.litmus |
104 | As above, but without the smp_mb() invocations. | 104 | As above, but without the smp_mb() invocations. |
105 | 105 | ||
106 | SB+mbonceonces.litmus | 106 | SB+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 | |||
123 | S+poonceonces.litmus | 123 | S+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 | ||
126 | S+wmbonceonce+poacquireonce.litmus | 126 | S+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 | ||
130 | WRC+poonceonces+Once.litmus | 130 | WRC+poonceonces+Once.litmus |
131 | WRC+pooncerelease+rmbonceonce+Once.litmus | 131 | WRC+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 | ||
146 | Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus | 146 | Z6.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 @@ | |||
1 | C S+wmbonceonce+poacquireonce | 1 | C 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 @@ | |||
1 | C SB+mbonceonces | 1 | C 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 @@ | |||
1 | C WRC+pooncerelease+rmbonceonce+Once | 1 | C 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 @@ | |||
1 | C Z6.0+pooncerelease+poacquirerelease+mbonceonce | 1 | C Z6.0+pooncerelease+poacquirerelease+fencembonceonce |
2 | 2 | ||
3 | (* | 3 | (* |
4 | * Result: Sometimes | 4 | * Result: Sometimes |