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