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