C 2+2w { [x] = 0; [y] = 0; } P0 (atomic_int* x, atomic_int* y) { atomic_store_explicit(x, 2, memory_order_relaxed); atomic_store_explicit(y, 1, memory_order_relaxed); } P1 (atomic_int* x, atomic_int* y) { atomic_store_explicit(y, 2, memory_order_relaxed); atomic_store_explicit(x, 1, memory_order_relaxed); } exists (x=2 /\ y=2)