Commit | Line | Data |
---|---|---|
b02eb5b0 PM |
1 | #!/bin/sh |
2 | # SPDX-License-Identifier: GPL-2.0+ | |
3 | # | |
2024436d PM |
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 | |
68f7bcab PM |
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. | |
b02eb5b0 PM |
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 | # | |
61f615cc | 29 | # Author: Paul E. McKenney <paulmck@linux.ibm.com> |
b02eb5b0 PM |
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 | |
2024436d PM |
40 | if test -z "$LKMM_HW_MAP_FILE" |
41 | then | |
42 | litmusout=$litmus.out | |
0838ba7e | 43 | lkmmout= |
2024436d PM |
44 | else |
45 | litmusout="`echo $litmus | | |
ee542816 | 46 | sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out" |
0838ba7e | 47 | lkmmout=$litmus.out |
2024436d PM |
48 | fi |
49 | if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout" | |
b02eb5b0 PM |
50 | then |
51 | : | |
52 | else | |
2024436d | 53 | echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file |
b02eb5b0 PM |
54 | exit 255 |
55 | fi | |
68f7bcab PM |
56 | if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout" |
57 | then | |
58 | datarace_modeled=1 | |
59 | fi | |
b02eb5b0 PM |
60 | if grep -q '^ \* Result: ' $litmus |
61 | then | |
62 | outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'` | |
68f7bcab PM |
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 | |
0838ba7e PM |
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 }'` | |
b02eb5b0 PM |
80 | else |
81 | outcome=specified | |
82 | fi | |
83 | ||
2024436d PM |
84 | grep '^Observation' $LKMM_DESTDIR/$litmusout |
85 | if grep -q '^Observation' $LKMM_DESTDIR/$litmusout | |
b02eb5b0 PM |
86 | then |
87 | : | |
2024436d | 88 | elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout |
02484d82 | 89 | then |
2024436d | 90 | badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout | |
02484d82 PM |
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 | |
2024436d | 95 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
02484d82 | 96 | then |
2024436d | 97 | echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1 |
02484d82 PM |
98 | fi |
99 | exit 254 | |
2024436d | 100 | elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout |
2c644d3f PM |
101 | then |
102 | echo ' !!! Timeout' $litmus | |
2024436d | 103 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
2c644d3f | 104 | then |
2024436d | 105 | echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1 |
2c644d3f PM |
106 | fi |
107 | exit 124 | |
b02eb5b0 PM |
108 | else |
109 | echo ' !!! Verification error' $litmus | |
2024436d | 110 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
b02eb5b0 | 111 | then |
2024436d | 112 | echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1 |
b02eb5b0 PM |
113 | fi |
114 | exit 255 | |
115 | fi | |
116 | if test "$outcome" = DEADLOCK | |
117 | then | |
2024436d | 118 | if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$' |
b02eb5b0 PM |
119 | then |
120 | ret=0 | |
121 | else | |
122 | echo " !!! Unexpected non-$outcome verification" $litmus | |
2024436d | 123 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
b02eb5b0 | 124 | then |
2024436d | 125 | echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1 |
b02eb5b0 PM |
126 | fi |
127 | ret=1 | |
128 | fi | |
2024436d | 129 | elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$' |
e253a403 PM |
130 | then |
131 | echo " !!! Unexpected non-$outcome deadlock" $litmus | |
2024436d | 132 | if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout |
e253a403 | 133 | then |
2024436d | 134 | echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1 |
e253a403 PM |
135 | fi |
136 | ret=1 | |
2024436d | 137 | elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe |
b02eb5b0 PM |
138 | then |
139 | ret=0 | |
140 | else | |
68f7bcab | 141 | if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled" |
b02eb5b0 | 142 | then |
2024436d PM |
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 | |
b02eb5b0 | 153 | fi |
b02eb5b0 | 154 | fi |
2024436d | 155 | tail -2 $LKMM_DESTDIR/$litmusout | head -1 |
b02eb5b0 | 156 | exit $ret |