Executions for behaviour: "1:R0=0 ; 1:R1=0 ; x=1"

Executions for behaviour: "1:R0=1 ; 1:R1=0 ; x=1"

Executions for behaviour: "1:R0=2 ; 1:R1=0 ; x=1"

Executions for behaviour: "1:R0=0 ; 1:R1=1 ; x=1"

Executions for behaviour: "1:R0=1 ; 1:R1=1 ; x=1"

Executions for behaviour: "1:R0=2 ; 1:R1=1 ; x=1"

Executions for behaviour: "1:R0=0 ; 1:R1=2 ; x=1"

Executions for behaviour: "1:R0=1 ; 1:R1=2 ; x=1"

Executions for behaviour: "1:R0=2 ; 1:R1=2 ; x=1"

Executions for behaviour: "1:R0=1 ; 1:R1=0 ; x=2"

Executions for behaviour: "1:R0=2 ; 1:R1=0 ; x=2"

Executions for behaviour: "1:R0=2 ; 1:R1=1 ; x=2"
ARM MP+pos+dmb
"PosWW Rfe DMBsRR Fre"
Cycle=Rfe DMBsRR Fre PosWW
Relax=
Safe=Rfe Fre PosWW DMBsRR
Prefetch=
Com=Rf Fr
Orig=PosWW Rfe DMBsRR Fre
{
%x0=x;
%x1=x;
}
P0 | P1 ;
MOV R0,#1 | LDR R0,[%x1] ;
STR R0,[%x0] | DMB ;
MOV R1,#2 | LDR R1,[%x1] ;
STR R1,[%x0] | ;
Observed
1:R0=0; 1:R1=0; x=1;
and 1:R0=1; 1:R1=0; x=1;
and 1:R0=2; 1:R1=0; x=1;
and 1:R0=0; 1:R1=1; x=1;
and 1:R0=1; 1:R1=1; x=1;
and 1:R0=2; 1:R1=1; x=1;
and 1:R0=0; 1:R1=2; x=1;
and 1:R0=1; 1:R1=2; x=1;
and 1:R0=2; 1:R1=2; x=1;
and 1:R0=1; 1:R1=0; x=2;
and 1:R0=2; 1:R1=0; x=2;
and 1:R0=2; 1:R1=1; x=2;