35 lines · plain
1C MP+polockmbonce+poacquiresilsil2 3(*4 * Result: Never5 *6 * Do spinlocks combined with smp_mb__after_spinlock() provide order7 * to outside observers using spin_is_locked() to sense the lock-held8 * state, ordered by acquire? Note that when the first spin_is_locked()9 * returns false and the second true, we know that the smp_load_acquire()10 * executed before the lock was acquired (loosely speaking).11 *)12 13{}14 15P0(spinlock_t *lo, int *x) // Producer16{17 spin_lock(lo);18 smp_mb__after_spinlock();19 WRITE_ONCE(*x, 1);20 spin_unlock(lo);21}22 23P1(spinlock_t *lo, int *x) // Consumer24{25 int r1;26 int r2;27 int r3;28 29 r1 = smp_load_acquire(x);30 r2 = spin_is_locked(lo);31 r3 = spin_is_locked(lo);32}33 34exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *)35