diff options
| author |   Paul E. McKenney <paulmck@kernel.org> | 2019-03-22 17:18:43 -0700 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@kernel.org> | 2023-03-24 10:24:14 -0700 |
| commit | 69d476c55761a74e636bb10e101e5aed6fb104fd (patch) | |
| tree | 07970986004d1ef8a66f73cbdc1b690b89dc2357 /tools/memory-model/scripts/runlitmushist.sh | |
| parent | tools/memory-model: Add -v flag to jingle7 runs (diff) | |
| download | wireguard-linux-69d476c55761a74e636bb10e101e5aed6fb104fd.tar.xz wireguard-linux-69d476c55761a74e636bb10e101e5aed6fb104fd.zip | |
tools/memory-model: Implement --hw support for checkghlitmus.sh
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@kernel.org>
Diffstat (limited to '')
| -rwxr-xr-x | tools/memory-model/scripts/runlitmushist.sh | 27 |
1 files changed, 17 insertions, 10 deletions
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 { |