diff options
Diffstat (limited to 'tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus')
| -rw-r--r-- | tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus index abf81e7a0895..a5ea3ed8f52e 100644 --- a/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus +++ b/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus @@ -10,17 +10,16 @@ C MP+polockonce+poacquiresilsil * speaking). *) -{ -} +{} -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; @@ -31,4 +30,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. *) |