Skip to content

Commit

Permalink
Merge branch 'for-mingo-lkmm' of git://git.kernel.org/pub/scm/linux/k…
Browse files Browse the repository at this point in the history
…ernel/git/paulmck/linux-rcu into locking/core

Pull LKMM updates from Paul E. McKenney.

Signed-off-by: Ingo Molnar <mingo@kernel.org>
  • Loading branch information
Ingo Molnar committed Feb 12, 2021
2 parents c11878f + 3d5c703 commit 3765d01
Showing 34 changed files with 42 additions and 138 deletions.
12 changes: 9 additions & 3 deletions tools/memory-model/Documentation/glossary.txt
Original file line number Diff line number Diff line change
@@ -33,10 +33,11 @@ Acquire: With respect to a lock, acquiring that lock, for example,
acquire loads.

When an acquire load returns the value stored by a release store
to that same variable, then all operations preceding that store
happen before any operations following that load acquire.
to that same variable, (in other words, the acquire load "reads
from" the release store), then all operations preceding that
store "happen before" any operations following that load acquire.

See also "Relaxed" and "Release".
See also "Happens-Before", "Reads-From", "Relaxed", and "Release".

Coherence (co): When one CPU's store to a given variable overwrites
either the value from another CPU's store or some later value,
@@ -119,6 +120,11 @@ Fully Ordered: An operation such as smp_mb() that orders all of
that orders all of its CPU's prior accesses, itself, and
all of its CPU's subsequent accesses.

Happens-Before (hb): A relation between two accesses in which LKMM
guarantees the first access precedes the second. For more
detail, please see the "THE HAPPENS-BEFORE RELATION: hb"
section of explanation.txt.

Marked Access: An access to a variable that uses an special function or
macro such as "r1 = READ_ONCE(x)" or "smp_store_release(&a, 1)".

2 changes: 1 addition & 1 deletion tools/memory-model/README
Original file line number Diff line number Diff line change
@@ -51,7 +51,7 @@ klitmus7 Compatibility Table
============ ==========
target Linux herdtools7
------------ ----------
-- 4.18 7.48 --
-- 4.14 7.48 --
4.15 -- 4.19 7.49 --
4.20 -- 5.5 7.54 --
5.6 -- 7.56 --
4 changes: 1 addition & 3 deletions tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus
Original file line number Diff line number Diff line change
@@ -7,9 +7,7 @@ C CoRR+poonceonce+Once
* reads from the same variable are ordered.
*)

{
int x;
}
{}

P0(int *x)
{
4 changes: 1 addition & 3 deletions tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus
Original file line number Diff line number Diff line change
@@ -7,9 +7,7 @@ C CoRW+poonceonce+Once
* a given variable and a later write to that same variable are ordered.
*)

{
int x;
}
{}

P0(int *x)
{
4 changes: 1 addition & 3 deletions tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus
Original file line number Diff line number Diff line change
@@ -7,9 +7,7 @@ C CoWR+poonceonce+Once
* given variable and a later read from that same variable are ordered.
*)

{
int x;
}
{}

P0(int *x)
{
4 changes: 1 addition & 3 deletions tools/memory-model/litmus-tests/CoWW+poonceonce.litmus
Original file line number Diff line number Diff line change
@@ -7,9 +7,7 @@ C CoWW+poonceonce
* writes to the same variable are ordered.
*)

{
int x;
}
{}

P0(int *x)
{
Original file line number Diff line number Diff line change
@@ -10,10 +10,7 @@ C IRIW+fencembonceonces+OnceOnce
* process? This litmus test exercises LKMM's "propagation" rule.
*)

{
int x;
int y;
}
{}

P0(int *x)
{
Original file line number Diff line number Diff line change
@@ -10,10 +10,7 @@ C IRIW+poonceonces+OnceOnce
* different process?
*)

{
int x;
int y;
}
{}

P0(int *x)
{
Original file line number Diff line number Diff line change
@@ -7,12 +7,7 @@ C ISA2+pooncelock+pooncelock+pombonce
* (in P0() and P1()) is visible to external process P2().
*)

{
spinlock_t mylock;
int x;
int y;
int z;
}
{}

P0(int *x, int *y, spinlock_t *mylock)
{
6 changes: 1 addition & 5 deletions tools/memory-model/litmus-tests/ISA2+poonceonces.litmus
Original file line number Diff line number Diff line change
@@ -9,11 +9,7 @@ C ISA2+poonceonces
* of the smp_load_acquire() invocations are replaced by READ_ONCE()?
*)

{
int x;
int y;
int z;
}
{}

P0(int *x, int *y)
{
Original file line number Diff line number Diff line change
@@ -11,11 +11,7 @@ C ISA2+pooncerelease+poacquirerelease+poacquireonce
* (AKA non-rf) link, so release-acquire is all that is needed.
*)

{
int x;
int y;
int z;
}
{}

P0(int *x, int *y)
{
Original file line number Diff line number Diff line change
@@ -11,10 +11,7 @@ C LB+fencembonceonce+ctrlonceonce
* another control dependency and order would still be maintained.)
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
Original file line number Diff line number Diff line change
@@ -8,10 +8,7 @@ C LB+poacquireonce+pooncerelease
* to the other?
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
5 changes: 1 addition & 4 deletions tools/memory-model/litmus-tests/LB+poonceonces.litmus
Original file line number Diff line number Diff line change
@@ -7,10 +7,7 @@ C LB+poonceonces
* be prevented even with no explicit ordering?
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
Original file line number Diff line number Diff line change
@@ -8,10 +8,7 @@ C MP+fencewmbonceonce+fencermbonceonce
* is usually better to use smp_store_release() and smp_load_acquire().
*)

