1C CoRR+poonceonce+Once 2 3{} 4 5P0(int *x) 6{ 7 WRITE_ONCE(*x, 1); 8} 9 10P1(int *x) 11{ 12 int r0; 13 int r1; 14 15 r0 = READ_ONCE(*x); 16 r1 = READ_ONCE(*x); 17} 18 19exists (1:r0=1 /\ 1:r1=0) 20