summaryrefslogtreecommitdiffstats
path: root/tools/memory-model
diff options
context:
space:
mode:
authorPaul E. McKenney <paulmck@linux.vnet.ibm.com>2018-12-03 18:04:50 -0500
committerIngo Molnar <mingo@kernel.org>2019-01-21 05:06:59 -0500
commitb02eb5b0961a06561b89f5b7f0dd171b750e5789 (patch)
tree5a1efe6d597916113e443f2f0596fe8d9120d4dc /tools/memory-model
parent5b735eb1ce481b2f1674a47c0995944b1cb6f5d5 (diff)
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. [ paulmck: History-check summary-line changes per Alan Stern feedback. ] Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Linus Torvalds <torvalds@linux-foundation.org> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Thomas Gleixner <tglx@linutronix.de> Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20181203230451.28921-2-paulmck@linux.ibm.com Signed-off-by: Ingo Molnar <mingo@kernel.org>
Diffstat (limited to 'tools/memory-model')
-rw-r--r--tools/memory-model/.gitignore1
-rw-r--r--tools/memory-model/README2
-rw-r--r--tools/memory-model/scripts/README70
-rwxr-xr-xtools/memory-model/scripts/checkalllitmus.sh53
-rw-r--r--tools/memory-model/scripts/checkghlitmus.sh65
-rwxr-xr-xtools/memory-model/scripts/checklitmus.sh74
-rw-r--r--tools/memory-model/scripts/checklitmushist.sh60
-rw-r--r--tools/memory-model/scripts/cmplitmushist.sh87
-rw-r--r--tools/memory-model/scripts/initlitmushist.sh68
-rw-r--r--tools/memory-model/scripts/judgelitmus.sh78
-rw-r--r--tools/memory-model/scripts/newlitmushist.sh61
-rw-r--r--tools/memory-model/scripts/parseargs.sh126
-rw-r--r--tools/memory-model/scripts/runlitmushist.sh87
13 files changed, 739 insertions, 93 deletions
diff --git a/tools/memory-model/.gitignore b/tools/memory-model/.gitignore
new file mode 100644
index 000000000000..b1d34c52f3c3
--- /dev/null
+++ b/tools/memory-model/.gitignore
@@ -0,0 +1 @@
litmus
diff --git a/tools/memory-model/README b/tools/memory-model/README
index acf9077cffaa..0f2c366518c6 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -156,6 +156,8 @@ lock.cat
156README 156README
157 This file. 157 This file.
158 158
159scripts Various scripts, see scripts/README.
160
159 161
160=========== 162===========
161LIMITATIONS 163LIMITATIONS
diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README
new file mode 100644
index 000000000000..29375a1fbbfa
--- /dev/null
+++ b/tools/memory-model/scripts/README
@@ -0,0 +1,70 @@
1 ============
2 LKMM SCRIPTS
3 ============
4
5
6These scripts are run from the tools/memory-model directory.
7
8checkalllitmus.sh
9
10 Run all litmus tests in the litmus-tests directory, checking
11 the results against the expected results recorded in the
12 "Result:" comment lines.
13
14checkghlitmus.sh
15
16 Run all litmus tests in the https://github.com/paulmckrcu/litmus
17 archive that are C-language and that have "Result:" comment lines
18 documenting expected results, comparing the actual results to
19 those expected.
20
21checklitmushist.sh
22
23 Run all litmus tests having .litmus.out files from previous
24 initlitmushist.sh or newlitmushist.sh runs, comparing the
25 herd output to that of the original runs.
26
27checklitmus.sh
28
29 Check a single litmus test against its "Result:" expected result.
30
31cmplitmushist.sh
32
33 Compare output from two different runs of the same litmus tests,
34 with the absolute pathnames of the tests to run provided one
35 name per line on standard input. Not normally run manually,
36 provided instead for use by other scripts.
37
38initlitmushist.sh
39
40 Run all litmus tests having no more than the specified number
41 of processes given a specified timeout, recording the results
42 in .litmus.out files.
43
44judgelitmus.sh
45
46 Given a .litmus file and its .litmus.out herd output, check the
47 .litmus.out file against the .litmus file's "Result:" comment to
48 judge whether the test ran correctly. Not normally run manually,
49 provided instead for use by other scripts.
50
51newlitmushist.sh
52
53 For all new or updated litmus tests having no more than the
54 specified number of processes given a specified timeout, run
55 and record the results in .litmus.out files.
56
57parseargs.sh
58
59 Parse command-line arguments. Not normally run manually,
60 provided instead for use by other scripts.
61
62runlitmushist.sh
63
64 Run the litmus tests whose absolute pathnames are provided one
65 name per line on standard input. Not normally run manually,
66 provided instead for use by other scripts.
67
68README
69
70 This file
diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh
index ca528f9a24d4..b35fcd61ecf6 100755
--- a/tools/memory-model/scripts/checkalllitmus.sh
+++ b/tools/memory-model/scripts/checkalllitmus.sh
@@ -1,42 +1,27 @@
1#!/bin/sh 1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
2# 3#
3# Run herd tests on all .litmus files in the specified directory (which 4# Run herd tests on all .litmus files in the litmus-tests directory
4# defaults to litmus-tests) and check each file's result against a "Result:" 5# and check each file's result against a "Result:" comment within that
5# comment within that litmus test. If the verification result does not 6# litmus test. If the verification result does not match that specified
6# match that specified in the litmus test, this script prints an error 7# in the litmus test, this script prints an error message prefixed with
7# message prefixed with "^^^". It also outputs verification results to 8# "^^^". It also outputs verification results to a file whose name is
8# a file whose name is that of the specified litmus test, but with ".out" 9# that of the specified litmus test, but with ".out" appended.
9# appended.
10# 10#
11# Usage: 11# Usage:
12# checkalllitmus.sh [ directory ] 12# checkalllitmus.sh
13# 13#
14# The LINUX_HERD_OPTIONS environment variable may be used to specify 14# Run this in the directory containing the memory model.
15# arguments to herd, whose default is defined by the checklitmus.sh script.
16# Thus, one would normally run this in the directory containing the memory
17# model, specifying the pathname of the litmus test to check.
18# 15#
19# This script makes no attempt to run the litmus tests concurrently. 16# This script makes no attempt to run the litmus tests concurrently.
20# 17#
21# This program is free software; you can redistribute it and/or modify
22# it under the terms of the GNU General Public License as published by
23# the Free Software Foundation; either version 2 of the License, or
24# (at your option) any later version.
25#
26# This program is distributed in the hope that it will be useful,
27# but WITHOUT ANY WARRANTY; without even the implied warranty of
28# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
29# GNU General Public License for more details.
30#
31# You should have received a copy of the GNU General Public License
32# along with this program; if not, you can access it online at
33# http://www.gnu.org/licenses/gpl-2.0.html.
34#
35# Copyright IBM Corporation, 2018 18# Copyright IBM Corporation, 2018
36# 19#
37# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> 20# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
38 21
39litmusdir=${1-litmus-tests} 22. scripts/parseargs.sh
23
24litmusdir=litmus-tests
40if test -d "$litmusdir" -a -r "$litmusdir" -a -x "$litmusdir" 25if test -d "$litmusdir" -a -r "$litmusdir" -a -x "$litmusdir"
41then 26then
42 : 27 :
@@ -45,6 +30,14 @@ else
45 exit 255 30 exit 255
46fi 31fi
47 32
33# Create any new directories that have appeared in the github litmus
34# repo since the last run.
35if test "$LKMM_DESTDIR" != "."
36then
37 find $litmusdir -type d -print |
38 ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
39fi
40
48# Find the checklitmus script. If it is not where we expect it, then 41# Find the checklitmus script. If it is not where we expect it, then
49# assume that the caller has the PATH environment variable set 42# assume that the caller has the PATH environment variable set
50# appropriately. 43# appropriately.
@@ -57,7 +50,7 @@ fi
57 50
58# Run the script on all the litmus tests in the specified directory 51# Run the script on all the litmus tests in the specified directory
59ret=0 52ret=0
60for i in litmus-tests/*.litmus 53for i in $litmusdir/*.litmus
61do 54do
62 if ! $clscript $i 55 if ! $clscript $i
63 then 56 then
@@ -66,8 +59,8 @@ do
66done 59done
67if test "$ret" -ne 0 60if test "$ret" -ne 0
68then 61then
69 echo " ^^^ VERIFICATION MISMATCHES" 62 echo " ^^^ VERIFICATION MISMATCHES" 1>&2
70else 63else
71 echo All litmus tests verified as was expected. 64 echo All litmus tests verified as was expected. 1>&2
72fi 65fi
73exit $ret 66exit $ret
diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh
new file mode 100644
index 000000000000..6589fbb6f653
--- /dev/null
+++ b/tools/memory-model/scripts/checkghlitmus.sh
@@ -0,0 +1,65 @@
1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
3#
4# Runs the C-language litmus tests having a maximum number of processes
5# to run, defaults to 6.
6#
7# sh checkghlitmus.sh
8#
9# Run from the Linux kernel tools/memory-model directory. See the
10# parseargs.sh scripts for arguments.
11
12. scripts/parseargs.sh
13
14T=/tmp/checkghlitmus.sh.$$
15trap 'rm -rf $T' 0
16mkdir $T
17
18# Clone the repository if it is not already present.
19if test -d litmus
20then
21 :
22else
23 git clone https://github.com/paulmckrcu/litmus
24 ( cd litmus; git checkout origin/master )
25fi
26
27# Create any new directories that have appeared in the github litmus
28# repo since the last run.
29if test "$LKMM_DESTDIR" != "."
30then
31 find litmus -type d -print |
32 ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
33fi
34
35# Create a list of the C-language litmus tests previously run.
36( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) |
37 sed -e 's/\.out$//' |
38 xargs -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' |
39 xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already
40
41# Create a list of C-language litmus tests with "Result:" commands and
42# no more than the specified number of processes.
43find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
44xargs < $T/list-C -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result
45xargs < $T/list-C-result -r grep -L "^P${LKMM_PROCS}" > $T/list-C-result-short
46
47# Form list of tests without corresponding .litmus.out files
48sort $T/list-C-already $T/list-C-result-short | uniq -u > $T/list-C-needed
49
50# Run any needed tests.
51if scripts/runlitmushist.sh < $T/list-C-needed > $T/run.stdout 2> $T/run.stderr
52then
53 errs=
54else
55 errs=1
56fi
57
58sed < $T/list-C-result-short -e 's,^,scripts/judgelitmus.sh ,' |
59 sh > $T/judge.stdout 2> $T/judge.stderr
60
61if test -n "$errs"
62then
63 cat $T/run.stderr 1>&2
64fi
65grep '!!!' $T/judge.stdout
diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh
index bf12a75c0719..dd08801a30b0 100755
--- a/tools/memory-model/scripts/checklitmus.sh
+++ b/tools/memory-model/scripts/checklitmus.sh
@@ -1,40 +1,24 @@
1#!/bin/sh 1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
2# 3#
3# Run a herd test and check the result against a "Result:" comment within 4# Run a herd test and invokes judgelitmus.sh to check the result against
4# the litmus test. If the verification result does not match that specified 5# a "Result:" comment within the litmus test. It also outputs verification
5# in the litmus test, this script prints an error message prefixed with
6# "^^^" and exits with a non-zero status. It also outputs verification
7# results to a file whose name is that of the specified litmus test, but 6# results to a file whose name is that of the specified litmus test, but
8# with ".out" appended. 7# with ".out" appended.
9# 8#
10# Usage: 9# Usage:
11# checklitmus.sh file.litmus 10# checklitmus.sh file.litmus
12# 11#
13# The LINUX_HERD_OPTIONS environment variable may be used to specify 12# Run this in the directory containing the memory model, specifying the
14# arguments to herd, which default to "-conf linux-kernel.cfg". Thus, 13# pathname of the litmus test to check. The caller is expected to have
15# one would normally run this in the directory containing the memory model, 14# properly set up the LKMM environment variables.
16# specifying the pathname of the litmus test to check.
17#
18# This program is free software; you can redistribute it and/or modify
19# it under the terms of the GNU General Public License as published by
20# the Free Software Foundation; either version 2 of the License, or
21# (at your option) any later version.
22#
23# This program is distributed in the hope that it will be useful,
24# but WITHOUT ANY WARRANTY; without even the implied warranty of
25# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
26# GNU General Public License for more details.
27#
28# You should have received a copy of the GNU General Public License
29# along with this program; if not, you can access it online at
30# http://www.gnu.org/licenses/gpl-2.0.html.
31# 15#
32# Copyright IBM Corporation, 2018 16# Copyright IBM Corporation, 2018
33# 17#
34# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> 18# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
35 19
36litmus=$1 20litmus=$1
37herdoptions=${LINUX_HERD_OPTIONS--conf linux-kernel.cfg} 21herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
38 22
39if test -f "$litmus" -a -r "$litmus" 23if test -f "$litmus" -a -r "$litmus"
40then 24then
@@ -43,44 +27,8 @@ else
43 echo ' --- ' error: \"$litmus\" is not a readable file 27 echo ' --- ' error: \"$litmus\" is not a readable file
44 exit 255 28 exit 255
45fi 29fi
46if grep -q '^ \* Result: ' $litmus
47then
48 outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
49else
50 outcome=specified
51fi
52 30
53echo Herd options: $herdoptions > $litmus.out 31echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
54/usr/bin/time herd7 -o ~/tmp $herdoptions $litmus >> $litmus.out 2>&1 32/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
55grep "Herd options:" $litmus.out 33
56grep '^Observation' $litmus.out 34scripts/judgelitmus.sh $litmus
57if grep -q '^Observation' $litmus.out
58then
59 :
60else
61 cat $litmus.out
62 echo ' ^^^ Verification error'
63 echo ' ^^^ Verification error' >> $litmus.out 2>&1
64 exit 255
65fi
66if test "$outcome" = DEADLOCK
67then
68 echo grep 3 and 4
69 if grep '^Observation' $litmus.out | grep -q 'Never 0 0$'
70 then
71 ret=0
72 else
73 echo " ^^^ Unexpected non-$outcome verification"
74 echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
75 ret=1
76 fi
77elif grep '^Observation' $litmus.out | grep -q $outcome || test "$outcome" = Maybe
78then
79 ret=0
80else
81 echo " ^^^ Unexpected non-$outcome verification"
82 echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
83 ret=1
84fi
85tail -2 $litmus.out | head -1
86exit $ret
diff --git a/tools/memory-model/scripts/checklitmushist.sh b/tools/memory-model/scripts/checklitmushist.sh
new file mode 100644
index 000000000000..1d210ffb7c8a
--- /dev/null
+++ b/tools/memory-model/scripts/checklitmushist.sh
@@ -0,0 +1,60 @@
1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
3#
4# Reruns the C-language litmus tests previously run that match the
5# specified criteria, and compares the result to that of the previous
6# runs from initlitmushist.sh and/or newlitmushist.sh.
7#
8# sh checklitmushist.sh
9#
10# Run from the Linux kernel tools/memory-model directory.
11# See scripts/parseargs.sh for list of arguments.
12#
13# Copyright IBM Corporation, 2018
14#
15# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
16
17. scripts/parseargs.sh
18
19T=/tmp/checklitmushist.sh.$$
20trap 'rm -rf $T' 0
21mkdir $T
22
23if test -d litmus
24then
25 :
26else
27 echo Run scripts/initlitmushist.sh first, need litmus repo.
28 exit 1
29fi
30
31# Create the results directory and populate it with subdirectories.
32# The initial output is created here to avoid clobbering the output
33# generated earlier.
34mkdir $T/results
35find litmus -type d -print | ( cd $T/results; sed -e 's/^/mkdir -p /' | sh )
36
37# Create the list of litmus tests already run, then remove those that
38# are excluded by this run's --procs argument.
39( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) |
40 sed -e 's/\.out$//' |
41 xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already
42xargs < $T/list-C-already -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
43
44# Redirect output, run tests, then restore destination directory.
45destdir="$LKMM_DESTDIR"
46LKMM_DESTDIR=$T/results; export LKMM_DESTDIR
47scripts/runlitmushist.sh < $T/list-C-short > $T/runlitmushist.sh.out 2>&1
48LKMM_DESTDIR="$destdir"; export LKMM_DESTDIR
49
50# Move the newly generated .litmus.out files to .litmus.out.new files
51# in the destination directory.
52cdir=`pwd`
53ddir=`awk -v c="$cdir" -v d="$LKMM_DESTDIR" \
54 'END { if (d ~ /^\//) print d; else print c "/" d; }' < /dev/null`
55( cd $T/results; find litmus -type f -name '*.litmus.out' -print |
56 sed -e 's,^.*$,cp & '"$ddir"'/&.new,' | sh )
57
58sed < $T/list-C-short -e 's,^,'"$LKMM_DESTDIR/"',' |
59 sh scripts/cmplitmushist.sh
60exit $?
diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh
new file mode 100644
index 000000000000..0f498aeeccf5
--- /dev/null
+++ b/tools/memory-model/scripts/cmplitmushist.sh
@@ -0,0 +1,87 @@
1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
3#
4# Compares .out and .out.new files for each name on standard input,
5# one full pathname per line. Outputs comparison results followed by
6# a summary.
7#
8# sh cmplitmushist.sh
9
10T=/tmp/cmplitmushist.sh.$$
11trap 'rm -rf $T' 0
12mkdir $T
13
14# comparetest oldpath newpath
15perfect=0
16obsline=0
17noobsline=0
18obsresult=0
19badcompare=0
20comparetest () {
21 grep -v 'maxresident)k\|minor)pagefaults\|^Time' $1 > $T/oldout
22 grep -v 'maxresident)k\|minor)pagefaults\|^Time' $2 > $T/newout
23 if cmp -s $T/oldout $T/newout && grep -q '^Observation' $1
24 then
25 echo Exact output match: $2
26 perfect=`expr "$perfect" + 1`
27 return 0
28 fi
29
30 grep '^Observation' $1 > $T/oldout
31 grep '^Observation' $2 > $T/newout
32 if test -s $T/oldout -o -s $T/newout
33 then
34 if cmp -s $T/oldout $T/newout
35 then
36 echo Matching Observation result and counts: $2
37 obsline=`expr "$obsline" + 1`
38 return 0
39 fi
40 else
41 echo Missing Observation line "(e.g., herd7 timeout)": $2
42 noobsline=`expr "$noobsline" + 1`
43 return 0
44 fi
45
46 grep '^Observation' $1 | awk '{ print $3 }' > $T/oldout
47 grep '^Observation' $2 | awk '{ print $3 }' > $T/newout
48 if cmp -s $T/oldout $T/newout
49 then
50 echo Matching Observation Always/Sometimes/Never result: $2
51 obsresult=`expr "$obsresult" + 1`
52 return 0
53 fi
54 echo ' !!!' Result changed: $2
55 badcompare=`expr "$badcompare" + 1`
56 return 1
57}
58
59sed -e 's/^.*$/comparetest &.out &.out.new/' > $T/cmpscript
60. $T/cmpscript > $T/cmpscript.out
61cat $T/cmpscript.out
62
63echo ' ---' Summary: 1>&2
64grep '!!!' $T/cmpscript.out 1>&2
65if test "$perfect" -ne 0
66then
67 echo Exact output matches: $perfect 1>&2
68fi
69if test "$obsline" -ne 0
70then
71 echo Matching Observation result and counts: $obsline 1>&2
72fi
73if test "$noobsline" -ne 0
74then
75 echo Missing Observation line "(e.g., herd7 timeout)": $noobsline 1>&2
76fi
77if test "$obsresult" -ne 0
78then
79 echo Matching Observation Always/Sometimes/Never result: $obsresult 1>&2
80fi
81if test "$badcompare" -ne 0
82then
83 echo "!!!" Result changed: $badcompare 1>&2
84 exit 1
85fi
86
87exit 0
diff --git a/tools/memory-model/scripts/initlitmushist.sh b/tools/memory-model/scripts/initlitmushist.sh
new file mode 100644
index 000000000000..956b6957484d
--- /dev/null
+++ b/tools/memory-model/scripts/initlitmushist.sh
@@ -0,0 +1,68 @@
1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
3#
4# Runs the C-language litmus tests matching the specified criteria.
5# Generates the output for each .litmus file into a corresponding
6# .litmus.out file, and does not judge the result.
7#
8# sh initlitmushist.sh
9#
10# Run from the Linux kernel tools/memory-model directory.
11# See scripts/parseargs.sh for list of arguments.
12#
13# This script can consume significant wallclock time and CPU, especially as
14# the value of --procs rises. On a four-core (eight hardware threads)
15# 2.5GHz x86 with a one-minute per-run timeout:
16#
17# --procs wallclock CPU timeouts tests
18# 1 0m11.241s 0m1.086s 0 19
19# 2 1m12.598s 2m8.459s 2 393
20# 3 1m30.007s 6m2.479s 4 2291
21# 4 3m26.042s 18m5.139s 9 3217
22# 5 4m26.661s 23m54.128s 13 3784
23# 6 4m41.900s 26m4.721s 13 4352
24# 7 5m51.463s 35m50.868s 13 4626
25# 8 10m5.235s 68m43.672s 34 5117
26# 9 15m57.80s 105m58.101s 69 5156
27# 10 16m14.13s 103m35.009s 69 5165
28# 20 27m48.55s 198m3.286s 156 5269
29#
30# Increasing the timeout on the 20-process run to five minutes increases
31# the runtime to about 90 minutes with the CPU time rising to about
32# 10 hours. On the other hand, it decreases the number of timeouts to 101.
33#
34# Note that there are historical tests for which herd7 will fail
35# completely, for example, litmus/manual/atomic/C-unlock-wait-00.litmus
36# contains a call to spin_unlock_wait(), which no longer exists in either
37# the kernel or LKMM.
38
39. scripts/parseargs.sh
40
41T=/tmp/initlitmushist.sh.$$
42trap 'rm -rf $T' 0
43mkdir $T
44
45if test -d litmus
46then
47 :
48else
49 git clone https://github.com/paulmckrcu/litmus
50 ( cd litmus; git checkout origin/master )
51fi
52
53# Create any new directories that have appeared in the github litmus
54# repo since the last run.
55if test "$LKMM_DESTDIR" != "."
56then
57 find litmus -type d -print |
58 ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
59fi
60
61# Create a list of the C-language litmus tests with no more than the
62# specified number of processes (per the --procs argument).
63find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
64xargs < $T/list-C -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
65
66scripts/runlitmushist.sh < $T/list-C-short
67
68exit 0
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
new file mode 100644
index 000000000000..0cc63875e395
--- /dev/null
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -0,0 +1,78 @@
1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
3#
4# Given a .litmus test and the corresponding .litmus.out file, check
5# the .litmus.out file against the "Result:" comment to judge whether
6# the test ran correctly.
7#
8# Usage:
9# judgelitmus.sh file.litmus
10#
11# Run this in the directory containing the memory model, specifying the
12# pathname of the litmus test to check.
13#
14# Copyright IBM Corporation, 2018
15#
16# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
17
18litmus=$1
19
20if test -f "$litmus" -a -r "$litmus"
21then
22 :
23else
24 echo ' --- ' error: \"$litmus\" is not a readable file
25 exit 255
26fi
27if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out
28then
29 :
30else
31 echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file
32 exit 255
33fi
34if grep -q '^ \* Result: ' $litmus
35then
36 outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
37else
38 outcome=specified
39fi
40
41grep '^Observation' $LKMM_DESTDIR/$litmus.out
42if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
43then
44 :
45else
46 echo ' !!! Verification error' $litmus
47 if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
48 then
49 echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1
50 fi
51 exit 255
52fi
53if test "$outcome" = DEADLOCK
54then
55 if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
56 then
57 ret=0
58 else
59 echo " !!! Unexpected non-$outcome verification" $litmus
60 if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
61 then
62 echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
63 fi
64 ret=1
65 fi
66elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
67then
68 ret=0
69else
70 echo " !!! Unexpected non-$outcome verification" $litmus
71 if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
72 then
73 echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
74 fi
75 ret=1
76fi
77tail -2 $LKMM_DESTDIR/$litmus.out | head -1
78exit $ret
diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh
new file mode 100644
index 000000000000..991f8f814881
--- /dev/null
+++ b/tools/memory-model/scripts/newlitmushist.sh
@@ -0,0 +1,61 @@
1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
3#
4# Runs the C-language litmus tests matching the specified criteria
5# that do not already have a corresponding .litmus.out file, and does
6# not judge the result.
7#
8# sh newlitmushist.sh
9#
10# Run from the Linux kernel tools/memory-model directory.
11# See scripts/parseargs.sh for list of arguments.
12#
13# Copyright IBM Corporation, 2018
14#
15# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
16
17. scripts/parseargs.sh
18
19T=/tmp/newlitmushist.sh.$$
20trap 'rm -rf $T' 0
21mkdir $T
22
23if test -d litmus
24then
25 :
26else
27 echo Run scripts/initlitmushist.sh first, need litmus repo.
28 exit 1
29fi
30
31# Create any new directories that have appeared in the github litmus
32# repo since the last run.
33if test "$LKMM_DESTDIR" != "."
34then
35 find litmus -type d -print |
36 ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
37fi
38
39# Create a list of the C-language litmus tests previously run.
40( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) |
41 sed -e 's/\.out$//' |
42 xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already
43
44# Form full list of litmus tests with no more than the specified
45# number of processes (per the --procs argument).
46find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C-all
47xargs < $T/list-C-all -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
48
49# Form list of new tests. Note: This does not handle litmus-test deletion!
50sort $T/list-C-already $T/list-C-short | uniq -u > $T/list-C-new
51
52# Form list of litmus tests that have changed since the last run.
53sed < $T/list-C-short -e 's,^.*$,if test & -nt '"$LKMM_DESTDIR"'/&.out; then echo &; fi,' > $T/list-C-script
54sh $T/list-C-script > $T/list-C-newer
55
56# Merge the list of new and of updated litmus tests: These must be (re)run.
57sort -u $T/list-C-new $T/list-C-newer > $T/list-C-needed
58
59scripts/runlitmushist.sh < $T/list-C-needed
60
61exit 0
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
new file mode 100644
index 000000000000..96b307c8d64a
--- /dev/null
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -0,0 +1,126 @@
1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
3#
4# the corresponding .litmus.out file, and does not judge the result.
5#
6# . scripts/parseargs.sh
7#
8# Include into other Linux kernel tools/memory-model scripts.
9#
10# Copyright IBM Corporation, 2018
11#
12# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
13
14T=/tmp/parseargs.sh.$$
15mkdir $T
16
17# Initialize one parameter: initparam name default
18initparam () {
19 echo if test -z '"$'$1'"' > $T/s
20 echo then >> $T/s
21 echo $1='"'$2'"' >> $T/s
22 echo export $1 >> $T/s
23 echo fi >> $T/s
24 echo $1_DEF='$'$1 >> $T/s
25 . $T/s
26}
27
28initparam LKMM_DESTDIR "."
29initparam LKMM_HERD_OPTIONS "-conf linux-kernel.cfg"
30initparam LKMM_JOBS `getconf _NPROCESSORS_ONLN`
31initparam LKMM_PROCS "3"
32initparam LKMM_TIMEOUT "1m"
33
34scriptname=$0
35
36usagehelp () {
37 echo "Usage $scriptname [ arguments ]"
38 echo " --destdir path (place for .litmus.out, default by .litmus)"
39 echo " --herdopts -conf linux-kernel.cfg ..."
40 echo " --jobs N (number of jobs, default one per CPU)"
41 echo " --procs N (litmus tests with at most this many processes)"
42 echo " --timeout N (herd7 timeout (e.g., 10s, 1m, 2hr, 1d, '')"
43 echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'"
44 exit 1
45}
46
47usage () {
48 usagehelp 1>&2
49}
50
51# checkarg --argname argtype $# arg mustmatch cannotmatch
52checkarg () {
53 if test $3 -le 1
54 then
55 echo $1 needs argument $2 matching \"$5\"
56 usage
57 fi
58 if echo "$4" | grep -q -e "$5"
59 then
60 :
61 else
62 echo $1 $2 \"$4\" must match \"$5\"
63 usage
64 fi
65 if echo "$4" | grep -q -e "$6"
66 then
67 echo $1 $2 \"$4\" must not match \"$6\"
68 usage
69 fi
70}
71
72while test $# -gt 0
73do
74 case "$1" in
75 --destdir)
76 checkarg --destdir "(path to directory)" "$#" "$2" '.\+' '^--'
77 LKMM_DESTDIR="$2"
78 mkdir $LKMM_DESTDIR > /dev/null 2>&1
79 if ! test -e "$LKMM_DESTDIR"
80 then
81 echo "Cannot create directory --destdir '$LKMM_DESTDIR'"
82 usage
83 fi
84 if test -d "$LKMM_DESTDIR" -a -w "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR"
85 then
86 :
87 else
88 echo "Directory --destdir '$LKMM_DESTDIR' insufficient permissions to create files"
89 usage
90 fi
91 shift
92 ;;
93 --herdopts|--herdopt)
94 checkarg --destdir "(herd options)" "$#" "$2" '.*' '^--'
95 LKMM_HERD_OPTIONS="$2"
96 shift
97 ;;
98 --jobs|--job)
99 checkarg --jobs "(number)" "$#" "$2" '^[0-9]\+$' '^--'
100 LKMM_JOBS="$2"
101 shift
102 ;;
103 --procs|--proc)
104 checkarg --procs "(number)" "$#" "$2" '^[0-9]\+$' '^--'
105 LKMM_PROCS="$2"
106 shift
107 ;;
108 --timeout)
109 checkarg --timeout "(timeout spec)" "$#" "$2" '^\([0-9]\+[smhd]\?\|\)$' '^--'
110 LKMM_TIMEOUT="$2"
111 shift
112 ;;
113 *)
114 echo Unknown argument $1
115 usage
116 ;;
117 esac
118 shift
119done
120if test -z "$LKMM_TIMEOUT"
121then
122 LKMM_TIMEOUT_CMD=""; export LKMM_TIMEOUT_CMD
123else
124 LKMM_TIMEOUT_CMD="timeout $LKMM_TIMEOUT"; export LKMM_TIMEOUT_CMD
125fi
126rm -rf $T
diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh
new file mode 100644
index 000000000000..e507f5f933d5
--- /dev/null
+++ b/tools/memory-model/scripts/runlitmushist.sh
@@ -0,0 +1,87 @@
1#!/bin/bash
2# SPDX-License-Identifier: GPL-2.0+
3#
4# Runs the C-language litmus tests specified on standard input, using up
5# to the specified number of CPUs (defaulting to all of them) and placing
6# the results in the specified directory (defaulting to the same place
7# the litmus test came from).
8#
9# sh runlitmushist.sh
10#
11# Run from the Linux kernel tools/memory-model directory.
12# This script uses environment variables produced by parseargs.sh.
13#
14# Copyright IBM Corporation, 2018
15#
16# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
17
18T=/tmp/runlitmushist.sh.$$
19trap 'rm -rf $T' 0
20mkdir $T
21
22if test -d litmus
23then
24 :
25else
26 echo Directory \"litmus\" missing, aborting run.
27 exit 1
28fi
29
30# Prefixes for per-CPU scripts
31for ((i=0;i<$LKMM_JOBS;i++))
32do
33 echo dir="$LKMM_DESTDIR" > $T/$i.sh
34 echo T=$T >> $T/$i.sh
35 echo herdoptions=\"$LKMM_HERD_OPTIONS\" >> $T/$i.sh
36 cat << '___EOF___' >> $T/$i.sh
37 runtest () {
38 echo ' ... ' /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 '>' $dir/$1.out '2>&1'
39 if /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 > $dir/$1.out 2>&1
40 then
41 if ! grep -q '^Observation ' $dir/$1.out
42 then
43 echo ' !!! Herd failed, no Observation:' $1
44 fi
45 else
46 exitcode=$?
47 if test "$exitcode" -eq 124
48 then
49 exitmsg="timed out"
50 else
51 exitmsg="failed, exit code $exitcode"
52 fi
53 echo ' !!! Herd' ${exitmsg}: $1
54 fi
55 }
56___EOF___
57done
58
59awk -v q="'" -v b='\\' '
60{
61 print "echo `grep " q "^P[0-9]" b "+(" q " " $0 " | tail -1 | sed -e " q "s/^P" b "([0-9]" b "+" b ")(.*$/" b "1/" q "` " $0
62}' | bash |
63sort -k1n |
64awk -v ncpu=$LKMM_JOBS -v t=$T '
65{
66 print "runtest " $2 >> t "/" NR % ncpu ".sh";
67}
68
69END {
70 for (i = 0; i < ncpu; i++) {
71 print "sh " t "/" i ".sh > " t "/" i ".sh.out 2>&1 &";
72 close(t "/" i ".sh");
73 }
74 print "wait";
75}' | sh
76cat $T/*.sh.out
77if grep -q '!!!' $T/*.sh.out
78then
79 echo ' ---' Summary: 1>&2
80 grep '!!!' $T/*.sh.out 1>&2
81 nfail="`grep '!!!' $T/*.sh.out | wc -l`"
82 echo 'Number of failed herd runs (e.g., timeout): ' $nfail 1>&2
83 exit 1
84else
85 echo All runs completed successfully. 1>&2
86 exit 0
87fi