Executions for behaviour:
"1:R1=2 ; 1:R2=0 ; 1:R3=0 ; 1:R4=1"

ARM RDWI ()
"is RR to same location in ppo?, internal write variation"
Prefetch=1:z=T
{
P1:R6=x; P1:R7=y; P1:R8=z;
P0:R7=y; P0:R8=z;
}
P0 |P1 ;
mov R1,1 |ldr R1,R7 ;
str R1,R8 |and R9,R1,0 ;
dmb |ldr R3,[R9,R6] ;
mov R2,2 |mov R10,1 ;
str R2,R7 |str R10,R6 ;
|ldr R4,R6 ;
|and R10,R4,0 ;
|ldr R2,[R10,R8];
Observed
1:R1=2; 1:R2=0; 1:R3=0; 1:R4=1;