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