OpenCL MP_ra_dev

{
[x] = 0;
[y] = 0;
}

P0 (global int* x, global atomic_int* y) {
 *x = 1;
 atomic_store_explicit(y, 1,
   memory_order_release,
   memory_scope_device);
}

P1 (global int* x, global atomic_int* y) {
 int r0 = atomic_load_explicit(y,
            memory_order_acquire,
	    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)