1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
#!/bin/sh
# SPDX-License-Identifier: GPL-2.0+
#
# 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.litmus.HW.out, where "HW" is the --hw argument.
# In addition, non-Sometimes verification results will be noted, but
# forgiven. Furthermore, if there is no "Result:" comment but there is
# an LKMM .litmus.out file, the observation in that file will be used
# to judge the assembly-language verification.
#
# Usage:
# judgelitmus.sh file.litmus
#
# Run this in the directory containing the memory model, specifying the
# pathname of the litmus test to check.
#
# Copyright IBM Corporation, 2018
#
# Author: Paul E. McKenney <paulmck@linux.ibm.com>
litmus=$1
if test -f "$litmus" -a -r "$litmus"
then
:
else
echo ' --- ' error: \"$litmus\" is not a readable file
exit 255
fi
if test -z "$LKMM_HW_MAP_FILE"
then
litmusout=$litmus.out
lkmmout=
else
litmusout="`echo $litmus |
sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out"
lkmmout=$litmus.out
fi
if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"
then
:
else
echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file
exit 255
fi
if grep -q '^ \* Result: ' $litmus
then
outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1
then
outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'`
else
outcome=specified
fi
grep '^Observation' $LKMM_DESTDIR/$litmusout
if grep -q '^Observation' $LKMM_DESTDIR/$litmusout
then
:
elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout
then
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/$litmusout
then
echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1
fi
exit 254
elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout
then
echo ' !!! Timeout' $litmus
if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
then
echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1
fi
exit 124
else
echo ' !!! Verification error' $litmus
if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
then
echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1
fi
exit 255
fi
if test "$outcome" = DEADLOCK
then
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/$litmusout
then
echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1
fi
ret=1
fi
elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'
then
echo " !!! Unexpected non-$outcome deadlock" $litmus
if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
then
echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1
fi
ret=1
elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe
then
ret=0
else
if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes
then
flag="--- Forgiven"
ret=0
else
flag="!!! Unexpected"
ret=1
fi
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
|
