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