diff options
Diffstat (limited to 'tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus')
-rw-r--r-- | tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus index 50f4d62bbf0e..ba91cc63e148 100644 --- a/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus +++ b/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus @@ -10,10 +10,9 @@ C MP+polockmbonce+poacquiresilsil * executed before the lock was acquired (loosely speaking). *) -{ -} +{} -P0(spinlock_t *lo, int *x) +P0(spinlock_t *lo, int *x) // Producer { spin_lock(lo); smp_mb__after_spinlock(); @@ -21,7 +20,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; @@ -32,4 +31,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. *) |