26 lines · plain
1C CoWR+poonceonce+Once2 3(*4 * Result: Never5 *6 * Test of write-read coherence, that is, whether or not a write to a7 * given variable and a later read from that same variable are ordered.8 *)9 10{}11 12P0(int *x)13{14 int r0;15 16 WRITE_ONCE(*x, 1);17 r0 = READ_ONCE(*x);18}19 20P1(int *x)21{22 WRITE_ONCE(*x, 2);23}24 25exists (x=1 /\ 0:r0=2)26