[PATCH RFC tools/memory-model 0/5] Additional proposed changes to LKMM

[PATCH RFC tools/memory-model 0/5] Additional proposed changes to LKMM

[Paul E. McKenney]

Hello!

This series contains a few additional changes to tools/memory-model,
however, the members of this series need more discussion and feedback
before they are ready for inclusion.

1.	Add LKMM test scripts.

2.	Add litmus test for full-up multicopy atomicity.

3.	Add experimental .cfg and .cat files for s390.  These are for
	expository purposes only, and would more likely be included in
	the herd tool than in the Linux kernel.

4.	Add LKMM support for spin_is_locked(), courtesy of Luc Maranget.
	It has been suggested that spin_is_locked() be removed from the
	kernel, but in the meantime we should at least have a definition
	of what it does.

5.	Flag litmus test demonstrating the A-cumulativity of
	smp_store_release() and LKMM's propagation rule.

							Thanx, Paul

------------------------------------------------------------------------

 linux-kernel.def                                       |    1 
 litmus-tests/.gitignore                                |    1 
 litmus-tests/IRIW+mbonceonces+OnceOnce.litmus          |    2 
 litmus-tests/MP+polockmbonce+poacquiresilsil.litmus    |   30 +++++
 litmus-tests/MP+polockonce+poacquiresilsil.litmus      |   29 +++++
 litmus-tests/README                                    |   19 +++
 litmus-tests/SB+poonceoncescoh.litmus                  |   31 ++++++
 litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus |    4 
 lock.cat                                               |   53 +++++++++-
 s390.cat                                               |   18 +++
 s390.cfg                                               |   21 ++++
 scripts/checkalllitmus.sh                              |   73 ++++++++++++++
 scripts/checklitmus.sh                                 |   86 +++++++++++++++++
 13 files changed, 359 insertions(+), 9 deletions(-)

[PATCH RFC tools/memory-model 1/5] EXP tools/memory-model: Add scripts to test memory model

[Paul E. McKenney]

This commit adds a pair of scripts that run the memory model on litmus
tests, checking that the verification result of each litmus test matches
the result flagged in the litmus test itself.  These scripts permit easier
checking of changes to the memory model against preconceived notions.

Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 tools/memory-model/litmus-tests/.gitignore   |  1 +
 tools/memory-model/scripts/checkalllitmus.sh | 73 +++++++++++++++++++++++
 tools/memory-model/scripts/checklitmus.sh    | 86 ++++++++++++++++++++++++++++
 3 files changed, 160 insertions(+)
 create mode 100644 tools/memory-model/litmus-tests/.gitignore
 create mode 100755 tools/memory-model/scripts/checkalllitmus.sh
 create mode 100755 tools/memory-model/scripts/checklitmus.sh

diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore
new file mode 100644
index 000000000000..6e2ddc54152f
--- /dev/null
+++ b/tools/memory-model/litmus-tests/.gitignore
@@ -0,0 +1 @@
+*.litmus.out
diff --git a/tools/memory-model/scripts/checkalllitmus.sh b/tools/memory-model/scripts/checkalllitmus.sh
new file mode 100755
index 000000000000..af0aa15ab84e
--- /dev/null
+++ b/tools/memory-model/scripts/checkalllitmus.sh
@@ -0,0 +1,73 @@
+#!/bin/sh
+#
+# Run herd tests on all .litmus files in the specified directory (which
+# defaults to litmus-tests) and check each file's result against a "Result:"
+# comment within that litmus test.  If the verification result does not
+# match that specified in the litmus test, this script prints an error
+# message prefixed with "^^^".  It also outputs verification results to
+# a file whose name is that of the specified litmus test, but with ".out"
+# appended.
+#
+# Usage:
+#	sh checkalllitmus.sh [ directory ]
+#
+# The LINUX_HERD_OPTIONS environment variable may be used to specify
+# arguments to herd, whose default is defined by the checklitmus.sh script.
+# Thus, one would normally run this in the directory containing the memory
+# model, specifying the pathname of the litmus test to check.
+#
+# This script makes no attempt to run the litmus tests concurrently.
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program; if not, you can access it online at
+# http://www.gnu.org/licenses/gpl-2.0.html.
+#
+# Copyright IBM Corporation, 2018
+#
+# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
+
+litmusdir=${1-litmus-tests}
+if test -d "$litmusdir" -a -r "$litmusdir" -a -x "$litmusdir"
+then
+	:
+else
+	echo ' --- ' error: $litmusdir is not an accessible directory
+	exit 255
+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 litmus-tests/*.litmus
+do
+	if ! $clscript $i
+	then
+		ret=1
+	fi
+done
+if test "$ret" -ne 0
+then
+	echo " ^^^ VERIFICATION MISMATCHES"
+else
+	echo All litmus tests verified as was expected.
+fi
+exit $ret
diff --git a/tools/memory-model/scripts/checklitmus.sh b/tools/memory-model/scripts/checklitmus.sh
new file mode 100755
index 000000000000..e2e477472844
--- /dev/null
+++ b/tools/memory-model/scripts/checklitmus.sh
@@ -0,0 +1,86 @@
+#!/bin/sh
+#
+# Run a herd test and check the result against a "Result:" comment within
+# the litmus test.  If the verification result does not match that specified
+# in the litmus test, this script prints an error message prefixed with
+# "^^^" and exits with a non-zero status.  It also outputs verification
+# results to a file whose name is that of the specified litmus test, but
+# with ".out" appended.
+#
+# Usage:
+#	sh checklitmus.sh file.litmus
+#
+# The LINUX_HERD_OPTIONS environment variable may be used to specify
+# arguments to herd, which default to "-conf linux-kernel.cfg".  Thus,
+# one would normally run this in the directory containing the memory model,
+# specifying the pathname of the litmus test to check.
+#
+# This program is free software; you can redistribute it and/or modify
+# it under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program; if not, you can access it online at
+# http://www.gnu.org/licenses/gpl-2.0.html.
+#
+# Copyright IBM Corporation, 2018
+#
+# Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
+
+litmus=$1
+herdoptions=${LINUX_HERD_OPTIONS--conf linux-kernel.cfg}
+
+if test -f "$litmus" -a -r "$litmus"
+then
+	:
+else
+	echo ' --- ' error: \"$litmus\" is not a readable file
+	exit 255
+fi
+if grep -q '^ \* Result: ' $litmus
+then
+	outcome=`grep -m 1 '^ \* Result: ' $litmus | awk '{ print $3 }'`
+else
+	outcome=specified
+fi
+
+echo Herd options: $herdoptions > $litmus.out
+/usr/bin/time herd7 -o ~/tmp $herdoptions $litmus >> $litmus.out 2>&1
+grep "Herd options:" $litmus.out
+grep '^Observation' $litmus.out
+if grep -q '^Observation' $litmus.out
+then
+	:
+else
+	cat $litmus.out
+	echo ' ^^^ Verification error'
+	echo ' ^^^ Verification error' >> $litmus.out 2>&1
+	exit 255
+fi
+if test "$outcome" = DEADLOCK
+then
+	echo grep 3 and 4
+	if grep '^Observation' $litmus.out | grep -q 'Never 0 0$'
+	then
+		ret=0
+	else
+		echo " ^^^ Unexpected non-$outcome verification"
+		echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
+		ret=1
+	fi
+elif grep '^Observation' $litmus.out | grep -q $outcome || test "$outcome" = Maybe
+then
+	ret=0
+else
+	echo " ^^^ Unexpected non-$outcome verification"
+	echo " ^^^ Unexpected non-$outcome verification" >> $litmus.out 2>&1
+	ret=1
+fi
+tail -2 $litmus.out | head -1
+exit $ret
-- 
2.5.2

[PATCH RFC tools/memory-model 2/5] tools/memory-model: Add litmus test for multicopy atomicity

[Paul E. McKenney]

This commit adds a litmus test suggested by Alan Stern that is forbidden
on multicopy atomic systems, but allowed on non-multicopy atomic systems.
Note that other-multicopy atomic systems are examples of non-multicopy
atomic systems.

Suggested-by: Alan Stern <stern@rowland.harvard.edu>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 .../litmus-tests/SB+poonceoncescoh.litmus          | 31 ++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus

diff --git a/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus b/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus
new file mode 100644
index 000000000000..991a2d6dec63
--- /dev/null
+++ b/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus
@@ -0,0 +1,31 @@
+C SB+poonceoncescoh
+
+(*
+ * Result: Sometimes
+ *
+ * This litmus test demonstrates that LKMM is not multicopy atomic.
+ *)
+
+{}
+
+P0(int *x, int *y)
+{
+	int r1;
+	int r2;
+
+	WRITE_ONCE(*x, 1);
+	r1 = READ_ONCE(*x);
+	r2 = READ_ONCE(*y);
+}
+
+P1(int *x, int *y)
+{
+	int r3;
+	int r4;
+
+	WRITE_ONCE(*y, 1);
+	r3 = READ_ONCE(*y);
+	r4 = READ_ONCE(*x);
+}
+
+exists (0:r2=0 /\ 1:r4=0 /\ 0:r1=1 /\ 1:r3=1)
-- 
2.5.2

[PATCH RFC tools/memory-model 3/5] EXP tools/memory-model: Add .cfg and .cat files for s390

[Paul E. McKenney]

This commit adds s390.cat and s390.cfg files to allow users to check
litmus tests for s390-specific code.  Note that this change only enables
herd7 checking of C-language litmus tests.  Larger changes are required
to enable the litmus7 and klitmus7 tools to check litmus tests on real
hardare.

Suggested-by: Martin Schwidefsky <schwidefsky@de.ibm.com>
Suggested-by: Christian Borntraeger <borntraeger@de.ibm.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
[ paulmck: Add fixes suggested by Alan Stern. ]
---
 tools/memory-model/s390.cat | 18 ++++++++++++++++++
 tools/memory-model/s390.cfg | 21 +++++++++++++++++++++
 2 files changed, 39 insertions(+)
 create mode 100644 tools/memory-model/s390.cat
 create mode 100644 tools/memory-model/s390.cfg

diff --git a/tools/memory-model/s390.cat b/tools/memory-model/s390.cat
new file mode 100644
index 000000000000..216bf33d3ffe
--- /dev/null
+++ b/tools/memory-model/s390.cat
@@ -0,0 +1,18 @@
+s390
+
+include "fences.cat"
+include "cos.cat"
+
+(* Fundamental coherence ordering *)
+let com = rf | co | fr
+acyclic po-loc | com as coherence
+
+(* Atomic *)
+empty rmw & (fre;coe) as atom
+
+(* Fences *)
+let mb = [M] ; fencerel(Mb) ; [M]
+
+(* TSO with multicopy atomicity (tso-mca) *)
+let po-ghb = ([R] ; po ; [M]) | ([M] ; po ; [W])
+acyclic mb | po-ghb | fr | rf | co as tso-mca
diff --git a/tools/memory-model/s390.cfg b/tools/memory-model/s390.cfg
new file mode 100644
index 000000000000..d77e05d2395c
--- /dev/null
+++ b/tools/memory-model/s390.cfg
@@ -0,0 +1,21 @@
+macros linux-kernel.def
+bell linux-kernel.bell
+model s390.cat
+graph columns
+squished true
+showevents noregs
+movelabel true
+fontsize 8
+xscale 2.0
+yscale 1.5
+arrowsize 0.8
+showinitrf false
+showfinalrf false
+showinitwrites false
+splines spline
+pad 0.1
+edgeattr hb,color,indigo
+edgeattr co,color,blue
+edgeattr mb,color,darkgreen
+edgeattr wmb,color,darkgreen
+edgeattr rmb,color,darkgreen
-- 
2.5.2

[PATCH RFC tools/memory-model 4/5] tools/memory-model: Add model support for spin_is_locked

[Paul E. McKenney]

From: Luc Maranget <Luc.Maranget@inria.fr>

This commit first adds a trivial macro for spin_is_locked() to
linux-kernel.def.

It also adds cat code for enumerating all possible matches of lock
write events (set LKW) with islocked events returning true (set RL,
for Read from Lock), and unlock write events (set UL) with islocked
events returning false (set RU, for Read from Unlock).  Note that this
intentionally does not model uniprocessor kernels (CONFIG_SMP=n) built
with CONFIG_DEBUG_SPINLOCK=n, in which spin_is_locked() unconditionally
returns zero.

It also adds a pair of litmus tests demonstrating the minimal ordering
provided by spin_is_locked() in conjunction with spin_lock().  Will Deacon
noted that this minimal ordering happens on ARMv8:
https://lkml.kernel.org/r/20180226162426.GB17158@arm.com

Notice that herd7 installations strictly older than version 7.49
do not handle the new constructs.

Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will.deacon@arm.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Ingo Molnar <mingo@redhat.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
---
 tools/memory-model/linux-kernel.def                |  1 +
 .../MP+polockmbonce+poacquiresilsil.litmus         | 30 ++++++++++++
 .../MP+polockonce+poacquiresilsil.litmus           | 29 ++++++++++++
 tools/memory-model/litmus-tests/README             | 10 ++++
 tools/memory-model/lock.cat                        | 53 ++++++++++++++++++++--
 5 files changed, 119 insertions(+), 4 deletions(-)
 create mode 100644 tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
 create mode 100644 tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus

diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index 6bd3bc431b3d..f0553bd37c08 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -38,6 +38,7 @@ cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W)
 spin_lock(X) { __lock(X); }
 spin_unlock(X) { __unlock(X); }
 spin_trylock(X) __trylock(X)
+spin_is_locked(X) __islocked(X)
 
 // RCU
 rcu_read_lock() { __fence{rcu-lock}; }
diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
new file mode 100644
index 000000000000..37357404a08d
--- /dev/null
+++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
@@ -0,0 +1,30 @@
+C MP+polockmbonce+poacquiresilsil
+
+(*
+ * Result: Never
+ *
+ * Do spinlocks combined with smp_mb__after_spinlock() provide order
+ * to outside observers using spin_is_locked() to sense the lock-held
+ * state, ordered by acquire?  Note that when the first spin_is_locked()
+ * returns false and the second true, we know that the smp_load_acquire()
+ * executed before the lock was acquired (loosely speaking).
+ *)
+
+{
+}
+
+P0 (spinlock_t *lo, int *x) {
+	spin_lock(lo);
+	smp_mb__after_spinlock();
+	WRITE_ONCE(*x,1);
+	spin_unlock(lo);
+}
+
+P1 (spinlock_t *lo, int *x) {
+	int r1; int r2; int r3;
+	r1 = smp_load_acquire(x);
+        r2 = spin_is_locked(lo);
+	r3 = spin_is_locked(lo);
+}
+
+exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
new file mode 100644
index 000000000000..ebc2668f95ff
--- /dev/null
+++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
@@ -0,0 +1,29 @@
+C MP+polockonce+poacquiresilsil
+
+(*
+ * Result: Sometimes
+ *
+ * Do spinlocks provide order to outside observers using spin_is_locked()
+ * to sense the lock-held state, ordered by acquire?  Note that when the
+ * first spin_is_locked() returns false and the second true, we know that
+ * the smp_load_acquire() executed before the lock was acquired (loosely
+ * speaking).
+ *)
+
+{
+}
+
+P0 (spinlock_t *lo, int *x) {
+	spin_lock(lo);
+	WRITE_ONCE(*x,1);
+	spin_unlock(lo);
+}
+
+P1 (spinlock_t *lo, int *x) {
+	int r1; int r2; int r3;
+	r1 = smp_load_acquire(x);
+        r2 = spin_is_locked(lo);
+	r3 = spin_is_locked(lo);
+}
+
+exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 04096fb8b8d9..6919909bbd0f 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -63,6 +63,16 @@ LB+poonceonces.litmus
 MP+onceassign+derefonce.litmus
 	As below, but with rcu_assign_pointer() and an rcu_dereference().
 
+MP+polockmbonce+poacquiresilsil.litmus
+	Protect the access with a lock and an smp_mb__after_spinlock()
+	in one process, and use an acquire load followed by a pair of
+	spin_is_locked() calls in the other process.
+
+MP+polockonce+poacquiresilsil.litmus
+	Protect the access with a lock in one process, and use an
+	acquire load followed by a pair of spin_is_locked() calls
+	in the other process.
+
 MP+polocks.litmus
 	As below, but with the second access of the writer process
 	and the first access of reader process protected by a lock.
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
index ba4a4ec6d313..3b1439edc818 100644
--- a/tools/memory-model/lock.cat
+++ b/tools/memory-model/lock.cat
@@ -5,7 +5,11 @@
  *)
 
 (* Generate coherence orders and handle lock operations *)
-
+(*
+ * Warning, crashes with herd7 versions strictly before 7.48.
+ * spin_islocked is functional from version 7.49.
+ *
+ *)
 include "cross.cat"
 
 (* From lock reads to their partner lock writes *)
@@ -32,12 +36,16 @@ flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
 (* The final value of a spinlock should not be tested *)
 flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
 
-
+(*
+ * Backward compatibility
+ *)
+let RL = try RL with emptyset (* defined herd7 >= 7.49 *)
+let RU = try RU with emptyset (* defined herd7 >= 7.49 *)
 (*
  * Put lock operations in their appropriate classes, but leave UL out of W
  * until after the co relation has been generated.
  *)
-let R = R | LKR | LF
+let R = R | LKR | LF | RL | RU
 let W = W | LKW
 
 let Release = Release | UL
@@ -72,8 +80,45 @@ let all-possible-rfe-lf =
 
 (* Generate all rf relations for LF events *)
 with rfe-lf from cross(all-possible-rfe-lf)
-let rf = rf | rfi-lf | rfe-lf
 
+let rf-lf = rfe-lf | rfi-lf
+
+(* rf for RL events, ie islocked returning true, similar to LF above *)
+
+(* islocked returning true inside a critical section
+ * must read from the opening lock
+ *)
+let rfi-rl = ([LKW] ; po-loc ; [RL]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
+
+(* islocked returning true outside critical sections can match any
+ * external lock.
+ *)
+let all-possible-rfe-rl =
+  let possible-rfe-lf r =
+    let pair-to-relation p = p ++ 0
+    in map pair-to-relation ((LKW * {r}) & loc & ext)
+  in map possible-rfe-lf (RL \ range(rfi-rl))
+
+with rfe-rl from cross(all-possible-rfe-rl)
+let rf-rl = rfe-rl | rfi-rl
+
+(* Read from unlock, ie islocked returning false, slightly different *)
+
+(* islocked returning false can read from the last po-previous unlock *)
+let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
+
+(* any islocked returning false can read from any external unlock *)
+let all-possible-rfe-ru =
+   let possible-rfe-ru r =
+     let pair-to-relation p = p ++ 0
+     in map pair-to-relation (((UL|IW) * {r}) & loc & ext)
+  in map possible-rfe-ru RU
+
+with rfe-ru from cross(all-possible-rfe-ru)
+let rf-ru = rfe-ru | rfi-ru
+
+(* Final rf relation *)
+let rf = rf | rf-lf | rf-rl | rf-ru
 
 (* Generate all co relations, including LKW events but not UL *)
 let co0 = co0 | ([IW] ; loc ; [LKW]) |
-- 
2.5.2

[PATCH RFC tools/memory-model 5/5] EXP tools/memory-model: Flag "cumulativity" and "propagation" tests

[Paul E. McKenney]

This commit flags WRC+pooncerelease+rmbonceonce+Once.litmus as being
forbidden by LKMM cumulativity and IRIW+mbonceonces+OnceOnce.litmus as
being forbidden by LKMM propagation.

Reported-by: Paolo Bonzini <pbonzini@redhat.com>
Suggested-by: Andrea Parri <andrea.parri@amarulasolutions.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
[ paulmck: Updated wording as suggested by Alan Stern. ]
---
 tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus | 2 +-
 tools/memory-model/litmus-tests/README                           | 9 ++++++---
 .../litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus       | 4 +++-
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
index 50d5db9ea983..98a3716efa37 100644
--- a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
+++ b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus
@@ -7,7 +7,7 @@ C IRIW+mbonceonces+OnceOnce
  * between each pairs of reads.  In other words, is smp_mb() sufficient to
  * cause two different reading processes to agree on the order of a pair
  * of writes, where each write is to a different variable by a different
- * process?
+ * process?  This litmus test exercises LKMM's "propagation" rule.
  *)
 
 {}
diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
index 6919909bbd0f..17eb9a8c222d 100644
--- a/tools/memory-model/litmus-tests/README
+++ b/tools/memory-model/litmus-tests/README
@@ -23,7 +23,8 @@ IRIW+mbonceonces+OnceOnce.litmus
 	between each pairs of reads.  In other words, is smp_mb()
 	sufficient to cause two different reading processes to agree on
 	the order of a pair of writes, where each write is to a different
-	variable by a different process?
+	variable by a different process?  This litmus test is forbidden
+	by LKMM's propagation rule.
 
 IRIW+poonceonces+OnceOnce.litmus
 	Test of independent reads from independent writes with nothing
@@ -119,8 +120,10 @@ S+wmbonceonce+poacquireonce.litmus
 
 WRC+poonceonces+Once.litmus
 WRC+pooncerelease+rmbonceonce+Once.litmus
-	These two are members of an extension of the MP litmus-test class
-	in which the first write is moved to a separate process.
+	These two are members of an extension of the MP litmus-test
+	class in which the first write is moved to a separate process.
+	The second is forbidden because smp_store_release() is
+	A-cumulative in LKMM.
 
 Z6.0+pooncelock+pooncelock+pombonce.litmus
 	Is the ordering provided by a spin_unlock() and a subsequent
diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
index 97fcbffde9a0..ad3448b941e6 100644
--- a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
+++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus
@@ -5,7 +5,9 @@ C WRC+pooncerelease+rmbonceonce+Once
  *
  * This litmus test is an extension of the message-passing pattern, where
  * the first write is moved to a separate process.  Because it features
- * a release and a read memory barrier, it should be forbidden.
+ * a release and a read memory barrier, it should be forbidden.  More
+ * specifically, this litmus test is forbidden because smp_store_release()
+ * is A-cumulative in LKMM.
  *)
 
 {}
-- 
2.5.2

Re: [PATCH RFC tools/memory-model 2/5] tools/memory-model: Add litmus test for multicopy atomicity

[Andrea Parri]

On Mon, Apr 16, 2018 at 09:22:48AM -0700, Paul E. McKenney wrote:
> This commit adds a litmus test suggested by Alan Stern that is forbidden
> on multicopy atomic systems, but allowed on non-multicopy atomic systems.
> Note that other-multicopy atomic systems are examples of non-multicopy
> atomic systems.
> 
> Suggested-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> ---
>  .../litmus-tests/SB+poonceoncescoh.litmus          | 31 ++++++++++++++++++++++
>  1 file changed, 31 insertions(+)
>  create mode 100644 tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus

We seem to be missing an entry in litmus-tests/README...


> 
> diff --git a/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus b/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus
> new file mode 100644
> index 000000000000..991a2d6dec63
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus
> @@ -0,0 +1,31 @@
> +C SB+poonceoncescoh
> +
> +(*
> + * Result: Sometimes
> + *
> + * This litmus test demonstrates that LKMM is not multicopy atomic.
> + *)
> +
> +{}
> +
> +P0(int *x, int *y)
> +{
> +	int r1;
> +	int r2;
> +
> +	WRITE_ONCE(*x, 1);
> +	r1 = READ_ONCE(*x);
> +	r2 = READ_ONCE(*y);
> +}
> +
> +P1(int *x, int *y)
> +{
> +	int r3;
> +	int r4;
> +
> +	WRITE_ONCE(*y, 1);
> +	r3 = READ_ONCE(*y);
> +	r4 = READ_ONCE(*x);
> +}
> +
> +exists (0:r2=0 /\ 1:r4=0 /\ 0:r1=1 /\ 1:r3=1)

This test has a normalised name:  why don't use that?

  Andrea


> -- 
> 2.5.2
> 

Re: [PATCH RFC tools/memory-model 4/5] tools/memory-model: Add model support for spin_is_locked

[Andrea Parri]

On Mon, Apr 16, 2018 at 09:22:50AM -0700, Paul E. McKenney wrote:
> From: Luc Maranget <Luc.Maranget@inria.fr>
> 
> This commit first adds a trivial macro for spin_is_locked() to
> linux-kernel.def.
> 
> It also adds cat code for enumerating all possible matches of lock
> write events (set LKW) with islocked events returning true (set RL,
> for Read from Lock), and unlock write events (set UL) with islocked
> events returning false (set RU, for Read from Unlock).  Note that this
> intentionally does not model uniprocessor kernels (CONFIG_SMP=n) built
> with CONFIG_DEBUG_SPINLOCK=n, in which spin_is_locked() unconditionally
> returns zero.
> 
> It also adds a pair of litmus tests demonstrating the minimal ordering
> provided by spin_is_locked() in conjunction with spin_lock().  Will Deacon
> noted that this minimal ordering happens on ARMv8:
> https://lkml.kernel.org/r/20180226162426.GB17158@arm.com
> 
> Notice that herd7 installations strictly older than version 7.49
> do not handle the new constructs.
> 
> Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
> Cc: Alan Stern <stern@rowland.harvard.edu>
> Cc: Will Deacon <will.deacon@arm.com>
> Cc: Peter Zijlstra <peterz@infradead.org>
> Cc: Boqun Feng <boqun.feng@gmail.com>
> Cc: Nicholas Piggin <npiggin@gmail.com>
> Cc: David Howells <dhowells@redhat.com>
> Cc: Jade Alglave <j.alglave@ucl.ac.uk>
> Cc: Luc Maranget <luc.maranget@inria.fr>
> Cc: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
> Cc: Akira Yokosawa <akiyks@gmail.com>
> Cc: Ingo Molnar <mingo@redhat.com>
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>

I understand that it's acceptable to not list all maintainers in the
commit message, but that does look like an omission...


> ---
>  tools/memory-model/linux-kernel.def                |  1 +
>  .../MP+polockmbonce+poacquiresilsil.litmus         | 30 ++++++++++++
>  .../MP+polockonce+poacquiresilsil.litmus           | 29 ++++++++++++
>  tools/memory-model/litmus-tests/README             | 10 ++++
>  tools/memory-model/lock.cat                        | 53 ++++++++++++++++++++--
>  5 files changed, 119 insertions(+), 4 deletions(-)
>  create mode 100644 tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
>  create mode 100644 tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> 
> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> index 6bd3bc431b3d..f0553bd37c08 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -38,6 +38,7 @@ cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W)
>  spin_lock(X) { __lock(X); }
>  spin_unlock(X) { __unlock(X); }
>  spin_trylock(X) __trylock(X)
> +spin_is_locked(X) __islocked(X)
>  
>  // RCU
>  rcu_read_lock() { __fence{rcu-lock}; }
> diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> new file mode 100644
> index 000000000000..37357404a08d
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> @@ -0,0 +1,30 @@
> +C MP+polockmbonce+poacquiresilsil
> +
> +(*
> + * Result: Never
> + *
> + * Do spinlocks combined with smp_mb__after_spinlock() provide order
> + * to outside observers using spin_is_locked() to sense the lock-held
> + * state, ordered by acquire?  Note that when the first spin_is_locked()
> + * returns false and the second true, we know that the smp_load_acquire()
> + * executed before the lock was acquired (loosely speaking).
> + *)
> +
> +{
> +}
> +
> +P0 (spinlock_t *lo, int *x) {
> +	spin_lock(lo);
> +	smp_mb__after_spinlock();
> +	WRITE_ONCE(*x,1);
> +	spin_unlock(lo);
> +}
> +
> +P1 (spinlock_t *lo, int *x) {
> +	int r1; int r2; int r3;
> +	r1 = smp_load_acquire(x);
> +        r2 = spin_is_locked(lo);
> +	r3 = spin_is_locked(lo);
> +}
> +
> +exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
> diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> new file mode 100644
> index 000000000000..ebc2668f95ff
> --- /dev/null
> +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> @@ -0,0 +1,29 @@
> +C MP+polockonce+poacquiresilsil
> +
> +(*
> + * Result: Sometimes
> + *
> + * Do spinlocks provide order to outside observers using spin_is_locked()
> + * to sense the lock-held state, ordered by acquire?  Note that when the
> + * first spin_is_locked() returns false and the second true, we know that
> + * the smp_load_acquire() executed before the lock was acquired (loosely
> + * speaking).
> + *)
> +
> +{
> +}
> +
> +P0 (spinlock_t *lo, int *x) {
> +	spin_lock(lo);
> +	WRITE_ONCE(*x,1);
> +	spin_unlock(lo);
> +}
> +
> +P1 (spinlock_t *lo, int *x) {
> +	int r1; int r2; int r3;
> +	r1 = smp_load_acquire(x);
> +        r2 = spin_is_locked(lo);
> +	r3 = spin_is_locked(lo);
> +}
> +
> +exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)

Please fix the style in the above litmus tests (c.f., e.g., your 2/5).


> diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> index 04096fb8b8d9..6919909bbd0f 100644
> --- a/tools/memory-model/litmus-tests/README
> +++ b/tools/memory-model/litmus-tests/README
> @@ -63,6 +63,16 @@ LB+poonceonces.litmus
>  MP+onceassign+derefonce.litmus
>  	As below, but with rcu_assign_pointer() and an rcu_dereference().
>  
> +MP+polockmbonce+poacquiresilsil.litmus
> +	Protect the access with a lock and an smp_mb__after_spinlock()
> +	in one process, and use an acquire load followed by a pair of
> +	spin_is_locked() calls in the other process.
> +
> +MP+polockonce+poacquiresilsil.litmus
> +	Protect the access with a lock in one process, and use an
> +	acquire load followed by a pair of spin_is_locked() calls
> +	in the other process.
> +
>  MP+polocks.litmus
>  	As below, but with the second access of the writer process
>  	and the first access of reader process protected by a lock.
> diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> index ba4a4ec6d313..3b1439edc818 100644
> --- a/tools/memory-model/lock.cat
> +++ b/tools/memory-model/lock.cat
> @@ -5,7 +5,11 @@
>   *)
>  
>  (* Generate coherence orders and handle lock operations *)
> -
> +(*
> + * Warning, crashes with herd7 versions strictly before 7.48.
> + * spin_islocked is functional from version 7.49.
> + *
> + *)
>  include "cross.cat"
>  
>  (* From lock reads to their partner lock writes *)
> @@ -32,12 +36,16 @@ flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
>  (* The final value of a spinlock should not be tested *)
>  flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
>  
> -
> +(*
> + * Backward compatibility
> + *)
> +let RL = try RL with emptyset (* defined herd7 >= 7.49 *)
> +let RU = try RU with emptyset (* defined herd7 >= 7.49 *)
>  (*
>   * Put lock operations in their appropriate classes, but leave UL out of W
>   * until after the co relation has been generated.
>   *)
> -let R = R | LKR | LF
> +let R = R | LKR | LF | RL | RU
>  let W = W | LKW
>  
>  let Release = Release | UL
> @@ -72,8 +80,45 @@ let all-possible-rfe-lf =
>  
>  (* Generate all rf relations for LF events *)
>  with rfe-lf from cross(all-possible-rfe-lf)
> -let rf = rf | rfi-lf | rfe-lf
>  
> +let rf-lf = rfe-lf | rfi-lf
> +
> +(* rf for RL events, ie islocked returning true, similar to LF above *)
> +
> +(* islocked returning true inside a critical section
> + * must read from the opening lock
> + *)
> +let rfi-rl = ([LKW] ; po-loc ; [RL]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
> +
> +(* islocked returning true outside critical sections can match any
> + * external lock.
> + *)

multi-lines comments are

(*
 * line
 * line
 *)


> +let all-possible-rfe-rl =
> +  let possible-rfe-lf r =
> +    let pair-to-relation p = p ++ 0
> +    in map pair-to-relation ((LKW * {r}) & loc & ext)
> +  in map possible-rfe-lf (RL \ range(rfi-rl))
> +
> +with rfe-rl from cross(all-possible-rfe-rl)
> +let rf-rl = rfe-rl | rfi-rl
> +
> +(* Read from unlock, ie islocked returning false, slightly different *)
> +
> +(* islocked returning false can read from the last po-previous unlock *)
> +let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
> +
> +(* any islocked returning false can read from any external unlock *)
> +let all-possible-rfe-ru =
> +   let possible-rfe-ru r =

please fix the alignment/indentation


> +     let pair-to-relation p = p ++ 0
> +     in map pair-to-relation (((UL|IW) * {r}) & loc & ext)

spaces around binary operators  ^^^^

  Andrea


> +  in map possible-rfe-ru RU
> +
> +with rfe-ru from cross(all-possible-rfe-ru)
> +let rf-ru = rfe-ru | rfi-ru
> +
> +(* Final rf relation *)
> +let rf = rf | rf-lf | rf-rl | rf-ru
>  
>  (* Generate all co relations, including LKW events but not UL *)
>  let co0 = co0 | ([IW] ; loc ; [LKW]) |
> -- 
> 2.5.2
> 

Re: [PATCH RFC tools/memory-model 2/5] tools/memory-model: Add litmus test for multicopy atomicity

[Paul E. McKenney]

On Wed, Apr 18, 2018 at 11:40:33AM +0200, Andrea Parri wrote:
> On Mon, Apr 16, 2018 at 09:22:48AM -0700, Paul E. McKenney wrote:
> > This commit adds a litmus test suggested by Alan Stern that is forbidden
> > on multicopy atomic systems, but allowed on non-multicopy atomic systems.
> > Note that other-multicopy atomic systems are examples of non-multicopy
> > atomic systems.
> > 
> > Suggested-by: Alan Stern <stern@rowland.harvard.edu>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> > ---
> >  .../litmus-tests/SB+poonceoncescoh.litmus          | 31 ++++++++++++++++++++++
> >  1 file changed, 31 insertions(+)
> >  create mode 100644 tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus
> 
> We seem to be missing an entry in litmus-tests/README...

We are, and I will add one once ...

> > diff --git a/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus b/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus
> > new file mode 100644
> > index 000000000000..991a2d6dec63
> > --- /dev/null
> > +++ b/tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus
> > @@ -0,0 +1,31 @@
> > +C SB+poonceoncescoh
> > +
> > +(*
> > + * Result: Sometimes
> > + *
> > + * This litmus test demonstrates that LKMM is not multicopy atomic.
> > + *)
> > +
> > +{}
> > +
> > +P0(int *x, int *y)
> > +{
> > +	int r1;
> > +	int r2;
> > +
> > +	WRITE_ONCE(*x, 1);
> > +	r1 = READ_ONCE(*x);
> > +	r2 = READ_ONCE(*y);
> > +}
> > +
> > +P1(int *x, int *y)
> > +{
> > +	int r3;
> > +	int r4;
> > +
> > +	WRITE_ONCE(*y, 1);
> > +	r3 = READ_ONCE(*y);
> > +	r4 = READ_ONCE(*x);
> > +}
> > +
> > +exists (0:r2=0 /\ 1:r4=0 /\ 0:r1=1 /\ 1:r3=1)
> 
> This test has a normalised name:  why don't use that?

... we come to agreement on the documentation on how to produce a
normalized name given a standard litmus test.

Ditto for the tests whose names include the string "silsil", but
those involve locking so might be considered lower priority.

							Thanx, Paul

Re: [PATCH RFC tools/memory-model 4/5] tools/memory-model: Add model support for spin_is_locked

[Paul E. McKenney]

On Wed, Apr 18, 2018 at 11:57:59AM +0200, Andrea Parri wrote:
> On Mon, Apr 16, 2018 at 09:22:50AM -0700, Paul E. McKenney wrote:
> > From: Luc Maranget <Luc.Maranget@inria.fr>
> > 
> > This commit first adds a trivial macro for spin_is_locked() to
> > linux-kernel.def.
> > 
> > It also adds cat code for enumerating all possible matches of lock
> > write events (set LKW) with islocked events returning true (set RL,
> > for Read from Lock), and unlock write events (set UL) with islocked
> > events returning false (set RU, for Read from Unlock).  Note that this
> > intentionally does not model uniprocessor kernels (CONFIG_SMP=n) built
> > with CONFIG_DEBUG_SPINLOCK=n, in which spin_is_locked() unconditionally
> > returns zero.
> > 
> > It also adds a pair of litmus tests demonstrating the minimal ordering
> > provided by spin_is_locked() in conjunction with spin_lock().  Will Deacon
> > noted that this minimal ordering happens on ARMv8:
> > https://lkml.kernel.org/r/20180226162426.GB17158@arm.com
> > 
> > Notice that herd7 installations strictly older than version 7.49
> > do not handle the new constructs.
> > 
> > Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
> > Cc: Alan Stern <stern@rowland.harvard.edu>
> > Cc: Will Deacon <will.deacon@arm.com>
> > Cc: Peter Zijlstra <peterz@infradead.org>
> > Cc: Boqun Feng <boqun.feng@gmail.com>
> > Cc: Nicholas Piggin <npiggin@gmail.com>
> > Cc: David Howells <dhowells@redhat.com>
> > Cc: Jade Alglave <j.alglave@ucl.ac.uk>
> > Cc: Luc Maranget <luc.maranget@inria.fr>
> > Cc: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
> > Cc: Akira Yokosawa <akiyks@gmail.com>
> > Cc: Ingo Molnar <mingo@redhat.com>
> > Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
> 
> I understand that it's acceptable to not list all maintainers in the
> commit message, but that does look like an omission...

One that is corrected by the "--cc parri.andrea@gmail.com" I give to
"git send-email", so people will not be able to slide submissions past
you using this mechanism.  But I had to rebase anyway, so I added
your "Cc:".  So now you are doubly covered!  ;-)

> > ---
> >  tools/memory-model/linux-kernel.def                |  1 +
> >  .../MP+polockmbonce+poacquiresilsil.litmus         | 30 ++++++++++++
> >  .../MP+polockonce+poacquiresilsil.litmus           | 29 ++++++++++++
> >  tools/memory-model/litmus-tests/README             | 10 ++++
> >  tools/memory-model/lock.cat                        | 53 ++++++++++++++++++++--
> >  5 files changed, 119 insertions(+), 4 deletions(-)
> >  create mode 100644 tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> >  create mode 100644 tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> > 
> > diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
> > index 6bd3bc431b3d..f0553bd37c08 100644
> > --- a/tools/memory-model/linux-kernel.def
> > +++ b/tools/memory-model/linux-kernel.def
> > @@ -38,6 +38,7 @@ cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W)
> >  spin_lock(X) { __lock(X); }
> >  spin_unlock(X) { __unlock(X); }
> >  spin_trylock(X) __trylock(X)
> > +spin_is_locked(X) __islocked(X)
> >  
> >  // RCU
> >  rcu_read_lock() { __fence{rcu-lock}; }
> > diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> > new file mode 100644
> > index 000000000000..37357404a08d
> > --- /dev/null
> > +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
> > @@ -0,0 +1,30 @@
> > +C MP+polockmbonce+poacquiresilsil
> > +
> > +(*
> > + * Result: Never
> > + *
> > + * Do spinlocks combined with smp_mb__after_spinlock() provide order
> > + * to outside observers using spin_is_locked() to sense the lock-held
> > + * state, ordered by acquire?  Note that when the first spin_is_locked()
> > + * returns false and the second true, we know that the smp_load_acquire()
> > + * executed before the lock was acquired (loosely speaking).
> > + *)
> > +
> > +{
> > +}
> > +
> > +P0 (spinlock_t *lo, int *x) {
> > +	spin_lock(lo);
> > +	smp_mb__after_spinlock();
> > +	WRITE_ONCE(*x,1);
> > +	spin_unlock(lo);
> > +}
> > +
> > +P1 (spinlock_t *lo, int *x) {
> > +	int r1; int r2; int r3;
> > +	r1 = smp_load_acquire(x);
> > +        r2 = spin_is_locked(lo);
> > +	r3 = spin_is_locked(lo);
> > +}
> > +
> > +exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
> > diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> > new file mode 100644
> > index 000000000000..ebc2668f95ff
> > --- /dev/null
> > +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus
> > @@ -0,0 +1,29 @@
> > +C MP+polockonce+poacquiresilsil
> > +
> > +(*
> > + * Result: Sometimes
> > + *
> > + * Do spinlocks provide order to outside observers using spin_is_locked()
> > + * to sense the lock-held state, ordered by acquire?  Note that when the
> > + * first spin_is_locked() returns false and the second true, we know that
> > + * the smp_load_acquire() executed before the lock was acquired (loosely
> > + * speaking).
> > + *)
> > +
> > +{
> > +}
> > +
> > +P0 (spinlock_t *lo, int *x) {
> > +	spin_lock(lo);
> > +	WRITE_ONCE(*x,1);
> > +	spin_unlock(lo);
> > +}
> > +
> > +P1 (spinlock_t *lo, int *x) {
> > +	int r1; int r2; int r3;
> > +	r1 = smp_load_acquire(x);
> > +        r2 = spin_is_locked(lo);
> > +	r3 = spin_is_locked(lo);
> > +}
> > +
> > +exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
> 
> Please fix the style in the above litmus tests (c.f., e.g., your 2/5).

Ah, that is a bit non-standard, isn't it?  Fixed!

> > diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README
> > index 04096fb8b8d9..6919909bbd0f 100644
> > --- a/tools/memory-model/litmus-tests/README
> > +++ b/tools/memory-model/litmus-tests/README
> > @@ -63,6 +63,16 @@ LB+poonceonces.litmus
> >  MP+onceassign+derefonce.litmus
> >  	As below, but with rcu_assign_pointer() and an rcu_dereference().
> >  
> > +MP+polockmbonce+poacquiresilsil.litmus
> > +	Protect the access with a lock and an smp_mb__after_spinlock()
> > +	in one process, and use an acquire load followed by a pair of
> > +	spin_is_locked() calls in the other process.
> > +
> > +MP+polockonce+poacquiresilsil.litmus
> > +	Protect the access with a lock in one process, and use an
> > +	acquire load followed by a pair of spin_is_locked() calls
> > +	in the other process.
> > +
> >  MP+polocks.litmus
> >  	As below, but with the second access of the writer process
> >  	and the first access of reader process protected by a lock.
> > diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
> > index ba4a4ec6d313..3b1439edc818 100644
> > --- a/tools/memory-model/lock.cat
> > +++ b/tools/memory-model/lock.cat
> > @@ -5,7 +5,11 @@
> >   *)
> >  
> >  (* Generate coherence orders and handle lock operations *)
> > -
> > +(*
> > + * Warning, crashes with herd7 versions strictly before 7.48.
> > + * spin_islocked is functional from version 7.49.
> > + *
> > + *)
> >  include "cross.cat"
> >  
> >  (* From lock reads to their partner lock writes *)
> > @@ -32,12 +36,16 @@ flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
> >  (* The final value of a spinlock should not be tested *)
> >  flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
> >  
> > -
> > +(*
> > + * Backward compatibility
> > + *)
> > +let RL = try RL with emptyset (* defined herd7 >= 7.49 *)
> > +let RU = try RU with emptyset (* defined herd7 >= 7.49 *)
> >  (*
> >   * Put lock operations in their appropriate classes, but leave UL out of W
> >   * until after the co relation has been generated.
> >   *)
> > -let R = R | LKR | LF
> > +let R = R | LKR | LF | RL | RU
> >  let W = W | LKW
> >  
> >  let Release = Release | UL
> > @@ -72,8 +80,45 @@ let all-possible-rfe-lf =
> >  
> >  (* Generate all rf relations for LF events *)
> >  with rfe-lf from cross(all-possible-rfe-lf)
> > -let rf = rf | rfi-lf | rfe-lf
> >  
> > +let rf-lf = rfe-lf | rfi-lf
> > +
> > +(* rf for RL events, ie islocked returning true, similar to LF above *)
> > +
> > +(* islocked returning true inside a critical section
> > + * must read from the opening lock
> > + *)
> > +let rfi-rl = ([LKW] ; po-loc ; [RL]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
> > +
> > +(* islocked returning true outside critical sections can match any
> > + * external lock.
> > + *)
> 
> multi-lines comments are
> 
> (*
>  * line
>  * line
>  *)

Last I knew, Linus was actually OK with the style above, or at least
the C-language equivalent.  But might as well make these consistent with
the rest of them.

> > +let all-possible-rfe-rl =
> > +  let possible-rfe-lf r =
> > +    let pair-to-relation p = p ++ 0
> > +    in map pair-to-relation ((LKW * {r}) & loc & ext)
> > +  in map possible-rfe-lf (RL \ range(rfi-rl))
> > +
> > +with rfe-rl from cross(all-possible-rfe-rl)
> > +let rf-rl = rfe-rl | rfi-rl
> > +
> > +(* Read from unlock, ie islocked returning false, slightly different *)
> > +
> > +(* islocked returning false can read from the last po-previous unlock *)
> > +let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
> > +
> > +(* any islocked returning false can read from any external unlock *)
> > +let all-possible-rfe-ru =
> > +   let possible-rfe-ru r =
> 
> please fix the alignment/indentation

Hmmm...  Three-space indentation vs. the two-space indentation that was
already in the file, both of which are different than the single-tab
indentation in linux-kernel.cat as well as elsewhere in the kernel.

Left to myself, I would convert this to single-tab indentation.

What to people think?

> > +     let pair-to-relation p = p ++ 0
> > +     in map pair-to-relation (((UL|IW) * {r}) & loc & ext)
> 
> spaces around binary operators  ^^^^

It now looks like this:

	in map pair-to-relation (((UL | IW) * {r}) & loc & ext)

Or it would, except that this conflicts with one of Alan's later patches.
I don't trust myself to resolve this conflict at the moment, but would
be happy to try it on a day when I haven't been beating my head on
Linux-kernel RCU continuously (it actually seems to be working now,
which must mean some mistake somewhere...).  If there is agreement that
this spacing change is the way we should go, of course.

Thoughts?

							Thanx, Paul

>   Andrea
> 
> 
> > +  in map possible-rfe-ru RU
> > +
> > +with rfe-ru from cross(all-possible-rfe-ru)
> > +let rf-ru = rfe-ru | rfi-ru
> > +
> > +(* Final rf relation *)
> > +let rf = rf | rf-lf | rf-rl | rf-ru
> >  
> >  (* Generate all co relations, including LKW events but not UL *)
> >  let co0 = co0 | ([IW] ; loc ; [LKW]) |
> > -- 
> > 2.5.2
> > 
>