C mp_sc { [x] = 0; [y] = 0; } P0 (atomic_int* y, int* x) { *x = 1; atomic_store(y,1); } P1 (atomic_int* y, int* x) { int r0 = atomic_load(y); int r1 = -1; if (1 == r0) { r1 = *x; } } exists (1:r0=1 /\ 1:r1=0)