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