Commit 71b7ff5e authored by Andrea Parri's avatar Andrea Parri Committed by Ingo Molnar
Browse files

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: default avatarAndrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: default avatarPaul E. McKenney <paulmck@linux.vnet.ibm.com>
Acked-by: default avatarAlan 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: default avatarIngo Molnar <mingo@kernel.org>
parent 0fcff171

tools/memory-model/Documentation/recipes.txt

+4 −4
Original line number Diff line number Diff line
@@ -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(&mylock);
@@ -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);

tools/memory-model/README

+10 −10
Original line number Diff line number Diff line
@@ -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 hardware:

For example, to run SB+fencembonceonces.litmus against hardware:



  $ mkdir mymodules

  $ klitmus7 -o mymodules litmus-tests/SB+mbonceonces.litmus

  $ klitmus7 -o mymodules litmus-tests/SB+fencembonceonces.litmus

  $ cd mymodules ; make

  $ sudo sh run.sh



The corresponding output includes:



  Test SB+mbonceonces Allowed

  Test SB+fencembonceonces Allowed

  Histogram (3 states)

  644580  :>0:r0=1; 1:r0=0;

  644328  :>0:r0=0; 1:r0=1;
@@ -86,8 +86,8 @@ The corresponding output includes: 
  Positive: 0, Negative: 2000000

  Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated

  Hash=d66d99523e2cac6b06e66f4c995ebb48

  Observation SB+mbonceonces Never 0 2000000

  Time SB+mbonceonces 0.16

  Observation SB+fencembonceonces Never 0 2000000

  Time SB+fencembonceonces 0.16



The "Positive: 0 Negative: 2000000" and the "Never 0 2000000" indicate

that during two million trials, the state specified in this litmus

tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus→tools/memory-model/litmus-tests/IRIW+fencembonceonces+OnceOnce.litmus

+1 −1
Original line number Diff line number Diff line 
C IRIW+mbonceonces+OnceOnce

C IRIW+fencembonceonces+OnceOnce



(*

 * Result: Never

tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus→tools/memory-model/litmus-tests/LB+fencembonceonce+ctrlonceonce.litmus

+1 −1
Original line number Diff line number Diff line 
C LB+ctrlonceonce+mbonceonce

C LB+fencembonceonce+ctrlonceonce



(*

 * Result: Never

tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus→tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus

+1 −1
Original line number Diff line number Diff line 
C MP+wmbonceonce+rmbonceonce

C MP+fencewmbonceonce+fencermbonceonce



(*

 * Result: Never

CRA Git | Maintained and supported by SUSTech CRA and CCSE