xref: /openbmc/linux/tools/memory-model/litmus-tests/MP+polockonce+poacquiresilsil.litmus (revision d0034a7a4ac7fae708146ac0059b9c47a1543f0d)
115553dcbSLuc MarangetC MP+polockonce+poacquiresilsil
215553dcbSLuc Maranget
315553dcbSLuc Maranget(*
415553dcbSLuc Maranget * Result: Sometimes
515553dcbSLuc Maranget *
615553dcbSLuc Maranget * Do spinlocks provide order to outside observers using spin_is_locked()
715553dcbSLuc Maranget * to sense the lock-held state, ordered by acquire?  Note that when the
815553dcbSLuc Maranget * first spin_is_locked() returns false and the second true, we know that
915553dcbSLuc Maranget * the smp_load_acquire() executed before the lock was acquired (loosely
1015553dcbSLuc Maranget * 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	WRITE_ONCE(*x, 1);
1915553dcbSLuc Maranget	spin_unlock(lo);
2015553dcbSLuc Maranget}
2115553dcbSLuc Maranget
22b6ff3084SPaul E. McKenneyP1(spinlock_t *lo, int *x) // Consumer
2315553dcbSLuc Maranget{
2415553dcbSLuc Maranget	int r1;
2515553dcbSLuc Maranget	int r2;
2615553dcbSLuc Maranget	int r3;
2715553dcbSLuc Maranget
2815553dcbSLuc Maranget	r1 = smp_load_acquire(x);
2915553dcbSLuc Maranget	r2 = spin_is_locked(lo);
3015553dcbSLuc Maranget	r3 = spin_is_locked(lo);
3115553dcbSLuc Maranget}
3215553dcbSLuc Maranget
33b6ff3084SPaul E. McKenneyexists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1) (* Bad outcome. *)
34