1C CoWR+poonceonce+Once 2 3(* 4 * Result: Never 5 * 6 * Test of write-read coherence, that is, whether or not a write to a 7 * 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