Additional proposed changes to LKMM

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 <[email protected]>

Signed-off-by Paul E. McKenney <[email protected]>

---
 .../litmus-tests/SB+poonceoncescoh.litmus          | 31 ++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus

tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus new file +21 -0

new file mode 100644
index 000000000000..991a2d6dec63
@@ -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)

Signature · 1 line

2.5.2

Quoted 5 lines · 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.

Quoted 6 lines

Suggested-by Alan Stern <[email protected]>

Signed-off-by Paul E. McKenney <[email protected]>

---
 .../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...

Quoted 31 lines

tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus new file +25 -0

new file mode 100644
index 000000000000..991a2d6dec63
@@ -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;
+

tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus line 31

Quoted 6 lines

tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus new file +6 -0

+	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?

From: Luc Maranget <[email protected]>

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/[email protected]

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

Signed-off-by Luc Maranget <[email protected]>

Cc Alan Stern <[email protected]>

Cc Will Deacon <[email protected]>

Cc Peter Zijlstra <[email protected]>

Cc Boqun Feng <[email protected]>

Cc Nicholas Piggin <[email protected]>

Cc David Howells <[email protected]>

Cc Jade Alglave <[email protected]>

Cc Luc Maranget <[email protected]>

Cc "Paul E. McKenney" <[email protected]>

Cc Akira Yokosawa <[email protected]>

Cc Ingo Molnar <[email protected]>

Signed-off-by Paul E. McKenney <[email protected]>

---
 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

tools/memory-model/linux-kernel.def +1 -0

index 6bd3bc431b3d..f0553bd37c08 100644
@@ -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}; }

tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus new file +30 -0

new file mode 100644
index 000000000000..37357404a08d
@@ -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)

tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus new file +19 -0

new file mode 100644
index 000000000000..ebc2668f95ff
@@ -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);

tools/memory-model/litmus-tests/README +10 -0

index 04096fb8b8d9..6919909bbd0f 100644
@@ -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.

tools/memory-model/lock.cat +13 -4

index ba4a4ec6d313..3b1439edc818 100644
@@ -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
+

tools/memory-model/lock.cat +7 -0

+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)

tools/memory-model/lock.cat +7 -0

+  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]) |

Signature · 1 line

2.5.2

Quoted 21 lines · Paul E. McKenney

From: Luc Maranget <[email protected]>

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/[email protected]

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

Quoted 13 lines

Signed-off-by Luc Maranget <[email protected]>

Cc Alan Stern <[email protected]>

Cc Will Deacon <[email protected]>

Cc Peter Zijlstra <[email protected]>

Cc Boqun Feng <[email protected]>

Cc Nicholas Piggin <[email protected]>

Cc David Howells <[email protected]>

Cc Jade Alglave <[email protected]>

Cc Luc Maranget <[email protected]>

Cc "Paul E. McKenney" <[email protected]>

Cc Akira Yokosawa <[email protected]>

Cc Ingo Molnar <[email protected]>

Signed-off-by Paul E. McKenney <[email protected]>

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

Quoted 87 lines

---
 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

tools/memory-model/linux-kernel.def +1 -0

index 6bd3bc431b3d..f0553bd37c08 100644
@@ -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}; }

tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus new file +30 -0

new file mode 100644
index 000000000000..37357404a08d
@@ -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)

tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus new file +23 -0

new file mode 100644
index 000000000000..ebc2668f95ff
@@ -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;

tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus line 29

Quoted 6 lines

tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus new file +6 -0

+	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).

Quoted 65 lines

tools/memory-model/litmus-tests/README +10 -0

index 04096fb8b8d9..6919909bbd0f 100644
@@ -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.

tools/memory-model/lock.cat +13 -4

index ba4a4ec6d313..3b1439edc818 100644
@@ -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
+

tools/memory-model/lock.cat let all-possible-rfe-lf = · line 95

Quoted 10 lines

tools/memory-model/lock.cat +10 -0

+(* 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
*)

Quoted 11 lines

tools/memory-model/lock.cat +11 -0

+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 *)
+

tools/memory-model/lock.cat let all-possible-rfe-lf = · line 112

Quoted 6 lines

tools/memory-model/lock.cat +6 -0

+(* 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

tools/memory-model/lock.cat let all-possible-rfe-lf = · line 114

Quoted 2 lines

tools/memory-model/lock.cat +2 -0

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

spaces around binary operators ^^^^

Andrea

Quoted 13 lines

tools/memory-model/lock.cat +7 -0

+  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]) |

Signature · 1 line

2.5.2