The following commit has been merged into the core/rcu branch of tip:
Commit-ID: b6ff30849ca723b78306514246b98ca5645d92f5
Gitweb: https://git.kernel.org/tip/b6ff30849ca723b78306514246b98ca5645d92f5
Author: Paul E. McKenney <paulmck@xxxxxxxxxx>
AuthorDate: Thu, 05 Nov 2020 13:39:28 -08:00
Committer: Paul E. McKenney <paulmck@xxxxxxxxxx>
CommitterDate: Fri, 06 Nov 2020 17:25:17 -08:00
tools/memory-model: Label MP tests' producers and consumers
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 <hannes@xxxxxxxxxxx>
Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx>
---
tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus | 6 +++---
tools/memory-model/litmus-tests/MP+onceassign+derefonce.litmus | 6 +++---
tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 6 +++---
tools/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 +++---
tools/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. *)
|