Updates to the formal memory model
cover Updates to the formal memory model
Hello, Ingo!
This series contains updates to the Linux kernel's formal memory model in tools/memory-model. These patches are ready for inclusion into -tip.
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".
There is another series in preparation to model SRCU, but this series requires hot-off-the presses changes to the herd tool that have not yet been released. This SRCU series is therefore targeting the merge window after the upcoming one. People wishing to experiment with the prototype SRCU model may obtain it from my -rcu tree at branch "dev", and use a bleeding-edge herd7 built from https://github.com/herd/herdtools7/,
version 7.51+2(dev), which is (commit 10403b24070c) or later.
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(-)
PATCH 1/3 tools/memory-model: Model smp_mb__after_unlock_lock()
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(-)
tools/memory-model/linux-kernel.bell +2 -1
@@ -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 *)
tools/memory-model/linux-kernel.cat +3 -1
@@ -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
tools/memory-model/linux-kernel.def +1 -0
@@ -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)
Signature · 1 line
2.17.1
tip-bot for Andrea Parri
merge bot[tip:locking/core] tools/memory-model: Model smp_mb__after_unlock_lock()
tools/memory-model: Model smp_mb__after_unlock_lock()
Commit-ID: 4607abbcf464ea2be14da444215d05c73025cf6e Gitweb: https://git.kernel.org/tip/4607abbcf464ea2be14da444215d05c73025cf6e Author: Andrea Parri <[email protected]> AuthorDate: Mon, 3 Dec 2018 15:04:49 -0800 Committer: Ingo Molnar <[email protected]> CommitDate: Tue, 4 Dec 2018 07:29:51 +0100
tools/memory-model: Model smp_mb__after_unlock_lock()
The kernel documents smp_mb__after_unlock_lock() the following way:
"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."
Formalize in LKMM 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(-)
tools/memory-model/linux-kernel.bell +2 -1
@@ -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 *)
tools/memory-model/linux-kernel.cat +3 -1
@@ -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
tools/memory-model/linux-kernel.def +1 -0
@@ -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)
tip-bot for Andrea Parri
merge bot[tip:locking/core] tools/memory-model: Model smp_mb__after_unlock_lock()
In reply to Paul E. McKenneytools/memory-model: Model smp_mb__after_unlock_lock()
Commit-ID: 5b735eb1ce481b2f1674a47c0995944b1cb6f5d5 Gitweb: https://git.kernel.org/tip/5b735eb1ce481b2f1674a47c0995944b1cb6f5d5 Author: Andrea Parri <[email protected]> AuthorDate: Mon, 3 Dec 2018 15:04:49 -0800 Committer: Ingo Molnar <[email protected]> CommitDate: Mon, 21 Jan 2019 11:06:55 +0100
tools/memory-model: Model smp_mb__after_unlock_lock()
The kernel documents smp_mb__after_unlock_lock() the following way:
"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."
Formalize in LKMM 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(-)
tools/memory-model/linux-kernel.bell +2 -1
@@ -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 *)
tools/memory-model/linux-kernel.cat +3 -1
@@ -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
tools/memory-model/linux-kernel.def +1 -0
@@ -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)
PATCH 2/3 EXP tools/memory-model: Add scripts to check github litmus tests
In reply to Paul E. McKenneyFrom: "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
tools/memory-model/.gitignore new file +1 -0
@@ -0,0 +1 @@ +litmus
tools/memory-model/README +2 -0
@@ -156,6 +156,8 @@ lock.cat README This file. +scripts Various scripts, see scripts/README. + =========== LIMITATIONS
tools/memory-model/scripts/README new file +70 -0
70 lines not on this page · raw message
tools/memory-model/scripts/checkalllitmus.sh +23 -30
86 lines not on this page · raw message
tools/memory-model/scripts/checkghlitmus.sh new file +65 -0
65 lines not on this page · raw message
tools/memory-model/scripts/checklitmus.sh +11 -63
95 lines not on this page · raw message
tools/memory-model/scripts/checklitmushist.sh new file +60 -0
60 lines not on this page · raw message
tools/memory-model/scripts/cmplitmushist.sh new file +87 -0
87 lines not on this page · raw message
tools/memory-model/scripts/initlitmushist.sh new file +68 -0
68 lines not on this page · raw message
tools/memory-model/scripts/judgelitmus.sh new file +78 -0
78 lines not on this page · raw message
tools/memory-model/scripts/newlitmushist.sh new file +61 -0
61 lines not on this page · raw message
tools/memory-model/scripts/parseargs.sh new file +126 -0
126 lines not on this page · raw message
tools/memory-model/scripts/runlitmushist.sh new file +87 -0
87 lines not on this page · raw message
Signature · 1 line
2.17.1
tip-bot for Paul E. McKenney
merge bot[tip:locking/core] tools/memory-model: Add scripts to check github litmus tests
tools/memory-model: Add scripts to check github litmus tests
Commit-ID: e188d24a382d609ec7ca6c1a00396202565b7831 Gitweb: https://git.kernel.org/tip/e188d24a382d609ec7ca6c1a00396202565b7831 Author: Paul E. McKenney <[email protected]> AuthorDate: Mon, 3 Dec 2018 15:04:50 -0800 Committer: Ingo Molnar <[email protected]> CommitDate: Tue, 4 Dec 2018 07:29:52 +0100
tools/memory-model: Add scripts to check github litmus tests
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(-)
tools/memory-model/.gitignore new file +1 -0
@@ -0,0 +1 @@ +litmus
tools/memory-model/README +2 -0
@@ -156,6 +156,8 @@ lock.cat README This file. +scripts Various scripts, see scripts/README. + =========== LIMITATIONS
tools/memory-model/scripts/README new file +70 -0
70 lines not on this page · raw message
tools/memory-model/scripts/checkalllitmus.sh +23 -30
86 lines not on this page · raw message
tools/memory-model/scripts/checkghlitmus.sh new file +65 -0
65 lines not on this page · raw message
tools/memory-model/scripts/checklitmus.sh +11 -63
95 lines not on this page · raw message
tools/memory-model/scripts/checklitmushist.sh new file +60 -0
60 lines not on this page · raw message
tools/memory-model/scripts/cmplitmushist.sh new file +87 -0
87 lines not on this page · raw message
tools/memory-model/scripts/initlitmushist.sh new file +68 -0
68 lines not on this page · raw message
tools/memory-model/scripts/judgelitmus.sh new file +78 -0
78 lines not on this page · raw message
tools/memory-model/scripts/newlitmushist.sh new file +61 -0
61 lines not on this page · raw message
tools/memory-model/scripts/parseargs.sh new file +126 -0
126 lines not on this page · raw message
tools/memory-model/scripts/runlitmushist.sh new file +87 -0
87 lines not on this page · raw message
tip-bot for Paul E. McKenney
merge bot[tip:locking/core] tools/memory-model: Add scripts to check github litmus tests
In reply to Paul E. McKenneytools/memory-model: Add scripts to check github litmus tests
Commit-ID: b02eb5b0961a06561b89f5b7f0dd171b750e5789 Gitweb: https://git.kernel.org/tip/b02eb5b0961a06561b89f5b7f0dd171b750e5789 Author: Paul E. McKenney <[email protected]> AuthorDate: Mon, 3 Dec 2018 15:04:50 -0800 Committer: Ingo Molnar <[email protected]> CommitDate: Mon, 21 Jan 2019 11:06:59 +0100
tools/memory-model: Add scripts to check github litmus tests
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(-)
tools/memory-model/.gitignore new file +1 -0
@@ -0,0 +1 @@ +litmus
tools/memory-model/README +2 -0
@@ -156,6 +156,8 @@ lock.cat README This file. +scripts Various scripts, see scripts/README. + =========== LIMITATIONS
tools/memory-model/scripts/README new file +70 -0
70 lines not on this page · raw message
tools/memory-model/scripts/checkalllitmus.sh +23 -30
86 lines not on this page · raw message
tools/memory-model/scripts/checkghlitmus.sh new file +65 -0
65 lines not on this page · raw message
tools/memory-model/scripts/checklitmus.sh +11 -63
95 lines not on this page · raw message
tools/memory-model/scripts/checklitmushist.sh new file +60 -0
60 lines not on this page · raw message
tools/memory-model/scripts/cmplitmushist.sh new file +87 -0
87 lines not on this page · raw message
tools/memory-model/scripts/initlitmushist.sh new file +68 -0
68 lines not on this page · raw message
tools/memory-model/scripts/judgelitmus.sh new file +78 -0
78 lines not on this page · raw message
tools/memory-model/scripts/newlitmushist.sh new file +61 -0
61 lines not on this page · raw message
tools/memory-model/scripts/parseargs.sh new file +126 -0
126 lines not on this page · raw message
tools/memory-model/scripts/runlitmushist.sh new file +87 -0
87 lines not on this page · raw message
PATCH 3/3 EXP tools/memory-model: Make scripts take "-j" abbreviation for "--jobs"
In reply to Paul E. McKenneyFrom: "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(-)
tools/memory-model/scripts/parseargs.sh +12 -2
@@ -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 ;;
Signature · 1 line
2.17.1
tip-bot for Paul E. McKenney
merge bot[tip:locking/core] tools/memory-model: Make scripts take "-j" abbreviation for "--jobs"
tools/memory-model: Make scripts take "-j" abbreviation for "--jobs"
Commit-ID: a6f1de04276d036b61c4d1dbd0367e6b430d8783 Gitweb: https://git.kernel.org/tip/a6f1de04276d036b61c4d1dbd0367e6b430d8783 Author: Paul E. McKenney <[email protected]> AuthorDate: Mon, 3 Dec 2018 15:04:51 -0800 Committer: Ingo Molnar <[email protected]> CommitDate: Tue, 4 Dec 2018 07:29:52 +0100
tools/memory-model: Make scripts take "-j" abbreviation for "--jobs"
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(-)
tools/memory-model/scripts/parseargs.sh +12 -2
@@ -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 ;;
tip-bot for Paul E. McKenney
merge bot[tip:locking/core] tools/memory-model: Make scripts take "-j" abbreviation for "--jobs"
In reply to Paul E. McKenneytools/memory-model: Make scripts take "-j" abbreviation for "--jobs"
Commit-ID: 910cc9591d1433c2e26bd1c210844b09c699dd89 Gitweb: https://git.kernel.org/tip/910cc9591d1433c2e26bd1c210844b09c699dd89 Author: Paul E. McKenney <[email protected]> AuthorDate: Mon, 3 Dec 2018 15:04:51 -0800 Committer: Ingo Molnar <[email protected]> CommitDate: Mon, 21 Jan 2019 11:07:04 +0100
tools/memory-model: Make scripts take "-j" abbreviation for "--jobs"
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(-)
tools/memory-model/scripts/parseargs.sh +12 -2
@@ -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 ;;
Akira Yokosawa
reviewerQuoted 11 lines · Paul E. McKenney
Hello, Ingo!
This series contains updates to the Linux kernel's formal memory model in
tools/memory-model. These patches are ready for inclusion into -tip.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".
Quoted 7 lines
There is another series in preparation to model SRCU, but this series requires hot-off-the presses changes to the herd tool that have not yet been released. This SRCU series is therefore targeting the merge window after the upcoming one. People wishing to experiment with the prototype SRCU model may obtain it from my -rcu tree at branch "dev", and use a bleeding-edge herd7 built from https://github.com/herd/herdtools7/,
version 7.51+2(dev), which is (commit10403b24070c) or later.
On the master branch of herdtools7, SRCU support was added in version 7.51+4(dev), which is commit 6ec9da1f4d58, or later.
Thanks, Akira
Quoted 23 lines
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(-)
Quoted 20 lines · Akira Yokosawa
Quoted 11 lines · Paul E. McKenney
Hello, Ingo!
This series contains updates to the Linux kernel's formal memory model in
tools/memory-model. These patches are ready for inclusion into -tip.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".
Quoted 7 lines
There is another series in preparation to model SRCU, but this series requires hot-off-the presses changes to the herd tool that have not yet been released. This SRCU series is therefore targeting the merge window after the upcoming one. People wishing to experiment with the prototype SRCU model may obtain it from my -rcu tree at branch "dev", and use a bleeding-edge herd7 built from https://github.com/herd/herdtools7/,
version 7.51+2(dev), which is (commit10403b24070c) or later.
Quoted 2 lines
On the master branch of herdtools7, SRCU support was added in version 7.51+4(dev), which is commit
6ec9da1f4d58, or later.
It has been working for me with version 7.51+2(dev), but perhaps I have just been getting lucky. It wouldn't be the first time! ;-)
Thanx, Paul
Quoted 26 lines
Thanks, Akira
Quoted 23 lines
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(-)
Akira Yokosawa
reviewerQuoted 21 lines · Paul E. McKenney
Quoted 20 lines · Akira Yokosawa
Quoted 18 lines · Paul E. McKenney
Hello, Ingo!
This series contains updates to the Linux kernel's formal memory model in
tools/memory-model. These patches are ready for inclusion into -tip.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".
There is another series in preparation to model SRCU, but this series requires hot-off-the presses changes to the herd tool that have not yet been released. This SRCU series is therefore targeting the merge window after the upcoming one. People wishing to experiment with the prototype SRCU model may obtain it from my -rcu tree at branch "dev", and use a bleeding-edge herd7 built from https://github.com/herd/herdtools7/,
version 7.51+2(dev), which is (commit10403b24070c) or later.
Quoted 5 lines
Quoted 2 lines
On the master branch of herdtools7, SRCU support was added in version 7.51+4(dev), which is commit
6ec9da1f4d58, or later.It has been working for me with version 7.51+2(dev), but perhaps I have just been getting lucky. It wouldn't be the first time! ;-)
Sounds like you've been at the HEAD of topic branch "srcu".
Thanks, Akira
Quoted 30 lines
Thanx, Paul
Quoted 26 lines
Thanks, Akira
Quoted 23 lines
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(-)
Quoted 22 lines · Akira Yokosawa
Quoted 21 lines · Paul E. McKenney
Quoted 20 lines · Akira Yokosawa
Quoted 18 lines · Paul E. McKenney
Hello, Ingo!
This series contains updates to the Linux kernel's formal memory model in
tools/memory-model. These patches are ready for inclusion into -tip.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".
There is another series in preparation to model SRCU, but this series requires hot-off-the presses changes to the herd tool that have not yet been released. This SRCU series is therefore targeting the merge window after the upcoming one. People wishing to experiment with the prototype SRCU model may obtain it from my -rcu tree at branch "dev", and use a bleeding-edge herd7 built from https://github.com/herd/herdtools7/,
version 7.51+2(dev), which is (commit10403b24070c) or later.
Quoted 7 lines
Quoted 5 lines
Quoted 2 lines
On the master branch of herdtools7, SRCU support was added in version 7.51+4(dev), which is commit
6ec9da1f4d58, or later.It has been working for me with version 7.51+2(dev), but perhaps I have just been getting lucky. It wouldn't be the first time! ;-)
Sounds like you've been at the HEAD of topic branch "srcu".
You are quite right. And this situation does confirm the wisdom of waiting until a herd release containing the SRCU support. ;-)
Thanx, Paul
Quoted 32 lines
Thanks, Akira
Quoted 30 lines
Thanx, Paul
Quoted 26 lines
Thanks, Akira
Quoted 23 lines
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(-)