Commit 2024436d authored by Paul E. McKenney's avatar Paul E. McKenney
Browse files

tools/memory-model: Make judgelitmus.sh handle hardware verifications 



This commit makes the judgelitmus.sh script check the --hw argument
(AKA the LKMM_HW_MAP_FILE environment variable) and to adjust its
judgment for a run where a C-language litmus test has been translated to
assembly and the assembly version verified.  In this case, the assembly
verification output is checked against the C-language script's "Result:"
comment.  However, because hardware can be stronger than LKMM requires,
the judgelitmus.sh script forgives verification mismatches featuring
a "Sometimes" in the C-language script and an "Always" or "Never"
assembly-language verification.

Note that deadlock is not forgiven, however, this should not normally be
an issue given that C-language tests containing locking, RCU, or SRCU
cannot be translated to assembly.  However, this issue can crop up in
litmus tests that mimic deadlock by using the "filter" clause to ignore
all executions.  It can also crop up when certain herd arguments are
used to autofilter everything that does not match the "exists" clause
in cases where the "exists" clause cannot be satisfied.

Signed-off-by: default avatarPaul E. McKenney <paulmck@kernel.org>
parent b1710979

tools/memory-model/scripts/README

+4 −4
Original line number Diff line number Diff line
@@ -43,10 +43,10 @@ initlitmushist.sh 


judgelitmus.sh



	Given a .litmus file and its .litmus.out herd7 output, check the

	.litmus.out file against the .litmus file's "Result:" comment to

	judge whether the test ran correctly.  Not normally run manually,

	provided instead for use by other scripts.

	Given a .litmus file and its herd7 output, check the output file

	against the .litmus file's "Result:" comment to judge whether

	the test ran correctly.  Not normally run manually, provided

	instead for use by other scripts.



newlitmushist.sh

tools/memory-model/scripts/judgelitmus.sh

+47 −28
Original line number Diff line number Diff line 
#!/bin/sh

# SPDX-License-Identifier: GPL-2.0+

#

# Given a .litmus test and the corresponding .litmus.out file, check

# the .litmus.out file against the "Result:" comment to judge whether

# the test ran correctly.

# Given a .litmus test and the corresponding litmus output file, check

# the .litmus.out file against the "Result:" comment to judge whether the

# test ran correctly.  If the --hw argument is omitted, check against the

# LKMM output, which is assumed to be in file.litmus.out.  If this argument

# is provided, this is assumed to be a hardware test, and the output is

# assumed to be in file.HW.litmus.out, where "HW" is the --hw argument.

# In addition, non-Sometimes verification results will be noted, but

# forgiven.

#

# Usage:

#	judgelitmus.sh file.litmus
@@ -24,11 +29,18 @@ else 
	echo ' --- ' error: \"$litmus\" is not a readable file

	exit 255

fi

if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out

if test -z "$LKMM_HW_MAP_FILE"

then

	litmusout=$litmus.out

else

	litmusout="`echo $litmus |

		sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out"

fi

if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"

then

	:

else

	echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file

	echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file

	exit 255

fi

if grep -q '^ \* Result: ' $litmus
@@ -38,69 +50,76 @@ else 
	outcome=specified

fi



grep '^Observation' $LKMM_DESTDIR/$litmus.out

if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out

grep '^Observation' $LKMM_DESTDIR/$litmusout

if grep -q '^Observation' $LKMM_DESTDIR/$litmusout

then

	:

elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out

elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout

then

	badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out |

	badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout |

		sed -e 's/^.*: Unknown macro //' |

		sed -e 's/ (User error).*$//'`

	badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus"

	echo $badmsg

	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out

	if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout

	then

		echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmus.out 2>&1

		echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1

	fi

	exit 254

elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out

elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout

then

	echo ' !!! Timeout' $litmus

	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out

	if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout

	then

		echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmus.out 2>&1

		echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1

	fi

	exit 124

else

	echo ' !!! Verification error' $litmus

	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out

	if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout

	then

		echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1

		echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1

	fi

	exit 255

fi

if test "$outcome" = DEADLOCK

then

	if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'

	if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'

	then

		ret=0

	else

		echo " !!! Unexpected non-$outcome verification" $litmus

		if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out

		if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout

		then

			echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1

			echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1

		fi

		ret=1

	fi

elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'

elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'

then

	echo " !!! Unexpected non-$outcome deadlock" $litmus

	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out

	if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout

	then

		echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1

		echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1

	fi

	ret=1

elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe

elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe

then

	ret=0

else

	echo " !!! Unexpected non-$outcome verification" $litmus

	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out

	if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes

	then

		echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1

	fi

		flag="--- Forgiven"

		ret=0

	else

		flag="!!! Unexpected"

		ret=1

	fi

tail -2 $LKMM_DESTDIR/$litmus.out | head -1

	echo " $flag non-$outcome verification" $litmus

	if ! grep -qe "$flag" $LKMM_DESTDIR/$litmusout

	then

		echo " $flag non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1

	fi

fi

tail -2 $LKMM_DESTDIR/$litmusout | head -1

exit $ret