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 31litmus=$1 32 33if test -f "$litmus" -a -r "$litmus" 34then 35 : 36else 37 echo ' --- ' error: \"$litmus\" is not a readable file 38 exit 255 39fi 40if test -z "$LKMM_HW_MAP_FILE" 41then 42 litmusout=$litmus.out 43 lkmmout= 44else 45 litmusout="`echo $litmus | 46 sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out" 47 lkmmout=$litmus.out 48fi 49if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout" 50then 51 : 52else 53 echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file 54 exit 255 55fi 56if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout" 57then 58 datarace_modeled=1 59fi 60if grep -q '^[( ]\* Result: ' $litmus 61then 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 77elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1 78then 79 outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'` 80else 81 outcome=specified 82fi 83 84grep '^Observation' $LKMM_DESTDIR/$litmusout 85if grep -q '^Observation' $LKMM_DESTDIR/$litmusout 86then 87 : 88elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout 89then 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 100elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout 101then 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 108else 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 115fi 116if test "$outcome" = DEADLOCK 117then 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 129elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$' 130then 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 137elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe 138then 139 ret=0 140else 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 154fi 155tail -2 $LKMM_DESTDIR/$litmusout | head -1 156exit $ret 157