{
int buf;
int flag;
}
{}

P0(int *buf, int *flag) // Producer
{
Original file line number Diff line number Diff line change
@@ -10,9 +10,7 @@ C MP+onceassign+derefonce
*)

{
int *p=y;
int x;
int y=0;
p=y;
}

P0(int *x, int **p) // Producer
Original file line number Diff line number Diff line change
@@ -10,10 +10,7 @@ C MP+polockmbonce+poacquiresilsil
* executed before the lock was acquired (loosely speaking).
*)

{
spinlock_t lo;
int x;
}
{}

P0(spinlock_t *lo, int *x) // Producer
{
Original file line number Diff line number Diff line change
@@ -10,10 +10,7 @@ C MP+polockonce+poacquiresilsil
* speaking).
*)

{
spinlock_t lo;
int x;
}
{}

P0(spinlock_t *lo, int *x) // Producer
{
6 changes: 1 addition & 5 deletions tools/memory-model/litmus-tests/MP+polocks.litmus
Original file line number Diff line number Diff line change
@@ -11,11 +11,7 @@ C MP+polocks
* to see all prior accesses by those other CPUs.
*)

{
spinlock_t mylock;
int buf;
int flag;
}
{}

P0(int *buf, int *flag, spinlock_t *mylock) // Producer
{
5 changes: 1 addition & 4 deletions tools/memory-model/litmus-tests/MP+poonceonces.litmus
Original file line number Diff line number Diff line change
@@ -7,10 +7,7 @@ C MP+poonceonces
* no ordering at all?
*)

{
int buf;
int flag;
}
{}

P0(int *buf, int *flag) // Producer
{
Original file line number Diff line number Diff line change
@@ -8,10 +8,7 @@ C MP+pooncerelease+poacquireonce
* pattern.
*)

{
int buf;
int flag;
}
{}

P0(int *buf, int *flag) // Producer
{
6 changes: 1 addition & 5 deletions tools/memory-model/litmus-tests/MP+porevlocks.litmus
Original file line number Diff line number Diff line change
@@ -11,11 +11,7 @@ C MP+porevlocks
* see all prior accesses by those other CPUs.
*)

{
spinlock_t mylock;
int buf;
int flag;
}
{}

P0(int *buf, int *flag, spinlock_t *mylock) // Consumer
{
5 changes: 1 addition & 4 deletions tools/memory-model/litmus-tests/R+fencembonceonces.litmus
Original file line number Diff line number Diff line change
@@ -9,10 +9,7 @@ C R+fencembonceonces
* cause the resulting test to be allowed.
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
5 changes: 1 addition & 4 deletions tools/memory-model/litmus-tests/R+poonceonces.litmus
Original file line number Diff line number Diff line change
@@ -8,10 +8,7 @@ C R+poonceonces
* store propagation delays.
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
Original file line number Diff line number Diff line change
@@ -7,10 +7,7 @@ C S+fencewmbonceonce+poacquireonce
* store against a subsequent store?
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
5 changes: 1 addition & 4 deletions tools/memory-model/litmus-tests/S+poonceonces.litmus
Original file line number Diff line number Diff line change
@@ -9,10 +9,7 @@ C S+poonceonces
* READ_ONCE(), is ordering preserved?
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
5 changes: 1 addition & 4 deletions tools/memory-model/litmus-tests/SB+fencembonceonces.litmus
Original file line number Diff line number Diff line change
@@ -9,10 +9,7 @@ C SB+fencembonceonces
* suffice, but not much else.)
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
5 changes: 1 addition & 4 deletions tools/memory-model/litmus-tests/SB+poonceonces.litmus
Original file line number Diff line number Diff line change
@@ -8,10 +8,7 @@ C SB+poonceonces
* variable that the preceding process reads.
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
Original file line number Diff line number Diff line change
@@ -6,10 +6,7 @@ C SB+rfionceonce-poonceonces
* This litmus test demonstrates that LKMM is not fully multicopy atomic.
*)

{
int x;
int y;
}
{}

P0(int *x, int *y)
{
5 changes: 1 addition & 4 deletions tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus
Original file line number Diff line number Diff line change
@@ -8,10 +8,7 @@ C WRC+poonceonces+Once
* test has no ordering at all.
*)

{
int x;
int y;
}
{}

P0(int *x)
{
Original file line number Diff line number Diff line change
@@ -10,10 +10,7 @@ C WRC+pooncerelease+fencermbonceonce+Once
* is A-cumulative in LKMM.
*)

{
int x;
int y;
}
{}

P0(int *x)
{
Original file line number Diff line number Diff line change
@@ -9,12 +9,7 @@ C Z6.0+pooncelock+poonceLock+pombonce
* by CPUs not holding that lock.
*)

{
spinlock_t mylock;
int x;
int y;
int z;
}
{}

P0(int *x, int *y, spinlock_t *mylock)
{
Loading

0 comments on commit 3765d01

Please sign in to comment.