1
0
Fork 0
mirror of synced 2025-03-06 20:59:54 +01:00
linux/tools/memory-model/litmus-tests/MP+porevlocks.litmus
Paul E. McKenney b6ff30849c tools/memory-model: Label MP tests' producers and consumers
This commit adds comments that label the MP tests' producer and consumer
processes, and also that label the "exists" clause as the bad outcome.

Reported-by: Johannes Weiner <hannes@cmpxchg.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
2020-11-06 17:25:17 -08:00

39 lines
870 B
Text

C MP+porevlocks
(*
* Result: Never
*
* This litmus test demonstrates how lock acquisitions and releases can
* stand in for smp_load_acquire() and smp_store_release(), respectively.
* In other words, when holding a given lock (or indeed after releasing a
* given lock), a CPU is not only guaranteed to see the accesses that other
* CPUs made while previously holding that lock, it is also guaranteed to
* see all prior accesses by those other CPUs.
*)
{
spinlock_t mylock;
int buf;
int flag;
}
P0(int *buf, int *flag, spinlock_t *mylock) // Consumer
{
int r0;
int r1;
r0 = READ_ONCE(*flag);
spin_lock(mylock);
r1 = READ_ONCE(*buf);
spin_unlock(mylock);
}
P1(int *buf, int *flag, spinlock_t *mylock) // Producer
{
spin_lock(mylock);
WRITE_ONCE(*buf, 1);
spin_unlock(mylock);
WRITE_ONCE(*flag, 1);
}
exists (0:r0=1 /\ 0:r1=0) (* Bad outcome. *)