C cppmem_iriw_relacq { [x] = 0; [y] = 0; } // This litmus test is ported from an example distributed // with the CppMem tool. Original is available online at: // http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/index.html P0 (atomic_int* x) { atomic_store_explicit(x, 1, memory_order_release); } P1 (atomic_int* y) { atomic_store_explicit(y, 1, memory_order_release); } P2 (atomic_int* x, atomic_int* y) { int r1 = atomic_load_explicit(x, memory_order_acquire); int r2 = atomic_load_explicit(y, memory_order_acquire); } P3 (atomic_int* x, atomic_int* y) { int r3 = atomic_load_explicit(y, memory_order_acquire); int r4 = atomic_load_explicit(x, memory_order_acquire); } exists (2:r1 = 1 /\ 2:r2 = 0 /\ 3:r3 = 1 /\ 3:r4 = 0)