1#!/bin/sh 2# 3# Run a herd test and check the result against a "Result:" comment within 4# the litmus test. If the verification result does not match that specified 5# in the litmus test, this script prints an error message prefixed with 6# "^^^" and exits with a non-zero status. It also outputs verification 7# results to a file whose name is that of the specified litmus test, but 8# with ".out" appended. 9# 10# Usage: 11# checklitmus.sh file.litmus 12# 13# The LINUX_HERD_OPTIONS environment variable may be used to specify 14# arguments to herd, which default to "-conf linux-kernel.cfg". Thus, 15# one would normally run this in the directory containing the memory model, 16# specifying the pathname of the litmus test to check. 17# 18# This program is free software; you can redistribute it and/or modify 19# it under the terms of the GNU General Public License as published by 20# the Free Software Foundation; either version 2 of the License, or 21# (at your option) any later version. 22# 23# This program is distributed in the hope that it will be useful, 24# but WITHOUT ANY WARRANTY; without even the implied warranty of 25# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 26# GNU General Public License for more details. 27# 28# You should have received a copy of the GNU General Public License 29# along with this program; if not, you can access it online at 30# http://www.gnu.org/licenses/gpl-2.0.html. 31# 32# Copyright IBM Corporation, 2018 33# 34# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com> 35 36litmus=$1 37herdoptions=${LINUX_HERD_OPTIONS--conf linux-kernel.cfg} 38 39if test -f "$litmus" -a -r "$litmus" 40then 41 : 42else 43 echo ' --- ' error: \"$litmus\" is not a readable file 44 exit 255 45fi 46if grep -q '^ \* Result: ' $litmus 47then 48 outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'` 49else 50 outcome=specified 51fi 52 53echo Herd options: $herdoptions > $litmus.out 54/usr/bin/time herd7 -o ~/tmp $herdoptions $litmus >> $litmus.out 2>&1 55grep "Herd options:" $litmus.out 56grep '^Observation' $litmus.out 57if grep -q '^Observation' $litmus.out 58then 59 : 60else 61 cat $litmus.out 62 echo ' ^^^ Verification error' 63 echo ' ^^^ Verification error' >> $litmus.out 2>&1 64 exit 255 65fi 66if test "$outcome" = DEADLOCK 67then 68 echo grep 3 and 4 69 if grep '^Observation' $litmus.out | grep -q 'Never 0 0$' 70 then 71 ret=0 72 else 73 echo " ^^^ Unexpected non-$outcome verification" 74 echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1 75 ret=1 76 fi 77elif grep '^Observation' $litmus.out | grep -q $outcome || test "$outcome" = Maybe 78then 79 ret=0 80else 81 echo " ^^^ Unexpected non-$outcome verification" 82 echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1 83 ret=1 84fi 85tail -2 $litmus.out | head -1 86exit $ret 87