diff options
author | Paul E. McKenney <paulmck@kernel.org> | 2019-03-20 12:39:27 -0700 |
---|---|---|
committer | Paul E. McKenney <paulmck@kernel.org> | 2023-03-24 10:24:14 -0700 |
commit | 579ecb2e4108af3689b1b814fff23f6a69907dab (patch) | |
tree | e79d566885fd4b9c3473209c03cf543260e98953 /tools/memory-model/scripts/checkalllitmus.sh | |
parent | e029374ba8483e1c59243a70bf0926f0ca8f54e2 (diff) | |
download | linux-stable-579ecb2e4108af3689b1b814fff23f6a69907dab.tar.gz linux-stable-579ecb2e4108af3689b1b814fff23f6a69907dab.tar.bz2 linux-stable-579ecb2e4108af3689b1b814fff23f6a69907dab.zip |
tools/memory-model: Hardware checking for check{,all}litmus.sh
This commit makes checklitmus.sh and checkalllitmus.sh check to see
if a hardware verification was specified (via the --hw command-line
argument, which sets the LKMM_HW_MAP_FILE environment variable).
If so, the C-language litmus test is converted to the specified type
of assembly-language litmus test and herd is run on it. Hardware is
permitted to be stronger than LKMM requires, so "Always" and "Never"
verifications of "Sometimes" C-language litmus tests are forgiven.
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'tools/memory-model/scripts/checkalllitmus.sh')
-rwxr-xr-x | tools/memory-model/scripts/checkalllitmus.sh | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh index 54d8da8c338e..2d3ee850a839 100755 --- a/tools/memory-model/scripts/checkalllitmus.sh +++ b/tools/memory-model/scripts/checkalllitmus.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/bin/bash # SPDX-License-Identifier: GPL-2.0+ # # Run herd7 tests on all .litmus files in the litmus-tests directory @@ -8,6 +8,11 @@ # "^^^". It also outputs verification results to a file whose name is # that of the specified litmus test, but with ".out" appended. # +# If the --hw argument is specified, this script translates the .litmus +# C-language file to the specified type of assembly and verifies that. +# But in this case, litmus tests using complex synchronization (such as +# locking, RCU, and SRCU) are cheerfully ignored. +# # Usage: # checkalllitmus.sh # @@ -38,21 +43,15 @@ then ( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh ) fi -# Find the checklitmus script. If it is not where we expect it, then -# assume that the caller has the PATH environment variable set -# appropriately. -if test -x scripts/checklitmus.sh -then - clscript=scripts/checklitmus.sh -else - clscript=checklitmus.sh -fi - # Run the script on all the litmus tests in the specified directory ret=0 for i in $litmusdir/*.litmus do - if ! $clscript $i + if test -n "$LKMM_HW_MAP_FILE" && ! scripts/simpletest.sh $i + then + continue + fi + if ! scripts/checklitmus.sh $i then ret=1 fi |