| C MP+polockonce+poacquiresilsil |
| |
| (* |
| * Result: Sometimes |
| * |
| * Do spinlocks provide order to outside observers using spin_is_locked() |
| * to sense the lock-held state, ordered by acquire? Note that when the |
| * first spin_is_locked() returns false and the second true, we know that |
| * the smp_load_acquire() executed before the lock was acquired (loosely |
| * speaking). |
| *) |
| |
| {} |
| |
| P0(spinlock_t *lo, int *x) // Producer |
| { |
| spin_lock(lo); |
| WRITE_ONCE(*x, 1); |
| spin_unlock(lo); |
| } |
| |
| P1(spinlock_t *lo, int *x) // Consumer |
| { |
| int r1; |
| int r2; |
| int r3; |
| |
| r1 = smp_load_acquire(x); |
| r2 = spin_is_locked(lo); |
| r3 = spin_is_locked(lo); |
| } |
| |
| exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *) |
