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