From b6ff30849ca723b78306514246b98ca5645d92f5 Mon Sep 17 00:00:00 2001 From: "Paul E. McKenney" Date: Thu, 5 Nov 2020 13:39:28 -0800 Subject: 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 Signed-off-by: Paul E. McKenney --- .../litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus') 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. *) -- cgit v1.2.3