linux-stable/tools/memory-model/scripts/checklitmus.sh
Paul E. McKenney 2fb6ae162f tools/memory-model: Add scripts to test memory model
This commit adds a pair of scripts that run the memory model on litmus
tests, checking that the verification result of each litmus test matches
the result flagged in the litmus test itself.  These scripts permit easier
checking of changes to the memory model against preconceived notions.

To run the scripts, go to the tools/memory-model directory and type
"scripts/checkalllitmus.sh".  If all is well, the last line printed will
be "All litmus tests verified as was expected."

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Cc: Andrew Morton <akpm@linux-foundation.org>
Cc: Linus Torvalds <torvalds@linux-foundation.org>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Thomas Gleixner <tglx@linutronix.de>
Cc: Will Deacon <will.deacon@arm.com>
Cc: akiyks@gmail.com
Cc: boqun.feng@gmail.com
Cc: dhowells@redhat.com
Cc: j.alglave@ucl.ac.uk
Cc: linux-arch@vger.kernel.org
Cc: luc.maranget@inria.fr
Cc: npiggin@gmail.com
Cc: parri.andrea@gmail.com
Cc: stern@rowland.harvard.edu
Link: http://lkml.kernel.org/r/1526340837-12222-9-git-send-email-paulmck@linux.vnet.ibm.com
Signed-off-by: Ingo Molnar <mingo@kernel.org>
2018-05-15 08:11:17 +02:00

86 lines
2.6 KiB
Bash

#!/bin/sh
#
# Run a herd test and check the result against a "Result:" comment within
# the litmus test. If the verification result does not match that specified
# in the litmus test, this script prints an error message prefixed with
# "^^^" and exits with a non-zero status. It also outputs verification
# results to a file whose name is that of the specified litmus test, but
# with ".out" appended.
#
# Usage:
# sh checklitmus.sh file.litmus
#
# The LINUX_HERD_OPTIONS environment variable may be used to specify
# arguments to herd, which default to "-conf linux-kernel.cfg". Thus,
# one would normally run this in the directory containing the memory model,
# specifying the pathname of the litmus test to check.
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program; if not, you can access it online at
# http://www.gnu.org/licenses/gpl-2.0.html.
#
# Copyright IBM Corporation, 2018
#
# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
litmus=$1
herdoptions=${LINUX_HERD_OPTIONS--conf linux-kernel.cfg}
if test -f "$litmus" -a -r "$litmus"
then
:
else
echo ' --- ' error: \"$litmus\" is not a readable file
exit 255
fi
if grep -q '^ \* Result: ' $litmus
then
outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
else
outcome=specified
fi
echo Herd options: $herdoptions > $litmus.out
/usr/bin/time herd7 -o ~/tmp $herdoptions $litmus >> $litmus.out 2>&1
grep "Herd options:" $litmus.out
grep '^Observation' $litmus.out
if grep -q '^Observation' $litmus.out
then
:
else
cat $litmus.out
echo ' ^^^ Verification error'
echo ' ^^^ Verification error' >> $litmus.out 2>&1
exit 255
fi
if test "$outcome" = DEADLOCK
then
echo grep 3 and 4
if grep '^Observation' $litmus.out | grep -q 'Never 0 0$'
then
ret=0
else
echo " ^^^ Unexpected non-$outcome verification"
echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
ret=1
fi
elif grep '^Observation' $litmus.out | grep -q $outcome || test "$outcome" = Maybe
then
ret=0
else
echo " ^^^ Unexpected non-$outcome verification"
echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
ret=1
fi
tail -2 $litmus.out | head -1
exit $ret