LXR linux/tools/memory-model/litmus-tests/MP+poonceonces.litmus

   1C MP+poonceonces
   2
   3(*
   4 * Result: Sometimes
   5 *
   6 * Can the counter-intuitive message-passing outcome be prevented with
   7 * no ordering at all?
   8 *)
   9
  10{}
  11
  12P0(int *buf, int *flag) // Producer
  13{
  14        WRITE_ONCE(*buf, 1);
  15        WRITE_ONCE(*flag, 1);
  16}
  17
  18P1(int *buf, int *flag) // Consumer
  19{
  20        int r0;
  21        int r1;
  22
  23        r0 = READ_ONCE(*flag);
  24        r1 = READ_ONCE(*buf);
  25}
  26
  27exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
  28