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