OpenCL ISA2 { [x] = 0; [y] = 0; [z] = 0; } P0 (global int* x, global atomic_int* y, global atomic_int* z) { *x = 1; atomic_store_explicit(y, 1, memory_order_release, memory_scope_work_group); } P1 (global int* x, global atomic_int* y, global atomic_int* z) { int r0 = atomic_load_explicit(y, memory_order_acquire, memory_scope_work_group); if (1 == r0) atomic_store_explicit(z, 1, memory_order_release, memory_scope_device); } P2 (global int* x, global atomic_int* y, global atomic_int* z) { int r1 = atomic_load_explicit(z, memory_order_acquire, memory_scope_device); int r2 = -1; if (1 == r1) r2 = *x; } scopeTree (device (work_group P0 P1) (work_group P2)) exists (1:r0=1 /\ 2:r1=1 /\ 2:r2=0)