memory-model/scripts/judgelitmus.sh

0001 #!/bin/sh
0002 # SPDX-License-Identifier: GPL-2.0+
0003 #
0004 # Given a .litmus test and the corresponding .litmus.out file, check
0005 # the .litmus.out file against the "Result:" comment to judge whether
0006 # the test ran correctly.
0007 #
0008 # Usage:
0009 #       judgelitmus.sh file.litmus
0010 #
0011 # Run this in the directory containing the memory model, specifying the
0012 # pathname of the litmus test to check.
0013 #
0014 # Copyright IBM Corporation, 2018
0015 #
0016 # Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
0017
0018 litmus=$1
0019
0020 if test -f "$litmus" -a -r "$litmus"
0021 then
0022         :
0023 else
0024         echo ' --- ' error: \"$litmus\" is not a readable file
0025         exit 255
0026 fi
0027 if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out
0028 then
0029         :
0030 else
0031         echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file
0032         exit 255
0033 fi
0034 if grep -q '^ \* Result: ' $litmus
0035 then
0036         outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
0037 else
0038         outcome=specified
0039 fi
0040
0041 grep '^Observation' $LKMM_DESTDIR/$litmus.out
0042 if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
0043 then
0044         :
0045 else
0046         echo ' !!! Verification error' $litmus
0047         if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
0048         then
0049                 echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1
0050         fi
0051         exit 255
0052 fi
0053 if test "$outcome" = DEADLOCK
0054 then
0055         if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
0056         then
0057                 ret=0
0058         else
0059                 echo " !!! Unexpected non-$outcome verification" $litmus
0060                 if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
0061                 then
0062                         echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
0063                 fi
0064                 ret=1
0065         fi
0066 elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
0067 then
0068         ret=0
0069 else
0070         echo " !!! Unexpected non-$outcome verification" $litmus
0071         if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
0072         then
0073                 echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
0074         fi
0075         ret=1
0076 fi
0077 tail -2 $LKMM_DESTDIR/$litmus.out | head -1
0078 exit $ret