OpenCL MP_sc_dev { [x] = 0; [y] = 0; } P0 (global int* x, global atomic_int* y) { *x = 1; atomic_store_explicit(y, 1, memory_order_seq_cst, memory_scope_device); } P1 (global int* x, global atomic_int* y) { int r0 = atomic_load_explicit(y, memory_order_seq_cst, memory_scope_device); int r1 = -1; if (1 == r0) r1 = *x; } scopeTree (device (work_group P0) (work_group P1)) exists (1:r0=1 /\ 1:r1=0)