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 --- .../memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus') 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. *) -- cgit v1.2.3