diff options
Diffstat (limited to 'tools/memory-model/litmus-tests')
29 files changed, 786 insertions, 0 deletions
diff --git a/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus new file mode 100644 index 000000000000..5b83d57f6ac5 --- /dev/null +++ b/tools/memory-model/litmus-tests/CoRR+poonceonce+Once.litmus @@ -0,0 +1,19 @@ +C CoRR+poonceonce+Once + +{} + +P0(int *x) +{ + WRITE_ONCE(*x, 1); +} + +P1(int *x) +{ + int r0; + int r1; + + r0 = READ_ONCE(*x); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 1:r1=0) diff --git a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus new file mode 100644 index 000000000000..fab91c13d52c --- /dev/null +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus @@ -0,0 +1,18 @@ +C CoRW+poonceonce+Once + +{} + +P0(int *x) +{ + int r0; + + r0 = READ_ONCE(*x); + WRITE_ONCE(*x, 1); +} + +P1(int *x) +{ + WRITE_ONCE(*x, 2); +} + +exists (x=2 /\ 0:r0=2) diff --git a/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus new file mode 100644 index 000000000000..6a35ec2042ea --- /dev/null +++ b/tools/memory-model/litmus-tests/CoWR+poonceonce+Once.litmus @@ -0,0 +1,18 @@ +C CoWR+poonceonce+Once + +{} + +P0(int *x) +{ + int r0; + + WRITE_ONCE(*x, 1); + r0 = READ_ONCE(*x); +} + +P1(int *x) +{ + WRITE_ONCE(*x, 2); +} + +exists (x=1 /\ 0:r0=2) diff --git a/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus new file mode 100644 index 000000000000..32a96b832021 --- /dev/null +++ b/tools/memory-model/litmus-tests/CoWW+poonceonce.litmus @@ -0,0 +1,11 @@ +C CoWW+poonceonce + +{} + +P0(int *x) +{ + WRITE_ONCE(*x, 1); + WRITE_ONCE(*x, 2); +} + +exists (x=1) diff --git a/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus new file mode 100644 index 000000000000..7eba2c68992b --- /dev/null +++ b/tools/memory-model/litmus-tests/IRIW+mbonceonces+OnceOnce.litmus @@ -0,0 +1,35 @@ +C IRIW+mbonceonces+OnceOnce + +{} + +P0(int *x) +{ + WRITE_ONCE(*x, 1); +} + +P1(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*x); + smp_mb(); + r1 = READ_ONCE(*y); +} + +P2(int *y) +{ + WRITE_ONCE(*y, 1); +} + +P3(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*y); + smp_mb(); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0) diff --git a/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus new file mode 100644 index 000000000000..b0556c6c75d4 --- /dev/null +++ b/tools/memory-model/litmus-tests/IRIW+poonceonces+OnceOnce.litmus @@ -0,0 +1,33 @@ +C IRIW+poonceonces+OnceOnce + +{} + +P0(int *x) +{ + WRITE_ONCE(*x, 1); +} + +P1(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*x); + r1 = READ_ONCE(*y); +} + +P2(int *y) +{ + WRITE_ONCE(*y, 1); +} + +P3(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*y); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 1:r1=0 /\ 3:r0=1 /\ 3:r1=0) diff --git a/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus new file mode 100644 index 000000000000..9a1a233d70c3 --- /dev/null +++ b/tools/memory-model/litmus-tests/ISA2+poonceonces.litmus @@ -0,0 +1,28 @@ +C ISA2+poonceonces + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 1); + WRITE_ONCE(*y, 1); +} + +P1(int *y, int *z) +{ + int r0; + + r0 = READ_ONCE(*y); + WRITE_ONCE(*z, 1); +} + +P2(int *x, int *z) +{ + int r0; + int r1; + + r0 = READ_ONCE(*z); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) diff --git a/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus new file mode 100644 index 000000000000..235195e87d4e --- /dev/null +++ b/tools/memory-model/litmus-tests/ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus @@ -0,0 +1,28 @@ +C ISA2+pooncerelease+poacquirerelease+poacquireonce + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 1); + smp_store_release(y, 1); +} + +P1(int *y, int *z) +{ + int r0; + + r0 = smp_load_acquire(y); + smp_store_release(z, 1); +} + +P2(int *x, int *z) +{ + int r0; + int r1; + + r0 = smp_load_acquire(z); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) diff --git a/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus new file mode 100644 index 000000000000..dd5ac3a8974a --- /dev/null +++ b/tools/memory-model/litmus-tests/LB+ctrlonceonce+mbonceonce.litmus @@ -0,0 +1,23 @@ +C LB+ctrlonceonce+mbonceonce + +{} + +P0(int *x, int *y) +{ + int r0; + + r0 = READ_ONCE(*x); + if (r0) + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r0; + + r0 = READ_ONCE(*y); + smp_mb(); + WRITE_ONCE(*x, 1); +} + +exists (0:r0=1 /\ 1:r0=1) diff --git a/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus new file mode 100644 index 000000000000..47bd61319d93 --- /dev/null +++ b/tools/memory-model/litmus-tests/LB+poacquireonce+pooncerelease.litmus @@ -0,0 +1,21 @@ +C LB+poacquireonce+pooncerelease + +{} + +P0(int *x, int *y) +{ + int r0; + + r0 = READ_ONCE(*x); + smp_store_release(y, 1); +} + +P1(int *x, int *y) +{ + int r0; + + r0 = smp_load_acquire(y); + WRITE_ONCE(*x, 1); +} + +exists (0:r0=1 /\ 1:r0=1) diff --git a/tools/memory-model/litmus-tests/LB+poonceonces.litmus b/tools/memory-model/litmus-tests/LB+poonceonces.litmus new file mode 100644 index 000000000000..a5cdf027e34b --- /dev/null +++ b/tools/memory-model/litmus-tests/LB+poonceonces.litmus @@ -0,0 +1,21 @@ +C LB+poonceonces + +{} + +P0(int *x, int *y) +{ + int r0; + + r0 = READ_ONCE(*x); + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r0; + + r0 = READ_ONCE(*y); + WRITE_ONCE(*x, 1); +} + +exists (0:r0=1 /\ 1:r0=1) diff --git a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus new file mode 100644 index 000000000000..1a2fe5830381 --- /dev/null +++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus @@ -0,0 +1,25 @@ +C MP+onceassign+derefonce.litmus + +{ +y=z; +z=0; +} + +P0(int *x, int **y) +{ + WRITE_ONCE(*x, 1); + rcu_assign_pointer(*y, x); +} + +P1(int *x, int **y) +{ + int *r0; + int r1; + + rcu_read_lock(); + r0 = rcu_dereference(*y); + r1 = READ_ONCE(*r0); + rcu_read_unlock(); +} + +exists (1:r0=x /\ 1:r1=0) diff --git a/tools/memory-model/litmus-tests/MP+polocks.litmus b/tools/memory-model/litmus-tests/MP+polocks.litmus new file mode 100644 index 000000000000..5fe6f1e3c452 --- /dev/null +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus @@ -0,0 +1,24 @@ +C MP+polocks + +{} + +P0(int *x, int *y, spinlock_t *mylock) +{ + WRITE_ONCE(*x, 1); + spin_lock(mylock); + WRITE_ONCE(*y, 1); + spin_unlock(mylock); +} + +P1(int *x, int *y, spinlock_t *mylock) +{ + int r0; + int r1; + + spin_lock(mylock); + r0 = READ_ONCE(*y); + spin_unlock(mylock); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 1:r1=0) diff --git a/tools/memory-model/litmus-tests/MP+poonceonces.litmus b/tools/memory-model/litmus-tests/MP+poonceonces.litmus new file mode 100644 index 000000000000..46e1ac7ba126 --- /dev/null +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus @@ -0,0 +1,20 @@ +C MP+poonceonces + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 1); + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*y); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 1:r1=0) diff --git a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus new file mode 100644 index 000000000000..0b00cc7293ba --- /dev/null +++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus @@ -0,0 +1,20 @@ +C MP+pooncerelease+poacquireonce + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 1); + smp_store_release(y, 1); +} + +P1(int *x, int *y) +{ + int r0; + int r1; + + r0 = smp_load_acquire(y); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 1:r1=0) diff --git a/tools/memory-model/litmus-tests/MP+porevlocks.litmus b/tools/memory-model/litmus-tests/MP+porevlocks.litmus new file mode 100644 index 000000000000..90d011c34f33 --- /dev/null +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus @@ -0,0 +1,24 @@ +C MP+porevlocks + +{} + +P0(int *x, int *y, spinlock_t *mylock) +{ + int r0; + int r1; + + r0 = READ_ONCE(*y); + spin_lock(mylock); + r1 = READ_ONCE(*x); + spin_unlock(mylock); +} + +P1(int *x, int *y, spinlock_t *mylock) +{ + spin_lock(mylock); + WRITE_ONCE(*x, 1); + spin_unlock(mylock); + WRITE_ONCE(*y, 1); +} + +exists (0:r0=1 /\ 0:r1=0) diff --git a/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus new file mode 100644 index 000000000000..604ad41ea0c2 --- /dev/null +++ b/tools/memory-model/litmus-tests/MP+wmbonceonce+rmbonceonce.litmus @@ -0,0 +1,22 @@ +C MP+wmbonceonce+rmbonceonce + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 1); + smp_wmb(); + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*y); + smp_rmb(); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 1:r1=0) diff --git a/tools/memory-model/litmus-tests/R+mbonceonces.litmus b/tools/memory-model/litmus-tests/R+mbonceonces.litmus new file mode 100644 index 000000000000..e69b9e3e9436 --- /dev/null +++ b/tools/memory-model/litmus-tests/R+mbonceonces.litmus @@ -0,0 +1,21 @@ +C R+mbonceonces + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 1); + smp_mb(); + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r0; + + WRITE_ONCE(*y, 2); + smp_mb(); + r0 = READ_ONCE(*x); +} + +exists (y=2 /\ 1:r0=0) diff --git a/tools/memory-model/litmus-tests/R+poonceonces.litmus b/tools/memory-model/litmus-tests/R+poonceonces.litmus new file mode 100644 index 000000000000..f7a12e00f82d --- /dev/null +++ b/tools/memory-model/litmus-tests/R+poonceonces.litmus @@ -0,0 +1,19 @@ +C R+poonceonces + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 1); + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r0; + + WRITE_ONCE(*y, 2); + r0 = READ_ONCE(*x); +} + +exists (y=2 /\ 1:r0=0) diff --git a/tools/memory-model/litmus-tests/README b/tools/memory-model/litmus-tests/README new file mode 100644 index 000000000000..9a3bb5949191 --- /dev/null +++ b/tools/memory-model/litmus-tests/README @@ -0,0 +1,125 @@ +This directory contains the following litmus tests: + +CoRR+poonceonce+Once.litmus + Test of read-read coherence, that is, whether or not two + successive reads from the same variable are ordered. + +CoRW+poonceonce+Once.litmus + Test of read-write coherence, that is, whether or not a read + from a given variable followed by a write to that same variable + are ordered. + +CoWR+poonceonce+Once.litmus + Test of write-read coherence, that is, whether or not a write + to a given variable followed by a read from that same variable + are ordered. + +CoWW+poonceonce.litmus + Test of write-write coherence, that is, whether or not two + successive writes to the same variable are ordered. + +IRIW+mbonceonces+OnceOnce.litmus + Test of independent reads from independent writes with smp_mb() + 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. + +IRIW+poonceonces+OnceOnce.litmus + Test of independent reads from independent writes with nothing + between each pairs of reads. In other words, is anything at all + needed 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. + +ISA2+poonceonces.litmus + As below, but with store-release replaced with WRITE_ONCE() + and load-acquire replaced with READ_ONCE(). + +ISA2+pooncerelease+poacquirerelease+poacquireonce.litmus + Can a release-acquire chain order a prior store against + a later load? + +LB+ctrlonceonce+mbonceonce.litmus + Does a control dependency and an smp_mb() suffice for the + load-buffering litmus test, where each process reads from one + of two variables then writes to the other? + +LB+poacquireonce+pooncerelease.litmus + Does a release-acquire pair suffice for the load-buffering + litmus test, where each process reads from one of two variables then + writes to the other? + +LB+poonceonces.litmus + As above, but with store-release replaced with WRITE_ONCE() + and load-acquire replaced with READ_ONCE(). + +MP+onceassign+derefonce.litmus + As below, but with rcu_assign_pointer() and an rcu_dereference(). + +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. + +MP+poonceonces.litmus + As below, but without the smp_rmb() and smp_wmb(). + +MP+pooncerelease+poacquireonce.litmus + As below, but with a release-acquire chain. + +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+wmbonceonce+rmbonceonce.litmus + Does a smp_wmb() (between the stores) and an smp_rmb() (between + the loads) suffice for the message-passing litmus test, where one + process writes data and then a flag, and the other process reads + the flag and then the data. (This is similar to the ISA2 tests, + but with two processes instead of three.) + +R+mbonceonces.litmus + This is the fully ordered (via smp_mb()) version of one of + the classic counterintuitive litmus tests that illustrates the + effects of store propagation delays. + +R+poonceonces.litmus + As above, but without the smp_mb() invocations. + +SB+mbonceonces.litmus + This is the fully ordered (again, via smp_mb() version of store + buffering, which forms the core of Dekker's mutual-exclusion + algorithm. + +SB+poonceonces.litmus + As above, but without the smp_mb() invocations. + +S+poonceonces.litmus + As below, but without the smp_wmb() and acquire load. + +S+wmbonceonce+poacquireonce.litmus + Can a smp_wmb(), instead of a release, and an acquire order + a prior store against a subsequent store? + +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. + +Z6.0+pooncelock+pooncelock+pombonce.litmus + Is the ordering provided by a spin_unlock() and a subsequent + spin_lock() sufficient to make ordering apparent to accesses + by a process not holding the lock? + +Z6.0+pooncelock+poonceLock+pombonce.litmus + As above, but with smp_mb__after_spinlock() immediately + following the spin_lock(). + +Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus + Is the ordering provided by a release-acquire chain sufficient + to make ordering apparent to accesses by a process that does + not participate in that release-acquire chain? + +A great many more litmus tests are available here: + + https://github.com/paulmckrcu/litmus diff --git a/tools/memory-model/litmus-tests/S+poonceonces.litmus b/tools/memory-model/litmus-tests/S+poonceonces.litmus new file mode 100644 index 000000000000..d0d541c8ec7d --- /dev/null +++ b/tools/memory-model/litmus-tests/S+poonceonces.litmus @@ -0,0 +1,19 @@ +C S+poonceonces + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 2); + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r0; + + r0 = READ_ONCE(*y); + WRITE_ONCE(*x, 1); +} + +exists (x=2 /\ 1:r0=1) diff --git a/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus new file mode 100644 index 000000000000..1d292d0d6603 --- /dev/null +++ b/tools/memory-model/litmus-tests/S+wmbonceonce+poacquireonce.litmus @@ -0,0 +1,20 @@ +C S+wmbonceonce+poacquireonce + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 2); + smp_wmb(); + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r0; + + r0 = smp_load_acquire(y); + WRITE_ONCE(*x, 1); +} + +exists (x=2 /\ 1:r0=1) diff --git a/tools/memory-model/litmus-tests/SB+mbonceonces.litmus b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus new file mode 100644 index 000000000000..b76caa5af1af --- /dev/null +++ b/tools/memory-model/litmus-tests/SB+mbonceonces.litmus @@ -0,0 +1,23 @@ +C SB+mbonceonces + +{} + +P0(int *x, int *y) +{ + int r0; + + WRITE_ONCE(*x, 1); + smp_mb(); + r0 = READ_ONCE(*y); +} + +P1(int *x, int *y) +{ + int r0; + + WRITE_ONCE(*y, 1); + smp_mb(); + r0 = READ_ONCE(*x); +} + +exists (0:r0=0 /\ 1:r0=0) diff --git a/tools/memory-model/litmus-tests/SB+poonceonces.litmus b/tools/memory-model/litmus-tests/SB+poonceonces.litmus new file mode 100644 index 000000000000..c1797e03807e --- /dev/null +++ b/tools/memory-model/litmus-tests/SB+poonceonces.litmus @@ -0,0 +1,21 @@ +C SB+poonceonces + +{} + +P0(int *x, int *y) +{ + int r0; + + WRITE_ONCE(*x, 1); + r0 = READ_ONCE(*y); +} + +P1(int *x, int *y) +{ + int r0; + + WRITE_ONCE(*y, 1); + r0 = READ_ONCE(*x); +} + +exists (0:r0=0 /\ 1:r0=0) diff --git a/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus new file mode 100644 index 000000000000..f5e7c92f61cc --- /dev/null +++ b/tools/memory-model/litmus-tests/WRC+poonceonces+Once.litmus @@ -0,0 +1,27 @@ +C WRC+poonceonces+Once + +{} + +P0(int *x) +{ + WRITE_ONCE(*x, 1); +} + +P1(int *x, int *y) +{ + int r0; + + r0 = READ_ONCE(*x); + WRITE_ONCE(*y, 1); +} + +P2(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*y); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) diff --git a/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus new file mode 100644 index 000000000000..e3d0018025dd --- /dev/null +++ b/tools/memory-model/litmus-tests/WRC+pooncerelease+rmbonceonce+Once.litmus @@ -0,0 +1,28 @@ +C WRC+pooncerelease+rmbonceonce+Once + +{} + +P0(int *x) +{ + WRITE_ONCE(*x, 1); +} + +P1(int *x, int *y) +{ + int r0; + + r0 = READ_ONCE(*x); + smp_store_release(y, 1); +} + +P2(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*y); + smp_rmb(); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0) diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus new file mode 100644 index 000000000000..9c2cb53e6ef0 --- /dev/null +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+poonceLock+pombonce.litmus @@ -0,0 +1,33 @@ +C Z6.0+pooncelock+poonceLock+pombonce + +{} + +P0(int *x, int *y, spinlock_t *mylock) +{ + spin_lock(mylock); + WRITE_ONCE(*x, 1); + WRITE_ONCE(*y, 1); + spin_unlock(mylock); +} + +P1(int *y, int *z, spinlock_t *mylock) +{ + int r0; + + spin_lock(mylock); + smp_mb__after_spinlock(); + r0 = READ_ONCE(*y); + WRITE_ONCE(*z, 1); + spin_unlock(mylock); +} + +P2(int *x, int *z) +{ + int r1; + + WRITE_ONCE(*z, 2); + smp_mb(); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ z=2 /\ 2:r1=0) diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus new file mode 100644 index 000000000000..c9a1f1a49ae1 --- /dev/null +++ b/tools/memory-model/litmus-tests/Z6.0+pooncelock+pooncelock+pombonce.litmus @@ -0,0 +1,32 @@ +C Z6.0+pooncelock+pooncelock+pombonce + +{} + +P0(int *x, int *y, spinlock_t *mylock) +{ + spin_lock(mylock); + WRITE_ONCE(*x, 1); + WRITE_ONCE(*y, 1); + spin_unlock(mylock); +} + +P1(int *y, int *z, spinlock_t *mylock) +{ + int r0; + + spin_lock(mylock); + r0 = READ_ONCE(*y); + WRITE_ONCE(*z, 1); + spin_unlock(mylock); +} + +P2(int *x, int *z) +{ + int r1; + + WRITE_ONCE(*z, 2); + smp_mb(); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ z=2 /\ 2:r1=0) diff --git a/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus new file mode 100644 index 000000000000..25409a033514 --- /dev/null +++ b/tools/memory-model/litmus-tests/Z6.0+pooncerelease+poacquirerelease+mbonceonce.litmus @@ -0,0 +1,28 @@ +C Z6.0+pooncerelease+poacquirerelease+mbonceonce + +{} + +P0(int *x, int *y) +{ + WRITE_ONCE(*x, 1); + smp_store_release(y, 1); +} + +P1(int *y, int *z) +{ + int r0; + + r0 = smp_load_acquire(y); + smp_store_release(z, 1); +} + +P2(int *x, int *z) +{ + int r1; + + WRITE_ONCE(*z, 2); + smp_mb(); + r1 = READ_ONCE(*x); +} + +exists (1:r0=1 /\ z=2 /\ 2:r1=0) |