0001 C MP+pooncerelease+poacquireonce
0002
0003 (*
0004 * Result: Never
0005 *
0006 * This litmus test demonstrates that smp_store_release() and
0007 * smp_load_acquire() provide sufficient ordering for the message-passing
0008 * pattern.
0009 *)
0010
0011 {}
0012
0013 P0(int *buf, int *flag) // Producer
0014 {
0015 WRITE_ONCE(*buf, 1);
0016 smp_store_release(flag, 1);
0017 }
0018
0019 P1(int *buf, int *flag) // Consumer
0020 {
0021 int r0;
0022 int r1;
0023
0024 r0 = smp_load_acquire(flag);
0025 r1 = READ_ONCE(*buf);
0026 }
0027
0028 exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
