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)