1C MP+polockmbonce+poacquiresilsil
2
3(*
4 * Result: Never
5 *
6 * Do spinlocks combined with smp_mb__after_spinlock() provide order
7 * to outside observers using spin_is_locked() to sense the lock-held
8 * 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	spinlock_t lo;
15	int x;
16}
17
18P0(spinlock_t *lo, int *x)
19{
20	spin_lock(lo);
21	smp_mb__after_spinlock();
22	WRITE_ONCE(*x, 1);
23	spin_unlock(lo);
24}
25
26P1(spinlock_t *lo, int *x)
27{
28	int r1;
29	int r2;
30	int r3;
31
32	r1 = smp_load_acquire(x);
33	r2 = spin_is_locked(lo);
34	r3 = spin_is_locked(lo);
35}
36
37exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)
38