C alpha-split-cache-example2 { int u = 0; int v = 0; int *p = &u; } P0(int **p, int *v) { WRITE_ONCE(*v, 1); smp_mb(); WRITE_ONCE(*p, v); } P1(int **p) { int *r1; int r2; r1 = READ_ONCE(*p); smp_read_barrier_depends(); r2 = READ_ONCE(*r1); } exists (1:r1=v /\ 1:r2=0);