diff options
Diffstat (limited to 'tools/memory-model')
8 files changed, 24 insertions, 24 deletions
diff --git a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus index f15e501849dd..c5c168d92973 100644 --- a/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus +++ b/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus @@ -13,14 +13,14 @@ C MP+fencewmbonceonce+fencermbonceonce int flag; } -P0(int *buf, int *flag) +P0(int *buf, int *flag) // Producer { WRITE_ONCE(*buf, 1); smp_wmb(); WRITE_ONCE(*flag, 1); } -P1(int *buf, int *flag) +P1(int *buf, int *flag) // Consumer { int r0; int r1; @@ -30,4 +30,4 @@ P1(int *buf, int *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+onceassign+derefonce.litmus b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus index ed8ee9bde0c9..20ff62649f1e 100644 --- a/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus +++ b/tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus @@ -15,13 +15,13 @@ C MP+onceassign+derefonce int y=0; } -P0(int *x, int **p) +P0(int *x, int **p) // Producer { WRITE_ONCE(*x, 1); rcu_assign_pointer(*p, x); } -P1(int *x, int **p) +P1(int *x, int **p) // Consumer { int *r0; int r1; @@ -32,4 +32,4 @@ P1(int *x, int **p) 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 b1b1266fb49a..153917ad5dc9 100644 --- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus @@ -15,7 +15,7 @@ C MP+polockmbonce+poacquiresilsil int x; } -P0(spinlock_t *lo, int *x) +P0(spinlock_t *lo, int *x) // Producer { spin_lock(lo); smp_mb__after_spinlock(); @@ -23,7 +23,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; @@ -34,4 +34,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 867c75d8b960..aad64397bb8c 100644 --- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus @@ -15,14 +15,14 @@ C MP+polockonce+poacquiresilsil int x; } -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; @@ -33,4 +33,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 4b0c2edcc029..21cbca6f3be4 100644 --- a/tools/memory-model/litmus-tests/MP+polocks.litmus +++ b/tools/memory-model/litmus-tests/MP+polocks.litmus @@ -17,7 +17,7 @@ C MP+polocks int flag; } -P0(int *buf, int *flag, spinlock_t *mylock) +P0(int *buf, int *flag, spinlock_t *mylock) // Producer { WRITE_ONCE(*buf, 1); spin_lock(mylock); @@ -25,7 +25,7 @@ P0(int *buf, int *flag, spinlock_t *mylock) spin_unlock(mylock); } -P1(int *buf, int *flag, spinlock_t *mylock) +P1(int *buf, int *flag, spinlock_t *mylock) // Consumer { int r0; int r1; @@ -36,4 +36,4 @@ P1(int *buf, int *flag, spinlock_t *mylock) 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 3010bbaec46c..9f9769d647c7 100644 --- a/tools/memory-model/litmus-tests/MP+poonceonces.litmus +++ b/tools/memory-model/litmus-tests/MP+poonceonces.litmus @@ -12,13 +12,13 @@ C MP+poonceonces int flag; } -P0(int *buf, int *flag) +P0(int *buf, int *flag) // Producer { WRITE_ONCE(*buf, 1); WRITE_ONCE(*flag, 1); } -P1(int *buf, int *flag) +P1(int *buf, int *flag) // Consumer { int r0; int r1; @@ -27,4 +27,4 @@ P1(int *buf, int *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 21e825d5dea6..cbe28e733443 100644 --- a/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus +++ b/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus @@ -13,13 +13,13 @@ C MP+pooncerelease+poacquireonce int flag; } -P0(int *buf, int *flag) +P0(int *buf, int *flag) // Producer { WRITE_ONCE(*buf, 1); smp_store_release(flag, 1); } -P1(int *buf, int *flag) +P1(int *buf, int *flag) // Consumer { int r0; int r1; @@ -28,4 +28,4 @@ P1(int *buf, int *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 9691d55b4e21..012041bd4feb 100644 --- a/tools/memory-model/litmus-tests/MP+porevlocks.litmus +++ b/tools/memory-model/litmus-tests/MP+porevlocks.litmus @@ -17,7 +17,7 @@ C MP+porevlocks int flag; } -P0(int *buf, int *flag, spinlock_t *mylock) +P0(int *buf, int *flag, spinlock_t *mylock) // Consumer { int r0; int r1; @@ -28,7 +28,7 @@ P0(int *buf, int *flag, spinlock_t *mylock) spin_unlock(mylock); } -P1(int *buf, int *flag, spinlock_t *mylock) +P1(int *buf, int *flag, spinlock_t *mylock) // Producer { spin_lock(mylock); WRITE_ONCE(*buf, 1); @@ -36,4 +36,4 @@ P1(int *buf, int *flag, spinlock_t *mylock) WRITE_ONCE(*flag, 1); } -exists (0:r0=1 /\ 0:r1=0) +exists (0:r0=1 /\ 0:r1=0) (* Bad outcome. *) |