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>
This commit is contained in:
Paul E. McKenney 2019-03-22 17:18:43 -07:00
parent d9313e05f0
commit 69d476c557
3 changed files with 42 additions and 14 deletions

View File

@ -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.

View File

@ -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

View File

@ -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,11 +46,17 @@ do
if test "$exitcode" -eq 124
then
exitmsg="timed out"
elif test "$exitcode" -eq 253
then
exitmsg=
else
exitmsg="failed, exit code $exitcode"
fi
if test -n "$exitmsg"
then
echo ' !!! Herd' ${exitmsg}: $1
fi
fi
}
___EOF___
done
@ -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 {