C example1 { [x] = 0; [y] = 0; } P0 (atomic_int* x, atomic_int* y) { atomic_store_explicit(x, 1, memory_order_relaxed); } P1 (atomic_int* x, atomic_int* y) { int r1 = atomic_load_explicit(x, memory_order_relaxed); int r2 = atomic_load_explicit(x, memory_order_relaxed); } P2 (atomic_int* x, atomic_int* y) { atomic_store_explicit(x, 2, memory_order_seq_cst); int r3 = atomic_load_explicit(y, memory_order_seq_cst); } P3 (atomic_int* x, atomic_int* y) { atomic_store_explicit(y, 1, memory_order_seq_cst); int r4 = atomic_load_explicit(x, memory_order_seq_cst); } exists (1:r1 = 1 /\ 1:r2 = 2 /\ 2:r3=0 /\ 3:r4=1)