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