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