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