tools/memory-model/scripts/judgelitmus.sh

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