Hello!
This series provides scripting updates that ease validating
the effects of changes to LKMM:
1. tools/memory-model: Document locking corner cases.
2. tools/memory-model: Make judgelitmus.sh note timeouts.
3. tools/memory-model: Make cmplitmushist.sh note timeouts.
4. tools/memory-model: Make judgelitmus.sh identify bad macros.
5. tools/memory-model: Make judgelitmus.sh detect hard deadlocks.
6. tools/memory-model: Fix paulmck email address on pre-existing
scripts.
7. tools/memory-model: Update parseargs.sh for hardware verification.
8. tools/memory-model: Make judgelitmus.sh handle hardware
verifications.
9. tools/memory-model: Add simpletest.sh to check locking, RCU,
and SRCU.
10. tools/memory-model: Fix checkalllitmus.sh comment.
11. tools/memory-model: Hardware checking for check{,all}litmus.sh.
12. tools/memory-model: Make judgelitmus.sh ransack .litmus.out files.
13. tools/memory-model: Split runlitmus.sh out of checklitmus.sh.
14. tools/memory-model: Make runlitmus.sh generate .litmus.out
for --hw.
15. tools/memory-model: Move from .AArch64.litmus.out to
.litmus.AArch.out.
16. tools/memory-model: Keep assembly-language litmus tests.
17. tools/memory-model: Allow herd to deduce CPU type.
18. tools/memory-model: Make runlitmus.sh check for jingle errors.
19. tools/memory-model: Add -v flag to jingle7 runs.
20. tools/memory-model: Implement --hw support for checkghlitmus.sh.
21. tools/memory-model: Fix scripting --jobs argument.
22. tools/memory-model: Make checkghlitmus.sh use mselect7.
23. tools/memory-model: Make history-check scripts use mselect7.
24. tools/memory-model: Add "--" to parseargs.sh for additional
arguments.
25. tools/memory-model: Repair parseargs.sh header comment.
26. tools/memory-model: Add checktheselitmus.sh to run specified
litmus tests.
27. tools/memory-model: Add data-race capabilities to judgelitmus.sh.
28. tools/memory-model: Make judgelitmus.sh handle scripted Result:
tag.
29. tools/memory-model: Use "-unroll 0" to keep --hw runs finite.
30. tools/memory-model: Use "grep -E" instead of "egrep", courtesy
of Tiezhu Yang.
31. tools/memory-model: Document LKMM test procedure.
Thanx, Paul
------------------------------------------------------------------------
b/Documentation/litmus-tests/locking/DCL-broken.litmus | 55 ++
b/Documentation/litmus-tests/locking/DCL-fixed.litmus | 56 ++
b/Documentation/litmus-tests/locking/RM-broken.litmus | 42 ++
b/Documentation/litmus-tests/locking/RM-fixed.litmus | 42 ++
b/tools/memory-model/Documentation/locking.txt | 320 +++++++++++++++++
b/tools/memory-model/litmus-tests/.gitignore | 2
b/tools/memory-model/scripts/README | 8
b/tools/memory-model/scripts/checkalllitmus.sh | 2
b/tools/memory-model/scripts/checkghlitmus.sh | 9
b/tools/memory-model/scripts/checklitmus.sh | 2
b/tools/memory-model/scripts/checklitmushist.sh | 2
b/tools/memory-model/scripts/checktheselitmus.sh | 43 ++
b/tools/memory-model/scripts/cmplitmushist.sh | 22 +
b/tools/memory-model/scripts/hwfnseg.sh | 20 +
b/tools/memory-model/scripts/initlitmushist.sh | 2
b/tools/memory-model/scripts/judgelitmus.sh | 8
b/tools/memory-model/scripts/newlitmushist.sh | 2
b/tools/memory-model/scripts/parseargs.sh | 2
b/tools/memory-model/scripts/runlitmus.sh | 69 +++
b/tools/memory-model/scripts/runlitmushist.sh | 2
b/tools/memory-model/scripts/simpletest.sh | 35 +
tools/memory-model/litmus-tests/.gitignore | 2
tools/memory-model/scripts/README | 40 ++
tools/memory-model/scripts/checkalllitmus.sh | 27 -
tools/memory-model/scripts/checkghlitmus.sh | 6
tools/memory-model/scripts/checklitmus.sh | 99 ++---
tools/memory-model/scripts/cmplitmushist.sh | 31 +
tools/memory-model/scripts/judgelitmus.sh | 156 ++++++--
tools/memory-model/scripts/newlitmushist.sh | 2
tools/memory-model/scripts/parseargs.sh | 19 -
tools/memory-model/scripts/runlitmus.sh | 75 ++-
tools/memory-model/scripts/runlitmushist.sh | 27 -
32 files changed, 1044 insertions(+), 185 deletions(-)
Currently, judgelitmus.sh treats timeouts (as in the "--timeout" argument)
as "!!! Verification error". This can be misleading because it is quite
possible that running the test longer would have produced a verification.
This commit therefore changes judgelitmus.sh to check for timeouts and
to report them with "!!! Timeout".
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/judgelitmus.sh | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index 0cc63875e395..d3c313b9a458 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -42,6 +42,14 @@ grep '^Observation' $LKMM_DESTDIR/$litmus.out
if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
then
:
+elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out
+then
+ echo ' !!! Timeout' $litmus
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ then
+ echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmus.out 2>&1
+ fi
+ exit 124
else
echo ' !!! Verification error' $litmus
if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
--
2.40.0.rc2
If a litmus test specifies "Result: Never" and if it contains an
unconditional ("hard") deadlock, then running checklitmus.sh on it will
not flag any errors, despite the fact that there are no executions.
This commit therefore updates judgelitmus.sh to complain about tests
with no executions that are marked, but not as "Result: DEADLOCK".
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/judgelitmus.sh | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index d40439c7b71e..84c62eee321b 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -83,6 +83,14 @@ then
fi
ret=1
fi
+elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
+then
+ echo " !!! Unexpected non-$outcome deadlock" $litmus
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ then
+ echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+ fi
+ ret=1
elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
then
ret=0
--
2.40.0.rc2
Currently, judgelitmus.sh treats use of unknown primitives (such as
srcu_read_lock() prior to SRCU support) as "!!! Verification error".
This can be misleading because it fails to call out typos and running
a version LKMM on a litmus test requiring a feature not provided by
that version. This commit therefore changes judgelitmus.sh to check
for unknown primitives and to report them, for example, with:
'!!! Current LKMM version does not know "rcu_write_lock"'.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/cmplitmushist.sh | 31 ++++++++++++++++++---
tools/memory-model/scripts/judgelitmus.sh | 12 ++++++++
2 files changed, 39 insertions(+), 4 deletions(-)
diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh
index b9c174dd8004..ca1ac8b64614 100755
--- a/tools/memory-model/scripts/cmplitmushist.sh
+++ b/tools/memory-model/scripts/cmplitmushist.sh
@@ -12,6 +12,7 @@ trap 'rm -rf $T' 0
mkdir $T
# comparetest oldpath newpath
+badmacnam=0
timedout=0
perfect=0
obsline=0
@@ -19,8 +20,26 @@ noobsline=0
obsresult=0
badcompare=0
comparetest () {
- if grep -q '^Command exited with non-zero status 124' $1 ||
- grep -q '^Command exited with non-zero status 124' $2
+ if grep -q ': Unknown macro ' $1 || grep -q ': Unknown macro ' $2
+ then
+ if grep -q ': Unknown macro ' $1
+ then
+ badname=`grep ': Unknown macro ' $1 |
+ sed -e 's/^.*: Unknown macro //' |
+ sed -e 's/ (User error).*$//'`
+ echo 'Current LKMM version does not know "'$badname'"' $1
+ fi
+ if grep -q ': Unknown macro ' $2
+ then
+ badname=`grep ': Unknown macro ' $2 |
+ sed -e 's/^.*: Unknown macro //' |
+ sed -e 's/ (User error).*$//'`
+ echo 'Current LKMM version does not know "'$badname'"' $2
+ fi
+ badmacnam=`expr "$badmacnam" + 1`
+ return 0
+ elif grep -q '^Command exited with non-zero status 124' $1 ||
+ grep -q '^Command exited with non-zero status 124' $2
then
if grep -q '^Command exited with non-zero status 124' $1 &&
grep -q '^Command exited with non-zero status 124' $2
@@ -56,7 +75,7 @@ comparetest () {
return 0
fi
else
- echo Missing Observation line "(e.g., herd7 timeout)": $2
+ echo Missing Observation line "(e.g., syntax error)": $2
noobsline=`expr "$noobsline" + 1`
return 0
fi
@@ -90,7 +109,7 @@ then
fi
if test "$noobsline" -ne 0
then
- echo Missing Observation line "(e.g., herd7 timeout)": $noobsline 1>&2
+ echo Missing Observation line "(e.g., syntax error)": $noobsline 1>&2
fi
if test "$obsresult" -ne 0
then
@@ -100,6 +119,10 @@ if test "$timedout" -ne 0
then
echo "!!!" Timed out: $timedout 1>&2
fi
+if test "$badmacnam" -ne 0
+then
+ echo "!!!" Unknown primitive: $badmacnam 1>&2
+fi
if test "$badcompare" -ne 0
then
echo "!!!" Result changed: $badcompare 1>&2
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index d3c313b9a458..d40439c7b71e 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -42,6 +42,18 @@ grep '^Observation' $LKMM_DESTDIR/$litmus.out
if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
then
:
+elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out
+then
+ badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out |
+ sed -e 's/^.*: Unknown macro //' |
+ sed -e 's/ (User error).*$//'`
+ badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus"
+ echo $badmsg
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ then
+ echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmus.out 2>&1
+ fi
+ exit 254
elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out
then
echo ' !!! Timeout' $litmus
--
2.40.0.rc2
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/checkalllitmus.sh | 2 +-
tools/memory-model/scripts/checklitmus.sh | 2 +-
tools/memory-model/scripts/checklitmushist.sh | 2 +-
tools/memory-model/scripts/judgelitmus.sh | 2 +-
tools/memory-model/scripts/newlitmushist.sh | 2 +-
tools/memory-model/scripts/parseargs.sh | 2 +-
tools/memory-model/scripts/runlitmushist.sh | 2 +-
7 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh
index 3c0c7fbbd223..10e14d94acee 100755
--- a/tools/memory-model/scripts/checkalllitmus.sh
+++ b/tools/memory-model/scripts/checkalllitmus.sh
@@ -17,7 +17,7 @@
#
# Copyright IBM Corporation, 2018
#
-# Author: Paul E. McKenney <[email protected]>
+# Author: Paul E. McKenney <[email protected]>
. scripts/parseargs.sh
diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh
index 11461ed40b5e..638b8c610894 100755
--- a/tools/memory-model/scripts/checklitmus.sh
+++ b/tools/memory-model/scripts/checklitmus.sh
@@ -15,7 +15,7 @@
#
# Copyright IBM Corporation, 2018
#
-# Author: Paul E. McKenney <[email protected]>
+# Author: Paul E. McKenney <[email protected]>
litmus=$1
herdoptions=${LKMM_HERD_OPTIONS--conf linux-kernel.cfg}
diff --git a/tools/memory-model/scripts/checklitmushist.sh b/tools/memory-model/scripts/checklitmushist.sh
index 1d210ffb7c8a..406ecfc0aee4 100755
--- a/tools/memory-model/scripts/checklitmushist.sh
+++ b/tools/memory-model/scripts/checklitmushist.sh
@@ -12,7 +12,7 @@
#
# Copyright IBM Corporation, 2018
#
-# Author: Paul E. McKenney <[email protected]>
+# Author: Paul E. McKenney <[email protected]>
. scripts/parseargs.sh
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index 84c62eee321b..d82133e75580 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -13,7 +13,7 @@
#
# Copyright IBM Corporation, 2018
#
-# Author: Paul E. McKenney <[email protected]>
+# Author: Paul E. McKenney <[email protected]>
litmus=$1
diff --git a/tools/memory-model/scripts/newlitmushist.sh b/tools/memory-model/scripts/newlitmushist.sh
index 991f8f814881..3f4b06e29988 100755
--- a/tools/memory-model/scripts/newlitmushist.sh
+++ b/tools/memory-model/scripts/newlitmushist.sh
@@ -12,7 +12,7 @@
#
# Copyright IBM Corporation, 2018
#
-# Author: Paul E. McKenney <[email protected]>
+# Author: Paul E. McKenney <[email protected]>
. scripts/parseargs.sh
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
index 40f52080fdbd..afe7bd23de6b 100755
--- a/tools/memory-model/scripts/parseargs.sh
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -9,7 +9,7 @@
#
# Copyright IBM Corporation, 2018
#
-# Author: Paul E. McKenney <[email protected]>
+# Author: Paul E. McKenney <[email protected]>
T=/tmp/parseargs.sh.$$
mkdir $T
diff --git a/tools/memory-model/scripts/runlitmushist.sh b/tools/memory-model/scripts/runlitmushist.sh
index 6ed376f495bb..852786fef179 100755
--- a/tools/memory-model/scripts/runlitmushist.sh
+++ b/tools/memory-model/scripts/runlitmushist.sh
@@ -13,7 +13,7 @@
#
# Copyright IBM Corporation, 2018
#
-# Author: Paul E. McKenney <[email protected]>
+# Author: Paul E. McKenney <[email protected]>
T=/tmp/runlitmushist.sh.$$
trap 'rm -rf $T' 0
--
2.40.0.rc2
Litmus tests involving atomic operations produce LL/SC loops on a number
of architectures, and unrolling these loops can result in excessive
verification times or even stack overflows. This commit therefore uses
the "-unroll 0" herd7 argument to avoid unrolling, on the grounds that
additional passes through an LL/SC loop should not change the verification.
Note however, that certain bugs in the mapping of the LL/SC loop to
machine instructions may go undetected. On the other hand, herd7 might
not be the best vehicle for finding such bugs in any case. (You do
stress-test your architecture-specific code, don't you?)
Suggested-by: Luc Maranget <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/runlitmus.sh | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index dfdb1f00fcc0..94608d4b6502 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -75,6 +75,6 @@ then
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
+/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -unroll 0 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1
exit $?
--
2.40.0.rc2
This commit adds a --hw argument to parseargs.sh to specify the CPU
family for a hardware verification. For example, "--hw AArch64" will
specify that a C-language litmus test is to be translated to ARMv8 and
the result verified. This will set the LKMM_HW_MAP_FILE environment
variable accordingly. If there is no --hw argument, this environment
variable will be set to the empty string.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/parseargs.sh | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/tools/memory-model/scripts/parseargs.sh b/tools/memory-model/scripts/parseargs.sh
index afe7bd23de6b..5f016fc3f3af 100755
--- a/tools/memory-model/scripts/parseargs.sh
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -27,6 +27,7 @@ initparam () {
initparam LKMM_DESTDIR "."
initparam LKMM_HERD_OPTIONS "-conf linux-kernel.cfg"
+initparam LKMM_HW_MAP_FILE ""
initparam LKMM_JOBS `getconf _NPROCESSORS_ONLN`
initparam LKMM_PROCS "3"
initparam LKMM_TIMEOUT "1m"
@@ -37,10 +38,11 @@ usagehelp () {
echo "Usage $scriptname [ arguments ]"
echo " --destdir path (place for .litmus.out, default by .litmus)"
echo " --herdopts -conf linux-kernel.cfg ..."
+ echo " --hw AArch64"
echo " --jobs N (number of jobs, default one per CPU)"
echo " --procs N (litmus tests with at most this many processes)"
echo " --timeout N (herd7 timeout (e.g., 10s, 1m, 2hr, 1d, '')"
- echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'"
+ echo "Defaults: --destdir '$LKMM_DESTDIR_DEF' --herdopts '$LKMM_HERD_OPTIONS_DEF' --hw '$LKMM_HW_MAP_FILE' --jobs '$LKMM_JOBS_DEF' --procs '$LKMM_PROCS_DEF' --timeout '$LKMM_TIMEOUT_DEF'"
exit 1
}
@@ -95,6 +97,11 @@ do
LKMM_HERD_OPTIONS="$2"
shift
;;
+ --hw)
+ checkarg --hw "(.map file architecture name)" "$#" "$2" '^[A-Za-z0-9_-]\+' '^--'
+ LKMM_HW_MAP_FILE="$2"
+ shift
+ ;;
-j[1-9]*)
njobs="`echo $1 | sed -e 's/^-j//'`"
trailchars="`echo $njobs | sed -e 's/[0-9]\+\(.*\)$/\1/'`"
--
2.40.0.rc2
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.40.0.rc2
Most Linux-kernel uses of locking are straightforward, but there are
corner-case uses that rely on less well-known aspects of the lock and
unlock primitives. This commit therefore adds a locking.txt and litmus
tests in Documentation/litmus-tests/locking to explain these corner-case
uses.
Signed-off-by: Paul E. McKenney <[email protected]>
---
.../litmus-tests/locking/DCL-broken.litmus | 55 +++
.../litmus-tests/locking/DCL-fixed.litmus | 56 +++
.../litmus-tests/locking/RM-broken.litmus | 42 +++
.../litmus-tests/locking/RM-fixed.litmus | 42 +++
tools/memory-model/Documentation/locking.txt | 320 ++++++++++++++++++
5 files changed, 515 insertions(+)
create mode 100644 Documentation/litmus-tests/locking/DCL-broken.litmus
create mode 100644 Documentation/litmus-tests/locking/DCL-fixed.litmus
create mode 100644 Documentation/litmus-tests/locking/RM-broken.litmus
create mode 100644 Documentation/litmus-tests/locking/RM-fixed.litmus
create mode 100644 tools/memory-model/Documentation/locking.txt
diff --git a/Documentation/litmus-tests/locking/DCL-broken.litmus b/Documentation/litmus-tests/locking/DCL-broken.litmus
new file mode 100644
index 000000000000..cfaa25ff82b1
--- /dev/null
+++ b/Documentation/litmus-tests/locking/DCL-broken.litmus
@@ -0,0 +1,55 @@
+C DCL-broken
+
+(*
+ * Result: Sometimes
+ *
+ * This litmus test demonstrates more than just locking is required to
+ * correctly implement double-checked locking.
+ *)
+
+{
+ int flag;
+ int data;
+ int lck;
+}
+
+P0(int *flag, int *data, int *lck)
+{
+ int r0;
+ int r1;
+ int r2;
+
+ r0 = READ_ONCE(*flag);
+ if (r0 == 0) {
+ spin_lock(lck);
+ r1 = READ_ONCE(*flag);
+ if (r1 == 0) {
+ WRITE_ONCE(*data, 1);
+ WRITE_ONCE(*flag, 1);
+ }
+ spin_unlock(lck);
+ }
+ r2 = READ_ONCE(*data);
+}
+
+P1(int *flag, int *data, int *lck)
+{
+ int r0;
+ int r1;
+ int r2;
+
+ r0 = READ_ONCE(*flag);
+ if (r0 == 0) {
+ spin_lock(lck);
+ r1 = READ_ONCE(*flag);
+ if (r1 == 0) {
+ WRITE_ONCE(*data, 1);
+ WRITE_ONCE(*flag, 1);
+ }
+ spin_unlock(lck);
+ }
+ r2 = READ_ONCE(*data);
+}
+
+locations [flag;data;lck;0:r0;0:r1;1:r0;1:r1]
+exists (0:r2=0 \/ 1:r2=0)
diff --git a/Documentation/litmus-tests/locking/DCL-fixed.litmus b/Documentation/litmus-tests/locking/DCL-fixed.litmus
new file mode 100644
index 000000000000..579d6c246f16
--- /dev/null
+++ b/Documentation/litmus-tests/locking/DCL-fixed.litmus
@@ -0,0 +1,56 @@
+C DCL-fixed
+
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that double-checked locking can be
+ * reliable given proper use of smp_load_acquire() and smp_store_release()
+ * in addition to the locking.
+ *)
+
+{
+ int flag;
+ int data;
+ int lck;
+}
+
+P0(int *flag, int *data, int *lck)
+{
+ int r0;
+ int r1;
+ int r2;
+
+ r0 = smp_load_acquire(flag);
+ if (r0 == 0) {
+ spin_lock(lck);
+ r1 = READ_ONCE(*flag);
+ if (r1 == 0) {
+ WRITE_ONCE(*data, 1);
+ smp_store_release(flag, 1);
+ }
+ spin_unlock(lck);
+ }
+ r2 = READ_ONCE(*data);
+}
+
+P1(int *flag, int *data, int *lck)
+{
+ int r0;
+ int r1;
+ int r2;
+
+ r0 = smp_load_acquire(flag);
+ if (r0 == 0) {
+ spin_lock(lck);
+ r1 = READ_ONCE(*flag);
+ if (r1 == 0) {
+ WRITE_ONCE(*data, 1);
+ smp_store_release(flag, 1);
+ }
+ spin_unlock(lck);
+ }
+ r2 = READ_ONCE(*data);
+}
+
+locations [flag;data;lck;0:r0;0:r1;1:r0;1:r1]
+exists (0:r2=0 \/ 1:r2=0)
diff --git a/Documentation/litmus-tests/locking/RM-broken.litmus b/Documentation/litmus-tests/locking/RM-broken.litmus
new file mode 100644
index 000000000000..c586ae4b547d
--- /dev/null
+++ b/Documentation/litmus-tests/locking/RM-broken.litmus
@@ -0,0 +1,42 @@
+C RM-broken
+
+(*
+ * Result: DEADLOCK
+ *
+ * This litmus test demonstrates that the old "roach motel" approach
+ * to locking, where code can be freely moved into critical sections,
+ * cannot be used in the Linux kernel.
+ *)
+
+{
+ int lck;
+ int x;
+ int y;
+}
+
+P0(int *x, int *y, int *lck)
+{
+ int r2;
+
+ spin_lock(lck);
+ r2 = atomic_inc_return(y);
+ WRITE_ONCE(*x, 1);
+ spin_unlock(lck);
+}
+
+P1(int *x, int *y, int *lck)
+{
+ int r0;
+ int r1;
+ int r2;
+
+ spin_lock(lck);
+ r0 = READ_ONCE(*x);
+ r1 = READ_ONCE(*x);
+ r2 = atomic_inc_return(y);
+ spin_unlock(lck);
+}
+
+locations [x;lck;0:r2;1:r0;1:r1;1:r2]
+filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+exists (1:r2=1)
diff --git a/Documentation/litmus-tests/locking/RM-fixed.litmus b/Documentation/litmus-tests/locking/RM-fixed.litmus
new file mode 100644
index 000000000000..672856736b42
--- /dev/null
+++ b/Documentation/litmus-tests/locking/RM-fixed.litmus
@@ -0,0 +1,42 @@
+C RM-fixed
+
+(*
+ * Result: Never
+ *
+ * This litmus test demonstrates that the old "roach motel" approach
+ * to locking, where code can be freely moved into critical sections,
+ * cannot be used in the Linux kernel.
+ *)
+
+{
+ int lck;
+ int x;
+ int y;
+}
+
+P0(int *x, int *y, int *lck)
+{
+ int r2;
+
+ spin_lock(lck);
+ r2 = atomic_inc_return(y);
+ WRITE_ONCE(*x, 1);
+ spin_unlock(lck);
+}
+
+P1(int *x, int *y, int *lck)
+{
+ int r0;
+ int r1;
+ int r2;
+
+ r0 = READ_ONCE(*x);
+ r1 = READ_ONCE(*x);
+ spin_lock(lck);
+ r2 = atomic_inc_return(y);
+ spin_unlock(lck);
+}
+
+locations [x;lck;0:r2;1:r0;1:r1;1:r2]
+filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+exists (1:r2=1)
diff --git a/tools/memory-model/Documentation/locking.txt b/tools/memory-model/Documentation/locking.txt
new file mode 100644
index 000000000000..4e05c6d53ab7
--- /dev/null
+++ b/tools/memory-model/Documentation/locking.txt
@@ -0,0 +1,320 @@
+Locking
+=======
+
+Locking is well-known and the common use cases are straightforward: Any
+CPU holding a given lock sees any changes previously seen or made by any
+CPU before it previously released that same lock. This last sentence
+is the only part of this document that most developers will need to read.
+
+However, developers who would like to also access lock-protected shared
+variables outside of their corresponding locks should continue reading.
+
+
+Locking and Prior Accesses
+--------------------------
+
+The basic rule of locking is worth repeating:
+
+ Any CPU holding a given lock sees any changes previously seen
+ or made by any CPU before it previously released that same lock.
+
+Note that this statement is a bit stronger than "Any CPU holding a
+given lock sees all changes made by any CPU during the time that CPU was
+previously holding this same lock". For example, consider the following
+pair of code fragments:
+
+ /* See MP+polocks.litmus. */
+ void CPU0(void)
+ {
+ WRITE_ONCE(x, 1);
+ spin_lock(&mylock);
+ WRITE_ONCE(y, 1);
+ spin_unlock(&mylock);
+ }
+
+ void CPU1(void)
+ {
+ spin_lock(&mylock);
+ r0 = READ_ONCE(y);
+ spin_unlock(&mylock);
+ r1 = READ_ONCE(x);
+ }
+
+The basic rule guarantees that if CPU0() acquires mylock before CPU1(),
+then both r0 and r1 must be set to the value 1. This also has the
+consequence that if the final value of r0 is equal to 1, then the final
+value of r1 must also be equal to 1. In contrast, the weaker rule would
+say nothing about the final value of r1.
+
+
+Locking and Subsequent Accesses
+-------------------------------
+
+The converse to the basic rule also holds: Any CPU holding a given
+lock will not see any changes that will be made by any CPU after it
+subsequently acquires this same lock. This converse statement is
+illustrated by the following litmus test:
+
+ /* See MP+porevlocks.litmus. */
+ void CPU0(void)
+ {
+ r0 = READ_ONCE(y);
+ spin_lock(&mylock);
+ r1 = READ_ONCE(x);
+ spin_unlock(&mylock);
+ }
+
+ void CPU1(void)
+ {
+ spin_lock(&mylock);
+ WRITE_ONCE(x, 1);
+ spin_unlock(&mylock);
+ WRITE_ONCE(y, 1);
+ }
+
+This converse to the basic rule guarantees that if CPU0() acquires
+mylock before CPU1(), then both r0 and r1 must be set to the value 0.
+This also has the consequence that if the final value of r1 is equal
+to 0, then the final value of r0 must also be equal to 0. In contrast,
+the weaker rule would say nothing about the final value of r0.
+
+These examples show only a single pair of CPUs, but the effects of the
+locking basic rule extend across multiple acquisitions of a given lock
+across multiple CPUs.
+
+
+Double-Checked Locking
+----------------------
+
+It is well known that more than just a lock is required to make
+double-checked locking work correctly, This litmus test illustrates
+one incorrect approach:
+
+ /* See Documentation/litmus-tests/locking/DCL-broken.litmus. */
+ P0(int *flag, int *data, int *lck)
+ {
+ int r0;
+ int r1;
+ int r2;
+
+ r0 = READ_ONCE(*flag);
+ if (r0 == 0) {
+ spin_lock(lck);
+ r1 = READ_ONCE(*flag);
+ if (r1 == 0) {
+ WRITE_ONCE(*data, 1);
+ WRITE_ONCE(*flag, 1);
+ }
+ spin_unlock(lck);
+ }
+ r2 = READ_ONCE(*data);
+ }
+ /* P1() is the exactly the same as P0(). */
+
+There are two problems. First, there is no ordering between the first
+READ_ONCE() of "flag" and the READ_ONCE() of "data". Second, there is
+no ordering between the two WRITE_ONCE() calls. It should therefore be
+no surprise that "r2" can be zero, and a quick herd7 run confirms this.
+
+One way to fix this is to use smp_load_acquire() and smp_store_release()
+as shown in this corrected version:
+
+ /* See Documentation/litmus-tests/locking/DCL-fixed.litmus. */
+ P0(int *flag, int *data, int *lck)
+ {
+ int r0;
+ int r1;
+ int r2;
+
+ r0 = smp_load_acquire(flag);
+ if (r0 == 0) {
+ spin_lock(lck);
+ r1 = READ_ONCE(*flag);
+ if (r1 == 0) {
+ WRITE_ONCE(*data, 1);
+ smp_store_release(flag, 1);
+ }
+ spin_unlock(lck);
+ }
+ r2 = READ_ONCE(*data);
+ }
+ /* P1() is the exactly the same as P0(). */
+
+The smp_load_acquire() guarantees that its load from "flags" will
+be ordered before the READ_ONCE() from data, thus solving the first
+problem. The smp_store_release() guarantees that its store will be
+ordered after the WRITE_ONCE() to "data", solving the second problem.
+The smp_store_release() pairs with the smp_load_acquire(), thus ensuring
+that the ordering provided by each actually takes effect. Again, a
+quick herd7 run confirms this.
+
+In short, if you access a lock-protected variable without holding the
+corresponding lock, you will need to provide additional ordering, in
+this case, via the smp_load_acquire() and the smp_store_release().
+
+
+Ordering Provided by a Lock to CPUs Not Holding That Lock
+---------------------------------------------------------
+
+It is not necessarily the case that accesses ordered by locking will be
+seen as ordered by CPUs not holding that lock. Consider this example:
+
+ /* See Z6.0+pooncelock+pooncelock+pombonce.litmus. */
+ void CPU0(void)
+ {
+ spin_lock(&mylock);
+ WRITE_ONCE(x, 1);
+ WRITE_ONCE(y, 1);
+ spin_unlock(&mylock);
+ }
+
+ void CPU1(void)
+ {
+ spin_lock(&mylock);
+ r0 = READ_ONCE(y);
+ WRITE_ONCE(z, 1);
+ spin_unlock(&mylock);
+ }
+
+ void CPU2(void)
+ {
+ WRITE_ONCE(z, 2);
+ smp_mb();
+ r1 = READ_ONCE(x);
+ }
+
+Counter-intuitive though it might be, it is quite possible to have
+the final value of r0 be 1, the final value of z be 2, and the final
+value of r1 be 0. The reason for this surprising outcome is that CPU2()
+never acquired the lock, and thus did not fully benefit from the lock's
+ordering properties.
+
+Ordering can be extended to CPUs not holding the lock by careful use
+of smp_mb__after_spinlock():
+
+ /* See Z6.0+pooncelock+poonceLock+pombonce.litmus. */
+ void CPU0(void)
+ {
+ spin_lock(&mylock);
+ WRITE_ONCE(x, 1);
+ WRITE_ONCE(y, 1);
+ spin_unlock(&mylock);
+ }
+
+ void CPU1(void)
+ {
+ spin_lock(&mylock);
+ smp_mb__after_spinlock();
+ r0 = READ_ONCE(y);
+ WRITE_ONCE(z, 1);
+ spin_unlock(&mylock);
+ }
+
+ void CPU2(void)
+ {
+ WRITE_ONCE(z, 2);
+ smp_mb();
+ r1 = READ_ONCE(x);
+ }
+
+This addition of smp_mb__after_spinlock() strengthens the lock
+acquisition sufficiently to rule out the counter-intuitive outcome.
+In other words, the addition of the smp_mb__after_spinlock() prohibits
+the counter-intuitive result where the final value of r0 is 1, the final
+value of z is 2, and the final value of r1 is 0.
+
+
+No Roach-Motel Locking!
+-----------------------
+
+This example requires familiarity with the herd7 "filter" clause, so
+please read up on that topic in litmus-tests.txt.
+
+It is tempting to allow memory-reference instructions to be pulled
+into a critical section, but this cannot be allowed in the general case.
+For example, consider a spin loop preceding a lock-based critical section.
+Now, herd7 does not model spin loops, but we can emulate one with two
+loads, with a "filter" clause to constrain the first to return the
+initial value and the second to return the updated value, as shown below:
+
+ /* See Documentation/litmus-tests/locking/RM-fixed.litmus. */
+ P0(int *x, int *y, int *lck)
+ {
+ int r2;
+
+ spin_lock(lck);
+ r2 = atomic_inc_return(y);
+ WRITE_ONCE(*x, 1);
+ spin_unlock(lck);
+ }
+
+ P1(int *x, int *y, int *lck)
+ {
+ int r0;
+ int r1;
+ int r2;
+
+ r0 = READ_ONCE(*x);
+ r1 = READ_ONCE(*x);
+ spin_lock(lck);
+ r2 = atomic_inc_return(y);
+ spin_unlock(lck);
+ }
+
+ filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+ exists (1:r2=1)
+
+The variable "x" is the control variable for the emulated spin loop.
+P0() sets it to "1" while holding the lock, and P1() emulates the
+spin loop by reading it twice, first into "1:r0" (which should get the
+initial value "0") and then into "1:r1" (which should get the updated
+value "1").
+
+The purpose of the variable "y" is to reject deadlocked executions.
+Only those executions where the final value of "y" have avoided deadlock.
+
+The "filter" clause takes all this into account, constraining "y" to
+equal "2", "1:r0" to equal "0", and "1:r1" to equal 1.
+
+Then the "exists" clause checks to see if P1() acquired its lock first,
+which should not happen given the filter clause because P0() updates
+"x" while holding the lock. And herd7 confirms this.
+
+But suppose that the compiler was permitted to reorder the spin loop
+into P1()'s critical section, like this:
+
+ /* See Documentation/litmus-tests/locking/RM-broken.litmus. */
+ P0(int *x, int *y, int *lck)
+ {
+ int r2;
+
+ spin_lock(lck);
+ r2 = atomic_inc_return(y);
+ WRITE_ONCE(*x, 1);
+ spin_unlock(lck);
+ }
+
+ P1(int *x, int *y, int *lck)
+ {
+ int r0;
+ int r1;
+ int r2;
+
+ spin_lock(lck);
+ r0 = READ_ONCE(*x);
+ r1 = READ_ONCE(*x);
+ r2 = atomic_inc_return(y);
+ spin_unlock(lck);
+ }
+
+ locations [x;lck;0:r2;1:r0;1:r1;1:r2]
+ filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+ exists (1:r2=1)
+
+If "1:r0" is equal to "0", "1:r1" can never equal "1" because P0()
+cannot update "x" while P1() holds the lock. And herd7 confirms this,
+showing zero executions matching the "filter" criteria.
+
+And this is why Linux-kernel lock and unlock primitives must prevent
+code from entering critical sections. It is not sufficient to only
+prevent code from leaving them.
--
2.40.0.rc2
This commit abstracts out common function to check a given litmus test
for locking, RCU, and SRCU in order to avoid duplicating code.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/simpletest.sh | 35 ++++++++++++++++++++++++
1 file changed, 35 insertions(+)
create mode 100755 tools/memory-model/scripts/simpletest.sh
diff --git a/tools/memory-model/scripts/simpletest.sh b/tools/memory-model/scripts/simpletest.sh
new file mode 100755
index 000000000000..7edc5d361665
--- /dev/null
+++ b/tools/memory-model/scripts/simpletest.sh
@@ -0,0 +1,35 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Give zero status if this is a simple test and non-zero otherwise.
+# Simple tests do not contain locking, RCU, or SRCU.
+#
+# Usage:
+# simpletest.sh file.litmus
+#
+# Copyright IBM Corporation, 2019
+#
+# Author: Paul E. McKenney <[email protected]>
+
+
+litmus=$1
+
+if test -f "$litmus" -a -r "$litmus"
+then
+ :
+else
+ echo ' --- ' error: \"$litmus\" is not a readable file
+ exit 255
+fi
+exclude="^[[:space:]]*\("
+exclude="${exclude}spin_lock(\|spin_unlock(\|spin_trylock(\|spin_is_locked("
+exclude="${exclude}\|rcu_read_lock(\|rcu_read_unlock("
+exclude="${exclude}\|synchronize_rcu(\|synchronize_rcu_expedited("
+exclude="${exclude}\|srcu_read_lock(\|srcu_read_unlock("
+exclude="${exclude}\|synchronize_srcu(\|synchronize_srcu_expedited("
+exclude="${exclude}\)"
+if grep -q $exclude $litmus
+then
+ exit 255
+fi
+exit 0
--
2.40.0.rc2
Currently, cmplitmushist.sh treats timeouts (as in the "--timeout"
argument) as "Missing Observation line". This can be misleading because
it is quite possible that running the test longer would have produced
a verification. This commit therefore changes cmplitmushist.sh to check
for timeouts and to report them with "Timed out".
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/cmplitmushist.sh | 22 +++++++++++++++++++++
1 file changed, 22 insertions(+)
diff --git a/tools/memory-model/scripts/cmplitmushist.sh b/tools/memory-model/scripts/cmplitmushist.sh
index 0f498aeeccf5..b9c174dd8004 100755
--- a/tools/memory-model/scripts/cmplitmushist.sh
+++ b/tools/memory-model/scripts/cmplitmushist.sh
@@ -12,12 +12,30 @@ trap 'rm -rf $T' 0
mkdir $T
# comparetest oldpath newpath
+timedout=0
perfect=0
obsline=0
noobsline=0
obsresult=0
badcompare=0
comparetest () {
+ if grep -q '^Command exited with non-zero status 124' $1 ||
+ grep -q '^Command exited with non-zero status 124' $2
+ then
+ if grep -q '^Command exited with non-zero status 124' $1 &&
+ grep -q '^Command exited with non-zero status 124' $2
+ then
+ echo Both runs timed out: $2
+ elif grep -q '^Command exited with non-zero status 124' $1
+ then
+ echo Old run timed out: $2
+ elif grep -q '^Command exited with non-zero status 124' $2
+ then
+ echo New run timed out: $2
+ fi
+ timedout=`expr "$timedout" + 1`
+ return 0
+ fi
grep -v 'maxresident)k\|minor)pagefaults\|^Time' $1 > $T/oldout
grep -v 'maxresident)k\|minor)pagefaults\|^Time' $2 > $T/newout
if cmp -s $T/oldout $T/newout && grep -q '^Observation' $1
@@ -78,6 +96,10 @@ if test "$obsresult" -ne 0
then
echo Matching Observation Always/Sometimes/Never result: $obsresult 1>&2
fi
+if test "$timedout" -ne 0
+then
+ echo "!!!" Timed out: $timedout 1>&2
+fi
if test "$badcompare" -ne 0
then
echo "!!!" Result changed: $badcompare 1>&2
--
2.40.0.rc2
This commit makes the judgelitmus.sh script check the --hw argument
(AKA the LKMM_HW_MAP_FILE environment variable) and to adjust its
judgment for a run where a C-language litmus test has been translated to
assembly and the assembly version verified. In this case, the assembly
verification output is checked against the C-language script's "Result:"
comment. However, because hardware can be stronger than LKMM requires,
the judgelitmus.sh script forgives verification mismatches featuring
a "Sometimes" in the C-language script and an "Always" or "Never"
assembly-language verification.
Note that deadlock is not forgiven, however, this should not normally be
an issue given that C-language tests containing locking, RCU, or SRCU
cannot be translated to assembly. However, this issue can crop up in
litmus tests that mimic deadlock by using the "filter" clause to ignore
all executions. It can also crop up when certain herd arguments are
used to autofilter everything that does not match the "exists" clause
in cases where the "exists" clause cannot be satisfied.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/README | 8 +--
tools/memory-model/scripts/judgelitmus.sh | 75 ++++++++++++++---------
2 files changed, 51 insertions(+), 32 deletions(-)
diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README
index 095c7eb36f9f..0e29a52044c1 100644
--- a/tools/memory-model/scripts/README
+++ b/tools/memory-model/scripts/README
@@ -43,10 +43,10 @@ initlitmushist.sh
judgelitmus.sh
- Given a .litmus file and its .litmus.out herd7 output, check the
- .litmus.out file against the .litmus file's "Result:" comment to
- judge whether the test ran correctly. Not normally run manually,
- provided instead for use by other scripts.
+ Given a .litmus file and its herd7 output, check the output file
+ against the .litmus file's "Result:" comment to judge whether
+ the test ran correctly. Not normally run manually, provided
+ instead for use by other scripts.
newlitmushist.sh
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index d82133e75580..6f3c60065c8b 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -1,9 +1,14 @@
#!/bin/sh
# SPDX-License-Identifier: GPL-2.0+
#
-# Given a .litmus test and the corresponding .litmus.out file, check
-# the .litmus.out file against the "Result:" comment to judge whether
-# the test ran correctly.
+# 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.HW.litmus.out, where "HW" is the --hw argument.
+# In addition, non-Sometimes verification results will be noted, but
+# forgiven.
#
# Usage:
# judgelitmus.sh file.litmus
@@ -24,11 +29,18 @@ else
echo ' --- ' error: \"$litmus\" is not a readable file
exit 255
fi
-if test -f "$LKMM_DESTDIR/$litmus".out -a -r "$LKMM_DESTDIR/$litmus".out
+if test -z "$LKMM_HW_MAP_FILE"
+then
+ litmusout=$litmus.out
+else
+ litmusout="`echo $litmus |
+ sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out"
+fi
+if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"
then
:
else
- echo ' --- ' error: \"$LKMM_DESTDIR/$litmus\".out is not a readable file
+ echo ' --- ' error: \"$LKMM_DESTDIR/$litmusout is not a readable file
exit 255
fi
if grep -q '^ \* Result: ' $litmus
@@ -38,69 +50,76 @@ else
outcome=specified
fi
-grep '^Observation' $LKMM_DESTDIR/$litmus.out
-if grep -q '^Observation' $LKMM_DESTDIR/$litmus.out
+grep '^Observation' $LKMM_DESTDIR/$litmusout
+if grep -q '^Observation' $LKMM_DESTDIR/$litmusout
then
:
-elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out
+elif grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout
then
- badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmus.out |
+ badname=`grep ': Unknown macro ' $LKMM_DESTDIR/$litmusout |
sed -e 's/^.*: Unknown macro //' |
sed -e 's/ (User error).*$//'`
badmsg=' !!! Current LKMM version does not know "'$badname'"'" $litmus"
echo $badmsg
- if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
then
- echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmus.out 2>&1
+ echo ' !!! '$badmsg >> $LKMM_DESTDIR/$litmusout 2>&1
fi
exit 254
-elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmus.out
+elif grep '^Command exited with non-zero status 124' $LKMM_DESTDIR/$litmusout
then
echo ' !!! Timeout' $litmus
- if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
then
- echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmus.out 2>&1
+ echo ' !!! Timeout' >> $LKMM_DESTDIR/$litmusout 2>&1
fi
exit 124
else
echo ' !!! Verification error' $litmus
- if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
then
- echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmus.out 2>&1
+ echo ' !!! Verification error' >> $LKMM_DESTDIR/$litmusout 2>&1
fi
exit 255
fi
if test "$outcome" = DEADLOCK
then
- if grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
+ if grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'
then
ret=0
else
echo " !!! Unexpected non-$outcome verification" $litmus
- if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
then
- echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
+ echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1
fi
ret=1
fi
-elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q 'Never 0 0$'
+elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q 'Never 0 0$'
then
echo " !!! Unexpected non-$outcome deadlock" $litmus
- if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ if ! grep -q '!!!' $LKMM_DESTDIR/$litmusout
then
- echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmus.out 2>&1
+ echo " !!! Unexpected non-$outcome deadlock" $litmus >> $LKMM_DESTDIR/$litmusout 2>&1
fi
ret=1
-elif grep '^Observation' $LKMM_DESTDIR/$litmus.out | grep -q $outcome || test "$outcome" = Maybe
+elif grep '^Observation' $LKMM_DESTDIR/$litmusout | grep -q $outcome || test "$outcome" = Maybe
then
ret=0
else
- echo " !!! Unexpected non-$outcome verification" $litmus
- if ! grep -q '!!!' $LKMM_DESTDIR/$litmus.out
+ if test -n "$LKMM_HW_MAP_FILE" -a "$outcome" = Sometimes
then
- echo " !!! Unexpected non-$outcome verification" >> $LKMM_DESTDIR/$litmus.out 2>&1
+ flag="--- Forgiven"
+ ret=0
+ else
+ flag="!!! Unexpected"
+ ret=1
+ fi
+ echo " $flag non-$outcome verification" $litmus
+ if ! grep -qe "$flag" $LKMM_DESTDIR/$litmusout
+ then
+ echo " $flag non-$outcome verification" >> $LKMM_DESTDIR/$litmusout 2>&1
fi
- ret=1
fi
-tail -2 $LKMM_DESTDIR/$litmus.out | head -1
+tail -2 $LKMM_DESTDIR/$litmusout | head -1
exit $ret
--
2.40.0.rc2
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.
[ paulmck: Apply Akira Yokosawa feedback. ]
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/litmus-tests/.gitignore | 2 +-
tools/memory-model/scripts/judgelitmus.sh | 4 ++--
tools/memory-model/scripts/runlitmus.sh | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore
index c492a1ddad91..d65462d64816 100644
--- a/tools/memory-model/litmus-tests/.gitignore
+++ b/tools/memory-model/litmus-tests/.gitignore
@@ -1,2 +1,2 @@
# SPDX-License-Identifier: GPL-2.0-only
-*.litmus.out
+*.out
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index fe9131f8eb96..9abda72fe013 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
@@ -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.40.0.rc2
This commit retains the assembly-language litmus tests generated from
the C-language litmus tests, appending the hardware tag to the original
C-language litmus test's filename. Thus, S+poonceonces.litmus.AArch64
contains the Armv8 assembly language corresponding to the C-language
S+poonceonces.litmus test.
This commit also updates the .gitignore to avoid committing these
automatically generated assembly-language litmus tests.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/litmus-tests/.gitignore | 2 +-
tools/memory-model/scripts/runlitmus.sh | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore
index d65462d64816..19c379cf069d 100644
--- a/tools/memory-model/litmus-tests/.gitignore
+++ b/tools/memory-model/litmus-tests/.gitignore
@@ -1,2 +1,2 @@
# SPDX-License-Identifier: GPL-2.0-only
-*.out
+*.litmus.*
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
index c84124b32bee..62b47c7e1ba9 100755
--- a/tools/memory-model/scripts/runlitmus.sh
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -69,7 +69,7 @@ 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
+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
exit $?
--
2.40.0.rc2
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.40.0.rc2
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.40.0.rc2
This commit prepares for adding --hw capability to github litmus-test
scripts by splitting runlitmus.sh (which simply runs the verification)
out of checklitmus.sh (which also judges the results).
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/checklitmus.sh | 57 ++-----------------
tools/memory-model/scripts/runlitmus.sh | 69 +++++++++++++++++++++++
2 files changed, 73 insertions(+), 53 deletions(-)
create mode 100755 tools/memory-model/scripts/runlitmus.sh
diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh
index 42ff11869cd6..4c1d0cf0ddad 100755
--- a/tools/memory-model/scripts/checklitmus.sh
+++ b/tools/memory-model/scripts/checklitmus.sh
@@ -1,15 +1,8 @@
#!/bin/sh
# SPDX-License-Identifier: GPL-2.0+
#
-# Run a herd7 test and invokes judgelitmus.sh to check the result against
-# a "Result:" comment within the litmus test. 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.
+# Invokes runlitmus.sh and judgelitmus.sh on its arguments to run the
+# specified litmus test and pass judgment on the results.
#
# Usage:
# checklitmus.sh file.litmus
@@ -22,47 +15,5 @@
#
# Author: Paul E. McKenney <[email protected]>
-litmus=$1
-if test -f "$litmus" -a -r "$litmus"
-then
- :
-else
- echo ' --- ' error: \"$litmus\" is not a readable file
- exit 255
-fi
-
-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
+scripts/runlitmus.sh $1
+scripts/judgelitmus.sh $1
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh
new file mode 100755
index 000000000000..91af859c0e90
--- /dev/null
+++ b/tools/memory-model/scripts/runlitmus.sh
@@ -0,0 +1,69 @@
+#!/bin/sh
+# SPDX-License-Identifier: GPL-2.0+
+#
+# Without the -hw argument, runs a herd7 test and 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.
+#
+# Either way, return the status of the herd7 command.
+#
+# Usage:
+# runlitmus.sh file.litmus
+#
+# Run this in the directory containing the memory model, specifying the
+# pathname of the litmus test to check. The caller is expected to have
+# properly set up the LKMM environment variables.
+#
+# Copyright IBM Corporation, 2019
+#
+# Author: Paul E. McKenney <[email protected]>
+
+litmus=$1
+if test -f "$litmus" -a -r "$litmus"
+then
+ :
+else
+ echo ' --- ' error: \"$litmus\" is not a readable file
+ exit 255
+fi
+
+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 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
+fi
+
+exit $?
--
2.40.0.rc2
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.40.0.rc2
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.40.0.rc2
From: Tiezhu Yang <[email protected]>
The latest version of grep claims the egrep is now obsolete so the build
now contains warnings that look like:
egrep: warning: egrep is obsolescent; using grep -E
fix this up by moving the related file to use "grep -E" instead.
sed -i "s/egrep/grep -E/g" `grep egrep -rwl tools/memory-model`
Here are the steps to install the latest grep:
wget http://ftp.gnu.org/gnu/grep/grep-3.8.tar.gz
tar xf grep-3.8.tar.gz
cd grep-3.8 && ./configure && make
sudo make install
export PATH=/usr/local/bin:$PATH
Signed-off-by: Tiezhu Yang <[email protected]>
Reviewed-by: Akira Yokosawa <[email protected]>
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/checkghlitmus.sh | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/tools/memory-model/scripts/checkghlitmus.sh b/tools/memory-model/scripts/checkghlitmus.sh
index cedd0290b73f..d3dfb321259f 100755
--- a/tools/memory-model/scripts/checkghlitmus.sh
+++ b/tools/memory-model/scripts/checkghlitmus.sh
@@ -36,13 +36,13 @@ fi
# 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 -E -l '^ \* Result: (Never|Sometimes|Always|DEADLOCK)' |
xargs -r grep -L "^P${LKMM_PROCS}"> $T/list-C-already
# Create a list of C-language litmus tests with "Result:" commands and
# no more than the specified number of processes.
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 -r grep -E -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 .out files
--
2.40.0.rc2
This commit documents how to run the various scripts in order to test
a potentially pervasive change to the memory model.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/README | 32 +++++++++++++++++++++++++++++++
1 file changed, 32 insertions(+)
diff --git a/tools/memory-model/scripts/README b/tools/memory-model/scripts/README
index cc2c4e5be9ec..fb39bd0fd1b9 100644
--- a/tools/memory-model/scripts/README
+++ b/tools/memory-model/scripts/README
@@ -76,3 +76,35 @@ runlitmushist.sh
README
This file
+
+Testing a change to LKMM might go as follows:
+
+ # Populate expected results without that change, and
+ # runs for about an hour on an 8-CPU x86 system:
+ scripts/initlitmushist.sh --timeout 10m --procs 10
+ # Incorporate the change:
+ git am -s -3 /path/to/patch # Or whatever it takes.
+
+ # Test the new version of LKMM as follows...
+
+ # Runs in seconds, good smoke test:
+ scripts/checkalllitmus.sh
+
+ # Compares results to those produced by initlitmushist.sh,
+ # and runs for about an hour on an 8-CPU x86 system:
+ scripts/checklitmushist.sh --timeout 10m --procs 10
+
+ # Checks results against Result tags, runs in minutes:
+ scripts/checkghlitmus.sh --timeout 10m --procs 10
+
+The checkghlitmus.sh should not report errors in cases where the
+checklitmushist.sh script did not also report a change. However,
+this check is nevertheless valuable because it can find errors in the
+original version of LKMM. Note however, that given the above procedure,
+an error in the original LKMM version that is fixed by the patch will
+be reported both as a mismatch by checklitmushist.sh and as an error
+by checkghlitmus.sh. One exception to this rule of thumb is when the
+test fails completely on the original version of LKMM and passes on the
+new version. In this case, checklitmushist.sh will report a mismatch
+and checkghlitmus.sh will report success. This happens when the change
+to LKMM introduces a new primitive for which litmus tests already existed.
--
2.40.0.rc2
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.40.0.rc2
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.40.0.rc2
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 2700481d20f0..1ec5d89fcfbb 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -57,10 +57,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.40.0.rc2
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.40.0.rc2
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.40.0.rc2
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.40.0.rc2
The judgelitmus.sh script currently relies solely on the "Result:"
comment in the .litmus file. This is problematic when using the --hw
argument, because it is necessary to check the hardware model against
LKMM even in the absence of "Result:" comments.
This commit therefore modifies judgelitmus.sh to check the observation
in a .litmus.out file, in case one was generated by a previous LKMM run.
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/judgelitmus.sh | 9 ++++++++-
1 file changed, 8 insertions(+), 1 deletion(-)
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index 6f3c60065c8b..fe9131f8eb96 100755
--- a/tools/memory-model/scripts/judgelitmus.sh
+++ b/tools/memory-model/scripts/judgelitmus.sh
@@ -8,7 +8,9 @@
# 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.
# In addition, non-Sometimes verification results will be noted, but
-# forgiven.
+# 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
@@ -32,9 +34,11 @@ fi
if test -z "$LKMM_HW_MAP_FILE"
then
litmusout=$litmus.out
+ lkmmout=
else
litmusout="`echo $litmus |
sed -e 's/\.litmus$/.'${LKMM_HW_MAP_FILE}'.litmus/'`.out"
+ lkmmout=$litmus.out
fi
if test -f "$LKMM_DESTDIR/$litmusout" -a -r "$LKMM_DESTDIR/$litmusout"
then
@@ -46,6 +50,9 @@ fi
if grep -q '^ \* Result: ' $litmus
then
outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
+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 }'`
else
outcome=specified
fi
--
2.40.0.rc2
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 7aa58755adfc..08ded5909860 100755
--- a/tools/memory-model/scripts/parseargs.sh
+++ b/tools/memory-model/scripts/parseargs.sh
@@ -1,7 +1,7 @@
#!/bin/sh
# SPDX-License-Identifier: GPL-2.0+
#
-# the corresponding .litmus.out file, and does not judge the result.
+# Parse arguments common to the various scripts.
#
# . scripts/parseargs.sh
#
--
2.40.0.rc2
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.
The reason for forgiving "Result:" mispredictions is that data races can
result in "interesting" compiler optimizations, so that all bets are off
in the data-race case.
[ paulmck: Apply Akira Yokosawa feedback. ]
Signed-off-by: Paul E. McKenney <[email protected]>
---
tools/memory-model/scripts/judgelitmus.sh | 40 ++++++++++++++++++-----
1 file changed, 32 insertions(+), 8 deletions(-)
diff --git a/tools/memory-model/scripts/judgelitmus.sh b/tools/memory-model/scripts/judgelitmus.sh
index 9abda72fe013..2700481d20f0 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
@@ -47,9 +53,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 +138,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.40.0.rc2
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.40.0.rc2
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.40.0.rc2
> create mode 100644 Documentation/litmus-tests/locking/DCL-broken.litmus
> create mode 100644 Documentation/litmus-tests/locking/DCL-fixed.litmus
> create mode 100644 Documentation/litmus-tests/locking/RM-broken.litmus
> create mode 100644 Documentation/litmus-tests/locking/RM-fixed.litmus
Unfortunately none of them were liked by klitmus7/gcc, the diff below
works for me but please double check.
Andrea
diff --git a/Documentation/litmus-tests/locking/DCL-broken.litmus b/Documentation/litmus-tests/locking/DCL-broken.litmus
index cfaa25ff82b1e..bfb7ba4316d69 100644
--- a/Documentation/litmus-tests/locking/DCL-broken.litmus
+++ b/Documentation/litmus-tests/locking/DCL-broken.litmus
@@ -10,10 +10,9 @@ C DCL-broken
{
int flag;
int data;
- int lck;
}
-P0(int *flag, int *data, int *lck)
+P0(int *flag, int *data, spinlock_t *lck)
{
int r0;
int r1;
@@ -32,7 +31,7 @@ P0(int *flag, int *data, int *lck)
r2 = READ_ONCE(*data);
}
-P1(int *flag, int *data, int *lck)
+P1(int *flag, int *data, spinlock_t *lck)
{
int r0;
int r1;
@@ -51,5 +50,5 @@ P1(int *flag, int *data, int *lck)
r2 = READ_ONCE(*data);
}
-locations [flag;data;lck;0:r0;0:r1;1:r0;1:r1]
+locations [flag;data;0:r0;0:r1;1:r0;1:r1]
exists (0:r2=0 \/ 1:r2=0)
diff --git a/Documentation/litmus-tests/locking/DCL-fixed.litmus b/Documentation/litmus-tests/locking/DCL-fixed.litmus
index 579d6c246f167..d1b60bcb0c8f3 100644
--- a/Documentation/litmus-tests/locking/DCL-fixed.litmus
+++ b/Documentation/litmus-tests/locking/DCL-fixed.litmus
@@ -11,10 +11,9 @@ C DCL-fixed
{
int flag;
int data;
- int lck;
}
-P0(int *flag, int *data, int *lck)
+P0(int *flag, int *data, spinlock_t *lck)
{
int r0;
int r1;
@@ -33,7 +32,7 @@ P0(int *flag, int *data, int *lck)
r2 = READ_ONCE(*data);
}
-P1(int *flag, int *data, int *lck)
+P1(int *flag, int *data, spinlock_t *lck)
{
int r0;
int r1;
@@ -52,5 +51,5 @@ P1(int *flag, int *data, int *lck)
r2 = READ_ONCE(*data);
}
-locations [flag;data;lck;0:r0;0:r1;1:r0;1:r1]
+locations [flag;data;0:r0;0:r1;1:r0;1:r1]
exists (0:r2=0 \/ 1:r2=0)
diff --git a/Documentation/litmus-tests/locking/RM-broken.litmus b/Documentation/litmus-tests/locking/RM-broken.litmus
index c586ae4b547de..b7ef30cedfe51 100644
--- a/Documentation/litmus-tests/locking/RM-broken.litmus
+++ b/Documentation/litmus-tests/locking/RM-broken.litmus
@@ -9,12 +9,11 @@ C RM-broken
*)
{
- int lck;
int x;
- int y;
+ atomic_t y;
}
-P0(int *x, int *y, int *lck)
+P0(int *x, atomic_t *y, spinlock_t *lck)
{
int r2;
@@ -24,7 +23,7 @@ P0(int *x, int *y, int *lck)
spin_unlock(lck);
}
-P1(int *x, int *y, int *lck)
+P1(int *x, atomic_t *y, spinlock_t *lck)
{
int r0;
int r1;
@@ -37,6 +36,6 @@ P1(int *x, int *y, int *lck)
spin_unlock(lck);
}
-locations [x;lck;0:r2;1:r0;1:r1;1:r2]
-filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+locations [x;0:r2;1:r0;1:r1;1:r2]
+filter (1:r0=0 /\ 1:r1=1)
exists (1:r2=1)
diff --git a/Documentation/litmus-tests/locking/RM-fixed.litmus b/Documentation/litmus-tests/locking/RM-fixed.litmus
index 672856736b42e..b628175596160 100644
--- a/Documentation/litmus-tests/locking/RM-fixed.litmus
+++ b/Documentation/litmus-tests/locking/RM-fixed.litmus
@@ -9,12 +9,11 @@ C RM-fixed
*)
{
- int lck;
int x;
- int y;
+ atomic_t y;
}
-P0(int *x, int *y, int *lck)
+P0(int *x, atomic_t *y, spinlock_t *lck)
{
int r2;
@@ -24,7 +23,7 @@ P0(int *x, int *y, int *lck)
spin_unlock(lck);
}
-P1(int *x, int *y, int *lck)
+P1(int *x, atomic_t *y, spinlock_t *lck)
{
int r0;
int r1;
@@ -37,6 +36,6 @@ P1(int *x, int *y, int *lck)
spin_unlock(lck);
}
-locations [x;lck;0:r2;1:r0;1:r1;1:r2]
-filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+locations [x;0:r2;1:r0;1:r1;1:r2]
+filter (1:r0=0 /\ 1:r1=1)
exists (1:r2=1)
On Wed, Mar 22, 2023 at 09:59:38AM +0100, Andrea Parri wrote:
> > create mode 100644 Documentation/litmus-tests/locking/DCL-broken.litmus
> > create mode 100644 Documentation/litmus-tests/locking/DCL-fixed.litmus
> > create mode 100644 Documentation/litmus-tests/locking/RM-broken.litmus
> > create mode 100644 Documentation/litmus-tests/locking/RM-fixed.litmus
>
> Unfortunately none of them were liked by klitmus7/gcc, the diff below
> works for me but please double check.
Applied with attribution, thank you!
I was surprised by the need to change the "locations" clauses, but
applied that change anyway. Ah, I take it that klitmus prints that,
but doesn't know how to print out a spinlock_t?
Dropping "y" from the "filter" clause also gave me pause, but I eventually
convinced myself that it was OK. But it would be good for others to
also take a close look.
Thanx, Paul
> Andrea
>
>
> diff --git a/Documentation/litmus-tests/locking/DCL-broken.litmus b/Documentation/litmus-tests/locking/DCL-broken.litmus
> index cfaa25ff82b1e..bfb7ba4316d69 100644
> --- a/Documentation/litmus-tests/locking/DCL-broken.litmus
> +++ b/Documentation/litmus-tests/locking/DCL-broken.litmus
> @@ -10,10 +10,9 @@ C DCL-broken
> {
> int flag;
> int data;
> - int lck;
> }
>
> -P0(int *flag, int *data, int *lck)
> +P0(int *flag, int *data, spinlock_t *lck)
> {
> int r0;
> int r1;
> @@ -32,7 +31,7 @@ P0(int *flag, int *data, int *lck)
> r2 = READ_ONCE(*data);
> }
>
> -P1(int *flag, int *data, int *lck)
> +P1(int *flag, int *data, spinlock_t *lck)
> {
> int r0;
> int r1;
> @@ -51,5 +50,5 @@ P1(int *flag, int *data, int *lck)
> r2 = READ_ONCE(*data);
> }
>
> -locations [flag;data;lck;0:r0;0:r1;1:r0;1:r1]
> +locations [flag;data;0:r0;0:r1;1:r0;1:r1]
> exists (0:r2=0 \/ 1:r2=0)
> diff --git a/Documentation/litmus-tests/locking/DCL-fixed.litmus b/Documentation/litmus-tests/locking/DCL-fixed.litmus
> index 579d6c246f167..d1b60bcb0c8f3 100644
> --- a/Documentation/litmus-tests/locking/DCL-fixed.litmus
> +++ b/Documentation/litmus-tests/locking/DCL-fixed.litmus
> @@ -11,10 +11,9 @@ C DCL-fixed
> {
> int flag;
> int data;
> - int lck;
> }
>
> -P0(int *flag, int *data, int *lck)
> +P0(int *flag, int *data, spinlock_t *lck)
> {
> int r0;
> int r1;
> @@ -33,7 +32,7 @@ P0(int *flag, int *data, int *lck)
> r2 = READ_ONCE(*data);
> }
>
> -P1(int *flag, int *data, int *lck)
> +P1(int *flag, int *data, spinlock_t *lck)
> {
> int r0;
> int r1;
> @@ -52,5 +51,5 @@ P1(int *flag, int *data, int *lck)
> r2 = READ_ONCE(*data);
> }
>
> -locations [flag;data;lck;0:r0;0:r1;1:r0;1:r1]
> +locations [flag;data;0:r0;0:r1;1:r0;1:r1]
> exists (0:r2=0 \/ 1:r2=0)
> diff --git a/Documentation/litmus-tests/locking/RM-broken.litmus b/Documentation/litmus-tests/locking/RM-broken.litmus
> index c586ae4b547de..b7ef30cedfe51 100644
> --- a/Documentation/litmus-tests/locking/RM-broken.litmus
> +++ b/Documentation/litmus-tests/locking/RM-broken.litmus
> @@ -9,12 +9,11 @@ C RM-broken
> *)
>
> {
> - int lck;
> int x;
> - int y;
> + atomic_t y;
> }
>
> -P0(int *x, int *y, int *lck)
> +P0(int *x, atomic_t *y, spinlock_t *lck)
> {
> int r2;
>
> @@ -24,7 +23,7 @@ P0(int *x, int *y, int *lck)
> spin_unlock(lck);
> }
>
> -P1(int *x, int *y, int *lck)
> +P1(int *x, atomic_t *y, spinlock_t *lck)
> {
> int r0;
> int r1;
> @@ -37,6 +36,6 @@ P1(int *x, int *y, int *lck)
> spin_unlock(lck);
> }
>
> -locations [x;lck;0:r2;1:r0;1:r1;1:r2]
> -filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
> +locations [x;0:r2;1:r0;1:r1;1:r2]
> +filter (1:r0=0 /\ 1:r1=1)
> exists (1:r2=1)
> diff --git a/Documentation/litmus-tests/locking/RM-fixed.litmus b/Documentation/litmus-tests/locking/RM-fixed.litmus
> index 672856736b42e..b628175596160 100644
> --- a/Documentation/litmus-tests/locking/RM-fixed.litmus
> +++ b/Documentation/litmus-tests/locking/RM-fixed.litmus
> @@ -9,12 +9,11 @@ C RM-fixed
> *)
>
> {
> - int lck;
> int x;
> - int y;
> + atomic_t y;
> }
>
> -P0(int *x, int *y, int *lck)
> +P0(int *x, atomic_t *y, spinlock_t *lck)
> {
> int r2;
>
> @@ -24,7 +23,7 @@ P0(int *x, int *y, int *lck)
> spin_unlock(lck);
> }
>
> -P1(int *x, int *y, int *lck)
> +P1(int *x, atomic_t *y, spinlock_t *lck)
> {
> int r0;
> int r1;
> @@ -37,6 +36,6 @@ P1(int *x, int *y, int *lck)
> spin_unlock(lck);
> }
>
> -locations [x;lck;0:r2;1:r0;1:r1;1:r2]
> -filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
> +locations [x;0:r2;1:r0;1:r1;1:r2]
> +filter (1:r0=0 /\ 1:r1=1)
> exists (1:r2=1)
> I was surprised by the need to change the "locations" clauses, but
> applied that change anyway. Ah, I take it that klitmus prints that,
> but doesn't know how to print out a spinlock_t?
Yep, this aligns with my understanding.
Andrea
Hi Paul,
On Mon, 20 Mar 2023 18:05:19 -0700, Paul E. McKenney wrote:
> Most Linux-kernel uses of locking are straightforward, but there are
> corner-case uses that rely on less well-known aspects of the lock and
> unlock primitives. This commit therefore adds a locking.txt and litmus
> tests in Documentation/litmus-tests/locking to explain these corner-case
> uses.
>
> Signed-off-by: Paul E. McKenney <[email protected]>
> ---
> .../litmus-tests/locking/DCL-broken.litmus | 55 +++
> .../litmus-tests/locking/DCL-fixed.litmus | 56 +++
> .../litmus-tests/locking/RM-broken.litmus | 42 +++
> .../litmus-tests/locking/RM-fixed.litmus | 42 +++
> tools/memory-model/Documentation/locking.txt | 320 ++++++++++++++++++
I think the documentation needs adjustment to cope with Andrea's change
of litmus tests.
Also, coding style of code snippets taken from litmus tests look somewhat
inconsistent with other snippets taken from MP+... litmus tests:
- Simple function signature such as "void CPU0(void)".
- No declaration of local variables.
- Indirection level of global variables.
- No "locations" clause
How about applying the diff below?
Thanks, Akira
-----
diff --git a/tools/memory-model/Documentation/locking.txt b/tools/memory-model/Documentation/locking.txt
index 4e05c6d53ab7..65c898c64a93 100644
--- a/tools/memory-model/Documentation/locking.txt
+++ b/tools/memory-model/Documentation/locking.txt
@@ -91,25 +91,21 @@ double-checked locking work correctly, This litmus test illustrates
one incorrect approach:
/* See Documentation/litmus-tests/locking/DCL-broken.litmus. */
- P0(int *flag, int *data, int *lck)
+ void CPU0(void)
{
- int r0;
- int r1;
- int r2;
-
- r0 = READ_ONCE(*flag);
+ r0 = READ_ONCE(flag);
if (r0 == 0) {
- spin_lock(lck);
- r1 = READ_ONCE(*flag);
+ spin_lock(&lck);
+ r1 = READ_ONCE(flag);
if (r1 == 0) {
- WRITE_ONCE(*data, 1);
- WRITE_ONCE(*flag, 1);
+ WRITE_ONCE(data, 1);
+ WRITE_ONCE(flag, 1);
}
- spin_unlock(lck);
+ spin_unlock(&lck);
}
- r2 = READ_ONCE(*data);
+ r2 = READ_ONCE(data);
}
- /* P1() is the exactly the same as P0(). */
+ /* CPU1() is the exactly the same as CPU0(). */
There are two problems. First, there is no ordering between the first
READ_ONCE() of "flag" and the READ_ONCE() of "data". Second, there is
@@ -120,25 +116,21 @@ One way to fix this is to use smp_load_acquire() and smp_store_release()
as shown in this corrected version:
/* See Documentation/litmus-tests/locking/DCL-fixed.litmus. */
- P0(int *flag, int *data, int *lck)
+ void CPU0(void)
{
- int r0;
- int r1;
- int r2;
-
- r0 = smp_load_acquire(flag);
+ r0 = smp_load_acquire(&flag);
if (r0 == 0) {
- spin_lock(lck);
- r1 = READ_ONCE(*flag);
+ spin_lock(&lck);
+ r1 = READ_ONCE(flag);
if (r1 == 0) {
- WRITE_ONCE(*data, 1);
- smp_store_release(flag, 1);
+ WRITE_ONCE(data, 1);
+ smp_store_release(&flag, 1);
}
- spin_unlock(lck);
+ spin_unlock(&lck);
}
- r2 = READ_ONCE(*data);
+ r2 = READ_ONCE(data);
}
- /* P1() is the exactly the same as P0(). */
+ /* CPU1() is the exactly the same as CPU0(). */
The smp_load_acquire() guarantees that its load from "flags" will
be ordered before the READ_ONCE() from data, thus solving the first
@@ -238,81 +230,67 @@ loads, with a "filter" clause to constrain the first to return the
initial value and the second to return the updated value, as shown below:
/* See Documentation/litmus-tests/locking/RM-fixed.litmus. */
- P0(int *x, int *y, int *lck)
+ void CPU0(void)
{
- int r2;
-
- spin_lock(lck);
- r2 = atomic_inc_return(y);
- WRITE_ONCE(*x, 1);
- spin_unlock(lck);
+ spin_lock(&lck);
+ r2 = atomic_inc_return(&y);
+ WRITE_ONCE(x, 1);
+ spin_unlock(&lck);
}
- P1(int *x, int *y, int *lck)
+ void CPU1(void)
{
- int r0;
- int r1;
- int r2;
-
- r0 = READ_ONCE(*x);
- r1 = READ_ONCE(*x);
- spin_lock(lck);
- r2 = atomic_inc_return(y);
- spin_unlock(lck);
+ r0 = READ_ONCE(x);
+ r1 = READ_ONCE(x);
+ spin_lock(&lck);
+ r2 = atomic_inc_return(&y);
+ spin_unlock(&lck);
}
- filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+ filter (1:r0=0 /\ 1:r1=1)
exists (1:r2=1)
The variable "x" is the control variable for the emulated spin loop.
-P0() sets it to "1" while holding the lock, and P1() emulates the
+CPU0() sets it to "1" while holding the lock, and CPU1() emulates the
spin loop by reading it twice, first into "1:r0" (which should get the
initial value "0") and then into "1:r1" (which should get the updated
value "1").
-The purpose of the variable "y" is to reject deadlocked executions.
-Only those executions where the final value of "y" have avoided deadlock.
+The "filter" clause takes this into account, constraining "1:r0" to
+equal "0" and "1:r1" to equal 1.
-The "filter" clause takes all this into account, constraining "y" to
-equal "2", "1:r0" to equal "0", and "1:r1" to equal 1.
-
-Then the "exists" clause checks to see if P1() acquired its lock first,
-which should not happen given the filter clause because P0() updates
+Then the "exists" clause checks to see if CPU1() acquired its lock first,
+which should not happen given the filter clause because CPU0() updates
"x" while holding the lock. And herd7 confirms this.
But suppose that the compiler was permitted to reorder the spin loop
-into P1()'s critical section, like this:
+into CPU1()'s critical section, like this:
/* See Documentation/litmus-tests/locking/RM-broken.litmus. */
- P0(int *x, int *y, int *lck)
+ void CPU0(void)
{
int r2;
- spin_lock(lck);
- r2 = atomic_inc_return(y);
- WRITE_ONCE(*x, 1);
- spin_unlock(lck);
+ spin_lock(&lck);
+ r2 = atomic_inc_return(&y);
+ WRITE_ONCE(x, 1);
+ spin_unlock(&lck);
}
- P1(int *x, int *y, int *lck)
+ void CPU1(void)
{
- int r0;
- int r1;
- int r2;
-
- spin_lock(lck);
- r0 = READ_ONCE(*x);
- r1 = READ_ONCE(*x);
- r2 = atomic_inc_return(y);
- spin_unlock(lck);
+ spin_lock(&lck);
+ r0 = READ_ONCE(x);
+ r1 = READ_ONCE(x);
+ r2 = atomic_inc_return(&y);
+ spin_unlock(&lck);
}
- locations [x;lck;0:r2;1:r0;1:r1;1:r2]
- filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+ filter (1:r0=0 /\ 1:r1=1)
exists (1:r2=1)
-If "1:r0" is equal to "0", "1:r1" can never equal "1" because P0()
-cannot update "x" while P1() holds the lock. And herd7 confirms this,
+If "1:r0" is equal to "0", "1:r1" can never equal "1" because CPU0()
+cannot update "x" while CPU1() holds the lock. And herd7 confirms this,
showing zero executions matching the "filter" criteria.
And this is why Linux-kernel lock and unlock primitives must prevent
On Thu, Mar 23, 2023 at 11:52:57AM +0900, Akira Yokosawa wrote:
> Hi Paul,
>
> On Mon, 20 Mar 2023 18:05:19 -0700, Paul E. McKenney wrote:
> > Most Linux-kernel uses of locking are straightforward, but there are
> > corner-case uses that rely on less well-known aspects of the lock and
> > unlock primitives. This commit therefore adds a locking.txt and litmus
> > tests in Documentation/litmus-tests/locking to explain these corner-case
> > uses.
> >
> > Signed-off-by: Paul E. McKenney <[email protected]>
> > ---
> > .../litmus-tests/locking/DCL-broken.litmus | 55 +++
> > .../litmus-tests/locking/DCL-fixed.litmus | 56 +++
> > .../litmus-tests/locking/RM-broken.litmus | 42 +++
> > .../litmus-tests/locking/RM-fixed.litmus | 42 +++
> > tools/memory-model/Documentation/locking.txt | 320 ++++++++++++++++++
>
> I think the documentation needs adjustment to cope with Andrea's change
> of litmus tests.
>
> Also, coding style of code snippets taken from litmus tests look somewhat
> inconsistent with other snippets taken from MP+... litmus tests:
>
> - Simple function signature such as "void CPU0(void)".
> - No declaration of local variables.
> - Indirection level of global variables.
> - No "locations" clause
>
> How about applying the diff below?
Good eyes, thank you! I will fold this in with attribution.
Thanx, Paul
> Thanks, Akira
>
> -----
> diff --git a/tools/memory-model/Documentation/locking.txt b/tools/memory-model/Documentation/locking.txt
> index 4e05c6d53ab7..65c898c64a93 100644
> --- a/tools/memory-model/Documentation/locking.txt
> +++ b/tools/memory-model/Documentation/locking.txt
> @@ -91,25 +91,21 @@ double-checked locking work correctly, This litmus test illustrates
> one incorrect approach:
>
> /* See Documentation/litmus-tests/locking/DCL-broken.litmus. */
> - P0(int *flag, int *data, int *lck)
> + void CPU0(void)
> {
> - int r0;
> - int r1;
> - int r2;
> -
> - r0 = READ_ONCE(*flag);
> + r0 = READ_ONCE(flag);
> if (r0 == 0) {
> - spin_lock(lck);
> - r1 = READ_ONCE(*flag);
> + spin_lock(&lck);
> + r1 = READ_ONCE(flag);
> if (r1 == 0) {
> - WRITE_ONCE(*data, 1);
> - WRITE_ONCE(*flag, 1);
> + WRITE_ONCE(data, 1);
> + WRITE_ONCE(flag, 1);
> }
> - spin_unlock(lck);
> + spin_unlock(&lck);
> }
> - r2 = READ_ONCE(*data);
> + r2 = READ_ONCE(data);
> }
> - /* P1() is the exactly the same as P0(). */
> + /* CPU1() is the exactly the same as CPU0(). */
>
> There are two problems. First, there is no ordering between the first
> READ_ONCE() of "flag" and the READ_ONCE() of "data". Second, there is
> @@ -120,25 +116,21 @@ One way to fix this is to use smp_load_acquire() and smp_store_release()
> as shown in this corrected version:
>
> /* See Documentation/litmus-tests/locking/DCL-fixed.litmus. */
> - P0(int *flag, int *data, int *lck)
> + void CPU0(void)
> {
> - int r0;
> - int r1;
> - int r2;
> -
> - r0 = smp_load_acquire(flag);
> + r0 = smp_load_acquire(&flag);
> if (r0 == 0) {
> - spin_lock(lck);
> - r1 = READ_ONCE(*flag);
> + spin_lock(&lck);
> + r1 = READ_ONCE(flag);
> if (r1 == 0) {
> - WRITE_ONCE(*data, 1);
> - smp_store_release(flag, 1);
> + WRITE_ONCE(data, 1);
> + smp_store_release(&flag, 1);
> }
> - spin_unlock(lck);
> + spin_unlock(&lck);
> }
> - r2 = READ_ONCE(*data);
> + r2 = READ_ONCE(data);
> }
> - /* P1() is the exactly the same as P0(). */
> + /* CPU1() is the exactly the same as CPU0(). */
>
> The smp_load_acquire() guarantees that its load from "flags" will
> be ordered before the READ_ONCE() from data, thus solving the first
> @@ -238,81 +230,67 @@ loads, with a "filter" clause to constrain the first to return the
> initial value and the second to return the updated value, as shown below:
>
> /* See Documentation/litmus-tests/locking/RM-fixed.litmus. */
> - P0(int *x, int *y, int *lck)
> + void CPU0(void)
> {
> - int r2;
> -
> - spin_lock(lck);
> - r2 = atomic_inc_return(y);
> - WRITE_ONCE(*x, 1);
> - spin_unlock(lck);
> + spin_lock(&lck);
> + r2 = atomic_inc_return(&y);
> + WRITE_ONCE(x, 1);
> + spin_unlock(&lck);
> }
>
> - P1(int *x, int *y, int *lck)
> + void CPU1(void)
> {
> - int r0;
> - int r1;
> - int r2;
> -
> - r0 = READ_ONCE(*x);
> - r1 = READ_ONCE(*x);
> - spin_lock(lck);
> - r2 = atomic_inc_return(y);
> - spin_unlock(lck);
> + r0 = READ_ONCE(x);
> + r1 = READ_ONCE(x);
> + spin_lock(&lck);
> + r2 = atomic_inc_return(&y);
> + spin_unlock(&lck);
> }
>
> - filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
> + filter (1:r0=0 /\ 1:r1=1)
> exists (1:r2=1)
>
> The variable "x" is the control variable for the emulated spin loop.
> -P0() sets it to "1" while holding the lock, and P1() emulates the
> +CPU0() sets it to "1" while holding the lock, and CPU1() emulates the
> spin loop by reading it twice, first into "1:r0" (which should get the
> initial value "0") and then into "1:r1" (which should get the updated
> value "1").
>
> -The purpose of the variable "y" is to reject deadlocked executions.
> -Only those executions where the final value of "y" have avoided deadlock.
> +The "filter" clause takes this into account, constraining "1:r0" to
> +equal "0" and "1:r1" to equal 1.
>
> -The "filter" clause takes all this into account, constraining "y" to
> -equal "2", "1:r0" to equal "0", and "1:r1" to equal 1.
> -
> -Then the "exists" clause checks to see if P1() acquired its lock first,
> -which should not happen given the filter clause because P0() updates
> +Then the "exists" clause checks to see if CPU1() acquired its lock first,
> +which should not happen given the filter clause because CPU0() updates
> "x" while holding the lock. And herd7 confirms this.
>
> But suppose that the compiler was permitted to reorder the spin loop
> -into P1()'s critical section, like this:
> +into CPU1()'s critical section, like this:
>
> /* See Documentation/litmus-tests/locking/RM-broken.litmus. */
> - P0(int *x, int *y, int *lck)
> + void CPU0(void)
> {
> int r2;
>
> - spin_lock(lck);
> - r2 = atomic_inc_return(y);
> - WRITE_ONCE(*x, 1);
> - spin_unlock(lck);
> + spin_lock(&lck);
> + r2 = atomic_inc_return(&y);
> + WRITE_ONCE(x, 1);
> + spin_unlock(&lck);
> }
>
> - P1(int *x, int *y, int *lck)
> + void CPU1(void)
> {
> - int r0;
> - int r1;
> - int r2;
> -
> - spin_lock(lck);
> - r0 = READ_ONCE(*x);
> - r1 = READ_ONCE(*x);
> - r2 = atomic_inc_return(y);
> - spin_unlock(lck);
> + spin_lock(&lck);
> + r0 = READ_ONCE(x);
> + r1 = READ_ONCE(x);
> + r2 = atomic_inc_return(&y);
> + spin_unlock(&lck);
> }
>
> - locations [x;lck;0:r2;1:r0;1:r1;1:r2]
> - filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
> + filter (1:r0=0 /\ 1:r1=1)
> exists (1:r2=1)
>
> -If "1:r0" is equal to "0", "1:r1" can never equal "1" because P0()
> -cannot update "x" while P1() holds the lock. And herd7 confirms this,
> +If "1:r0" is equal to "0", "1:r1" can never equal "1" because CPU0()
> +cannot update "x" while CPU1() holds the lock. And herd7 confirms this,
> showing zero executions matching the "filter" criteria.
>
> And this is why Linux-kernel lock and unlock primitives must prevent
>
>
>
On Thu, 23 Mar 2023 11:52:15 -0700, Paul E. McKenney wrote:
> On Thu, Mar 23, 2023 at 11:52:57AM +0900, Akira Yokosawa wrote:
>> Hi Paul,
>>
>> On Mon, 20 Mar 2023 18:05:19 -0700, Paul E. McKenney wrote:
>>> Most Linux-kernel uses of locking are straightforward, but there are
>>> corner-case uses that rely on less well-known aspects of the lock and
>>> unlock primitives. This commit therefore adds a locking.txt and litmus
>>> tests in Documentation/litmus-tests/locking to explain these corner-case
>>> uses.
>>>
>>> Signed-off-by: Paul E. McKenney <[email protected]>
>>> ---
>>> .../litmus-tests/locking/DCL-broken.litmus | 55 +++
>>> .../litmus-tests/locking/DCL-fixed.litmus | 56 +++
>>> .../litmus-tests/locking/RM-broken.litmus | 42 +++
>>> .../litmus-tests/locking/RM-fixed.litmus | 42 +++
>>> tools/memory-model/Documentation/locking.txt | 320 ++++++++++++++++++
>>
>> I think the documentation needs adjustment to cope with Andrea's change
>> of litmus tests.
>>
>> Also, coding style of code snippets taken from litmus tests look somewhat
>> inconsistent with other snippets taken from MP+... litmus tests:
>>
>> - Simple function signature such as "void CPU0(void)".
>> - No declaration of local variables.
>> - Indirection level of global variables.
>> - No "locations" clause
>>
>> How about applying the diff below?
>
> Good eyes, thank you! I will fold this in with attribution.
Feel free to add
Reviewed-by: Akira Yokosawa <[email protected]>
Thanks, Akira
>
> Thanx, Paul
>
>> Thanks, Akira
On Fri, Mar 24, 2023 at 08:30:38AM +0900, Akira Yokosawa wrote:
> On Thu, 23 Mar 2023 11:52:15 -0700, Paul E. McKenney wrote:
> > On Thu, Mar 23, 2023 at 11:52:57AM +0900, Akira Yokosawa wrote:
> >> Hi Paul,
> >>
> >> On Mon, 20 Mar 2023 18:05:19 -0700, Paul E. McKenney wrote:
> >>> Most Linux-kernel uses of locking are straightforward, but there are
> >>> corner-case uses that rely on less well-known aspects of the lock and
> >>> unlock primitives. This commit therefore adds a locking.txt and litmus
> >>> tests in Documentation/litmus-tests/locking to explain these corner-case
> >>> uses.
> >>>
> >>> Signed-off-by: Paul E. McKenney <[email protected]>
> >>> ---
> >>> .../litmus-tests/locking/DCL-broken.litmus | 55 +++
> >>> .../litmus-tests/locking/DCL-fixed.litmus | 56 +++
> >>> .../litmus-tests/locking/RM-broken.litmus | 42 +++
> >>> .../litmus-tests/locking/RM-fixed.litmus | 42 +++
> >>> tools/memory-model/Documentation/locking.txt | 320 ++++++++++++++++++
> >>
> >> I think the documentation needs adjustment to cope with Andrea's change
> >> of litmus tests.
> >>
> >> Also, coding style of code snippets taken from litmus tests look somewhat
> >> inconsistent with other snippets taken from MP+... litmus tests:
> >>
> >> - Simple function signature such as "void CPU0(void)".
> >> - No declaration of local variables.
> >> - Indirection level of global variables.
> >> - No "locations" clause
> >>
> >> How about applying the diff below?
> >
> > Good eyes, thank you! I will fold this in with attribution.
>
> Feel free to add
>
> Reviewed-by: Akira Yokosawa <[email protected]>
Thank you, I will apply on my next full rebase.
Thanx, Paul