157 lines · bash
1#!/bin/sh2# SPDX-License-Identifier: GPL-2.0+3#4# Given a .litmus test and the corresponding litmus output file, check5# the .litmus.out file against the "Result:" comment to judge whether the6# test ran correctly. If the --hw argument is omitted, check against the7# LKMM output, which is assumed to be in file.litmus.out. If either a8# "DATARACE" marker in the "Result:" comment or a "Flag data-race" marker9# in the LKMM output is present, the other must also be as well, at least10# for litmus tests having a "Result:" comment. In this case, a failure of11# the Always/Sometimes/Never portion of the "Result:" prediction will be12# noted, but forgiven.13#14# If the --hw argument is provided, this is assumed to be a hardware15# test, and the output is assumed to be in file.litmus.HW.out, where16# "HW" is the --hw argument. In addition, non-Sometimes verification17# results will be noted, but forgiven. Furthermore, if there is no18# "Result:" comment but there is an LKMM .litmus.out file, the observation19# in that file will be used to judge the assembly-language verification.20#21# Usage:22# judgelitmus.sh file.litmus23#24# Run this in the directory containing the memory model, specifying the25# pathname of the litmus test to check.26#27# Copyright IBM Corporation, 201828#29# Author: Paul E. McKenney <paulmck@linux.ibm.com>30 31litmus=$132 33if test -f "$litmus" -a -r "$litmus"34then35 :36else37 echo ' --- ' error: \"$litmus\" is not a readable file38 exit 25539fi40if test -z "$LKMM_HW_MAP_FILE"41then42 litmusout=$litmus.out43 lkmmout=44else45 litmusout="`echo $litmus |46 sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out"47 lkmmout=$litmus.out48fi49if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"50then51 :52else53 echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file54 exit 25555fi56if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout"57then58 datarace_modeled=159fi60if grep -q '^[( ]\* Result: ' $litmus61then62 outcome=`grep -m 1 '^[( ]\* Result: ' $litmus | awk '{ print $3 }'`63 if grep -m1 '^[( ]\* Result: .* DATARACE' $litmus64 then65 datarace_predicted=166 fi67 if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE"68 then69 echo '!!! Predicted data race not modeled' $litmus70 exit 25271 elif test -z "$datarace_predicted" -a -n "$datarace_modeled"72 then73 # Note that hardware models currently don't model data races74 echo '!!! Unexpected data race modeled' $litmus75 exit 25376 fi77elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&178then79 outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'`80else81 outcome=specified82fi83 84grep '^Observation' $LKMM_DESTDIR/$litmusout85if grep -q '^Observation' $LKMM_DESTDIR/$litmusout86then87 :88elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout89then90 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 $badmsg95 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout96 then97 echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&198 fi99 exit 254100elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout101then102 echo ' !!! Timeout' $litmus103 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout104 then105 echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1106 fi107 exit 124108else109 echo ' !!! Verification error' $litmus110 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout111 then112 echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1113 fi114 exit 255115fi116if test "$outcome" = DEADLOCK117then118 if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'119 then120 ret=0121 else122 echo " !!! Unexpected non-$outcome verification" $litmus123 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout124 then125 echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1126 fi127 ret=1128 fi129elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'130then131 echo " !!! Unexpected non-$outcome deadlock" $litmus132 if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout133 then134 echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1135 fi136 ret=1137elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe138then139 ret=0140else141 if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled"142 then143 flag="--- Forgiven"144 ret=0145 else146 flag="!!! Unexpected"147 ret=1148 fi149 echo " $flag non-$outcome verification" $litmus150 if ! grep -qe "$flag" $LKMM_DESTDIR/$litmusout151 then152 echo " $flag non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1153 fi154fi155tail -2 $LKMM_DESTDIR/$litmusout | head -1156exit $ret157