0001 C MP+poonceonces
0002
0003 (*
0004 * Result: Sometimes
0005 *
0006 * Can the counter-intuitive message-passing outcome be prevented with
0007 * no ordering at all?
0008 *)
0009
0010 {}
0011
0012 P0(int *buf, int *flag) // Producer
0013 {
0014 WRITE_ONCE(*buf, 1);
0015 WRITE_ONCE(*flag, 1);
0016 }
0017
0018 P1(int *buf, int *flag) // Consumer
0019 {
0020 int r0;
0021 int r1;
0022
0023 r0 = READ_ONCE(*flag);
0024 r1 = READ_ONCE(*buf);
0025 }
0026
0027 exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
