C CoRW+poonceonce+Once (* * Result: Never * * Test of read-write coherence, that is, whether or not a read from * a given variable and a later write to that same variable are ordered. *) {} P0(int *x) { int r0; r0 = READ_ONCE(*x); WRITE_ONCE(*x, 1); } P1(int *x) { WRITE_ONCE(*x, 2); } exists (x=2 /\ 0:r0=2)
