[tip:locking/core] tools/memory-model: Rename litmus tests to comply to norm7
Commit-ID: 71b7ff5ebc9b1d5aa95eb48d6388234f1304fd19
Gitweb: https://git.kernel.org/tip/71b7ff5ebc9b1d5aa95eb48d6388234f1304fd19
Author: Andrea Parri
AuthorDate: Mon, 16 Jul 2018 11:06:05 -0700
Committer: Ingo Molnar
CommitDate: Tue, 17 Jul 2018 09:30:36 +0200
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
Signed-off-by: Paul E. McKenney
Acked-by: Alan Stern
Cc: Akira Yokosawa
Cc: Boqun Feng
Cc: David Howells
Cc: Jade Alglave
Cc: Linus Torvalds
Cc: Luc Maranget
Cc: Nicholas Piggin
Cc: Peter Zijlstra
Cc: Thomas Gleixner
Cc: Will Deacon
Cc: linux-a...@vger.kernel.org
Cc: parri.and...@gmail.com
Link:
http://lkml.kernel.org/r/20180716180605.16115-14-paul...@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar
---
tools/memory-model/Documentation/recipes.txt | 8
tools/memory-model/README| 20 ++--
litmus => IRIW+fencembonceonces+OnceOnce.litmus} | 2 +-
...litmus => LB+fencembonceonce+ctrlonceonce.litmus} | 2 +-
...s => MP+fencewmbonceonce+fencermbonceonce.litmus} | 2 +-
...+mbonceonces.litmus => R+fencembonceonces.litmus} | 2 +-
tools/memory-model/litmus-tests/README | 16
...itmus => S+fencewmbonceonce+poacquireonce.litmus} | 2 +-
...mbonceonces.litmus => SB+fencembonceonces.litmus} | 2 +-
...> WRC+pooncerelease+fencermbonceonce+Once.litmus} | 2 +-
...erelease+poacquirerelease+fencembonceonce.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
locking will be seen as ordered by CPUs not holding that lock.
Consider this example:
- /* See Z6.0+pooncelock+pooncelock+pombonce.litmus. */
+ /* See Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus. */
void CPU0(void)
{
spin_lock();
@@ -292,7 +292,7 @@ and to use smp_load_acquire() instead of smp_rmb().
However, the older
smp_wmb() and smp_rmb() APIs are still heavily used, so it is important
to understand their use cases. The general approach is shown below:
- /* See MP+wmbonceonce+rmbonceonce.litmus. */
+ /* See MP+fencewmbonceonce+fencermbonceonce.litmus. */
void CPU0(void)
{
WRITE_ONCE(x, 1);
@@ -360,7 +360,7 @@ can be seen in the LB+poonceonces.litmus litmus test.
One way of avoiding the counter-intuitive outcome is through the use of a
control dependency paired with a full memory barrier:
- /* See LB+ctrlonceonce+mbonceonce.litmus. */
+ /* See LB+fencembonceonce+ctrlonceonce.litmus. */
void CPU0(void)
{
r0 = READ_ONCE(x);
@@ -476,7 +476,7 @@ that one CPU first stores to one variable and then loads
from a second,
while another CPU stores to the second variable and then loads from the
first. Preserving order requires nothing less than full barriers:
- /* See SB+mbonceonces.litmus. */
+ /* See SB+fencembonceonces.litmus. */
void CPU0(void)
{
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
The memory model is used, in conjunction with "herd7", to exhaustively
explore the state space of small litmus tests.
-For example, to run SB+mbonceonces.litmus against the memory model:
+For example, to run SB+fencembonceonces.litmus against the memory model:
- $ herd7 -conf linux-kernel.cfg litmus-tests/SB+mbonceonces.litmus
+ $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
Here is the corresponding output:
- Test SB+mbonceonces Allowed
+ Test SB+fencembonceonces Allowed
States 3
0:r0=0; 1:r0=1;
0:r0=1; 1:r0=0;
@@ -50,8 +50,8 @@ Here is the corresponding output:
Witnesses
Positive: 0 Negative: 3
Condition exists (0:r0=0 /\ 1:r0=0)
- Observation SB+mbonceonces Never 0 3
- Time SB+mbonceonces 0.01
+ Observation SB+fencembonceonces Never 0 3
+ Time SB+fencembonceonces 0.01
Hash=d66d99523e2cac6b06e66f4c995ebb48
The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
@@ -67,16 +67,16 @@ BASIC USAGE: KLITMUS7
The "klitmus7" tool converts a litmus test into a Linux kernel module,
which may then be loaded and run.
-For example, to run SB+mbonceonces.litmus against
[tip:locking/core] tools/memory-model: Rename litmus tests to comply to norm7
Commit-ID: 71b7ff5ebc9b1d5aa95eb48d6388234f1304fd19
Gitweb: https://git.kernel.org/tip/71b7ff5ebc9b1d5aa95eb48d6388234f1304fd19
Author: Andrea Parri
AuthorDate: Mon, 16 Jul 2018 11:06:05 -0700
Committer: Ingo Molnar
CommitDate: Tue, 17 Jul 2018 09:30:36 +0200
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
Signed-off-by: Paul E. McKenney
Acked-by: Alan Stern
Cc: Akira Yokosawa
Cc: Boqun Feng
Cc: David Howells
Cc: Jade Alglave
Cc: Linus Torvalds
Cc: Luc Maranget
Cc: Nicholas Piggin
Cc: Peter Zijlstra
Cc: Thomas Gleixner
Cc: Will Deacon
Cc: linux-a...@vger.kernel.org
Cc: parri.and...@gmail.com
Link:
http://lkml.kernel.org/r/20180716180605.16115-14-paul...@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar
---
tools/memory-model/Documentation/recipes.txt | 8
tools/memory-model/README| 20 ++--
litmus => IRIW+fencembonceonces+OnceOnce.litmus} | 2 +-
...litmus => LB+fencembonceonce+ctrlonceonce.litmus} | 2 +-
...s => MP+fencewmbonceonce+fencermbonceonce.litmus} | 2 +-
...+mbonceonces.litmus => R+fencembonceonces.litmus} | 2 +-
tools/memory-model/litmus-tests/README | 16
...itmus => S+fencewmbonceonce+poacquireonce.litmus} | 2 +-
...mbonceonces.litmus => SB+fencembonceonces.litmus} | 2 +-
...> WRC+pooncerelease+fencermbonceonce+Once.litmus} | 2 +-
...erelease+poacquirerelease+fencembonceonce.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
locking will be seen as ordered by CPUs not holding that lock.
Consider this example:
- /* See Z6.0+pooncelock+pooncelock+pombonce.litmus. */
+ /* See Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus. */
void CPU0(void)
{
spin_lock();
@@ -292,7 +292,7 @@ and to use smp_load_acquire() instead of smp_rmb().
However, the older
smp_wmb() and smp_rmb() APIs are still heavily used, so it is important
to understand their use cases. The general approach is shown below:
- /* See MP+wmbonceonce+rmbonceonce.litmus. */
+ /* See MP+fencewmbonceonce+fencermbonceonce.litmus. */
void CPU0(void)
{
WRITE_ONCE(x, 1);
@@ -360,7 +360,7 @@ can be seen in the LB+poonceonces.litmus litmus test.
One way of avoiding the counter-intuitive outcome is through the use of a
control dependency paired with a full memory barrier:
- /* See LB+ctrlonceonce+mbonceonce.litmus. */
+ /* See LB+fencembonceonce+ctrlonceonce.litmus. */
void CPU0(void)
{
r0 = READ_ONCE(x);
@@ -476,7 +476,7 @@ that one CPU first stores to one variable and then loads
from a second,
while another CPU stores to the second variable and then loads from the
first. Preserving order requires nothing less than full barriers:
- /* See SB+mbonceonces.litmus. */
+ /* See SB+fencembonceonces.litmus. */
void CPU0(void)
{
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
The memory model is used, in conjunction with "herd7", to exhaustively
explore the state space of small litmus tests.
-For example, to run SB+mbonceonces.litmus against the memory model:
+For example, to run SB+fencembonceonces.litmus against the memory model:
- $ herd7 -conf linux-kernel.cfg litmus-tests/SB+mbonceonces.litmus
+ $ herd7 -conf linux-kernel.cfg litmus-tests/SB+fencembonceonces.litmus
Here is the corresponding output:
- Test SB+mbonceonces Allowed
+ Test SB+fencembonceonces Allowed
States 3
0:r0=0; 1:r0=1;
0:r0=1; 1:r0=0;
@@ -50,8 +50,8 @@ Here is the corresponding output:
Witnesses
Positive: 0 Negative: 3
Condition exists (0:r0=0 /\ 1:r0=0)
- Observation SB+mbonceonces Never 0 3
- Time SB+mbonceonces 0.01
+ Observation SB+fencembonceonces Never 0 3
+ Time SB+fencembonceonces 0.01
Hash=d66d99523e2cac6b06e66f4c995ebb48
The "Positive: 0 Negative: 3" and the "Never 0 3" each indicate that
@@ -67,16 +67,16 @@ BASIC USAGE: KLITMUS7
The "klitmus7" tool converts a litmus test into a Linux kernel module,
which may then be loaded and run.
-For example, to run SB+mbonceonces.litmus against
