Commit 02484d82 authored by Paul E. McKenney's avatar Paul E. McKenney
Browse files

tools/memory-model: Make judgelitmus.sh identify bad macros 



Currently, judgelitmus.sh treats use of unknown primitives (such as
srcu_read_lock() prior to SRCU support) as "!!! Verification error".
This can be misleading because it fails to call out typos and running
a version LKMM on a litmus test requiring a feature not provided by
that version.  This commit therefore changes judgelitmus.sh to check
for unknown primitives and to report them, for example, with:

	'!!! Current LKMM version does not know "rcu_write_lock"'.

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

tools/memory-model/scripts/cmplitmushist.sh

+27 −4
Original line number Diff line number Diff line
@@ -12,6 +12,7 @@ trap 'rm -rf $T' 0 
mkdir $T



# comparetest oldpath newpath

badmacnam=0

timedout=0

perfect=0

obsline=0
@@ -19,7 +20,25 @@ noobsline=0 
obsresult=0

badcompare=0

comparetest () {

	if grep -q '^Command exited with non-zero status 124' $1 ||

	if grep -q ': Unknown macro ' $1 || grep -q ': Unknown macro ' $2

	then

		if grep -q ': Unknown macro ' $1

		then

			badname=`grep ': Unknown macro ' $1 |

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

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

			echo 'Current LKMM version does not know "'$badname'"' $1

		fi

		if grep -q ': Unknown macro ' $2

		then

			badname=`grep ': Unknown macro ' $2 |

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

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

			echo 'Current LKMM version does not know "'$badname'"' $2

		fi

		badmacnam=`expr "$badmacnam" + 1`

		return 0

	elif grep -q '^Command exited with non-zero status 124' $1 ||

	     grep -q '^Command exited with non-zero status 124' $2

	then

		if grep -q '^Command exited with non-zero status 124' $1 &&
@@ -56,7 +75,7 @@ comparetest () { 
			return 0

		fi

	else

		echo Missing Observation line "(e.g., herd7 timeout)": $2

		echo Missing Observation line "(e.g., syntax error)": $2

		noobsline=`expr "$noobsline" + 1`

		return 0

	fi
@@ -90,7 +109,7 @@ then 
fi

if test "$noobsline" -ne 0

then

	echo Missing Observation line "(e.g., herd7 timeout)": $noobsline 1>&2

	echo Missing Observation line "(e.g., syntax error)": $noobsline 1>&2

fi

if test "$obsresult" -ne 0

then
@@ -100,6 +119,10 @@ if test "$timedout" -ne 0 
then

	echo "!!!" Timed out: $timedout 1>&2

fi

if test "$badmacnam" -ne 0

then

	echo "!!!" Unknown primitive: $badmacnam 1>&2

fi

if test "$badcompare" -ne 0

then

	echo "!!!" Result changed: $badcompare 1>&2

tools/memory-model/scripts/judgelitmus.sh

+12 −0
Original line number Diff line number Diff line
@@ -42,6 +42,18 @@ grep '^Observation' $LKMM_DESTDIR/$litmus.out 
if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out

then

	:

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

then

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

		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

	then

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

	fi

	exit 254

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

then

	echo ' !!! Timeout' $litmus