summaryrefslogtreecommitdiff
path: root/tools/memory-model
diff options
context:
space:
mode:
authorPaul E. McKenney <paulmck@kernel.org>2019-03-18 13:40:57 -0700
committerPaul E. McKenney <paulmck@kernel.org>2023-03-24 10:24:13 -0700
commit02484d826fda923f829fc47350ee99fd3cbd3414 (patch)
tree7f8aaa865aa0c218aa66f6eff81e184ec379eb70 /tools/memory-model
parentb1da11c936e28d60a02f13c9ea27fdc3d1759b38 (diff)
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: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'tools/memory-model')
-rwxr-xr-xtools/memory-model/scripts/cmplitmushist.sh31
-rwxr-xr-xtools/memory-model/scripts/judgelitmus.sh12
2 files changed, 39 insertions, 4 deletions
diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh
index b9c174dd8004..ca1ac8b64614 100755
--- a/tools/memory-model/scripts/cmplitmushist.sh
+++ b/tools/memory-model/scripts/cmplitmushist.sh
@@ -12,6 +12,7 @@ trap 'rm -rf $T' 0
mkdir $T
# comparetest oldpath newpath
+badmacnam=0
timedout=0
perfect=0
obsline=0
@@ -19,8 +20,26 @@ noobsline=0
obsresult=0
badcompare=0
comparetest () {
- if grep -q '^Command exited with non-zero status 124' $1 ||
- grep -q '^Command exited with non-zero status 124' $2
+ 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 &&
grep -q '^Command exited with non-zero status 124' $2
@@ -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
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index d3c313b9a458..d40439c7b71e 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -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