linux/tools/memory-model/litmus-tests/MP+polockmbonce+poacquiresilsil.litmus
Paul E. McKenney 1947bfcf81 tools/memory-model: Add types to litmus tests
This commit adds type information for global variables in the litmus
tests in order to allow easier use with klitmus7.

Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-11-06 17:25:16 -08:00

38 lines
727 B
Plaintext

C MP+polockmbonce+poacquiresilsil
(*
* Result: Never
*
* Do spinlocks combined with smp_mb__after_spinlock() provide order
* to outside observers using spin_is_locked() to sense the lock-held
* state, ordered by acquire? Note that when the first spin_is_locked()
* returns false and the second true, we know that the smp_load_acquire()
* executed before the lock was acquired (loosely speaking).
*)
{
spinlock_t lo;
int x;
}
P0(spinlock_t *lo, int *x)
{
spin_lock(lo);
smp_mb__after_spinlock();
WRITE_ONCE(*x, 1);
spin_unlock(lo);
}
P1(spinlock_t *lo, int *x)
{
int r1;
int r2;
int r3;
r1 = smp_load_acquire(x);
r2 = spin_is_locked(lo);
r3 = spin_is_locked(lo);
}
exists (1:r1=1 /\ 1:r2=0 /\ 1:r3=1)