36 lines · plain
1C WRC+poonceonces+Once2 3(*4 * Result: Sometimes5 *6 * This litmus test is an extension of the message-passing pattern,7 * where the first write is moved to a separate process. Note that this8 * test has no ordering at all.9 *)10 11{}12 13P0(int *x)14{15 WRITE_ONCE(*x, 1);16}17 18P1(int *x, int *y)19{20 int r0;21 22 r0 = READ_ONCE(*x);23 WRITE_ONCE(*y, 1);24}25 26P2(int *x, int *y)27{28 int r0;29 int r1;30 31 r0 = READ_ONCE(*y);32 r1 = READ_ONCE(*x);33}34 35exists (1:r0=1 /\ 2:r0=1 /\ 2:r1=0)36