summaryrefslogtreecommitdiffstats
path: root/tools/memory-model/scripts/judgelitmus.sh
blob: 1ec5d89fcfbb2a2f6e93803882c94104b20d992d (plain)
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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
#!/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 either a
# "DATARACE" marker in the "Result:" comment or a "Flag data-race" marker
# in the LKMM output is present, the other must also be as well, at least
# for litmus tests having a "Result:" comment. In this case, a failure of
# the Always/Sometimes/Never portion of the "Result:" prediction will be
# noted, but forgiven.
#
# If the --hw 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 '^Flag data-race$' "$LKMM_DESTDIR/$litmusout"
then
	datarace_modeled=1
fi
if grep -q '^[( ]\* Result: ' $litmus
then
	outcome=`grep -m 1 '^[( ]\* Result: ' $litmus | awk '{ print $3 }'`
	if grep -m1 '^[( ]\* Result: .* DATARACE' $litmus
	then
		datarace_predicted=1
	fi
	if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE"
	then
		echo '!!! Predicted data race not modeled' $litmus
		exit 252
	elif test -z "$datarace_predicted" -a -n "$datarace_modeled"
	then
		# Note that hardware models currently don't model data races
		echo '!!! Unexpected data race modeled' $litmus
		exit 253
	fi
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 \) -o -n "$datarace_modeled"
	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