diff options
Diffstat (limited to 'tools/memory-model/litmus-tests')
13 files changed, 157 insertions, 53 deletions
diff --git a/tools/memory-model/litmus-tests/.gitignore b/tools/memory-model/litmus-tests/.gitignore index c492a1ddad91..19c379cf069d 100644 --- a/tools/memory-model/litmus-tests/.gitignore +++ b/tools/memory-model/litmus-tests/.gitignore @@ -1,2 +1,2 @@ # SPDX-License-Identifier: GPL-2.0-only -*.litmus.out +*.litmus.* diff --git a/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus new file mode 100644 index 000000000000..eb34123a6ffe --- /dev/null +++ b/tools/memory-model/litmus-tests/LB+unlocklockonceonce+poacquireonce.litmus @@ -0,0 +1,35 @@ +C LB+unlocklockonceonce+poacquireonce + +(* + * Result: Never + * + * If two locked critical sections execute on the same CPU, all accesses + * in the first must execute before any accesses in the second, even if the + * critical sections are protected by different locks. Note: Even when a + * write executes before a read, their memory effects can be reordered from + * the viewpoint of another CPU (the kind of reordering allowed by TSO). + *) + +{} + +P0(spinlock_t *s, spinlock_t *t, int *x, int *y) +{ + int r1; + + spin_lock(s); + r1 = READ_ONCE(*x); + spin_unlock(s); + spin_lock(t); + WRITE_ONCE(*y, 1); + spin_unlock(t); +} + +P1(int *x, int *y) +{ + int r2; + + r2 = smp_load_acquire(y); + WRITE_ONCE(*x, 1); +} + +exists (0:r1=1 /\ 1:r2=1) diff --git a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus index a273da9faa6d..f8ca1229857a 100644 --- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus +++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus @@ -10,21 +10,21 @@ C MP+fencewmbonceonce+fencermbonceonce {} -P0(int *x, int *y) +P0(int *buf, int *flag) // Producer { - WRITE_ONCE(*x, 1); + WRITE_ONCE(*buf, 1); smp_wmb(); - WRITE_ONCE(*y, 1); + WRITE_ONCE(*flag, 1); } -P1(int *x, int *y) +P1(int *buf, int *flag) // Consumer { int r0; int r1; - r0 = READ_ONCE(*y); + r0 = READ_ONCE(*flag); smp_rmb(); - r1 = READ_ONCE(*x); + r1 = READ_ONCE(*buf); } -exists (1:r0=1 /\ 1:r1=0) +exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *) diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus index 97731b4bbdd8..d84160b9c1ae 100644 --- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus +++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus @@ -10,25 +10,24 @@ C MP+onceassign+derefonce *) { -y=z; -z=0; +p=y; } -P0(int *x, int **y) +P0(int *x, int **p) // Producer { WRITE_ONCE(*x, 1); - rcu_assign_pointer(*y, x); + rcu_assign_pointer(*p, x); } -P1(int *x, int **y) +P1(int *x, int **p) // Consumer { int *r0; int r1; rcu_read_lock(); - r0 = rcu_dereference(*y); + r0 = rcu_dereference(*p); r1 = READ_ONCE(*r0); rcu_read_unlock(); } -exists (1:r0=x /\ 1:r1=0) +exists (1:r0=x /\ 1:r1=0) (* Bad outcome. *) diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus index 50f4d62bbf0e..ba91cc63e148 100644 --- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus @@ -10,10 +10,9 @@ C MP+polockmbonce+poacquiresilsil * executed before the lock was acquired (loosely speaking). *) -{ -} +{} -P0(spinlock_t *lo, int *x) +P0(spinlock_t *lo, int *x) // Producer { spin_lock(lo); smp_mb__after_spinlock(); @@ -21,7 +20,7 @@ P0(spinlock_t *lo, int *x) spin_unlock(lo); } -P1(spinlock_t *lo, int *x) +P1(spinlock_t *lo, int *x) // Consumer { int r1; int r2; @@ -32,4 +31,4 @@ P1(spinlock_t *lo, int *x) r3 = spin_is_locked(lo); } -exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) +exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *) diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus index abf81e7a0895..a5ea3ed8f52e 100644 --- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus @@ -10,17 +10,16 @@ C MP+polockonce+poacquiresilsil * speaking). *) -{ -} +{} -P0(spinlock_t *lo, int *x) +P0(spinlock_t *lo, int *x) // Producer { spin_lock(lo); WRITE_ONCE(*x, 1); spin_unlock(lo); } -P1(spinlock_t *lo, int *x) +P1(spinlock_t *lo, int *x) // Consumer { int r1; int r2; @@ -31,4 +30,4 @@ P1(spinlock_t *lo, int *x) r3 = spin_is_locked(lo); } -exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) +exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *) diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus index 712a4fcdf6ce..e6af05f70069 100644 --- a/tools/memory-model/litmus-tests/MP+polocks.litmus +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus @@ -13,23 +13,23 @@ C MP+polocks {} -P0(int *x, int *y, spinlock_t *mylock) +P0(int *buf, int *flag, spinlock_t *mylock) // Producer { - WRITE_ONCE(*x, 1); + WRITE_ONCE(*buf, 1); spin_lock(mylock); - WRITE_ONCE(*y, 1); + WRITE_ONCE(*flag, 1); spin_unlock(mylock); } -P1(int *x, int *y, spinlock_t *mylock) +P1(int *buf, int *flag, spinlock_t *mylock) // Consumer { int r0; int r1; spin_lock(mylock); - r0 = READ_ONCE(*y); + r0 = READ_ONCE(*flag); spin_unlock(mylock); - r1 = READ_ONCE(*x); + r1 = READ_ONCE(*buf); } -exists (1:r0=1 /\ 1:r1=0) +exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *) diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus index 172f0145301c..ba9c99c6cf65 100644 --- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus @@ -9,19 +9,19 @@ C MP+poonceonces {} -P0(int *x, int *y) +P0(int *buf, int *flag) // Producer { - WRITE_ONCE(*x, 1); - WRITE_ONCE(*y, 1); + WRITE_ONCE(*buf, 1); + WRITE_ONCE(*flag, 1); } -P1(int *x, int *y) +P1(int *buf, int *flag) // Consumer { int r0; int r1; - r0 = READ_ONCE(*y); - r1 = READ_ONCE(*x); + r0 = READ_ONCE(*flag); + r1 = READ_ONCE(*buf); } -exists (1:r0=1 /\ 1:r1=0) +exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *) diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus index d52c68429722..f174bfe61702 100644 --- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus +++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus @@ -10,19 +10,19 @@ C MP+pooncerelease+poacquireonce {} -P0(int *x, int *y) +P0(int *buf, int *flag) // Producer { - WRITE_ONCE(*x, 1); - smp_store_release(y, 1); + WRITE_ONCE(*buf, 1); + smp_store_release(flag, 1); } -P1(int *x, int *y) +P1(int *buf, int *flag) // Consumer { int r0; int r1; - r0 = smp_load_acquire(y); - r1 = READ_ONCE(*x); + r0 = smp_load_acquire(flag); + r1 = READ_ONCE(*buf); } -exists (1:r0=1 /\ 1:r1=0) +exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *) diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus index 72c9276b363e..b9599141160e 100644 --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus @@ -13,23 +13,23 @@ C MP+porevlocks {} -P0(int *x, int *y, spinlock_t *mylock) +P0(int *buf, int *flag, spinlock_t *mylock) // Consumer { int r0; int r1; - r0 = READ_ONCE(*y); + r0 = READ_ONCE(*flag); spin_lock(mylock); - r1 = READ_ONCE(*x); + r1 = READ_ONCE(*buf); spin_unlock(mylock); } -P1(int *x, int *y, spinlock_t *mylock) +P1(int *buf, int *flag, spinlock_t *mylock) // Producer { spin_lock(mylock); - WRITE_ONCE(*x, 1); + WRITE_ONCE(*buf, 1); spin_unlock(mylock); - WRITE_ONCE(*y, 1); + WRITE_ONCE(*flag, 1); } -exists (0:r0=1 /\ 0:r1=0) +exists (0:r0=1 /\ 0:r1=0) (* Bad outcome. *) diff --git a/tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus new file mode 100644 index 000000000000..2feb1398be71 --- /dev/null +++ b/tools/memory-model/litmus-tests/MP+unlocklockonceonce+fencermbonceonce.litmus @@ -0,0 +1,33 @@ +C MP+unlocklockonceonce+fencermbonceonce + +(* + * Result: Never + * + * If two locked critical sections execute on the same CPU, stores in the + * first must propagate to each CPU before stores in the second do, even if + * the critical sections are protected by different locks. + *) + +{} + +P0(spinlock_t *s, spinlock_t *t, int *x, int *y) +{ + spin_lock(s); + WRITE_ONCE(*x, 1); + spin_unlock(s); + spin_lock(t); + WRITE_ONCE(*y, 1); + spin_unlock(t); +} + +P1(int *x, int *y) +{ + int r1; + int r2; + + r1 = READ_ONCE(*y); + smp_rmb(); + r2 = READ_ONCE(*x); +} + +exists (1:r1=1 /\ 1:r2=0) diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README index 681f9067fa9e..d311a0ff1ae6 100644 --- a/tools/memory-model/litmus-tests/README +++ b/tools/memory-model/litmus-tests/README @@ -63,6 +63,10 @@ LB+poonceonces.litmus As above, but with store-release replaced with WRITE_ONCE() and load-acquire replaced with READ_ONCE(). +LB+unlocklockonceonce+poacquireonce.litmus + Does a unlock+lock pair provides ordering guarantee between a + load and a store? + MP+onceassign+derefonce.litmus As below, but with rcu_assign_pointer() and an rcu_dereference(). @@ -90,6 +94,10 @@ MP+porevlocks.litmus As below, but with the first access of the writer process and the second access of reader process protected by a lock. +MP+unlocklockonceonce+fencermbonceonce.litmus + Does a unlock+lock pair provides ordering guarantee between a + store and another store? + MP+fencewmbonceonce+fencermbonceonce.litmus Does a smp_wmb() (between the stores) and an smp_rmb() (between the loads) suffice for the message-passing litmus test, where one diff --git a/tools/memory-model/litmus-tests/dep+plain.litmus b/tools/memory-model/litmus-tests/dep+plain.litmus new file mode 100644 index 000000000000..ebf84daa9a59 --- /dev/null +++ b/tools/memory-model/litmus-tests/dep+plain.litmus @@ -0,0 +1,31 @@ +C dep+plain + +(* + * Result: Never + * + * This litmus test demonstrates that in LKMM, plain accesses + * carry dependencies much like accesses to registers: + * The data stored to *z1 and *z2 by P0() originates from P0()'s + * READ_ONCE(), and therefore using that data to compute the + * conditional of P0()'s if-statement creates a control dependency + * from that READ_ONCE() to P0()'s WRITE_ONCE(). + *) + +{} + +P0(int *x, int *y, int *z1, int *z2) +{ + int a = READ_ONCE(*x); + *z1 = a; + *z2 = *z1; + if (*z2 == 1) + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r = smp_load_acquire(y); + smp_store_release(x, r); +} + +exists (x=1 /\ y=1) |