tools/memory-model/scripts/runlitmus.sh

   1 #!/bin/sh
   2 # SPDX-License-Identifier: GPL-2.0+
   3 #
   4 # Without the -hw argument, runs a herd7 test and outputs verification
   5 # results to a file whose name is that of the specified litmus test,
   6 # but with ".out" appended.
   7 #
   8 # If the --hw argument is specified, this script translates the .litmus
   9 # C-language file to the specified type of assembly and verifies that.
  10 # But in this case, litmus tests using complex synchronization (such as
  11 # locking, RCU, and SRCU) are cheerfully ignored.
  12 #
  13 # Either way, return the status of the herd7 command.
  14 #
  15 # Usage:
  16 #       runlitmus.sh file.litmus
  17 #
  18 # Run this in the directory containing the memory model, specifying the
  19 # pathname of the litmus test to check.  The caller is expected to have
  20 # properly set up the LKMM environment variables.
  21 #
  22 # Copyright IBM Corporation, 2019
  23 #
  24 # Author: Paul E. McKenney <paulmck@linux.ibm.com>
  25
  26 litmus=$1
  27 if test -f "$litmus" -a -r "$litmus"
  28 then
  29         :
  30 else
  31         echo ' !!! ' error: \"$litmus\" is not a readable file
  32         exit 255
  33 fi
  34
  35 if test -z "$LKMM_HW_MAP_FILE" -o ! -e $LKMM_DESTDIR/$litmus.out
  36 then
  37         # LKMM run
  38         herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
  39         echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
  40         /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
  41         ret=$?
  42         if test -z "$LKMM_HW_MAP_FILE"
  43         then
  44                 exit $ret
  45         fi
  46         echo " --- " Automatically generated LKMM output for '"'--hw $LKMM_HW_MAP_FILE'"' run
  47 fi
  48
  49 # Hardware run
  50
  51 T=/tmp/checklitmushw.sh.$$
  52 trap 'rm -rf $T' 0 2
  53 mkdir $T
  54
  55 # Generate filenames
  56 mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
  57 themefile="$T/${LKMM_HW_MAP_FILE}.theme"
  58 herdoptions="-model $LKMM_HW_CAT_FILE"
  59 hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`
  60 hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
  61
  62 # Don't run on litmus tests with complex synchronization
  63 if ! scripts/simpletest.sh $litmus
  64 then
  65         echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
  66         exit 254
  67 fi
  68
  69 # Generate the assembly code and run herd7 on it.
  70 gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
  71 jingle7 -v -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
  72 if grep -q "Generated 0 tests" $T/$hwlitmusfile.jingle7.out
  73 then
  74         echo ' !!! ' jingle7 failed, errors in $hwlitmus.err
  75         cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err
  76         exit 253
  77 fi
  78 /usr/bin/time $LKMM_TIMEOUT_CMD herd7 -unroll 0 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
  79
  80 exit $?