1 #!/bin/sh
2 # SPDX-License-Identifier: GPL-2.0+
3 #
4 # Given a .litmus test and the corresponding litmus output file, check
5 # the .litmus.out file against the "Result:" comment to judge whether the
6 # test ran correctly. If the --hw argument is omitted, check against the
7 # LKMM output, which is assumed to be in file.litmus.out. If either a
8 # "DATARACE" marker in the "Result:" comment or a "Flag data-race" marker
9 # in the LKMM output is present, the other must also be as well, at least
10 # for litmus tests having a "Result:" comment. In this case, a failure of
11 # the Always/Sometimes/Never portion of the "Result:" prediction will be
12 # noted, but forgiven.
13 #
14 # If the --hw argument is provided, this is assumed to be a hardware
15 # test, and the output is assumed to be in file.litmus.HW.out, where
16 # "HW" is the --hw argument. In addition, non-Sometimes verification
17 # results will be noted, but forgiven. Furthermore, if there is no
18 # "Result:" comment but there is an LKMM .litmus.out file, the observation
19 # in that file will be used to judge the assembly-language verification.
20 #
21 # Usage:
22 # judgelitmus.sh file.litmus
23 #
24 # Run this in the directory containing the memory model, specifying the
25 # pathname of the litmus test to check.
26 #
27 # Copyright IBM Corporation, 2018
28 #
29 # Author: Paul E. McKenney <paulmck@linux.ibm.com>
30
31 litmus=$1
32
33 if test -f "$litmus" -a -r "$litmus"
34 then
35 :
36 else
37 echo ' --- ' error: \"$litmus\" is not a readable file
38 exit 255
39 fi
40 if test -z "$LKMM_HW_MAP_FILE"
41 then
42 litmusout=$litmus.out
43 lkmmout=
44 else
45 litmusout="`echo $litmus |
46 sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out"
47 lkmmout=$litmus.out
48 fi
49 if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"
50 then
51 :
52 else
53 echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file
54 exit 255
55 fi
56 if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout"
57 then
58 datarace_modeled=1
59 fi
60 if grep -q '^[( ]\* Result: ' $litmus
61 then
62 outcome=`grep -m 1 '^[( ]\* Result: ' $litmus | awk '{ print $3 }'`
63 if grep -m1 '^[( ]\* Result: .* DATARACE' $litmus
64 then
65 datarace_predicted=1
66 fi
67 if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE"
68 then
69 echo '!!! Predicted data race not modeled' $litmus
70 exit 252
71 elif test -z "$datarace_predicted" -a -n "$datarace_modeled"
72 then
73 # Note that hardware models currently don't model data races
74 echo '!!! Unexpected data race modeled' $litmus
75 exit 253
76 fi
77 elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1
78 then
79 outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'`
80 else
81 outcome=specified
82 fi
83
84 grep '^Observation' $LKMM_DESTDIR/$litmusout
85 if grep -q '^Observation' $LKMM_DESTDIR/$litmusout
86 then
87 :
88 elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout
89 then
90 badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout |
91 sed -e 's/^.*: Unknown macro //' |
92 sed -e 's/ (User error).*$//'`
93 badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus"
94 echo $badmsg
95 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
96 then
97 echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1
98 fi
99 exit 254
100 elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout
101 then
102 echo ' !!! Timeout' $litmus
103 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
104 then
105 echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1
106 fi
107 exit 124
108 else
109 echo ' !!! Verification error' $litmus
110 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
111 then
112 echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1
113 fi
114 exit 255
115 fi
116 if test "$outcome" = DEADLOCK
117 then
118 if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'
119 then
120 ret=0
121 else
122 echo " !!! Unexpected non-$outcome verification" $litmus
123 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
124 then
125 echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1
126 fi
127 ret=1
128 fi
129 elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'
130 then
131 echo " !!! Unexpected non-$outcome deadlock" $litmus
132 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
133 then
134 echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1
135 fi
136 ret=1
137 elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe
138 then
139 ret=0
140 else
141 if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled"
142 then
143 flag="--- Forgiven"
144 ret=0
145 else
146 flag="!!! Unexpected"
147 ret=1
148 fi
149 echo " $flag non-$outcome verification" $litmus
150 if ! grep -qe "$flag" $LKMM_DESTDIR/$litmusout
151 then
152 echo " $flag non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1
153 fi
154 fi
155 tail -2 $LKMM_DESTDIR/$litmusout | head -1
156 exit $ret
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.