Hello!
This series contains LKMM updates:
1. Make scripts be executable.
2-3. Make LKMM scripts note timeouts instead of just saying that
the validation was bad.
4. Make LKMM scripts identify litmus-test typos and use of
unsupported primitives instead of just saying that the validation
was bad.
5. Make LKMM scripts detect unconditional deadlocks.
6. Fix email address on LKMM scripts.
7-29. Leverage Boqun Feng's C-to-assembly litmus-test-translation
capability to allow verifying LKMM against hardware models for
checkalllitmus.sh. This is a work in progress.
30. Use cumul-fence instead of fence in ->prop example, courtesy
of Joel Fernandes.
31. Update the informal documentation, courtesy of Andrea Parri.
Thanx, Paul
------------------------------------------------------------------------
Documentation/explanation.txt | 53 +++++++--------
README | 18 ++---
litmus-tests/.gitignore | 4 -
scripts/README | 16 +++-
scripts/checkalllitmus.sh | 29 ++++----
scripts/checkghlitmus.sh | 11 +--
scripts/checklitmus.sh | 101 ++++++++++++-----------------
scripts/checklitmushist.sh | 2
scripts/checktheselitmus.sh | 43 ++++++++++++
scripts/cmplitmushist.sh | 53 ++++++++++++++-
scripts/hwfnseg.sh | 20 +++++
scripts/initlitmushist.sh | 2
scripts/judgelitmus.sh | 142 +++++++++++++++++++++++++++++++----------
scripts/newlitmushist.sh | 4 -
scripts/parseargs.sh | 21 ++++--
scripts/runlitmus.sh | 144 ++++++++++++++++++++++++++++++++----------
scripts/runlitmushist.sh | 30 +++++---
scripts/simpletest.sh | 35 ++++++++++
18 files changed, 514 insertions(+), 214 deletions(-)
From: "Joel Fernandes (Google)" <[email protected]>
To reduce ambiguity in the more exotic ->prop ordering example, this
commit uses the term cumul-fence instead of the term fence for the two
fences, so that the implict ->rfe on loads/stores to Y are covered by
the description.
Link: https://lore.kernel.org/lkml/[email protected]
Suggested-by: Alan Stern <[email protected]>
Signed-off-by: Joel Fernandes (Google) <[email protected]>
Acked-by: Alan Stern <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/Documentation/explanation.txt | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 68caa9a976d0..634dc6db26c4 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -1302,7 +1302,7 @@ followed by an arbitrary number of cumul-fence links, ending with an
rfe link. You can concoct more exotic examples, containing more than
one fence, although this quickly leads to diminishing returns in terms
of complexity. For instance, here's an example containing a coe link
-followed by two fences and an rfe link, utilizing the fact that
+followed by two cumul-fences and an rfe link, utilizing the fact that
release fences are A-cumulative:
int x, y, z;
@@ -1334,10 +1334,10 @@ If x = 2, r0 = 1, and r2 = 1 after this code runs then there is a prop
link from P0's store to its load. This is because P0's store gets
overwritten by P1's store since x = 2 at the end (a coe link), the
smp_wmb() ensures that P1's store to x propagates to P2 before the
-store to y does (the first fence), the store to y propagates to P2
+store to y does (the first cumul-fence), the store to y propagates to P2
before P2's load and store execute, P2's smp_store_release()
guarantees that the stores to x and y both propagate to P0 before the
-store to z does (the second fence), and P0's load executes after the
+store to z does (the second cumul-fence), and P0's load executes after the
store to z has propagated to P0 (an rfe link).
In summary, the fact that the hb relation links memory access events
--
2.17.1
The scripts that generate the litmus tests in the "auto" directory of
the https://github.com/paulmckrcu/litmus archive place the "Result:"
tag into a single-line ocaml comment, which judgelitmus.sh currently
does not recognize. This commit therefore makes judgelitmus.sh
recognize both the multiline comment format that it currently does
and the automatically generated single-line format.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/judgelitmus.sh | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index eaa2cc7d3b36..6408c012bdf5 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -51,10 +51,10 @@ if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout"
then
datarace_modeled=1
fi
-if grep -q '^ \* Result: ' $litmus
+if grep -q '^[( ]\* Result: ' $litmus
then
- outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
- if grep -m1 '^ \* Result: .* DATARACE' $litmus
+ outcome=`grep -m 1 '^[( ]\* Result: ' $litmus | awk '{ print $3 }'`
+ if grep -m1 '^[( ]\* Result: .* DATARACE' $litmus
then
datarace_predicted=1
fi
--
2.17.1
The checkghlitmus.sh script currently uses grep to ignore non-C-language
litmus tests, which is a bit fragile. This commit therefore enlists the
aid of "mselect7 -arch C", given Luc Maraget's recent modifications that
allow mselect7 to operate in filter mode.
This change requires herdtools 7.52-32-g1da3e0e50977 or later.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/checkghlitmus.sh | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh
index 2ea220d2564b..cedd0290b73f 100755
--- a/tools/memory-model/scripts/checkghlitmus.sh
+++ b/tools/memory-model/scripts/checkghlitmus.sh
@@ -41,7 +41,7 @@ fi
# Create a list of C-language litmus tests with "Result:" commands and
# no more than the specified number of processes.
-find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
+find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C
xargs < $T/list-C -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result
xargs < $T/list-C-result -r grep -L "^P${LKMM_PROCS}" > $T/list-C-result-short
--
2.17.1
The history-check scripts currently use grep to ignore non-C-language
litmus tests, which is a bit fragile. This commit therefore enlists the
aid of "mselect7 -arch C", given Luc Maraget's recent modifications that
allow mselect7 to operate in filter mode.
This change requires herdtools 7.52-32-g1da3e0e50977 or later.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/initlitmushist.sh | 2 +-
tools/memory-model/scripts/newlitmushist.sh | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/tools/memory-model/scripts/initlitmushist.sh b/tools/memory-model/scripts/initlitmushist.sh
index 956b6957484d..31ea782955d3 100755
--- a/tools/memory-model/scripts/initlitmushist.sh
+++ b/tools/memory-model/scripts/initlitmushist.sh
@@ -60,7 +60,7 @@ fi
# Create a list of the C-language litmus tests with no more than the
# specified number of processes (per the --procs argument).
-find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
+find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C
xargs < $T/list-C -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
scripts/runlitmushist.sh < $T/list-C-short
diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh
index 3f4b06e29988..25235e2049cf 100755
--- a/tools/memory-model/scripts/newlitmushist.sh
+++ b/tools/memory-model/scripts/newlitmushist.sh
@@ -43,7 +43,7 @@ fi
# Form full list of litmus tests with no more than the specified
# number of processes (per the --procs argument).
-find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C-all
+find litmus -name '*.litmus' -print | mselect7 -arch C > $T/list-C-all
xargs < $T/list-C-all -r grep -L "^P${LKMM_PROCS}" > $T/list-C-short
# Form list of new tests. Note: This does not handle litmus-test deletion!
--
2.17.1
When the github scripts see ".litmus.out", they assume that there must be
a corresponding C-language ".litmus" file. Won't they be disappointed
when they instead see nothing, or, worse yet, the corresponding
assembly-language litmus test? This commit therefore swaps the hardware
tag with the "litmus" to avoid this sort of disappointment.
This commit also adjusts the .gitignore file so as to avoid adding these
new ".out" files to git.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/litmus-tests/.gitignore | 2 +-
tools/memory-model/scripts/judgelitmus.sh | 2 +-
tools/memory-model/scripts/runlitmus.sh | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore
index 6e2ddc54152f..f47cb2045f13 100644
--- a/tools/memory-model/litmus-tests/.gitignore
+++ b/tools/memory-model/litmus-tests/.gitignore
@@ -1 +1 @@
-*.litmus.out
+*.out
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index fe9131f8eb96..ca9a19829d79 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -37,7 +37,7 @@ then
lkmmout=
else
litmusout="`echo $litmus |
- sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out"
+ sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`.out"
lkmmout=$litmus.out
fi
if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 2865a9661b07..c84124b32bee 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -57,7 +57,7 @@ catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
themefile="$T/${LKMM_HW_MAP_FILE}.theme"
herdoptions="-model $LKMM_HW_CAT_FILE"
-hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
+hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.litmus.'${LKMM_HW_MAP_FILE}'/'`
hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
# Don't run on litmus tests with complex synchronization
--
2.17.1
This commit adds functionality to judgelitmus.sh to allow it to handle
both the "DATARACE" markers in the "Result:" comments in litmus tests
and the "Flag data-race" markers in LKMM output. For C-language tests,
if either marker is present, the other must also be as well, at least for
litmus tests having a "Result:" comment. If the LKMM output indicates
a data race, then failures of the Always/Sometimes/Never portion of the
"Result:" prediction are forgiven.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++++++++-
1 file changed, 19 insertions(+), 1 deletion(-)
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index ca9a19829d79..eaa2cc7d3b36 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -47,9 +47,27 @@ else
echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file
exit 255
fi
+if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout"
+then
+ datarace_modeled=1
+fi
if grep -q '^ \* Result: ' $litmus
then
outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
+ if grep -m1 '^ \* Result: .* DATARACE' $litmus
+ then
+ datarace_predicted=1
+ fi
+ if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE"
+ then
+ echo '!!! Predicted data race not modeled' $litmus
+ exit 252
+ elif test -z "$datarace_predicted" -a -n "$datarace_modeled"
+ then
+ # Note that hardware models currently don't model data races
+ echo '!!! Unexpected data race modeled' $litmus
+ exit 253
+ fi
elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1
then
outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'`
@@ -114,7 +132,7 @@ elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$o
then
ret=0
else
- if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes
+ if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled"
then
flag="--- Forgiven"
ret=0
--
2.17.1
The checkalllitmus.sh runs litmus tests in the litmus-tests directory,
not those in the github archive, so this commit updates the comment to
reflect this reality.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/checkalllitmus.sh | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh
index 10e14d94acee..54d8da8c338e 100755
--- a/tools/memory-model/scripts/checkalllitmus.sh
+++ b/tools/memory-model/scripts/checkalllitmus.sh
@@ -30,8 +30,8 @@ else
exit 255
fi
-# Create any new directories that have appeared in the github litmus
-# repo since the last run.
+# Create any new directories that have appeared in the litmus-tests
+# directory since the last run.
if test "$LKMM_DESTDIR" != "."
then
find $litmusdir -type d -print |
--
2.17.1
It turns out that the jingle7 tool is currently a bit picky about
the litmus tests it is willing to process. This commit therefore
ensures that jingle7 failures are reported.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/runlitmus.sh | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index afb196d7ef10..5f2d29b460ff 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -69,6 +69,11 @@ fi
# Generate the assembly code and run herd7 on it.
gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
+if grep -q "Generated 0 tests" $T/$hwlitmusfile.jingle7.out
+then
+ echo ' !!! ' jingle7 failed, no $hwlitmus generated
+ exit 253
+fi
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
exit $?
--
2.17.1
From: Andrea Parri <[email protected]>
The formal memory consistency model has added support for plain accesses
(and data races). While updating the informal documentation to describe
this addition to the model is highly desirable and important future work,
update the informal documentation to at least acknowledge such addition.
Signed-off-by: Andrea Parri <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Boqun Feng <[email protected]>
Cc: Nicholas Piggin <[email protected]>
Cc: David Howells <[email protected]>
Cc: Jade Alglave <[email protected]>
Cc: Luc Maranget <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Akira Yokosawa <[email protected]>
Cc: Daniel Lustig <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
Acked-by: Alan Stern <[email protected]>
---
.../Documentation/explanation.txt | 47 +++++++++----------
tools/memory-model/README | 18 +++----
2 files changed, 30 insertions(+), 35 deletions(-)
diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
index 634dc6db26c4..488f11f6c588 100644
--- a/tools/memory-model/Documentation/explanation.txt
+++ b/tools/memory-model/Documentation/explanation.txt
@@ -42,7 +42,8 @@ linux-kernel.bell and linux-kernel.cat files that make up the formal
version of the model; they are extremely terse and their meanings are
far from clear.
-This document describes the ideas underlying the LKMM. It is meant
+This document describes the ideas underlying the LKMM, but excluding
+the modeling of bare C (or plain) shared memory accesses. It is meant
for people who want to understand how the model was designed. It does
not go into the details of the code in the .bell and .cat files;
rather, it explains in English what the code expresses symbolically.
@@ -354,31 +355,25 @@ be extremely complex.
Optimizing compilers have great freedom in the way they translate
source code to object code. They are allowed to apply transformations
that add memory accesses, eliminate accesses, combine them, split them
-into pieces, or move them around. Faced with all these possibilities,
-the LKMM basically gives up. It insists that the code it analyzes
-must contain no ordinary accesses to shared memory; all accesses must
-be performed using READ_ONCE(), WRITE_ONCE(), or one of the other
-atomic or synchronization primitives. These primitives prevent a
-large number of compiler optimizations. In particular, it is
-guaranteed that the compiler will not remove such accesses from the
-generated code (unless it can prove the accesses will never be
-executed), it will not change the order in which they occur in the
-code (within limits imposed by the C standard), and it will not
-introduce extraneous accesses.
-
-This explains why the MP and SB examples above used READ_ONCE() and
-WRITE_ONCE() rather than ordinary memory accesses. Thanks to this
-usage, we can be certain that in the MP example, P0's write event to
-buf really is po-before its write event to flag, and similarly for the
-other shared memory accesses in the examples.
-
-Private variables are not subject to this restriction. Since they are
-not shared between CPUs, they can be accessed normally without
-READ_ONCE() or WRITE_ONCE(), and there will be no ill effects. In
-fact, they need not even be stored in normal memory at all -- in
-principle a private variable could be stored in a CPU register (hence
-the convention that these variables have names starting with the
-letter 'r').
+into pieces, or move them around. The use of READ_ONCE(), WRITE_ONCE(),
+or one of the other atomic or synchronization primitives prevents a
+large number of compiler optimizations. In particular, it is guaranteed
+that the compiler will not remove such accesses from the generated code
+(unless it can prove the accesses will never be executed), it will not
+change the order in which they occur in the code (within limits imposed
+by the C standard), and it will not introduce extraneous accesses.
+
+The MP and SB examples above used READ_ONCE() and WRITE_ONCE() rather
+than ordinary memory accesses. Thanks to this usage, we can be certain
+that in the MP example, the compiler won't reorder P0's write event to
+buf and P0's write event to flag, and similarly for the other shared
+memory accesses in the examples.
+
+Since private variables are not shared between CPUs, they can be
+accessed normally without READ_ONCE() or WRITE_ONCE(). In fact, they
+need not even be stored in normal memory at all -- in principle a
+private variable could be stored in a CPU register (hence the convention
+that these variables have names starting with the letter 'r').
A WARNING
diff --git a/tools/memory-model/README b/tools/memory-model/README
index 2b87f3971548..fc07b52f2028 100644
--- a/tools/memory-model/README
+++ b/tools/memory-model/README
@@ -167,15 +167,15 @@ scripts Various scripts, see scripts/README.
LIMITATIONS
===========
-The Linux-kernel memory model has the following limitations:
-
-1. Compiler optimizations are not modeled. Of course, the use
- of READ_ONCE() and WRITE_ONCE() limits the compiler's ability
- to optimize, but there is Linux-kernel code that uses bare C
- memory accesses. Handling this code is on the to-do list.
- For more information, see Documentation/explanation.txt (in
- particular, the "THE PROGRAM ORDER RELATION: po AND po-loc"
- and "A WARNING" sections).
+The Linux-kernel memory model (LKMM) has the following limitations:
+
+1. Compiler optimizations are not accurately modeled. Of course,
+ the use of READ_ONCE() and WRITE_ONCE() limits the compiler's
+ ability to optimize, but under some circumstances it is possible
+ for the compiler to undermine the memory model. For more
+ information, see Documentation/explanation.txt (in particular,
+ the "THE PROGRAM ORDER RELATION: po AND po-loc" and "A WARNING"
+ sections).
Note that this limitation in turn limits LKMM's ability to
accurately model address, control, and data dependencies.
--
2.17.1
This commit simplifies life a bit by making all of the scripts in
tools/memory-model/scripts be executable.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/checkghlitmus.sh | 0
tools/memory-model/scripts/checklitmushist.sh | 0
tools/memory-model/scripts/cmplitmushist.sh | 0
tools/memory-model/scripts/initlitmushist.sh | 0
tools/memory-model/scripts/judgelitmus.sh | 0
tools/memory-model/scripts/newlitmushist.sh | 0
tools/memory-model/scripts/parseargs.sh | 0
tools/memory-model/scripts/runlitmushist.sh | 0
8 files changed, 0 insertions(+), 0 deletions(-)
mode change 100644 => 100755 tools/memory-model/scripts/checkghlitmus.sh
mode change 100644 => 100755 tools/memory-model/scripts/checklitmushist.sh
mode change 100644 => 100755 tools/memory-model/scripts/cmplitmushist.sh
mode change 100644 => 100755 tools/memory-model/scripts/initlitmushist.sh
mode change 100644 => 100755 tools/memory-model/scripts/judgelitmus.sh
mode change 100644 => 100755 tools/memory-model/scripts/newlitmushist.sh
mode change 100644 => 100755 tools/memory-model/scripts/parseargs.sh
mode change 100644 => 100755 tools/memory-model/scripts/runlitmushist.sh
diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/checklitmushist.sh b/tools/memory-model/scripts/checklitmushist.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/initlitmushist.sh b/tools/memory-model/scripts/initlitmushist.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
old mode 100644
new mode 100755
diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh
old mode 100644
new mode 100755
--
2.17.1
Adding the -v flag to jingle7 invocations gives much useful information
on why jingle7 didn't like a given litmus test. This commit therefore
adds this flag and saves off any such information into a .err file.
Suggested-by: Luc Maranget <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/runlitmus.sh | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 5f2d29b460ff..dfdb1f00fcc0 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -68,10 +68,11 @@ fi
# Generate the assembly code and run herd7 on it.
gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
-jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
+jingle7 -v -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
if grep -q "Generated 0 tests" $T/$hwlitmusfile.jingle7.out
then
- echo ' !!! ' jingle7 failed, no $hwlitmus generated
+ echo ' !!! ' jingle7 failed, errors in $hwlitmus.err
+ cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err
exit 253
fi
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
--
2.17.1
Currently, the scripts specify the CPU's .cat file to herd. But this is
pointless because herd will select a good and sufficient .cat file from
the assembly-language litmus test itself. This commit therefore removes
the -model argument to herd, allowing herd to figure the CPU family out
itself.
Note that the user can override herd's choice using the "--herdopts"
argument to the scripts.
Suggested-by: Luc Maranget <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/runlitmus.sh | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 62b47c7e1ba9..afb196d7ef10 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -53,7 +53,6 @@ trap 'rm -rf $T' 0 2
mkdir $T
# Generate filenames
-catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
themefile="$T/${LKMM_HW_MAP_FILE}.theme"
herdoptions="-model $LKMM_HW_CAT_FILE"
@@ -70,6 +69,6 @@ fi
# Generate the assembly code and run herd7 on it.
gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out
-/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
exit $?
--
2.17.1
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 <[email protected]>
---
tools/memory-model/scripts/checkalllitmus.sh | 23 +++++------
tools/memory-model/scripts/checklitmus.sh | 42 ++++++++++++++++++--
2 files changed, 49 insertions(+), 16 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
diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh
index 638b8c610894..42ff11869cd6 100755
--- a/tools/memory-model/scripts/checklitmus.sh
+++ b/tools/memory-model/scripts/checklitmus.sh
@@ -6,6 +6,11 @@
# 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:
# checklitmus.sh file.litmus
#
@@ -18,8 +23,6 @@
# Author: Paul E. McKenney <[email protected]>
litmus=$1
-herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
-
if test -f "$litmus" -a -r "$litmus"
then
:
@@ -28,7 +31,38 @@ else
exit 255
fi
-echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
-/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+if test -z "$LKMM_HW_MAP_FILE"
+then
+ # LKMM run
+ herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
+ echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
+ /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+else
+ # Hardware run
+
+ T=/tmp/checklitmushw.sh.$$
+ trap 'rm -rf $T' 0 2
+ mkdir $T
+
+ # Generate filenames
+ catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
+ mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
+ themefile="$T/${LKMM_HW_MAP_FILE}.theme"
+ herdoptions="-model $LKMM_HW_CAT_FILE"
+ hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
+ hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
+
+ # Don't run on litmus tests with complex synchronization
+ if ! scripts/simpletest.sh $litmus
+ then
+ echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
+ exit 254
+ fi
+
+ # Generate the assembly code and run herd7 on it.
+ gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
+ jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out
+ /usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+fi
scripts/judgelitmus.sh $litmus
--
2.17.1
Currently, parseargs.sh expects to consume all the command-line arguments,
which prevents the calling script from having any of its own arguments.
This commit therefore causes parseargs.sh to stop consuming arguments
when it encounters a "--" argument, leaving any remaining arguments for
the calling script.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/parseargs.sh | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
index 25a81ac0dfdf..7aa58755adfc 100755
--- a/tools/memory-model/scripts/parseargs.sh
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -83,7 +83,7 @@ do
echo "Cannot create directory --destdir '$LKMM_DESTDIR'"
usage
fi
- if test -d "$LKMM_DESTDIR" -a -w "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR"
+ if test -d "$LKMM_DESTDIR" -a -x "$LKMM_DESTDIR"
then
:
else
@@ -127,6 +127,10 @@ do
LKMM_TIMEOUT="$2"
shift
;;
+ --)
+ shift
+ break
+ ;;
*)
echo Unknown argument $1
usage
--
2.17.1
The parseargs.sh regular expression for the --jobs argument incorrectly
requires that the number of jobs be at least 10, that is, have at least
two digits. This commit therefore adjusts this regular expression to
allow single-digit numbers of jobs to be specified.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/parseargs.sh | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
index 5f016fc3f3af..25a81ac0dfdf 100755
--- a/tools/memory-model/scripts/parseargs.sh
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -113,7 +113,7 @@ do
LKMM_JOBS="`echo $njobs | sed -e 's/^\([0-9]\+\).*$/\1/'`"
;;
--jobs|--job|-j)
- checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]\+$' '^--'
+ checkarg --jobs "(number)" "$#" "$2" '^[1-9][0-9]*$' '^--'
LKMM_JOBS="$2"
shift
;;
--
2.17.1
This commit adds a checktheselitmus.sh script that runs the litmus tests
specified on the command line. This is useful for verifying fixes to
specific litmus tests.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/README | 8 ++++
.../memory-model/scripts/checktheselitmus.sh | 43 +++++++++++++++++++
2 files changed, 51 insertions(+)
create mode 100755 tools/memory-model/scripts/checktheselitmus.sh
diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README
index 0e29a52044c1..cc2c4e5be9ec 100644
--- a/tools/memory-model/scripts/README
+++ b/tools/memory-model/scripts/README
@@ -27,6 +27,14 @@ checklitmushist.sh
checklitmus.sh
Check a single litmus test against its "Result:" expected result.
+ Not intended to for manual use.
+
+checktheselitmus.sh
+
+ Check the specified list of litmus tests against their "Result:"
+ expected results. This takes optional parseargs.sh arguments,
+ followed by "--" followed by pathnames starting from the current
+ directory.
cmplitmushist.sh
diff --git a/tools/memory-model/scripts/checktheselitmus.sh b/tools/memory-model/scripts/checktheselitmus.sh
new file mode 100755
index 000000000000..10eeb5ecea6d
--- /dev/null
+++ b/tools/memory-model/scripts/checktheselitmus.sh
@@ -0,0 +1,43 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Invokes checklitmus.sh on its arguments to run the specified litmus
+# test and pass judgment on the results.
+#
+# Usage:
+# checktheselitmus.sh -- [ file1.litmus [ file2.litmus ... ] ]
+#
+# Run this in the directory containing the memory model, specifying the
+# pathname of the litmus test to check. The usual parseargs.sh arguments
+# can be specified prior to the "--".
+#
+# This script is intended for use with pathnames that start from the
+# tools/memory-model directory. If some of the pathnames instead start at
+# the root directory, they all must do so and the "--destdir /" parseargs.sh
+# argument must be specified prior to the "--". Alternatively, some other
+# "--destdir" argument can be supplied as long as the needed subdirectories
+# are populated.
+#
+# Copyright IBM Corporation, 2018
+#
+# Author: Paul E. McKenney <[email protected]>
+
+. scripts/parseargs.sh
+
+ret=0
+for i in "$@"
+do
+ if scripts/checklitmus.sh $i
+ then
+ :
+ else
+ ret=1
+ fi
+done
+if test "$ret" -ne 0
+then
+ echo " ^^^ VERIFICATION MISMATCHES" 1>&2
+else
+ echo All litmus tests verified as was expected. 1>&2
+fi
+exit $ret
--
2.17.1
In the absence of "Result:" comments, the runlitmus.sh script relies on
litmus.out files from prior LKMM runs. This can be a bit user-hostile,
so this commit makes runlitmus.sh generate any needed .litmus.out files
that don't already exist.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/runlitmus.sh | 54 ++++++++++++++-----------
1 file changed, 30 insertions(+), 24 deletions(-)
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index 91af859c0e90..2865a9661b07 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -28,42 +28,48 @@ if test -f "$litmus" -a -r "$litmus"
then
:
else
- echo ' --- ' error: \"$litmus\" is not a readable file
+ echo ' !!! ' error: \"$litmus\" is not a readable file
exit 255
fi
-if test -z "$LKMM_HW_MAP_FILE"
+if test -z "$LKMM_HW_MAP_FILE" -o ! -e $LKMM_DESTDIR/$litmus.out
then
# LKMM run
herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
echo Herd options: $herdoptions > $LKMM_DESTDIR/$litmus.out
/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
-else
- # Hardware run
+ ret=$?
+ if test -z "$LKMM_HW_MAP_FILE"
+ then
+ exit $ret
+ fi
+ echo " --- " Automatically generated LKMM output for '"'--hw $LKMM_HW_MAP_FILE'"' run
+fi
- T=/tmp/checklitmushw.sh.$$
- trap 'rm -rf $T' 0 2
- mkdir $T
+# Hardware run
- # Generate filenames
- catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
- mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
- themefile="$T/${LKMM_HW_MAP_FILE}.theme"
- herdoptions="-model $LKMM_HW_CAT_FILE"
- hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
- hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
+T=/tmp/checklitmushw.sh.$$
+trap 'rm -rf $T' 0 2
+mkdir $T
- # Don't run on litmus tests with complex synchronization
- if ! scripts/simpletest.sh $litmus
- then
- echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
- exit 254
- fi
+# Generate filenames
+catfile="`echo $LKMM_HW_MAP_FILE | tr '[A-Z]' '[a-z]'`.cat"
+mapfile="Linux2${LKMM_HW_MAP_FILE}.map"
+themefile="$T/${LKMM_HW_MAP_FILE}.theme"
+herdoptions="-model $LKMM_HW_CAT_FILE"
+hwlitmus=`echo $litmus | sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`
+hwlitmusfile=`echo $hwlitmus | sed -e 's,^.*/,,'`
- # Generate the assembly code and run herd on it.
- gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
- jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out
- /usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+# Don't run on litmus tests with complex synchronization
+if ! scripts/simpletest.sh $litmus
+then
+ echo ' --- ' error: \"$litmus\" contains locking, RCU, or SRCU
+ exit 254
fi
+# Generate the assembly code and run herd7 on it.
+gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile
+jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out
+/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1
+
exit $?
--
2.17.1
This commits enables the "--hw" argument for the checkghlitmus.sh script,
causing it to convert any applicable C-language litmus tests to the
specified flavor of assembly language, to verify these assembly-language
litmus tests, and checking compatibility of the outcomes.
Note that the conversion does not yet handle locking, RCU, SRCU, plain
C-language memory accesses, or casts.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/checkghlitmus.sh | 9 ++++---
tools/memory-model/scripts/hwfnseg.sh | 20 +++++++++++++++
tools/memory-model/scripts/runlitmushist.sh | 27 +++++++++++++--------
3 files changed, 42 insertions(+), 14 deletions(-)
create mode 100755 tools/memory-model/scripts/hwfnseg.sh
diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh
index 6589fbb6f653..2ea220d2564b 100755
--- a/tools/memory-model/scripts/checkghlitmus.sh
+++ b/tools/memory-model/scripts/checkghlitmus.sh
@@ -10,6 +10,7 @@
# parseargs.sh scripts for arguments.
. scripts/parseargs.sh
+. scripts/hwfnseg.sh
T=/tmp/checkghlitmus.sh.$$
trap 'rm -rf $T' 0
@@ -32,9 +33,9 @@ then
( cd "$LKMM_DESTDIR"; sed -e 's/^/mkdir -p /' | sh )
fi
-# Create a list of the C-language litmus tests previously run.
-( cd $LKMM_DESTDIR; find litmus -name '*.litmus.out' -print ) |
- sed -e 's/\.out$//' |
+# Create a list of the specified litmus tests previously run.
+( cd $LKMM_DESTDIR; find litmus -name "*.litmus${hwfnseg}.out" -print ) |
+ sed -e "s/${hwfnseg}"'\.out$//' |
xargs -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' |
xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already
@@ -44,7 +45,7 @@ find litmus -name '*.litmus' -exec grep -l -m 1 "^C " {} \; > $T/list-C
xargs < $T/list-C -r egrep -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' > $T/list-C-result
xargs < $T/list-C-result -r grep -L "^P${LKMM_PROCS}" > $T/list-C-result-short
-# Form list of tests without corresponding .litmus.out files
+# Form list of tests without corresponding .out files
sort $T/list-C-already $T/list-C-result-short | uniq -u > $T/list-C-needed
# Run any needed tests.
diff --git a/tools/memory-model/scripts/hwfnseg.sh b/tools/memory-model/scripts/hwfnseg.sh
new file mode 100755
index 000000000000..580c3281181c
--- /dev/null
+++ b/tools/memory-model/scripts/hwfnseg.sh
@@ -0,0 +1,20 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Generate the hardware extension to the litmus-test filename, or the
+# empty string if this is an LKMM run. The extension is placed in
+# the shell variable hwfnseg.
+#
+# Usage:
+# . hwfnseg.sh
+#
+# Copyright IBM Corporation, 2019
+#
+# Author: Paul E. McKenney <[email protected]>
+
+if test -z "$LKMM_HW_MAP_FILE"
+then
+ hwfnseg=
+else
+ hwfnseg=".$LKMM_HW_MAP_FILE"
+fi
diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh
index 852786fef179..c6c2bdc67a50 100755
--- a/tools/memory-model/scripts/runlitmushist.sh
+++ b/tools/memory-model/scripts/runlitmushist.sh
@@ -15,6 +15,8 @@
#
# Author: Paul E. McKenney <[email protected]>
+. scripts/hwfnseg.sh
+
T=/tmp/runlitmushist.sh.$$
trap 'rm -rf $T' 0
mkdir $T
@@ -30,15 +32,12 @@ fi
# Prefixes for per-CPU scripts
for ((i=0;i<$LKMM_JOBS;i++))
do
- echo dir="$LKMM_DESTDIR" > $T/$i.sh
echo T=$T >> $T/$i.sh
- echo herdoptions=\"$LKMM_HERD_OPTIONS\" >> $T/$i.sh
cat << '___EOF___' >> $T/$i.sh
runtest () {
- echo ' ... ' /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 '>' $dir/$1.out '2>&1'
- if /usr/bin/time $LKMM_TIMEOUT_CMD herd7 $herdoptions $1 > $dir/$1.out 2>&1
+ if scripts/runlitmus.sh $1
then
- if ! grep -q '^Observation ' $dir/$1.out
+ if ! grep -q '^Observation ' $LKMM_DESTDIR/$1$2.out
then
echo ' !!! Herd failed, no Observation:' $1
fi
@@ -47,10 +46,16 @@ do
if test "$exitcode" -eq 124
then
exitmsg="timed out"
+ elif test "$exitcode" -eq 253
+ then
+ exitmsg=
else
exitmsg="failed, exit code $exitcode"
fi
- echo ' !!! Herd' ${exitmsg}: $1
+ if test -n "$exitmsg"
+ then
+ echo ' !!! Herd' ${exitmsg}: $1
+ fi
fi
}
___EOF___
@@ -59,11 +64,13 @@ done
awk -v q="'" -v b='\\' '
{
print "echo `grep " q "^P[0-9]" b "+(" q " " $0 " | tail -1 | sed -e " q "s/^P" b "([0-9]" b "+" b ")(.*$/" b "1/" q "` " $0
-}' | bash |
-sort -k1n |
-awk -v ncpu=$LKMM_JOBS -v t=$T '
+}' | sh | sort -k1n |
+awk -v dq='"' -v hwfnseg="$hwfnseg" -v ncpu="$LKMM_JOBS" -v t="$T" '
{
- print "runtest " $2 >> t "/" NR % ncpu ".sh";
+ print "if test -z " dq hwfnseg dq " || scripts/simpletest.sh " dq $2 dq
+ print "then"
+ print "\techo runtest " dq $2 dq " " hwfnseg " >> " t "/" NR % ncpu ".sh";
+ print "fi"
}
END {
--
2.17.1
Hi Paul,
(CC: using Andrea's gmail address, adding Daniel)
Sorry for slow response, but please find inline comments below.
On Thu, 1 Aug 2019 15:20:52 -0700, Paul E. McKenney wrote:
> This commit adds functionality to judgelitmus.sh to allow it to handle
> both the "DATARACE" markers in the "Result:" comments in litmus tests
> and the "Flag data-race" markers in LKMM output. For C-language tests,
> if either marker is present, the other must also be as well, at least for
> litmus tests having a "Result:" comment. If the LKMM output indicates
> a data race, then failures of the Always/Sometimes/Never portion of the
> "Result:" prediction are forgiven.
I'd like to see the reason _why_ they can be forgiven. Also, updating
the header comment of judgelitimus.sh to mention these expansions would
be of much help.
My guess is any data-race would moot the Always/Sometimes/Never
prediction.
This reminds me that update of LKMM documentation regarding plain
accesses (data races) is yet to come.
Thanks, Akira
>
> Signed-off-by: Paul E. McKenney <[email protected]>
> ---
> tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++++++++-
> 1 file changed, 19 insertions(+), 1 deletion(-)
>
> diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
> index ca9a19829d79..eaa2cc7d3b36 100755
> --- a/tools/memory-model/scripts/judgelitmus.sh
> +++ b/tools/memory-model/scripts/judgelitmus.sh
> @@ -47,9 +47,27 @@ else
> echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file
> exit 255
> fi
> +if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout"
> +then
> + datarace_modeled=1
> +fi
> if grep -q '^ \* Result: ' $litmus
> then
> outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
> + if grep -m1 '^ \* Result: .* DATARACE' $litmus
> + then
> + datarace_predicted=1
> + fi
> + if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE"
> + then
> + echo '!!! Predicted data race not modeled' $litmus
> + exit 252
> + elif test -z "$datarace_predicted" -a -n "$datarace_modeled"
> + then
> + # Note that hardware models currently don't model data races
> + echo '!!! Unexpected data race modeled' $litmus
> + exit 253
> + fi
> elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1
> then
> outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'`
> @@ -114,7 +132,7 @@ elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$o
> then
> ret=0
> else
> - if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes
> + if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled"
> then
> flag="--- Forgiven"
> ret=0
>
On Mon, Aug 12, 2019 at 11:32:35PM +0900, Akira Yokosawa wrote:
> Hi Paul,
> (CC: using Andrea's gmail address, adding Daniel)
Good point, I did forget to update at my end. Fixed, thank you!
> Sorry for slow response, but please find inline comments below.
>
> On Thu, 1 Aug 2019 15:20:52 -0700, Paul E. McKenney wrote:
> > This commit adds functionality to judgelitmus.sh to allow it to handle
> > both the "DATARACE" markers in the "Result:" comments in litmus tests
> > and the "Flag data-race" markers in LKMM output. For C-language tests,
> > if either marker is present, the other must also be as well, at least for
> > litmus tests having a "Result:" comment. If the LKMM output indicates
> > a data race, then failures of the Always/Sometimes/Never portion of the
> > "Result:" prediction are forgiven.
>
> I'd like to see the reason _why_ they can be forgiven. Also, updating
> the header comment of judgelitimus.sh to mention these expansions would
> be of much help.
>
> My guess is any data-race would moot the Always/Sometimes/Never
> prediction.
Exactly. And good point, I will update the commit log to make this
explicit.
> This reminds me that update of LKMM documentation regarding plain
> accesses (data races) is yet to come.
Yes, this one is still on the to-do list. Timely reminder, though! ;-)
Thanx, Paul
> Thanks, Akira
>
> >
> > Signed-off-by: Paul E. McKenney <[email protected]>
> > ---
> > tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++++++++-
> > 1 file changed, 19 insertions(+), 1 deletion(-)
> >
> > diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
> > index ca9a19829d79..eaa2cc7d3b36 100755
> > --- a/tools/memory-model/scripts/judgelitmus.sh
> > +++ b/tools/memory-model/scripts/judgelitmus.sh
> > @@ -47,9 +47,27 @@ else
> > echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file
> > exit 255
> > fi
> > +if grep -q '^Flag data-race$' "$LKMM_DESTDIR/$litmusout"
> > +then
> > + datarace_modeled=1
> > +fi
> > if grep -q '^ \* Result: ' $litmus
> > then
> > outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
> > + if grep -m1 '^ \* Result: .* DATARACE' $litmus
> > + then
> > + datarace_predicted=1
> > + fi
> > + if test -n "$datarace_predicted" -a -z "$datarace_modeled" -a -z "$LKMM_HW_MAP_FILE"
> > + then
> > + echo '!!! Predicted data race not modeled' $litmus
> > + exit 252
> > + elif test -z "$datarace_predicted" -a -n "$datarace_modeled"
> > + then
> > + # Note that hardware models currently don't model data races
> > + echo '!!! Unexpected data race modeled' $litmus
> > + exit 253
> > + fi
> > elif test -n "$LKMM_HW_MAP_FILE" && grep -q '^Observation' $LKMM_DESTDIR/$lkmmout > /dev/null 2>&1
> > then
> > outcome=`grep -m 1 '^Observation ' $LKMM_DESTDIR/$lkmmout | awk '{ print $3 }'`
> > @@ -114,7 +132,7 @@ elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$o
> > then
> > ret=0
> > else
> > - if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes
> > + if test \( -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes \) -o -n "$datarace_modeled"
> > then
> > flag="--- Forgiven"
> > ret=0
> >
>
Hi Paul,
I see some inconsistency between the header comment of judgelitmus.sh
and the updated script.
This patch set updates the header. It is relative to current lkmm-dev
of -rcu.
Patch 1/2 corresponds to ("tools/memory-model: Move from
.AArch64.litmus.out to .litmus.AArch.out").
Patch 2/2 corresponds to ("tools/memory-model: Add data-race
capabilities to judgelitmus.sh").
You should be able to use each patch as a fix-up commit respectively.
I'm OK either with them applied at the head of the branch or
with them merged into your commits.
Thanks, Akira
--
Akira Yokosawa (2):
tools/memory-model: Reflect updated file name convention in
judgelitmus.sh
tools/memory-model: Mention data-race capability in jugdelitmus.sh's
header
tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++-------
1 file changed, 13 insertions(+), 7 deletions(-)
--
2.17.1
From 6251ebb775a81f1ac158f197ad8110b8f98c4248 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <[email protected]>
Date: Wed, 14 Aug 2019 17:20:54 +0900
Subject: [PATCH 1/2] tools/memory-model: Reflect updated file name convention in judgelitmus.sh
Commit ("tools/memory-model: Move from .AArch64.litmus.out to
.litmus.AArch.out") swapped "HW" and "litmus" part in .out file name.
Reflect the change in header comment in judgelitmus.sh
Signed-off-by: Akira Yokosawa <[email protected]>
---
tools/memory-model/scripts/judgelitmus.sh | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index 6408c012bdf5..c91130814593 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -6,7 +6,7 @@
# test ran correctly. If the --hw argument is omitted, check against the
# LKMM output, which is assumed to be in file.litmus.out. If this argument
# is provided, this is assumed to be a hardware test, and the output is
-# assumed to be in file.HW.litmus.out, where "HW" is the --hw argument.
+# assumed to be in file.litmus.HW.out, where "HW" is the --hw argument.
# In addition, non-Sometimes verification results will be noted, but
# forgiven. Furthermore, if there is no "Result:" comment but there is
# an LKMM .litmus.out file, the observation in that file will be used
--
2.17.1
From 67092cb93f7a0fd3c4f9a300637e4f5c61fc944a Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <[email protected]>
Date: Wed, 14 Aug 2019 17:48:25 +0900
Subject: [PATCH 2/2] tools/memory-model: Mention data-race capability in jugdelitmus.sh's header
Replicate description of data-race capability from the change log of
commit ("tools/memory-model: Add data-race capabilities to
judgelitmus.sh") in the header comment.
Signed-off-by: Akira Yokosawa <[email protected]>
---
tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++-------
1 file changed, 13 insertions(+), 7 deletions(-)
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index c91130814593..1ec5d89fcfbb 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -4,13 +4,19 @@
# Given a .litmus test and the corresponding litmus output file, check
# the .litmus.out file against the "Result:" comment to judge whether the
# test ran correctly. If the --hw argument is omitted, check against the
-# LKMM output, which is assumed to be in file.litmus.out. If this argument
-# is provided, this is assumed to be a hardware test, and the output is
-# assumed to be in file.litmus.HW.out, where "HW" is the --hw argument.
-# In addition, non-Sometimes verification results will be noted, but
-# forgiven. Furthermore, if there is no "Result:" comment but there is
-# an LKMM .litmus.out file, the observation in that file will be used
-# to judge the assembly-language verification.
+# LKMM output, which is assumed to be in file.litmus.out. If either a
+# "DATARACE" marker in the "Result:" comment or a "Flag data-race" marker
+# in the LKMM output is present, the other must also be as well, at least
+# for litmus tests having a "Result:" comment. In this case, a failure of
+# the Always/Sometimes/Never portion of the "Result:" prediction will be
+# noted, but forgiven.
+#
+# If the --hw argument is provided, this is assumed to be a hardware
+# test, and the output is assumed to be in file.litmus.HW.out, where
+# "HW" is the --hw argument. In addition, non-Sometimes verification
+# results will be noted, but forgiven. Furthermore, if there is no
+# "Result:" comment but there is an LKMM .litmus.out file, the observation
+# in that file will be used to judge the assembly-language verification.
#
# Usage:
# judgelitmus.sh file.litmus
--
2.17.1
On Thu, Aug 15, 2019 at 12:11:36AM +0900, Akira Yokosawa wrote:
> Hi Paul,
>
> I see some inconsistency between the header comment of judgelitmus.sh
> and the updated script.
>
> This patch set updates the header. It is relative to current lkmm-dev
> of -rcu.
>
> Patch 1/2 corresponds to ("tools/memory-model: Move from
> .AArch64.litmus.out to .litmus.AArch.out").
>
> Patch 2/2 corresponds to ("tools/memory-model: Add data-race
> capabilities to judgelitmus.sh").
>
> You should be able to use each patch as a fix-up commit respectively.
> I'm OK either with them applied at the head of the branch or
> with them merged into your commits.
Good catches, thank you for looking these commits over! I will squash
your changes into the original commits with attribution.
Thanx, Paul
> Thanks, Akira
> --
> Akira Yokosawa (2):
> tools/memory-model: Reflect updated file name convention in
> judgelitmus.sh
> tools/memory-model: Mention data-race capability in jugdelitmus.sh's
> header
>
> tools/memory-model/scripts/judgelitmus.sh | 20 +++++++++++++-------
> 1 file changed, 13 insertions(+), 7 deletions(-)
>
> --
> 2.17.1
>
>