Additional proposed changes to LKMM
cover Additional proposed changes to LKMM
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(-)
RFC PATCH 1/5 EXP tools/memory-model: Add scripts to test memory model
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.
--- 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
tools/memory-model/litmus-tests/.gitignore new file +1 -0
@@ -0,0 +1 @@ +*.litmus.out
tools/memory-model/scripts/checkalllitmus.sh new file +73 -0
73 lines not on this page · raw message
tools/memory-model/scripts/checklitmus.sh new file +86 -0
86 lines not on this page · raw message
Signature · 1 line
2.5.2
RFC PATCH 2/5 tools/memory-model: Add litmus test for multicopy atomicity
In reply to Paul E. McKenneyThis 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.
--- .../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 +31 -0
@@ -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)
Signature · 1 line
2.5.2
RFC PATCH 3/5 EXP tools/memory-model: Add .cfg and .cat files for s390
In reply to Paul E. McKenneyThis 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.
--- 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
tools/memory-model/s390.cat new file +18 -0
@@ -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
tools/memory-model/s390.cfg new file +21 -0
@@ -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
Signature · 1 line
2.5.2
RFC PATCH 5/5 EXP tools/memory-model: Flag "cumulativity" and "propagation" tests
In reply to Paul E. McKenneyThis commit flags WRC+pooncerelease+rmbonceonce+Once.litmus as being forbidden by LKMM cumulativity and IRIW+mbonceonces+OnceOnce.litmus as being forbidden by LKMM propagation.
--- 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(-)
tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus +1 -1
@@ -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. *) {}
tools/memory-model/litmus-tests/README +6 -3
@@ -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
tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus +3 -1
@@ -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. *) {}
Signature · 1 line
2.5.2
RFC PATCH 4/5 tools/memory-model: Add model support for spin_is_locked
In reply to Paul E. McKenneyFrom: 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.
--- 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
@@ -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
@@ -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 +29 -0
@@ -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)
tools/memory-model/litmus-tests/README +10 -0
@@ -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 +49 -4
76 lines not on this page · raw message
Signature · 1 line
2.5.2
Re: [PATCH RFC tools/memory-model 2/5] tools/memory-model: Add litmus test for multicopy atomicity
In reply to Paul E. McKenneyQuoted 11 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.
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 28 lines
tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus new file +21
-0@@ -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)
tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus line 31
Quoted 10 lines
tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus new file +10
-0+{ + 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
Quoted 3 lines
Signature · 1 line
2.5.2
Re: [PATCH RFC tools/memory-model 4/5] tools/memory-model: Add model support for spin_is_locked
In reply to Paul E. McKenneyQuoted 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 withCONFIG_DEBUG_SPINLOCK=n, in whichspin_is_locked()unconditionally returns zero.It also adds a pair of litmus tests demonstrating the minimal ordering provided by
spin_is_locked()in conjunction withspin_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 83 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.litmustools/memory-model/linux-kernel.def +1
-0@@ -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@@ -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@@ -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/MP+polockonce+poacquiresilsil.litmus line 29
Quoted 10 lines
tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus new file +10
-0+} + +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).
Quoted 65 lines
tools/memory-model/litmus-tests/README +10
-0@@ -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@@ -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 7 lines
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 let all-possible-rfe-lf = · line 112
Quoted 10 lines
tools/memory-model/lock.cat +10
-0+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
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
Re: [PATCH RFC tools/memory-model 2/5] tools/memory-model: Add litmus test for multicopy atomicity
In reply to Andrea ParriQuoted 6 lines · Andrea Parri
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 8 lines
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.litmusWe seem to be missing an entry in litmus-tests/README...
We are, and I will add one once ...
Quoted 31 lines
Quoted 31 lines
tools/memory-model/litmus-tests/SB+poonceoncescoh.litmus new file +25
-0@@ -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; +
Quoted 8 lines
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?
... 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
In reply to Andrea ParriQuoted 36 lines · Andrea Parri
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 withCONFIG_DEBUG_SPINLOCK=n, in whichspin_is_locked()unconditionally returns zero.It also adds a pair of litmus tests demonstrating the minimal ordering provided by
spin_is_locked()in conjunction withspin_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]>
Quoted 2 lines
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 [email protected]" 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! ;-)
Quoted 87 lines
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.litmustools/memory-model/linux-kernel.def +1
-0@@ -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@@ -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@@ -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;
Quoted 8 lines
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).
Ah, that is a bit non-standard, isn't it? Fixed!
Quoted 78 lines
Quoted 65 lines
tools/memory-model/litmus-tests/README +10
-0@@ -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@@ -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
Quoted 4 lines
(*
* 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.
Quoted 11 lines
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 *) +
Quoted 8 lines
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
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?
Quoted 4 lines
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 ^^^^
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
Quoted 17 lines
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