xref: /openbmc/linux/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus (revision d0034a7a4ac7fae708146ac0059b9c47a1543f0d)
115553dcbSLuc MarangetC MP+polockmbonce+poacquiresilsil
215553dcbSLuc Maranget
315553dcbSLuc Maranget(*
415553dcbSLuc Maranget * Result: Never
515553dcbSLuc Maranget *
615553dcbSLuc Maranget * Do spinlocks combined with smp_mb__after_spinlock() provide order
715553dcbSLuc Maranget * to outside observers using spin_is_locked() to sense the lock-held
815553dcbSLuc Maranget * state, ordered by acquire?  Note that when the first spin_is_locked()
915553dcbSLuc Maranget * returns false and the second true, we know that the smp_load_acquire()
1015553dcbSLuc Maranget * executed before the lock was acquired (loosely speaking).
1115553dcbSLuc Maranget *)
1215553dcbSLuc Maranget
13*5c587f9bSAkira Yokosawa{}
1415553dcbSLuc Maranget
15b6ff3084SPaul E. McKenneyP0(spinlock_t *lo, int *x) // Producer
1615553dcbSLuc Maranget{
1715553dcbSLuc Maranget	spin_lock(lo);
1815553dcbSLuc Maranget	smp_mb__after_spinlock();
1915553dcbSLuc Maranget	WRITE_ONCE(*x, 1);
2015553dcbSLuc Maranget	spin_unlock(lo);
2115553dcbSLuc Maranget}
2215553dcbSLuc Maranget
23b6ff3084SPaul E. McKenneyP1(spinlock_t *lo, int *x) // Consumer
2415553dcbSLuc Maranget{
2515553dcbSLuc Maranget	int r1;
2615553dcbSLuc Maranget	int r2;
2715553dcbSLuc Maranget	int r3;
2815553dcbSLuc Maranget
2915553dcbSLuc Maranget	r1 = smp_load_acquire(x);
3015553dcbSLuc Maranget	r2 = spin_is_locked(lo);
3115553dcbSLuc Maranget	r3 = spin_is_locked(lo);
3215553dcbSLuc Maranget}
3315553dcbSLuc Maranget
34b6ff3084SPaul E. McKenneyexists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *)
35