Commit 579ecb2e authored by Paul E. McKenney's avatar Paul E. McKenney
Browse files

tools/memory-model: Hardware checking for check{,all}litmus.sh 



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: default avatarPaul E. McKenney <paulmck@kernel.org>
parent e029374b

tools/memory-model/scripts/checkalllitmus.sh

+11 −12
Original line number Diff line number Diff line 
#!/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

tools/memory-model/scripts/checklitmus.sh

+38 −4
Original line number Diff line number Diff line
@@ -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



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