linux-stable/tools/memory-model/litmus-tests/MP+pooncerelease+poacquireonce.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

31 lines
486 B
Text

C MP+pooncerelease+poacquireonce
(*
* Result: Never
*
* This litmus test demonstrates that smp_store_release() and
* smp_load_acquire() provide sufficient ordering for the message-passing
* pattern.
*)
{
int buf;
int flag;
}
P0(int *buf, int *flag) // Producer
{
WRITE_ONCE(*buf, 1);
smp_store_release(flag, 1);
}
P1(int *buf, int *flag) // Consumer
{
int r0;
int r1;
r0 = smp_load_acquire(flag);
r1 = READ_ONCE(*buf);
}
exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)