0001 C MP+polockonce+poacquiresilsil
0002
0003 (*
0004 * Result: Sometimes
0005 *
0006 * Do spinlocks provide order to outside observers using spin_is_locked()
0007 * to sense the lock-held state, ordered by acquire? Note that when the
0008 * first spin_is_locked() returns false and the second true, we know that
0009 * the smp_load_acquire() executed before the lock was acquired (loosely
0010 * speaking).
0011 *)
0012
0013 {}
0014
0015 P0(spinlock_t *lo, int *x) // Producer
0016 {
0017 spin_lock(lo);
0018 WRITE_ONCE(*x, 1);
0019 spin_unlock(lo);
0020 }
0021
0022 P1(spinlock_t *lo, int *x) // Consumer
0023 {
0024 int r1;
0025 int r2;
0026 int r3;
0027
0028 r1 = smp_load_acquire(x);
0029 r2 = spin_is_locked(lo);
0030 r3 = spin_is_locked(lo);
0031 }
0032
0033 exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *)
