linux/tools/memory-model/litmus-tests/MP+fencewmbonceonce+fencermbonceonce.litmus
<<
>>
Prefs
   1C MP+fencewmbonceonce+fencermbonceonce
   2
   3(*
   4 * Result: Never
   5 *
   6 * This litmus test demonstrates that smp_wmb() and smp_rmb() provide
   7 * sufficient ordering for the message-passing pattern.  However, it
   8 * is usually better to use smp_store_release() and smp_load_acquire().
   9 *)
  10
  11{}
  12
  13P0(int *buf, int *flag) // Producer
  14{
  15        WRITE_ONCE(*buf, 1);
  16        smp_wmb();
  17        WRITE_ONCE(*flag, 1);
  18}
  19
  20P1(int *buf, int *flag) // Consumer
  21{
  22        int r0;
  23        int r1;
  24
  25        r0 = READ_ONCE(*flag);
  26        smp_rmb();
  27        r1 = READ_ONCE(*buf);
  28}
  29
  30exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
  31