C super-detour2 { } P0(int *x, int *y, int *u, int *v) { int r0; int r1; r0 = READ_ONCE(*v); WRITE_ONCE(*x, r0); r1 = READ_ONCE(*y); WRITE_ONCE(*u, r1); } P1(int *x, int *z) { int r2; int r3; r2 = smp_load_acquire(x); r3 = READ_ONCE(*z); } P2(int *z, int *y) { WRITE_ONCE(*z, 1); smp_wmb(); WRITE_ONCE(*y, 1); } P3(int *u, int *w) { int r4; int r5; r4 = smp_load_acquire(u); r5 = READ_ONCE(*w); } P4(int *w, int *v) { WRITE_ONCE(*w, 1); smp_wmb(); WRITE_ONCE(*v, 1); } Observed 3:r5=0; 3:r4=1; 1:r3=1; 1:r2=1; 0:r1=1; 0:r0=1; and 3:r5=0; 3:r4=1; 1:r3=0; 1:r2=1; 0:r1=1; 0:r0=1; and 3:r5=0; 3:r4=1; 1:r3=1; 1:r2=0; 0:r1=1; 0:r0=1; and 3:r5=0; 3:r4=1; 1:r3=0; 1:r2=0; 0:r1=1; 0:r0=1;