C MP+poonceonces | |
(* | |
* Result: Sometimes | |
* | |
* Can the counter-intuitive message-passing outcome be prevented with | |
* no ordering at all? | |
*) | |
{} | |
P0(int *buf, int *flag) // Producer | |
{ | |
WRITE_ONCE(*buf, 1); | |
WRITE_ONCE(*flag, 1); | |
} | |
P1(int *buf, int *flag) // Consumer | |
{ | |
int r0; | |
int r1; | |
r0 = READ_ONCE(*flag); | |
r1 = READ_ONCE(*buf); | |
} | |
exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *) |