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