Test super-detour2

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;