1C MP+polockonce+poacquiresilsil 2 3(* 4 * Result: Sometimes 5 * 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 the 8 * first spin_is_locked() returns false and the second true, we know that 9 * the smp_load_acquire() executed before the lock was acquired (loosely 10 * speaking). 11 *) 12 13{} 14 15P0(spinlock_t *lo, int *x) // Producer 16{ 17 spin_lock(lo); 18 WRITE_ONCE(*x, 1); 19 spin_unlock(lo); 20} 21 22P1(spinlock_t *lo, int *x) // Consumer 23{ 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