Hello! This series contains LKMM updates: 1. Make scripts be executable. 2-3. Make LKMM scripts note timeouts instead of just saying that the validation was bad. 4. Make LKMM scripts identify litmus-test typos and use of unsupported primitives instead of just saying that the validation was bad. 5. Make LKMM scripts detect unconditional deadlocks. 6. Fix email address on LKMM scripts. 7-29. Leverage Boqun Feng's C-to-assembly litmus-test-translation capability to allow verifying LKMM against hardware models for checkalllitmus.sh. This is a work in progress. 30. Use cumul-fence instead of fence in ->prop example, courtesy of Joel Fernandes. 31. Update the informal documentation, courtesy of Andrea Parri. Thanx, Paul ------------------------------------------------------------------------ Documentation/explanation.txt | 53 +++++++-------- README | 18 ++--- litmus-tests/.gitignore | 4 - scripts/README | 16 +++- scripts/checkalllitmus.sh | 29 ++++---- scripts/checkghlitmus.sh | 11 +-- scripts/checklitmus.sh | 101 ++++++++++++----------------- scripts/checklitmushist.sh | 2 scripts/checktheselitmus.sh | 43 ++++++++++++ scripts/cmplitmushist.sh | 53 ++++++++++++++- scripts/hwfnseg.sh | 20 +++++ scripts/initlitmushist.sh | 2 scripts/judgelitmus.sh | 142 +++++++++++++++++++++++++++++++---------- scripts/newlitmushist.sh | 4 - scripts/parseargs.sh | 21 ++++-- scripts/runlitmus.sh | 144 ++++++++++++++++++++++++++++++++---------- scripts/runlitmushist.sh | 30 +++++--- scripts/simpletest.sh | 35 ++++++++++ 18 files changed, 514 insertions(+), 214 deletions(-)
This commit simplifies life a bit by making all of the scripts in tools/memory-model/scripts be executable. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/checkghlitmus.sh | 0 tools/memory-model/scripts/checklitmushist.sh | 0 tools/memory-model/scripts/cmplitmushist.sh | 0 tools/memory-model/scripts/initlitmushist.sh | 0 tools/memory-model/scripts/judgelitmus.sh | 0 tools/memory-model/scripts/newlitmushist.sh | 0 tools/memory-model/scripts/parseargs.sh | 0 tools/memory-model/scripts/runlitmushist.sh | 0 8 files changed, 0 insertions(+), 0 deletions(-) mode change 100644 => 100755 tools/memory-model/scripts/checkghlitmus.sh mode change 100644 => 100755 tools/memory-model/scripts/checklitmushist.sh mode change 100644 => 100755 tools/memory-model/scripts/cmplitmushist.sh mode change 100644 => 100755 tools/memory-model/scripts/initlitmushist.sh mode change 100644 => 100755 tools/memory-model/scripts/judgelitmus.sh mode change 100644 => 100755 tools/memory-model/scripts/newlitmushist.sh mode change 100644 => 100755 tools/memory-model/scripts/parseargs.sh mode change 100644 => 100755 tools/memory-model/scripts/runlitmushist.sh diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh old mode 100644 new mode 100755 diff --git a/tools/memory-model/scripts/checklitmushist.sh b/tools/memory-model/scripts/checklitmushist.sh old mode 100644 new mode 100755 diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh old mode 100644 new mode 100755 diff --git a/tools/memory-model/scripts/initlitmushist.sh b/tools/memory-model/scripts/initlitmushist.sh old mode 100644 new mode 100755 diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh old mode 100644 new mode 100755 diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh old mode 100644 new mode 100755 diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh old mode 100644 new mode 100755 diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh old mode 100644 new mode 100755 -- 2.17.1
Currently, judgelitmus.sh treats timeouts (as in the "--timeout" argument) as "!!! Verification error". This can be misleading because it is quite possible that running the test longer would have produced a verification. This commit therefore changes judgelitmus.sh to check for timeouts and to report them with "!!! Timeout". Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/judgelitmus.sh | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index 0cc63875e395..d3c313b9a458 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -42,6 +42,14 @@ grep '^Observation' $LKMM_DESTDIR/$litmus.out if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out then : +elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out +then + echo ' !!! Timeout' $litmus + if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + then + echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmus.out 2>&1 + fi + exit 124 else echo ' !!! Verification error' $litmus if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out -- 2.17.1
Currently, cmplitmushist.sh treats timeouts (as in the "--timeout" argument) as "Missing Observation line". This can be misleading because it is quite possible that running the test longer would have produced a verification. This commit therefore changes cmplitmushist.sh to check for timeouts and to report them with "Timed out". Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/cmplitmushist.sh | 22 +++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh index 0f498aeeccf5..b9c174dd8004 100755 --- a/tools/memory-model/scripts/cmplitmushist.sh +++ b/tools/memory-model/scripts/cmplitmushist.sh @@ -12,12 +12,30 @@ trap 'rm -rf $T' 0 mkdir $T # comparetest oldpath newpath +timedout=0 perfect=0 obsline=0 noobsline=0 obsresult=0 badcompare=0 comparetest () { + if grep -q '^Command exited with non-zero status 124' $1 || + grep -q '^Command exited with non-zero status 124' $2 + then + if grep -q '^Command exited with non-zero status 124' $1 && + grep -q '^Command exited with non-zero status 124' $2 + then + echo Both runs timed out: $2 + elif grep -q '^Command exited with non-zero status 124' $1 + then + echo Old run timed out: $2 + elif grep -q '^Command exited with non-zero status 124' $2 + then + echo New run timed out: $2 + fi + timedout=`expr "$timedout" + 1` + return 0 + fi grep -v 'maxresident)k\|minor)pagefaults\|^Time' $1 > $T/oldout grep -v 'maxresident)k\|minor)pagefaults\|^Time' $2 > $T/newout if cmp -s $T/oldout $T/newout && grep -q '^Observation' $1 @@ -78,6 +96,10 @@ if test "$obsresult" -ne 0 then echo Matching Observation Always/Sometimes/Never result: $obsresult 1>&2 fi +if test "$timedout" -ne 0 +then + echo "!!!" Timed out: $timedout 1>&2 +fi if test "$badcompare" -ne 0 then echo "!!!" Result changed: $badcompare 1>&2 -- 2.17.1
Currently, judgelitmus.sh treats use of unknown primitives (such as srcu_read_lock() prior to SRCU support) as "!!! Verification error". This can be misleading because it fails to call out typos and running a version LKMM on a litmus test requiring a feature not provided by that version. This commit therefore changes judgelitmus.sh to check for unknown primitives and to report them, for example, with: '!!! Current LKMM version does not know "rcu_write_lock"'. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/cmplitmushist.sh | 31 ++++++++++++++++++--- tools/memory-model/scripts/judgelitmus.sh | 12 ++++++++ 2 files changed, 39 insertions(+), 4 deletions(-) diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh index b9c174dd8004..ca1ac8b64614 100755 --- a/tools/memory-model/scripts/cmplitmushist.sh +++ b/tools/memory-model/scripts/cmplitmushist.sh @@ -12,6 +12,7 @@ trap 'rm -rf $T' 0 mkdir $T # comparetest oldpath newpath +badmacnam=0 timedout=0 perfect=0 obsline=0 @@ -19,8 +20,26 @@ noobsline=0 obsresult=0 badcompare=0 comparetest () { - if grep -q '^Command exited with non-zero status 124' $1 || - grep -q '^Command exited with non-zero status 124' $2 + if grep -q ': Unknown macro ' $1 || grep -q ': Unknown macro ' $2 + then + if grep -q ': Unknown macro ' $1 + then + badname=`grep ': Unknown macro ' $1 | + sed -e 's/^.*: Unknown macro //' | + sed -e 's/ (User error).*$//'` + echo 'Current LKMM version does not know "'$badname'"' $1 + fi + if grep -q ': Unknown macro ' $2 + then + badname=`grep ': Unknown macro ' $2 | + sed -e 's/^.*: Unknown macro //' | + sed -e 's/ (User error).*$//'` + echo 'Current LKMM version does not know "'$badname'"' $2 + fi + badmacnam=`expr "$badmacnam" + 1` + return 0 + elif grep -q '^Command exited with non-zero status 124' $1 || + grep -q '^Command exited with non-zero status 124' $2 then if grep -q '^Command exited with non-zero status 124' $1 && grep -q '^Command exited with non-zero status 124' $2 @@ -56,7 +75,7 @@ comparetest () { return 0 fi else - echo Missing Observation line "(e.g., herd7 timeout)": $2 + echo Missing Observation line "(e.g., syntax error)": $2 noobsline=`expr "$noobsline" + 1` return 0 fi @@ -90,7 +109,7 @@ then fi if test "$noobsline" -ne 0 then - echo Missing Observation line "(e.g., herd7 timeout)": $noobsline 1>&2 + echo Missing Observation line "(e.g., syntax error)": $noobsline 1>&2 fi if test "$obsresult" -ne 0 then @@ -100,6 +119,10 @@ if test "$timedout" -ne 0 then echo "!!!" Timed out: $timedout 1>&2 fi +if test "$badmacnam" -ne 0 +then + echo "!!!" Unknown primitive: $badmacnam 1>&2 +fi if test "$badcompare" -ne 0 then echo "!!!" Result changed: $badcompare 1>&2 diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index d3c313b9a458..d40439c7b71e 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -42,6 +42,18 @@ grep '^Observation' $LKMM_DESTDIR/$litmus.out if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out then : +elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out +then + badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out | + sed -e 's/^.*: Unknown macro //' | + sed -e 's/ (User error).*$//'` + badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus" + echo $badmsg + if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + then + echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmus.out 2>&1 + fi + exit 254 elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out then echo ' !!! Timeout' $litmus -- 2.17.1
If a litmus test specifies "Result: Never" and if it contains an unconditional ("hard") deadlock, then running checklitmus.sh on it will not flag any errors, despite the fact that there are no executions. This commit therefore updates judgelitmus.sh to complain about tests with no executions that are marked, but not as "Result: DEADLOCK". Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/judgelitmus.sh | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index d40439c7b71e..84c62eee321b 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -83,6 +83,14 @@ then fi ret=1 fi +elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$' +then + echo " !!! Unexpected non-$outcome deadlock" $litmus + if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + then + echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1 + fi + ret=1 elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe then ret=0 -- 2.17.1
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/checkalllitmus.sh | 2 +- tools/memory-model/scripts/checklitmus.sh | 2 +- tools/memory-model/scripts/checklitmushist.sh | 2 +- tools/memory-model/scripts/judgelitmus.sh | 2 +- tools/memory-model/scripts/newlitmushist.sh | 2 +- tools/memory-model/scripts/parseargs.sh | 2 +- tools/memory-model/scripts/runlitmushist.sh | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh index 3c0c7fbbd223..10e14d94acee 100755 --- a/tools/memory-model/scripts/checkalllitmus.sh +++ b/tools/memory-model/scripts/checkalllitmus.sh @@ -17,7 +17,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> . scripts/parseargs.sh diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh index 11461ed40b5e..638b8c610894 100755 --- a/tools/memory-model/scripts/checklitmus.sh +++ b/tools/memory-model/scripts/checklitmus.sh @@ -15,7 +15,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> litmus=$1 herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg} diff --git a/tools/memory-model/scripts/checklitmushist.sh b/tools/memory-model/scripts/checklitmushist.sh index 1d210ffb7c8a..406ecfc0aee4 100755 --- a/tools/memory-model/scripts/checklitmushist.sh +++ b/tools/memory-model/scripts/checklitmushist.sh @@ -12,7 +12,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> . scripts/parseargs.sh diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index 84c62eee321b..d82133e75580 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -13,7 +13,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> litmus=$1 diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh index 991f8f814881..3f4b06e29988 100755 --- a/tools/memory-model/scripts/newlitmushist.sh +++ b/tools/memory-model/scripts/newlitmushist.sh @@ -12,7 +12,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> . scripts/parseargs.sh diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh index 40f52080fdbd..afe7bd23de6b 100755 --- a/tools/memory-model/scripts/parseargs.sh +++ b/tools/memory-model/scripts/parseargs.sh @@ -9,7 +9,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> T=/tmp/parseargs.sh.$$ mkdir $T diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh index 6ed376f495bb..852786fef179 100755 --- a/tools/memory-model/scripts/runlitmushist.sh +++ b/tools/memory-model/scripts/runlitmushist.sh @@ -13,7 +13,7 @@ # # Copyright IBM Corporation, 2018 # -# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> +# Author: Paul E. McKenney <paulmck@linux.ibm.com> T=/tmp/runlitmushist.sh.$$ trap 'rm -rf $T' 0 -- 2.17.1
This commit adds a --hw argument to parseargs.sh to specify the CPU family for a hardware verification. For example, "--hw AArch64" will specify that a C-language litmus test is to be translated to ARMv8 and the result verified. This will set the LKMM_HW_MAP_FILE environment variable accordingly. If there is no --hw argument, this environment variable will be set to the empty string. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/parseargs.sh | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh index afe7bd23de6b..5f016fc3f3af 100755 --- a/tools/memory-model/scripts/parseargs.sh +++ b/tools/memory-model/scripts/parseargs.sh @@ -27,6 +27,7 @@ initparam () { initparam LKMM_DESTDIR "." initparam LKMM_HERD_OPTIONS "-conf linux-kernel.cfg" +initparam LKMM_HW_MAP_FILE "" initparam LKMM_JOBS `getconf _NPROCESSORS_ONLN` initparam LKMM_PROCS "3" initparam LKMM_TIMEOUT "1m" @@ -37,10 +38,11 @@ usagehelp () { echo "Usage $scriptname [ arguments ]" echo " --destdir path (place for .litmus.out, default by .litmus)" echo " --herdopts -conf linux-kernel.cfg ..." + echo " --hw AArch64" echo " --jobs N (number of jobs, default one per CPU)" echo " --procs N (litmus tests with at most this many processes)" echo " --timeout N (herd7 timeout (e.g., 10s, 1m, 2hr, 1d, '')" - echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'" + echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --hw '$LKMM_HW_MAP_FILE' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'" exit 1 } @@ -95,6 +97,11 @@ do LKMM_HERD_OPTIONS="$2" shift ;; + --hw) + checkarg --hw "(.map file architecture name)" "$#" "$2" '^[A-Za-z0-9_-]\+' '^--' + LKMM_HW_MAP_FILE="$2" + shift + ;; -j[1-9]*) njobs="`echo $1 | sed -e 's/^-j//'`" trailchars="`echo $njobs | sed -e 's/[0-9]\+\(.*\)$/\1/'`" -- 2.17.1
This commit makes the judgelitmus.sh script check the --hw argument (AKA the LKMM_HW_MAP_FILE environment variable) and to adjust its judgment for a run where a C-language litmus test has been translated to assembly and the assembly version verified. In this case, the assembly verification output is checked against the C-language script's "Result:" comment. However, because hardware can be stronger than LKMM requires, the judgelitmus.sh script forgives verification mismatches featuring a "Sometimes" in the C-language script and an "Always" or "Never" assembly-language verification. Note that deadlock is not forgiven, however, this should not normally be an issue given that C-language tests containing locking, RCU, or SRCU cannot be translated to assembly. However, this issue can crop up in litmus tests that mimic deadlock by using the "filter" clause to ignore all executions. It can also crop up when certain herd arguments are used to autofilter everything that does not match the "exists" clause in cases where the "exists" clause cannot be satisfied. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/README | 8 +-- tools/memory-model/scripts/judgelitmus.sh | 75 ++++++++++++++--------- 2 files changed, 51 insertions(+), 32 deletions(-) diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README index 095c7eb36f9f..0e29a52044c1 100644 --- a/tools/memory-model/scripts/README +++ b/tools/memory-model/scripts/README @@ -43,10 +43,10 @@ initlitmushist.sh judgelitmus.sh - Given a .litmus file and its .litmus.out herd7 output, check the - .litmus.out file against the .litmus file's "Result:" comment to - judge whether the test ran correctly. Not normally run manually, - provided instead for use by other scripts. + Given a .litmus file and its herd7 output, check the output file + against the .litmus file's "Result:" comment to judge whether + the test ran correctly. Not normally run manually, provided + instead for use by other scripts. newlitmushist.sh diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index d82133e75580..6f3c60065c8b 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -1,9 +1,14 @@ #!/bin/sh # SPDX-License-Identifier: GPL-2.0+ # -# Given a .litmus test and the corresponding .litmus.out file, check -# the .litmus.out file against the "Result:" comment to judge whether -# the test ran correctly. +# Given a .litmus test and the corresponding litmus output file, check +# the .litmus.out file against the "Result:" comment to judge whether the +# test ran correctly. If the --hw argument is omitted, check against the +# LKMM output, which is assumed to be in file.litmus.out. If this argument +# is provided, this is assumed to be a hardware test, and the output is +# assumed to be in file.HW.litmus.out, where "HW" is the --hw argument. +# In addition, non-Sometimes verification results will be noted, but +# forgiven. # # Usage: # judgelitmus.sh file.litmus @@ -24,11 +29,18 @@ else echo ' --- ' error: \"$litmus\" is not a readable file exit 255 fi -if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out +if test -z "$LKMM_HW_MAP_FILE" +then + litmusout=$litmus.out +else + litmusout="`echo $litmus | + sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out" +fi +if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout" then : else - echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file + echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file exit 255 fi if grep -q '^ \* Result: ' $litmus @@ -38,69 +50,76 @@ else outcome=specified fi -grep '^Observation' $LKMM_DESTDIR/$litmus.out -if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out +grep '^Observation' $LKMM_DESTDIR/$litmusout +if grep -q '^Observation' $LKMM_DESTDIR/$litmusout then : -elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out +elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout then - badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out | + badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout | sed -e 's/^.*: Unknown macro //' | sed -e 's/ (User error).*$//'` badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus" echo $badmsg - if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout then - echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmus.out 2>&1 + echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1 fi exit 254 -elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out +elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout then echo ' !!! Timeout' $litmus - if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout then - echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmus.out 2>&1 + echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1 fi exit 124 else echo ' !!! Verification error' $litmus - if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout then - echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1 + echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1 fi exit 255 fi if test "$outcome" = DEADLOCK then - if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$' + if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$' then ret=0 else echo " !!! Unexpected non-$outcome verification" $litmus - if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout then - echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1 + echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1 fi ret=1 fi -elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$' +elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$' then echo " !!! Unexpected non-$outcome deadlock" $litmus - if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout then - echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1 + echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1 fi ret=1 -elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe +elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe then ret=0 else - echo " !!! Unexpected non-$outcome verification" $litmus - if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out + if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes then - echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1 + flag="--- Forgiven" + ret=0 + else + flag="!!! Unexpected" + ret=1 + fi + echo " $flag non-$outcome verification" $litmus + if ! grep -qe "$flag" $LKMM_DESTDIR/$litmusout + then + echo " $flag non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1 fi - ret=1 fi -tail -2 $LKMM_DESTDIR/$litmus.out | head -1 +tail -2 $LKMM_DESTDIR/$litmusout | head -1 exit $ret -- 2.17.1
This commit abstracts out common function to check a given litmus test for locking, RCU, and SRCU in order to avoid duplicating code. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/simpletest.sh | 35 ++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100755 tools/memory-model/scripts/simpletest.sh diff --git a/tools/memory-model/scripts/simpletest.sh b/tools/memory-model/scripts/simpletest.sh new file mode 100755 index 000000000000..7edc5d361665 --- /dev/null +++ b/tools/memory-model/scripts/simpletest.sh @@ -0,0 +1,35 @@ +#!/bin/sh +# SPDX-License-Identifier: GPL-2.0+ +# +# Give zero status if this is a simple test and non-zero otherwise. +# Simple tests do not contain locking, RCU, or SRCU. +# +# Usage: +# simpletest.sh file.litmus +# +# Copyright IBM Corporation, 2019 +# +# Author: Paul E. McKenney <paulmck@linux.ibm.com> + + +litmus=$1 + +if test -f "$litmus" -a -r "$litmus" +then + : +else + echo ' --- ' error: \"$litmus\" is not a readable file + exit 255 +fi +exclude="^[[:space:]]*\(" +exclude="${exclude}spin_lock(\|spin_unlock(\|spin_trylock(\|spin_is_locked(" +exclude="${exclude}\|rcu_read_lock(\|rcu_read_unlock(" +exclude="${exclude}\|synchronize_rcu(\|synchronize_rcu_expedited(" +exclude="${exclude}\|srcu_read_lock(\|srcu_read_unlock(" +exclude="${exclude}\|synchronize_srcu(\|synchronize_srcu_expedited(" +exclude="${exclude}\)" +if grep -q $exclude $litmus +then + exit 255 +fi +exit 0 -- 2.17.1
The checkalllitmus.sh runs litmus tests in the litmus-tests directory, not those in the github archive, so this commit updates the comment to reflect this reality. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/checkalllitmus.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh index 10e14d94acee..54d8da8c338e 100755 --- a/tools/memory-model/scripts/checkalllitmus.sh +++ b/tools/memory-model/scripts/checkalllitmus.sh @@ -30,8 +30,8 @@ else exit 255 fi -# Create any new directories that have appeared in the github litmus -# repo since the last run. +# Create any new directories that have appeared in the litmus-tests +# directory since the last run. if test "$LKMM_DESTDIR" != "." then find $litmusdir -type d -print | -- 2.17.1
This commit makes checklitmus.sh and checkalllitmus.sh check to see if a hardware verification was specified (via the --hw command-line argument, which sets the LKMM_HW_MAP_FILE environment variable). If so, the C-language litmus test is converted to the specified type of assembly-language litmus test and herd is run on it. Hardware is permitted to be stronger than LKMM requires, so "Always" and "Never" verifications of "Sometimes" C-language litmus tests are forgiven. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/checkalllitmus.sh | 23 +++++------ tools/memory-model/scripts/checklitmus.sh | 42 ++++++++++++++++++-- 2 files changed, 49 insertions(+), 16 deletions(-) diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh index 54d8da8c338e..2d3ee850a839 100755 --- a/tools/memory-model/scripts/checkalllitmus.sh +++ b/tools/memory-model/scripts/checkalllitmus.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/bin/bash # SPDX-License-Identifier: GPL-2.0+ # # Run herd7 tests on all .litmus files in the litmus-tests directory @@ -8,6 +8,11 @@ # "^^^". It also outputs verification results to a file whose name is # that of the specified litmus test, but with ".out" appended. # +# If the --hw argument is specified, this script translates the .litmus +# C-language file to the specified type of assembly and verifies that. +# But in this case, litmus tests using complex synchronization (such as +# locking, RCU, and SRCU) are cheerfully ignored. +# # Usage: # checkalllitmus.sh # @@ -38,21 +43,15 @@ then ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh ) fi -# Find the checklitmus script. If it is not where we expect it, then -# assume that the caller has the PATH environment variable set -# appropriately. -if test -x scripts/checklitmus.sh -then - clscript=scripts/checklitmus.sh -else - clscript=checklitmus.sh -fi - # Run the script on all the litmus tests in the specified directory ret=0 for i in $litmusdir/*.litmus do - if ! $clscript $i + if test -n "$LKMM_HW_MAP_FILE" && ! scripts/simpletest.sh $i + then + continue + fi + if ! scripts/checklitmus.sh $i then ret=1 fi diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh index 638b8c610894..42ff11869cd6 100755 --- a/tools/memory-model/scripts/checklitmus.sh +++ b/tools/memory-model/scripts/checklitmus.sh @@ -6,6 +6,11 @@ # results to a file whose name is that of the specified litmus test, but # with ".out" appended. # +# If the --hw argument is specified, this script translates the .litmus +# C-language file to the specified type of assembly and verifies that. +# But in this case, litmus tests using complex synchronization (such as +# locking, RCU, and SRCU) are cheerfully ignored. +# # Usage: # checklitmus.sh file.litmus # @@ -18,8 +23,6 @@ # Author: Paul E. McKenney <paulmck@linux.ibm.com> litmus=$1 -herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg} - if test -f "$litmus" -a -r "$litmus" then : @@ -28,7 +31,38 @@ else exit 255 fi -echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out -/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1 +if test -z "$LKMM_HW_MAP_FILE" +then + # LKMM run + herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg} + echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out + /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1 +else + # Hardware run + + T=/tmp/checklitmushw.sh.$$ + trap 'rm -rf $T' 0 2 + mkdir $T + + # Generate filenames + catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat" + mapfile="Linux2${LKMM_HW_MAP_FILE}.map" + themefile="$T/${LKMM_HW_MAP_FILE}.theme" + herdoptions="-model $LKMM_HW_CAT_FILE" + hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'` + hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'` + + # Don't run on litmus tests with complex synchronization + if ! scripts/simpletest.sh $litmus + then + echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU + exit 254 + fi + + # Generate the assembly code and run herd7 on it. + gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile + jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out + /usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1 +fi scripts/judgelitmus.sh $litmus -- 2.17.1
The judgelitmus.sh script currently relies solely on the "Result:" comment in the .litmus file. This is problematic when using the --hw argument, because it is necessary to check the hardware model against LKMM even in the absence of "Result:" comments. This commit therefore modifies judgelitmus.sh to check the observation in a .litmus.out file, in case one was generated by a previous LKMM run. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/judgelitmus.sh | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index 6f3c60065c8b..fe9131f8eb96 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -8,7 +8,9 @@ # is provided, this is assumed to be a hardware test, and the output is # assumed to be in file.HW.litmus.out, where "HW" is the --hw argument. # In addition, non-Sometimes verification results will be noted, but -# forgiven. +# forgiven. Furthermore, if there is no "Result:" comment but there is +# an LKMM .litmus.out file, the observation in that file will be used +# to judge the assembly-language verification. # # Usage: # judgelitmus.sh file.litmus @@ -32,9 +34,11 @@ fi if test -z "$LKMM_HW_MAP_FILE" then litmusout=$litmus.out + lkmmout= else litmusout="`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out" + lkmmout=$litmus.out fi if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout" then @@ -46,6 +50,9 @@ fi if grep -q '^ \* Result: ' $litmus then outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'` +elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1 +then + outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'` else outcome=specified fi -- 2.17.1
This commit prepares for adding --hw capability to github litmus-test scripts by splitting runlitmus.sh (which simply runs the verification) out of checklitmus.sh (which also judges the results). Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/checklitmus.sh | 57 ++----------------- tools/memory-model/scripts/runlitmus.sh | 69 +++++++++++++++++++++++ 2 files changed, 73 insertions(+), 53 deletions(-) create mode 100755 tools/memory-model/scripts/runlitmus.sh diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh index 42ff11869cd6..4c1d0cf0ddad 100755 --- a/tools/memory-model/scripts/checklitmus.sh +++ b/tools/memory-model/scripts/checklitmus.sh @@ -1,15 +1,8 @@ #!/bin/sh # SPDX-License-Identifier: GPL-2.0+ # -# Run a herd7 test and invokes judgelitmus.sh to check the result against -# a "Result:" comment within the litmus test. It also outputs verification -# results to a file whose name is that of the specified litmus test, but -# with ".out" appended. -# -# If the --hw argument is specified, this script translates the .litmus -# C-language file to the specified type of assembly and verifies that. -# But in this case, litmus tests using complex synchronization (such as -# locking, RCU, and SRCU) are cheerfully ignored. +# Invokes runlitmus.sh and judgelitmus.sh on its arguments to run the +# specified litmus test and pass judgment on the results. # # Usage: # checklitmus.sh file.litmus @@ -22,47 +15,5 @@ # # Author: Paul E. McKenney <paulmck@linux.ibm.com> -litmus=$1 -if test -f "$litmus" -a -r "$litmus" -then - : -else - echo ' --- ' error: \"$litmus\" is not a readable file - exit 255 -fi - -if test -z "$LKMM_HW_MAP_FILE" -then - # LKMM run - herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg} - echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out - /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1 -else - # Hardware run - - T=/tmp/checklitmushw.sh.$$ - trap 'rm -rf $T' 0 2 - mkdir $T - - # Generate filenames - catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat" - mapfile="Linux2${LKMM_HW_MAP_FILE}.map" - themefile="$T/${LKMM_HW_MAP_FILE}.theme" - herdoptions="-model $LKMM_HW_CAT_FILE" - hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'` - hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'` - - # Don't run on litmus tests with complex synchronization - if ! scripts/simpletest.sh $litmus - then - echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU - exit 254 - fi - - # Generate the assembly code and run herd7 on it. - gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile - jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out - /usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1 -fi - -scripts/judgelitmus.sh $litmus +scripts/runlitmus.sh $1 +scripts/judgelitmus.sh $1 diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh new file mode 100755 index 000000000000..91af859c0e90 --- /dev/null +++ b/tools/memory-model/scripts/runlitmus.sh @@ -0,0 +1,69 @@ +#!/bin/sh +# SPDX-License-Identifier: GPL-2.0+ +# +# Without the -hw argument, runs a herd7 test and outputs verification +# results to a file whose name is that of the specified litmus test, +# but with ".out" appended. +# +# If the --hw argument is specified, this script translates the .litmus +# C-language file to the specified type of assembly and verifies that. +# But in this case, litmus tests using complex synchronization (such as +# locking, RCU, and SRCU) are cheerfully ignored. +# +# Either way, return the status of the herd7 command. +# +# Usage: +# runlitmus.sh file.litmus +# +# Run this in the directory containing the memory model, specifying the +# pathname of the litmus test to check. The caller is expected to have +# properly set up the LKMM environment variables. +# +# Copyright IBM Corporation, 2019 +# +# Author: Paul E. McKenney <paulmck@linux.ibm.com> + +litmus=$1 +if test -f "$litmus" -a -r "$litmus" +then + : +else + echo ' --- ' error: \"$litmus\" is not a readable file + exit 255 +fi + +if test -z "$LKMM_HW_MAP_FILE" +then + # LKMM run + herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg} + echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out + /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1 +else + # Hardware run + + T=/tmp/checklitmushw.sh.$$ + trap 'rm -rf $T' 0 2 + mkdir $T + + # Generate filenames + catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat" + mapfile="Linux2${LKMM_HW_MAP_FILE}.map" + themefile="$T/${LKMM_HW_MAP_FILE}.theme" + herdoptions="-model $LKMM_HW_CAT_FILE" + hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'` + hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'` + + # Don't run on litmus tests with complex synchronization + if ! scripts/simpletest.sh $litmus + then + echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU + exit 254 + fi + + # Generate the assembly code and run herd on it. + gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile + jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out + /usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1 +fi + +exit $? -- 2.17.1
In the absence of "Result:" comments, the runlitmus.sh script relies on litmus.out files from prior LKMM runs. This can be a bit user-hostile, so this commit makes runlitmus.sh generate any needed .litmus.out files that don't already exist. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/runlitmus.sh | 54 ++++++++++++++----------- 1 file changed, 30 insertions(+), 24 deletions(-) diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh index 91af859c0e90..2865a9661b07 100755 --- a/tools/memory-model/scripts/runlitmus.sh +++ b/tools/memory-model/scripts/runlitmus.sh @@ -28,42 +28,48 @@ if test -f "$litmus" -a -r "$litmus" then : else - echo ' --- ' error: \"$litmus\" is not a readable file + echo ' !!! ' error: \"$litmus\" is not a readable file exit 255 fi -if test -z "$LKMM_HW_MAP_FILE" +if test -z "$LKMM_HW_MAP_FILE" -o ! -e $LKMM_DESTDIR/$litmus.out then # LKMM run herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg} echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1 -else - # Hardware run + ret=$? + if test -z "$LKMM_HW_MAP_FILE" + then + exit $ret + fi + echo " --- " Automatically generated LKMM output for '"'--hw $LKMM_HW_MAP_FILE'"' run +fi - T=/tmp/checklitmushw.sh.$$ - trap 'rm -rf $T' 0 2 - mkdir $T +# Hardware run - # Generate filenames - catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat" - mapfile="Linux2${LKMM_HW_MAP_FILE}.map" - themefile="$T/${LKMM_HW_MAP_FILE}.theme" - herdoptions="-model $LKMM_HW_CAT_FILE" - hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'` - hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'` +T=/tmp/checklitmushw.sh.$$ +trap 'rm -rf $T' 0 2 +mkdir $T - # Don't run on litmus tests with complex synchronization - if ! scripts/simpletest.sh $litmus - then - echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU - exit 254 - fi +# Generate filenames +catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat" +mapfile="Linux2${LKMM_HW_MAP_FILE}.map" +themefile="$T/${LKMM_HW_MAP_FILE}.theme" +herdoptions="-model $LKMM_HW_CAT_FILE" +hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'` +hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'` - # Generate the assembly code and run herd on it. - gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile - jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out - /usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1 +# Don't run on litmus tests with complex synchronization +if ! scripts/simpletest.sh $litmus +then + echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU + exit 254 fi +# Generate the assembly code and run herd7 on it. +gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile +jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out +/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1 + exit $? -- 2.17.1
When the github scripts see ".litmus.out", they assume that there must be a corresponding C-language ".litmus" file. Won't they be disappointed when they instead see nothing, or, worse yet, the corresponding assembly-language litmus test? This commit therefore swaps the hardware tag with the "litmus" to avoid this sort of disappointment. This commit also adjusts the .gitignore file so as to avoid adding these new ".out" files to git. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/litmus-tests/.gitignore | 2 +- tools/memory-model/scripts/judgelitmus.sh | 2 +- tools/memory-model/scripts/runlitmus.sh | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore index 6e2ddc54152f..f47cb2045f13 100644 --- a/tools/memory-model/litmus-tests/.gitignore +++ b/tools/memory-model/litmus-tests/.gitignore @@ -1 +1 @@ -*.litmus.out +*.out diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index fe9131f8eb96..ca9a19829d79 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -37,7 +37,7 @@ then lkmmout= else litmusout="`echo $litmus | - sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out" + sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out" lkmmout=$litmus.out fi if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout" diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh index 2865a9661b07..c84124b32bee 100755 --- a/tools/memory-model/scripts/runlitmus.sh +++ b/tools/memory-model/scripts/runlitmus.sh @@ -57,7 +57,7 @@ catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat" mapfile="Linux2${LKMM_HW_MAP_FILE}.map" themefile="$T/${LKMM_HW_MAP_FILE}.theme" herdoptions="-model $LKMM_HW_CAT_FILE" -hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'` +hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'` hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'` # Don't run on litmus tests with complex synchronization -- 2.17.1
This commit retains the assembly-language litmus tests generated from the C-language litmus tests, appending the hardware tag to the original C-language litmus test's filename. Thus, S+poonceonces.litmus.AArch64 contains the Armv8 assembly language corresponding to the C-language S+poonceonces.litmus test. This commit also updates the .gitignore to avoid commiting these automatically generated assembly-language litmus tests. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/litmus-tests/.gitignore | 2 +- tools/memory-model/scripts/runlitmus.sh | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore index f47cb2045f13..848e62d2a9b3 100644 --- a/tools/memory-model/litmus-tests/.gitignore +++ b/tools/memory-model/litmus-tests/.gitignore @@ -1 +1 @@ -*.out +*.litmus.* diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh index c84124b32bee..62b47c7e1ba9 100755 --- a/tools/memory-model/scripts/runlitmus.sh +++ b/tools/memory-model/scripts/runlitmus.sh @@ -69,7 +69,7 @@ fi # Generate the assembly code and run herd7 on it. gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile -jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out -/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1 +jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out +/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 exit $? -- 2.17.1
Currently, the scripts specify the CPU's .cat file to herd. But this is pointless because herd will select a good and sufficient .cat file from the assembly-language litmus test itself. This commit therefore removes the -model argument to herd, allowing herd to figure the CPU family out itself. Note that the user can override herd's choice using the "--herdopts" argument to the scripts. Suggested-by: Luc Maranget <luc.maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/runlitmus.sh | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh index 62b47c7e1ba9..afb196d7ef10 100755 --- a/tools/memory-model/scripts/runlitmus.sh +++ b/tools/memory-model/scripts/runlitmus.sh @@ -53,7 +53,6 @@ trap 'rm -rf $T' 0 2 mkdir $T # Generate filenames -catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat" mapfile="Linux2${LKMM_HW_MAP_FILE}.map" themefile="$T/${LKMM_HW_MAP_FILE}.theme" herdoptions="-model $LKMM_HW_CAT_FILE" @@ -70,6 +69,6 @@ fi # Generate the assembly code and run herd7 on it. gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out -/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 +/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 exit $? -- 2.17.1
It turns out that the jingle7 tool is currently a bit picky about the litmus tests it is willing to process. This commit therefore ensures that jingle7 failures are reported. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/runlitmus.sh | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh index afb196d7ef10..5f2d29b460ff 100755 --- a/tools/memory-model/scripts/runlitmus.sh +++ b/tools/memory-model/scripts/runlitmus.sh @@ -69,6 +69,11 @@ fi # Generate the assembly code and run herd7 on it. gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out +if grep -q "Generated 0 tests" $T/$hwlitmusfile.jingle7.out +then + echo ' !!! ' jingle7 failed, no $hwlitmus generated + exit 253 +fi /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 exit $? -- 2.17.1
Adding the -v flag to jingle7 invocations gives much useful information on why jingle7 didn't like a given litmus test. This commit therefore adds this flag and saves off any such information into a .err file. Suggested-by: Luc Maranget <luc.maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/runlitmus.sh | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh index 5f2d29b460ff..dfdb1f00fcc0 100755 --- a/tools/memory-model/scripts/runlitmus.sh +++ b/tools/memory-model/scripts/runlitmus.sh @@ -68,10 +68,11 @@ fi # Generate the assembly code and run herd7 on it. gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile -jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out +jingle7 -v -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out if grep -q "Generated 0 tests" $T/$hwlitmusfile.jingle7.out then - echo ' !!! ' jingle7 failed, no $hwlitmus generated + echo ' !!! ' jingle7 failed, errors in $hwlitmus.err + cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err exit 253 fi /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 -- 2.17.1
This commits enables the "--hw" argument for the checkghlitmus.sh script, causing it to convert any applicable C-language litmus tests to the specified flavor of assembly language, to verify these assembly-language litmus tests, and checking compatibility of the outcomes. Note that the conversion does not yet handle locking, RCU, SRCU, plain C-language memory accesses, or casts. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/checkghlitmus.sh | 9 ++++--- tools/memory-model/scripts/hwfnseg.sh | 20 +++++++++++++++ tools/memory-model/scripts/runlitmushist.sh | 27 +++++++++++++-------- 3 files changed, 42 insertions(+), 14 deletions(-) create mode 100755 tools/memory-model/scripts/hwfnseg.sh diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh index 6589fbb6f653..2ea220d2564b 100755 --- a/tools/memory-model/scripts/checkghlitmus.sh +++ b/tools/memory-model/scripts/checkghlitmus.sh @@ -10,6 +10,7 @@ # parseargs.sh scripts for arguments. . scripts/parseargs.sh +. scripts/hwfnseg.sh T=/tmp/checkghlitmus.sh.$$ trap 'rm -rf $T' 0 @@ -32,9 +33,9 @@ then ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh ) fi -# Create a list of the C-language litmus tests previously run. -( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) | - sed -e 's/\.out$//' | +# Create a list of the specified litmus tests previously run. +( cd $LKMM_DESTDIR; find litmus -name "*.litmus${hwfnseg}.out" -print ) | + sed -e "s/${hwfnseg}"'\.out$//' | xargs -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' | xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already @@ -44,7 +45,7 @@ find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C xargs < $T/list-C -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result xargs < $T/list-C-result -r grep -L "^P${LKMM_PROCS}" > $T/list-C-result-short -# Form list of tests without corresponding .litmus.out files +# Form list of tests without corresponding .out files sort $T/list-C-already $T/list-C-result-short | uniq -u > $T/list-C-needed # Run any needed tests. diff --git a/tools/memory-model/scripts/hwfnseg.sh b/tools/memory-model/scripts/hwfnseg.sh new file mode 100755 index 000000000000..580c3281181c --- /dev/null +++ b/tools/memory-model/scripts/hwfnseg.sh @@ -0,0 +1,20 @@ +#!/bin/sh +# SPDX-License-Identifier: GPL-2.0+ +# +# Generate the hardware extension to the litmus-test filename, or the +# empty string if this is an LKMM run. The extension is placed in +# the shell variable hwfnseg. +# +# Usage: +# . hwfnseg.sh +# +# Copyright IBM Corporation, 2019 +# +# Author: Paul E. McKenney <paulmck@linux.ibm.com> + +if test -z "$LKMM_HW_MAP_FILE" +then + hwfnseg= +else + hwfnseg=".$LKMM_HW_MAP_FILE" +fi diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh index 852786fef179..c6c2bdc67a50 100755 --- a/tools/memory-model/scripts/runlitmushist.sh +++ b/tools/memory-model/scripts/runlitmushist.sh @@ -15,6 +15,8 @@ # # Author: Paul E. McKenney <paulmck@linux.ibm.com> +. scripts/hwfnseg.sh + T=/tmp/runlitmushist.sh.$$ trap 'rm -rf $T' 0 mkdir $T @@ -30,15 +32,12 @@ fi # Prefixes for per-CPU scripts for ((i=0;i<$LKMM_JOBS;i++)) do - echo dir="$LKMM_DESTDIR" > $T/$i.sh echo T=$T >> $T/$i.sh - echo herdoptions=\"$LKMM_HERD_OPTIONS\" >> $T/$i.sh cat << '___EOF___' >> $T/$i.sh runtest () { - echo ' ... ' /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 '>' $dir/$1.out '2>&1' - if /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 > $dir/$1.out 2>&1 + if scripts/runlitmus.sh $1 then - if ! grep -q '^Observation ' $dir/$1.out + if ! grep -q '^Observation ' $LKMM_DESTDIR/$1$2.out then echo ' !!! Herd failed, no Observation:' $1 fi @@ -47,10 +46,16 @@ do if test "$exitcode" -eq 124 then exitmsg="timed out" + elif test "$exitcode" -eq 253 + then + exitmsg= else exitmsg="failed, exit code $exitcode" fi - echo ' !!! Herd' ${exitmsg}: $1 + if test -n "$exitmsg" + then + echo ' !!! Herd' ${exitmsg}: $1 + fi fi } ___EOF___ @@ -59,11 +64,13 @@ done awk -v q="'" -v b='\\' ' { 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 -}' | bash | -sort -k1n | -awk -v ncpu=$LKMM_JOBS -v t=$T ' +}' | sh | sort -k1n | +awk -v dq='"' -v hwfnseg="$hwfnseg" -v ncpu="$LKMM_JOBS" -v t="$T" ' { - print "runtest " $2 >> t "/" NR % ncpu ".sh"; + print "if test -z " dq hwfnseg dq " || scripts/simpletest.sh " dq $2 dq + print "then" + print "\techo runtest " dq $2 dq " " hwfnseg " >> " t "/" NR % ncpu ".sh"; + print "fi" } END { -- 2.17.1
The parseargs.sh regular expression for the --jobs argument incorrectly requires that the number of jobs be at least 10, that is, have at least two digits. This commit therefore adjusts this regular expression to allow single-digit numbers of jobs to be specified. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/parseargs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh index 5f016fc3f3af..25a81ac0dfdf 100755 --- a/tools/memory-model/scripts/parseargs.sh +++ b/tools/memory-model/scripts/parseargs.sh @@ -113,7 +113,7 @@ do LKMM_JOBS="`echo $njobs | sed -e 's/^\([0-9]\+\).*$/\1/'`" ;; --jobs|--job|-j) - checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]\+$' '^--' + checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]*$' '^--' LKMM_JOBS="$2" shift ;; -- 2.17.1
The checkghlitmus.sh script currently uses grep to ignore non-C-language litmus tests, which is a bit fragile. This commit therefore enlists the aid of "mselect7 -arch C", given Luc Maraget's recent modifications that allow mselect7 to operate in filter mode. This change requires herdtools 7.52-32-g1da3e0e50977 or later. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/checkghlitmus.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh index 2ea220d2564b..cedd0290b73f 100755 --- a/tools/memory-model/scripts/checkghlitmus.sh +++ b/tools/memory-model/scripts/checkghlitmus.sh @@ -41,7 +41,7 @@ fi # Create a list of C-language litmus tests with "Result:" commands and # no more than the specified number of processes. -find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C +find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C xargs < $T/list-C -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result xargs < $T/list-C-result -r grep -L "^P${LKMM_PROCS}" > $T/list-C-result-short -- 2.17.1
The history-check scripts currently use grep to ignore non-C-language litmus tests, which is a bit fragile. This commit therefore enlists the aid of "mselect7 -arch C", given Luc Maraget's recent modifications that allow mselect7 to operate in filter mode. This change requires herdtools 7.52-32-g1da3e0e50977 or later. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/initlitmushist.sh | 2 +- tools/memory-model/scripts/newlitmushist.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/memory-model/scripts/initlitmushist.sh b/tools/memory-model/scripts/initlitmushist.sh index 956b6957484d..31ea782955d3 100755 --- a/tools/memory-model/scripts/initlitmushist.sh +++ b/tools/memory-model/scripts/initlitmushist.sh @@ -60,7 +60,7 @@ fi # Create a list of the C-language litmus tests with no more than the # specified number of processes (per the --procs argument). -find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C +find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C xargs < $T/list-C -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short scripts/runlitmushist.sh < $T/list-C-short diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh index 3f4b06e29988..25235e2049cf 100755 --- a/tools/memory-model/scripts/newlitmushist.sh +++ b/tools/memory-model/scripts/newlitmushist.sh @@ -43,7 +43,7 @@ fi # Form full list of litmus tests with no more than the specified # number of processes (per the --procs argument). -find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C-all +find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C-all xargs < $T/list-C-all -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short # Form list of new tests. Note: This does not handle litmus-test deletion! -- 2.17.1
Currently, parseargs.sh expects to consume all the command-line arguments, which prevents the calling script from having any of its own arguments. This commit therefore causes parseargs.sh to stop consuming arguments when it encounters a "--" argument, leaving any remaining arguments for the calling script. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/parseargs.sh | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh index 25a81ac0dfdf..7aa58755adfc 100755 --- a/tools/memory-model/scripts/parseargs.sh +++ b/tools/memory-model/scripts/parseargs.sh @@ -83,7 +83,7 @@ do echo "Cannot create directory --destdir '$LKMM_DESTDIR'" usage fi - if test -d "$LKMM_DESTDIR" -a -w "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR" + if test -d "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR" then : else @@ -127,6 +127,10 @@ do LKMM_TIMEOUT="$2" shift ;; + --) + shift + break + ;; *) echo Unknown argument $1 usage -- 2.17.1
Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/parseargs.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh index 7aa58755adfc..08ded5909860 100755 --- a/tools/memory-model/scripts/parseargs.sh +++ b/tools/memory-model/scripts/parseargs.sh @@ -1,7 +1,7 @@ #!/bin/sh # SPDX-License-Identifier: GPL-2.0+ # -# the corresponding .litmus.out file, and does not judge the result. +# Parse arguments common to the various scripts. # # . scripts/parseargs.sh # -- 2.17.1
This commit adds a checktheselitmus.sh script that runs the litmus tests specified on the command line. This is useful for verifying fixes to specific litmus tests. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/README | 8 ++++ .../memory-model/scripts/checktheselitmus.sh | 43 +++++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100755 tools/memory-model/scripts/checktheselitmus.sh diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README index 0e29a52044c1..cc2c4e5be9ec 100644 --- a/tools/memory-model/scripts/README +++ b/tools/memory-model/scripts/README @@ -27,6 +27,14 @@ checklitmushist.sh checklitmus.sh Check a single litmus test against its "Result:" expected result. + Not intended to for manual use. + +checktheselitmus.sh + + Check the specified list of litmus tests against their "Result:" + expected results. This takes optional parseargs.sh arguments, + followed by "--" followed by pathnames starting from the current + directory. cmplitmushist.sh diff --git a/tools/memory-model/scripts/checktheselitmus.sh b/tools/memory-model/scripts/checktheselitmus.sh new file mode 100755 index 000000000000..10eeb5ecea6d --- /dev/null +++ b/tools/memory-model/scripts/checktheselitmus.sh @@ -0,0 +1,43 @@ +#!/bin/sh +# SPDX-License-Identifier: GPL-2.0+ +# +# Invokes checklitmus.sh on its arguments to run the specified litmus +# test and pass judgment on the results. +# +# Usage: +# checktheselitmus.sh -- [ file1.litmus [ file2.litmus ... ] ] +# +# Run this in the directory containing the memory model, specifying the +# pathname of the litmus test to check. The usual parseargs.sh arguments +# can be specified prior to the "--". +# +# This script is intended for use with pathnames that start from the +# tools/memory-model directory. If some of the pathnames instead start at +# the root directory, they all must do so and the "--destdir /" parseargs.sh +# argument must be specified prior to the "--". Alternatively, some other +# "--destdir" argument can be supplied as long as the needed subdirectories +# are populated. +# +# Copyright IBM Corporation, 2018 +# +# Author: Paul E. McKenney <paulmck@linux.ibm.com> + +. scripts/parseargs.sh + +ret=0 +for i in "$@" +do + if scripts/checklitmus.sh $i + then + : + else + ret=1 + fi +done +if test "$ret" -ne 0 +then + echo " ^^^ VERIFICATION MISMATCHES" 1>&2 +else + echo All litmus tests verified as was expected. 1>&2 +fi +exit $ret -- 2.17.1
This commit adds functionality to judgelitmus.sh to allow it to handle both the "DATARACE" markers in the "Result:" comments in litmus tests and the "Flag data-race" markers in LKMM output. For C-language tests, if either marker is present, the other must also be as well, at least for litmus tests having a "Result:" comment. If the LKMM output indicates a data race, then failures of the Always/Sometimes/Never portion of the "Result:" prediction are forgiven. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index ca9a19829d79..eaa2cc7d3b36 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -47,9 +47,27 @@ else echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file exit 255 fi +if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout" +then + datarace_modeled=1 +fi if grep -q '^ \* Result: ' $litmus then outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'` + if grep -m1 '^ \* Result: .* DATARACE' $litmus + then + datarace_predicted=1 + fi + if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE" + then + echo '!!! Predicted data race not modeled' $litmus + exit 252 + elif test -z "$datarace_predicted" -a -n "$datarace_modeled" + then + # Note that hardware models currently don't model data races + echo '!!! Unexpected data race modeled' $litmus + exit 253 + fi elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1 then outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'` @@ -114,7 +132,7 @@ elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$o then ret=0 else - if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes + if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled" then flag="--- Forgiven" ret=0 -- 2.17.1
The scripts that generate the litmus tests in the "auto" directory of the https://github.com/paulmckrcu/litmus archive place the "Result:" tag into a single-line ocaml comment, which judgelitmus.sh currently does not recognize. This commit therefore makes judgelitmus.sh recognize both the multiline comment format that it currently does and the automatically generated single-line format. Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/judgelitmus.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index eaa2cc7d3b36..6408c012bdf5 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -51,10 +51,10 @@ if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout" then datarace_modeled=1 fi -if grep -q '^ \* Result: ' $litmus +if grep -q '^[( ]\* Result: ' $litmus then - outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'` - if grep -m1 '^ \* Result: .* DATARACE' $litmus + outcome=`grep -m 1 '^[( ]\* Result: ' $litmus | awk '{ print $3 }'` + if grep -m1 '^[( ]\* Result: .* DATARACE' $litmus then datarace_predicted=1 fi -- 2.17.1
Litmus tests involving atomic operations produce LL/SC loops on a number of architectures, and unrolling these loops can result in excessive verification times or even stack overflows. This commit therefore uses the "-unroll 0" herd7 argument to avoid unrolling, on the grounds that additional passes through an LL/SC loop should not change the verification. Note however, that certain bugs in the mapping of the LL/SC loop to machine instructions may go undetected. On the other hand, herd7 might not be the best vehicle for finding such bugs in any case. (You do stress-test your architecture-specific code, don't you?) Suggested-by: Luc Maranget <luc.maranget@inria.fr> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/scripts/runlitmus.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh index dfdb1f00fcc0..94608d4b6502 100755 --- a/tools/memory-model/scripts/runlitmus.sh +++ b/tools/memory-model/scripts/runlitmus.sh @@ -75,6 +75,6 @@ then cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err exit 253 fi -/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 +/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -unroll 0 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 exit $? -- 2.17.1
From: "Joel Fernandes (Google)" <joel@joelfernandes.org> To reduce ambiguity in the more exotic ->prop ordering example, this commit uses the term cumul-fence instead of the term fence for the two fences, so that the implict ->rfe on loads/stores to Y are covered by the description. Link: https://lore.kernel.org/lkml/20190729121745.GA140682@google.com Suggested-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org> Acked-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> --- tools/memory-model/Documentation/explanation.txt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt index 68caa9a976d0..634dc6db26c4 100644 --- a/tools/memory-model/Documentation/explanation.txt +++ b/tools/memory-model/Documentation/explanation.txt @@ -1302,7 +1302,7 @@ followed by an arbitrary number of cumul-fence links, ending with an rfe link. You can concoct more exotic examples, containing more than one fence, although this quickly leads to diminishing returns in terms of complexity. For instance, here's an example containing a coe link -followed by two fences and an rfe link, utilizing the fact that +followed by two cumul-fences and an rfe link, utilizing the fact that release fences are A-cumulative: int x, y, z; @@ -1334,10 +1334,10 @@ If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop link from P0's store to its load. This is because P0's store gets overwritten by P1's store since x = 2 at the end (a coe link), the smp_wmb() ensures that P1's store to x propagates to P2 before the -store to y does (the first fence), the store to y propagates to P2 +store to y does (the first cumul-fence), the store to y propagates to P2 before P2's load and store execute, P2's smp_store_release() guarantees that the stores to x and y both propagate to P0 before the -store to z does (the second fence), and P0's load executes after the +store to z does (the second cumul-fence), and P0's load executes after the store to z has propagated to P0 (an rfe link). In summary, the fact that the hb relation links memory access events -- 2.17.1
From: Andrea Parri <andrea.parri@amarulasolutions.com> The formal memory consistency model has added support for plain accesses (and data races). While updating the informal documentation to describe this addition to the model is highly desirable and important future work, update the informal documentation to at least acknowledge such addition. Signed-off-by: Andrea Parri <andrea.parri@amarulasolutions.com> Cc: Will Deacon <will.deacon@arm.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: "Paul E. McKenney" <paulmck@linux.ibm.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Daniel Lustig <dlustig@nvidia.com> Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> Acked-by: Alan Stern <stern@rowland.harvard.edu> --- .../Documentation/explanation.txt | 47 +++++++++---------- tools/memory-model/README | 18 +++---- 2 files changed, 30 insertions(+), 35 deletions(-) diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt index 634dc6db26c4..488f11f6c588 100644 --- a/tools/memory-model/Documentation/explanation.txt +++ b/tools/memory-model/Documentation/explanation.txt @@ -42,7 +42,8 @@ linux-kernel.bell and linux-kernel.cat files that make up the formal version of the model; they are extremely terse and their meanings are far from clear. -This document describes the ideas underlying the LKMM. It is meant +This document describes the ideas underlying the LKMM, but excluding +the modeling of bare C (or plain) shared memory accesses. It is meant for people who want to understand how the model was designed. It does not go into the details of the code in the .bell and .cat files; rather, it explains in English what the code expresses symbolically. @@ -354,31 +355,25 @@ be extremely complex. Optimizing compilers have great freedom in the way they translate source code to object code. They are allowed to apply transformations that add memory accesses, eliminate accesses, combine them, split them -into pieces, or move them around. Faced with all these possibilities, -the LKMM basically gives up. It insists that the code it analyzes -must contain no ordinary accesses to shared memory; all accesses must -be performed using READ_ONCE(), WRITE_ONCE(), or one of the other -atomic or synchronization primitives. These primitives prevent a -large number of compiler optimizations. In particular, it is -guaranteed that the compiler will not remove such accesses from the -generated code (unless it can prove the accesses will never be -executed), it will not change the order in which they occur in the -code (within limits imposed by the C standard), and it will not -introduce extraneous accesses. - -This explains why the MP and SB examples above used READ_ONCE() and -WRITE_ONCE() rather than ordinary memory accesses. Thanks to this -usage, we can be certain that in the MP example, P0's write event to -buf really is po-before its write event to flag, and similarly for the -other shared memory accesses in the examples. - -Private variables are not subject to this restriction. Since they are -not shared between CPUs, they can be accessed normally without -READ_ONCE() or WRITE_ONCE(), and there will be no ill effects. In -fact, they need not even be stored in normal memory at all -- in -principle a private variable could be stored in a CPU register (hence -the convention that these variables have names starting with the -letter 'r'). +into pieces, or move them around. The use of READ_ONCE(), WRITE_ONCE(), +or one of the other atomic or synchronization primitives prevents a +large number of compiler optimizations. In particular, it is guaranteed +that the compiler will not remove such accesses from the generated code +(unless it can prove the accesses will never be executed), it will not +change the order in which they occur in the code (within limits imposed +by the C standard), and it will not introduce extraneous accesses. + +The MP and SB examples above used READ_ONCE() and WRITE_ONCE() rather +than ordinary memory accesses. Thanks to this usage, we can be certain +that in the MP example, the compiler won't reorder P0's write event to +buf and P0's write event to flag, and similarly for the other shared +memory accesses in the examples. + +Since private variables are not shared between CPUs, they can be +accessed normally without READ_ONCE() or WRITE_ONCE(). In fact, they +need not even be stored in normal memory at all -- in principle a +private variable could be stored in a CPU register (hence the convention +that these variables have names starting with the letter 'r'). A WARNING diff --git a/tools/memory-model/README b/tools/memory-model/README index 2b87f3971548..fc07b52f2028 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -167,15 +167,15 @@ scripts Various scripts, see scripts/README. LIMITATIONS =========== -The Linux-kernel memory model has the following limitations: - -1. Compiler optimizations are not modeled. Of course, the use - of READ_ONCE() and WRITE_ONCE() limits the compiler's ability - to optimize, but there is Linux-kernel code that uses bare C - memory accesses. Handling this code is on the to-do list. - For more information, see Documentation/explanation.txt (in - particular, the "THE PROGRAM ORDER RELATION: po AND po-loc" - and "A WARNING" sections). +The Linux-kernel memory model (LKMM) has the following limitations: + +1. Compiler optimizations are not accurately modeled. Of course, + the use of READ_ONCE() and WRITE_ONCE() limits the compiler's + ability to optimize, but under some circumstances it is possible + for the compiler to undermine the memory model. For more + information, see Documentation/explanation.txt (in particular, + the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING" + sections). Note that this limitation in turn limits LKMM's ability to accurately model address, control, and data dependencies. -- 2.17.1
Hi Paul, (CC: using Andrea's gmail address, adding Daniel) Sorry for slow response, but please find inline comments below. On Thu, 1 Aug 2019 15:20:52 -0700, Paul E. McKenney wrote: > This commit adds functionality to judgelitmus.sh to allow it to handle > both the "DATARACE" markers in the "Result:" comments in litmus tests > and the "Flag data-race" markers in LKMM output. For C-language tests, > if either marker is present, the other must also be as well, at least for > litmus tests having a "Result:" comment. If the LKMM output indicates > a data race, then failures of the Always/Sometimes/Never portion of the > "Result:" prediction are forgiven. I'd like to see the reason _why_ they can be forgiven. Also, updating the header comment of judgelitimus.sh to mention these expansions would be of much help. My guess is any data-race would moot the Always/Sometimes/Never prediction. This reminds me that update of LKMM documentation regarding plain accesses (data races) is yet to come. Thanks, Akira > > Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> > --- > tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++++++++- > 1 file changed, 19 insertions(+), 1 deletion(-) > > diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh > index ca9a19829d79..eaa2cc7d3b36 100755 > --- a/tools/memory-model/scripts/judgelitmus.sh > +++ b/tools/memory-model/scripts/judgelitmus.sh > @@ -47,9 +47,27 @@ else > echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file > exit 255 > fi > +if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout" > +then > + datarace_modeled=1 > +fi > if grep -q '^ \* Result: ' $litmus > then > outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'` > + if grep -m1 '^ \* Result: .* DATARACE' $litmus > + then > + datarace_predicted=1 > + fi > + if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE" > + then > + echo '!!! Predicted data race not modeled' $litmus > + exit 252 > + elif test -z "$datarace_predicted" -a -n "$datarace_modeled" > + then > + # Note that hardware models currently don't model data races > + echo '!!! Unexpected data race modeled' $litmus > + exit 253 > + fi > elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1 > then > outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'` > @@ -114,7 +132,7 @@ elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$o > then > ret=0 > else > - if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes > + if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled" > then > flag="--- Forgiven" > ret=0 >
On Mon, Aug 12, 2019 at 11:32:35PM +0900, Akira Yokosawa wrote: > Hi Paul, > (CC: using Andrea's gmail address, adding Daniel) Good point, I did forget to update at my end. Fixed, thank you! > Sorry for slow response, but please find inline comments below. > > On Thu, 1 Aug 2019 15:20:52 -0700, Paul E. McKenney wrote: > > This commit adds functionality to judgelitmus.sh to allow it to handle > > both the "DATARACE" markers in the "Result:" comments in litmus tests > > and the "Flag data-race" markers in LKMM output. For C-language tests, > > if either marker is present, the other must also be as well, at least for > > litmus tests having a "Result:" comment. If the LKMM output indicates > > a data race, then failures of the Always/Sometimes/Never portion of the > > "Result:" prediction are forgiven. > > I'd like to see the reason _why_ they can be forgiven. Also, updating > the header comment of judgelitimus.sh to mention these expansions would > be of much help. > > My guess is any data-race would moot the Always/Sometimes/Never > prediction. Exactly. And good point, I will update the commit log to make this explicit. > This reminds me that update of LKMM documentation regarding plain > accesses (data races) is yet to come. Yes, this one is still on the to-do list. Timely reminder, though! ;-) Thanx, Paul > Thanks, Akira > > > > > Signed-off-by: Paul E. McKenney <paulmck@linux.ibm.com> > > --- > > tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++++++++- > > 1 file changed, 19 insertions(+), 1 deletion(-) > > > > diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh > > index ca9a19829d79..eaa2cc7d3b36 100755 > > --- a/tools/memory-model/scripts/judgelitmus.sh > > +++ b/tools/memory-model/scripts/judgelitmus.sh > > @@ -47,9 +47,27 @@ else > > echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file > > exit 255 > > fi > > +if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout" > > +then > > + datarace_modeled=1 > > +fi > > if grep -q '^ \* Result: ' $litmus > > then > > outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'` > > + if grep -m1 '^ \* Result: .* DATARACE' $litmus > > + then > > + datarace_predicted=1 > > + fi > > + if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE" > > + then > > + echo '!!! Predicted data race not modeled' $litmus > > + exit 252 > > + elif test -z "$datarace_predicted" -a -n "$datarace_modeled" > > + then > > + # Note that hardware models currently don't model data races > > + echo '!!! Unexpected data race modeled' $litmus > > + exit 253 > > + fi > > elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1 > > then > > outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'` > > @@ -114,7 +132,7 @@ elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$o > > then > > ret=0 > > else > > - if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes > > + if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled" > > then > > flag="--- Forgiven" > > ret=0 > > >
Hi Paul, I see some inconsistency between the header comment of judgelitmus.sh and the updated script. This patch set updates the header. It is relative to current lkmm-dev of -rcu. Patch 1/2 corresponds to ("tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out"). Patch 2/2 corresponds to ("tools/memory-model: Add data-race capabilities to judgelitmus.sh"). You should be able to use each patch as a fix-up commit respectively. I'm OK either with them applied at the head of the branch or with them merged into your commits. Thanks, Akira -- Akira Yokosawa (2): tools/memory-model: Reflect updated file name convention in judgelitmus.sh tools/memory-model: Mention data-race capability in jugdelitmus.sh's header tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) -- 2.17.1
From 6251ebb775a81f1ac158f197ad8110b8f98c4248 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa <akiyks@gmail.com> Date: Wed, 14 Aug 2019 17:20:54 +0900 Subject: [PATCH 1/2] tools/memory-model: Reflect updated file name convention in judgelitmus.sh Commit ("tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out") swapped "HW" and "litmus" part in .out file name. Reflect the change in header comment in judgelitmus.sh Signed-off-by: Akira Yokosawa <akiyks@gmail.com> --- tools/memory-model/scripts/judgelitmus.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index 6408c012bdf5..c91130814593 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -6,7 +6,7 @@ # test ran correctly. If the --hw argument is omitted, check against the # LKMM output, which is assumed to be in file.litmus.out. If this argument # is provided, this is assumed to be a hardware test, and the output is -# assumed to be in file.HW.litmus.out, where "HW" is the --hw argument. +# assumed to be in file.litmus.HW.out, where "HW" is the --hw argument. # In addition, non-Sometimes verification results will be noted, but # forgiven. Furthermore, if there is no "Result:" comment but there is # an LKMM .litmus.out file, the observation in that file will be used -- 2.17.1
From 67092cb93f7a0fd3c4f9a300637e4f5c61fc944a Mon Sep 17 00:00:00 2001 From: Akira Yokosawa <akiyks@gmail.com> Date: Wed, 14 Aug 2019 17:48:25 +0900 Subject: [PATCH 2/2] tools/memory-model: Mention data-race capability in jugdelitmus.sh's header Replicate description of data-race capability from the change log of commit ("tools/memory-model: Add data-race capabilities to judgelitmus.sh") in the header comment. Signed-off-by: Akira Yokosawa <akiyks@gmail.com> --- tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh index c91130814593..1ec5d89fcfbb 100755 --- a/tools/memory-model/scripts/judgelitmus.sh +++ b/tools/memory-model/scripts/judgelitmus.sh @@ -4,13 +4,19 @@ # Given a .litmus test and the corresponding litmus output file, check # the .litmus.out file against the "Result:" comment to judge whether the # test ran correctly. If the --hw argument is omitted, check against the -# LKMM output, which is assumed to be in file.litmus.out. If this argument -# is provided, this is assumed to be a hardware test, and the output is -# assumed to be in file.litmus.HW.out, where "HW" is the --hw argument. -# In addition, non-Sometimes verification results will be noted, but -# forgiven. Furthermore, if there is no "Result:" comment but there is -# an LKMM .litmus.out file, the observation in that file will be used -# to judge the assembly-language verification. +# LKMM output, which is assumed to be in file.litmus.out. If either a +# "DATARACE" marker in the "Result:" comment or a "Flag data-race" marker +# in the LKMM output is present, the other must also be as well, at least +# for litmus tests having a "Result:" comment. In this case, a failure of +# the Always/Sometimes/Never portion of the "Result:" prediction will be +# noted, but forgiven. +# +# If the --hw argument is provided, this is assumed to be a hardware +# test, and the output is assumed to be in file.litmus.HW.out, where +# "HW" is the --hw argument. In addition, non-Sometimes verification +# results will be noted, but forgiven. Furthermore, if there is no +# "Result:" comment but there is an LKMM .litmus.out file, the observation +# in that file will be used to judge the assembly-language verification. # # Usage: # judgelitmus.sh file.litmus -- 2.17.1
On Thu, Aug 15, 2019 at 12:11:36AM +0900, Akira Yokosawa wrote: > Hi Paul, > > I see some inconsistency between the header comment of judgelitmus.sh > and the updated script. > > This patch set updates the header. It is relative to current lkmm-dev > of -rcu. > > Patch 1/2 corresponds to ("tools/memory-model: Move from > .AArch64.litmus.out to .litmus.AArch.out"). > > Patch 2/2 corresponds to ("tools/memory-model: Add data-race > capabilities to judgelitmus.sh"). > > You should be able to use each patch as a fix-up commit respectively. > I'm OK either with them applied at the head of the branch or > with them merged into your commits. Good catches, thank you for looking these commits over! I will squash your changes into the original commits with attribution. Thanx, Paul > Thanks, Akira > -- > Akira Yokosawa (2): > tools/memory-model: Reflect updated file name convention in > judgelitmus.sh > tools/memory-model: Mention data-race capability in jugdelitmus.sh's > header > > tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++------- > 1 file changed, 13 insertions(+), 7 deletions(-) > > -- > 2.17.1 > >