tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw

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@kernel.org>
This commit is contained in:
Paul E. McKenney 2019-03-20 16:41:41 -07:00
parent 08203824c0
commit dbf0b425a6

View file

@ -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
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
ret=$?
if test -z "$LKMM_HW_MAP_FILE"
then
echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
exit 254
exit $ret
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
echo " --- " Automatically generated LKMM output for '"'--hw $LKMM_HW_MAP_FILE'"' run
fi
# 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
exit $?