linux/tools/memory-model/scripts/runlitmus.sh
Paul E. McKenney ee542816ac tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out
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.

[ paulmck: Apply Akira Yokosawa feedback. ]
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2023-03-24 10:24:14 -07:00

75 lines
2.3 KiB
Bash
Executable file

#!/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" -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
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
# 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$/.litmus.'${LKMM_HW_MAP_FILE}'/'`
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 $?