Run RDWI in model, using armmem
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]; exists (P1:R1=2 /\ P1:R2=0 /\ P1:R3=0 /\ P1:R4=1)