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.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
  18 litmus=$1
  19
  20 if test -f "$litmus" -a -r "$litmus"
  21 then
  22         :
  23 else
  24         echo ' --- ' error: \"$litmus\" is not a readable file
  25         exit 255
  26 fi
  27 if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out
  28 then
  29         :
  30 else
  31         echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file
  32         exit 255
  33 fi
  34 if grep -q '^ \* Result: ' $litmus
  35 then
  36         outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
  37 else
  38         outcome=specified
  39 fi
  40
  41 grep '^Observation' $LKMM_DESTDIR/$litmus.out
  42 if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
  43 then
  44         :
  45 else
  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
  52 fi
  53 if test "$outcome" = DEADLOCK
  54 then
  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
  66 elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
  67 then
  68         ret=0
  69 else
  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
  76 fi
  77 tail -2 $LKMM_DESTDIR/$litmus.out | head -1
  78 exit $ret