diff options
| author | Paul E. McKenney <paulmck@kernel.org> | 2020-11-06 00:39:28 +0300 |
|---|---|---|
| committer | Paul E. McKenney <paulmck@kernel.org> | 2020-11-07 04:25:17 +0300 |
| commit | b6ff30849ca723b78306514246b98ca5645d92f5 (patch) | |
| tree | b4110e2cd58cfd0988663fded8e780aae8ba8e47 /tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | |
| parent | acc4bdc55dcb7d7fe0be736999572a55e121873f (diff) | |
| download | linux-b6ff30849ca723b78306514246b98ca5645d92f5.tar.xz | |
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@cmpxchg.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Diffstat (limited to 'tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus')
| -rw-r--r-- | tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 6 |
1 files changed, 3 insertions, 3 deletions
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. *) |