LKMM updates for v4.21/v5.0

Hello!

This series contains updates for the Linux-kernel memory model:

1. Model smp_mb__after_unlock_lock(), courtesy of Andrea Parri.

2. Add scripts to check github litmus tests.

3. Make scripts take "-j" abbreviation for "--jobs".

Thanx, Paul

------------------------------------------------------------------------

 .gitignore                 |    1 
 README                     |    2 
 linux-kernel.bell          |    3 
 linux-kernel.cat           |    4 -
 linux-kernel.def           |    1 
 scripts/README             |   70 ++++++++++++++++++++++
 scripts/checkalllitmus.sh  |   53 +++++++----------
 scripts/checkghlitmus.sh   |   65 ++++++++++++++++++++
 scripts/checklitmus.sh     |   74 +++--------------------
 scripts/checklitmushist.sh |   60 +++++++++++++++++++
 scripts/cmplitmushist.sh   |   87 +++++++++++++++++++++++++++
 scripts/initlitmushist.sh  |   68 +++++++++++++++++++++
 scripts/judgelitmus.sh     |   78 +++++++++++++++++++++++++
 scripts/newlitmushist.sh   |   61 +++++++++++++++++++
 scripts/parseargs.sh       |  140 ++++++++++++++++++++++++++++++++++++++++++++-
 scripts/runlitmushist.sh   |   87 +++++++++++++++++++++++++++
 16 files changed, 757 insertions(+), 97 deletions(-)

From: Andrea Parri <[email protected]>

From the header comment for smp_mb__after_unlock_lock():

"Place this after a lock-acquisition primitive to guarantee that
an UNLOCK+LOCK pair acts as a full barrier. This guarantee applies if the UNLOCK and LOCK are executed by the same CPU or if the UNLOCK and LOCK operate on the same lock variable."

This formalizes the above guarantee by defining (new) mb-links according to the law:

([M] ; po ; [UL] ; (co | po) ; [LKW] ;
fencerel(After-unlock-lock) ; [M])

where the component ([UL] ; co ; [LKW]) identifies "UNLOCK+LOCK pairs on the same lock variable" and the component ([UL] ; po ; [LKW]) identifies "UNLOCK+LOCK pairs executed by the same CPU".

In particular, the LKMM forbids the following two behaviors (the second litmus test below is based on

Documentation/RCU/Design/Memory-Ordering/Tree-RCU-Memory-Ordering.html

c.f., Section "Tree RCU Grace Period Memory Ordering Building Blocks"):

C after-unlock-lock-same-cpu

(*
* Result: Never
*)

{}

P0(spinlock_t *s, spinlock_t *t, int *x, int *y)

{
	int r0;

	spin_lock(s);
	WRITE_ONCE(*x, 1);
	spin_unlock(s);
	spin_lock(t);
	smp_mb__after_unlock_lock();
	r0 = READ_ONCE(*y);
	spin_unlock(t);
}

P1(int *x, int *y)

{
	int r0;

	WRITE_ONCE(*y, 1);
	smp_mb();
	r0 = READ_ONCE(*x);
}

exists (0:r0=0 /\ 1:r0=0)

C after-unlock-lock-same-lock-variable

(*
* Result: Never
*)

{}

P0(spinlock_t *s, int *x, int *y)

{
	int r0;

	spin_lock(s);
	WRITE_ONCE(*x, 1);
	r0 = READ_ONCE(*y);
	spin_unlock(s);
}

P1(spinlock_t *s, int *y, int *z)

{
	int r0;

	spin_lock(s);
	smp_mb__after_unlock_lock();
	WRITE_ONCE(*y, 1);
	r0 = READ_ONCE(*z);
	spin_unlock(s);
}

P2(int *z, int *x)

{
	int r0;

	WRITE_ONCE(*z, 1);
	smp_mb();
	r0 = READ_ONCE(*x);
}

exists (0:r0=0 /\ 1:r0=0 /\ 2:r0=0)

---
 tools/memory-model/linux-kernel.bell | 3 ++-
 tools/memory-model/linux-kernel.cat  | 4 +++-
 tools/memory-model/linux-kernel.def  | 1 +
 3 files changed, 6 insertions(+), 2 deletions(-)

index b84fb2f67109..796513362c05 100644
@@ -29,7 +29,8 @@ enum Barriers = 'wmb (*smp_wmb*) ||
 		'sync-rcu (*synchronize_rcu*) ||
 		'before-atomic (*smp_mb__before_atomic*) ||
 		'after-atomic (*smp_mb__after_atomic*) ||
-		'after-spinlock (*smp_mb__after_spinlock*)
+		'after-spinlock (*smp_mb__after_spinlock*) ||
+		'after-unlock-lock (*smp_mb__after_unlock_lock*)
 instructions F[Barriers]
 
 (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)

index 882fc33274ac..8f23c74a96fd 100644
@@ -30,7 +30,9 @@ let wmb = [W] ; fencerel(Wmb) ; [W]
 let mb = ([M] ; fencerel(Mb) ; [M]) |
 	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
 	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
-	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
+	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
+	([M] ; po ; [UL] ; (co | po) ; [LKW] ;
+		fencerel(After-unlock-lock) ; [M])
 let gp = po ; [Sync-rcu] ; po?
 
 let strong-fence = mb | gp

index 6fa3eb28d40b..b27911cc087d 100644
@@ -23,6 +23,7 @@ smp_wmb() { __fence{wmb}; }
 smp_mb__before_atomic() { __fence{before-atomic}; }
 smp_mb__after_atomic() { __fence{after-atomic}; }
 smp_mb__after_spinlock() { __fence{after-spinlock}; }
+smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; }
 
 // Exchange
 xchg(X,V)  __xchg{mb}(X,V)

2.17.1

From: "Paul E. McKenney" <[email protected]>

The https://github.com/paulmckrcu/litmus repository contains a large number of C-language litmus tests that include "Result:" comments predicting the verification result. This commit adds a number of scripts that run tests on these litmus tests:

checkghlitmus.sh:
Runs all litmus tests in the https://github.com/paulmckrcu/litmus
archive that are C-language and that have "Result:" comment lines documenting expected results, comparing the actual results to those expected. Clones the repository if it has not already been cloned into the "tools/memory-model/litmus" directory.

initlitmushist.sh
Run all litmus tests having no more than the specified number of processes given a specified timeout, recording the results in .litmus.out files. Clones the repository if it has not already been cloned into the "tools/memory-model/litmus" directory.

newlitmushist.sh
For all new or updated litmus tests having no more than the specified number of processes given a specified timeout, run and record the results in .litmus.out files.

checklitmushist.sh
Run all litmus tests having .litmus.out files from previous initlitmushist.sh or newlitmushist.sh runs, comparing the herd output to that of the original runs.

The above scripts will run litmus tests concurrently, by default with one job per available CPU. Giving any of these scripts the --help argument will cause them to print usage information.

This commit also adds a number of helper scripts that are not intended to be invoked from the command line:

cmplitmushist.sh: Compare the output of two different runs of the same
litmus test.

judgelitmus.sh: Compare the output of a litmus test to its "Result:"
comment line.

parseargs.sh: Parse command-line arguments.

runlitmushist.sh: Run the litmus tests whose pathnames are provided one
per line on standard input.

While in the area, this commit also makes the existing checklitmus.sh and checkalllitmus.sh scripts use parseargs.sh in order to provide a bit of uniformity. In addition, per-litmus-test status output is directed to stdout, while end-of-test summary information is directed to stderr. Finally, the error flag standardizes on "!!!" to assist those familiar with rcutorture output.

The defaults for the parseargs.sh arguments may be overridden by using environment variables: LKMM_DESTDIR for --destdir, LKMM_HERD_OPTIONS for --herdoptions, LKMM_JOBS for --jobs, LKMM_PROCS for --procs, and LKMM_TIMEOUT for --timeout.

---
 tools/memory-model/.gitignore                 |   1 +
 tools/memory-model/README                     |   2 +
 tools/memory-model/scripts/README             |  70 ++++++++++
 tools/memory-model/scripts/checkalllitmus.sh  |  53 ++++----
 tools/memory-model/scripts/checkghlitmus.sh   |  65 +++++++++
 tools/memory-model/scripts/checklitmus.sh     |  74 ++--------
 tools/memory-model/scripts/checklitmushist.sh |  60 +++++++++
 tools/memory-model/scripts/cmplitmushist.sh   |  87 ++++++++++++
 tools/memory-model/scripts/initlitmushist.sh  |  68 ++++++++++
 tools/memory-model/scripts/judgelitmus.sh     |  78 +++++++++++
 tools/memory-model/scripts/newlitmushist.sh   |  61 +++++++++
 tools/memory-model/scripts/parseargs.sh       | 126 ++++++++++++++++++
 tools/memory-model/scripts/runlitmushist.sh   |  87 ++++++++++++
 13 files changed, 739 insertions(+), 93 deletions(-)
 create mode 100644 tools/memory-model/.gitignore
 create mode 100644 tools/memory-model/scripts/README
 create mode 100755 tools/memory-model/scripts/checkghlitmus.sh
 create mode 100755 tools/memory-model/scripts/checklitmushist.sh
 create mode 100644 tools/memory-model/scripts/cmplitmushist.sh
 create mode 100755 tools/memory-model/scripts/initlitmushist.sh
 create mode 100755 tools/memory-model/scripts/judgelitmus.sh
 create mode 100755 tools/memory-model/scripts/newlitmushist.sh
 create mode 100755 tools/memory-model/scripts/parseargs.sh
 create mode 100755 tools/memory-model/scripts/runlitmushist.sh

new file mode 100644
index 000000000000..b1d34c52f3c3
@@ -0,0 +1 @@
+litmus

index acf9077cffaa..0f2c366518c6 100644
@@ -156,6 +156,8 @@ lock.cat
 README
 	This file.
 
+scripts	Various scripts, see scripts/README.
+
 
 ===========
 LIMITATIONS

2.17.1

From: "Paul E. McKenney" <[email protected]>

The "--jobs" argument to the litmus-test scripts is similar to the "-jN" argument to "make", so this commit allows the "-jN" form as well. While in the area, it also prohibits the various forms of "-j0".

---
 tools/memory-model/scripts/parseargs.sh | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

index 96b307c8d64a..859e1d581e05 100755
@@ -95,8 +95,18 @@ do
 		LKMM_HERD_OPTIONS="$2"
 		shift
 		;;
-	--jobs|--job)
-		checkarg --jobs "(number)" "$#" "$2" '^[0-9]\+$' '^--'
+	-j[1-9]*)
+		njobs="`echo $1 | sed -e 's/^-j//'`"
+		trailchars="`echo $njobs | sed -e 's/[0-9]\+\(.*\)$/\1/'`"
+		if test -n "$trailchars"
+		then
+			echo $1 trailing characters "'$trailchars'"
+			usagehelp
+		fi
+		LKMM_JOBS="`echo $njobs | sed -e 's/^\([0-9]\+\).*$/\1/'`"
+		;;
+	--jobs|--job|-j)
+		checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]\+$' '^--'
 		LKMM_JOBS="$2"
 		shift
 		;;

2.17.1