From: "Paul E. McKenney" <[email protected]> This commit adds comments that label the MP tests' producer and consumer processes, and also that label the "exists" clause as the bad outcome.
Reported-by: Johannes Weiner <[email protected]> Signed-off-by: Paul E. McKenney <[email protected]> --- .../litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus | 6 +++--- tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus | 6 +++--- .../litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 6 +++--- .../memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 6 +++--- tools/memory-model/litmus-tests/MP+polocks.litmus | 6 +++--- tools/memory-model/litmus-tests/MP+poonceonces.litmus | 6 +++--- .../memory-model/litmus-tests/MP+pooncerelease+poacquireonce.litmus | 6 +++--- tools/memory-model/litmus-tests/MP+porevlocks.litmus | 6 +++--- 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 f15e501..c5c168d 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 ed8ee9b..20ff626 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 b1b1266..153917a 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 867c75d..aad6439 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 4b0c2ed..21cbca6 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 3010bba..9f9769d 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 21e825d..cbe28e7 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 9691d55..012041b 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. *) -- 2.9.5
