xref: /linux/tools/memory-model/scripts/judgelitmus.sh (revision 26fbb4c8c7c3ee9a4c3b4de555a8587b5a19154e)
1#!/bin/sh
2# SPDX-License-Identifier: GPL-2.0+
3#
4# Given a .litmus test and the corresponding .litmus.out file, check
5# the .litmus.out file against the "Result:" comment to judge whether
6# the test ran correctly.
7#
8# Usage:
9#	judgelitmus.sh file.litmus
10#
11# Run this in the directory containing the memory model, specifying the
12# pathname of the litmus test to check.
13#
14# Copyright IBM Corporation, 2018
15#
16# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
17
18litmus=$1
19
20if test -f "$litmus" -a -r "$litmus"
21then
22	:
23else
24	echo ' --- ' error: \"$litmus\" is not a readable file
25	exit 255
26fi
27if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out
28then
29	:
30else
31	echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file
32	exit 255
33fi
34if grep -q '^ \* Result: ' $litmus
35then
36	outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
37else
38	outcome=specified
39fi
40
41grep '^Observation' $LKMM_DESTDIR/$litmus.out
42if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
43then
44	:
45else
46	echo ' !!! Verification error' $litmus
47	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
48	then
49		echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1
50	fi
51	exit 255
52fi
53if test "$outcome" = DEADLOCK
54then
55	if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
56	then
57		ret=0
58	else
59		echo " !!! Unexpected non-$outcome verification" $litmus
60		if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
61		then
62			echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
63		fi
64		ret=1
65	fi
66elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
67then
68	ret=0
69else
70	echo " !!! Unexpected non-$outcome verification" $litmus
71	if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
72	then
73		echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
74	fi
75	ret=1
76fi
77tail -2 $LKMM_DESTDIR/$litmus.out | head -1
78exit $ret
79