Test 2+2W+dmbs+reads

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=0 ; 3:R2=0 ; x=1 ; y=1"

Executions for behaviour: "2:R1=1 ; 2:R2=2 ; 3:R1=0 ; 3:R2=0 ; x=1 ; y=1"

Executions for behaviour: "2:R1=0 ; 2:R2=0 ; 3:R1=2 ; 3:R2=0 ; x=1 ; y=1"

Executions for behaviour: "2:R1=1 ; 2:R2=1 ; 3:R1=2 ; 3:R2=0 ; x=1 ; y=1"

Executions for behaviour: "2:R1=2 ; 2:R2=2 ; 3:R1=2 ; 3:R2=0 ; x=1 ; y=1"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=1 ; 3:R2=1 ; x=1 ; y=1"

Executions for behaviour: "2:R1=1 ; 2:R2=2 ; 3:R1=1 ; 3:R2=1 ; x=1 ; y=1"

Executions for behaviour: "2:R1=1 ; 2:R2=1 ; 3:R1=1 ; 3:R2=2 ; x=1 ; y=1"

Executions for behaviour: "2:R1=2 ; 2:R2=2 ; 3:R1=1 ; 3:R2=2 ; x=1 ; y=1"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=2 ; 3:R2=2 ; x=1 ; y=1"

Executions for behaviour: "2:R1=1 ; 2:R2=2 ; 3:R1=2 ; 3:R2=2 ; x=1 ; y=1"

Executions for behaviour: "2:R1=1 ; 2:R2=0 ; 3:R1=0 ; 3:R2=0 ; x=2 ; y=1"

Executions for behaviour: "2:R1=0 ; 2:R2=0 ; 3:R1=2 ; 3:R2=0 ; x=2 ; y=1"

Executions for behaviour: "2:R1=0 ; 2:R2=1 ; 3:R1=2 ; 3:R2=0 ; x=2 ; y=1"

Executions for behaviour: "2:R1=1 ; 2:R2=1 ; 3:R1=2 ; 3:R2=0 ; x=2 ; y=1"

Executions for behaviour: "2:R1=2 ; 2:R2=2 ; 3:R1=2 ; 3:R2=0 ; x=2 ; y=1"

Executions for behaviour: "2:R1=1 ; 2:R2=0 ; 3:R1=1 ; 3:R2=1 ; x=2 ; y=1"

Executions for behaviour: "2:R1=1 ; 2:R2=0 ; 3:R1=2 ; 3:R2=2 ; x=2 ; y=1"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=0 ; 3:R2=0 ; x=1 ; y=2"

Executions for behaviour: "2:R1=1 ; 2:R2=1 ; 3:R1=1 ; 3:R2=0 ; x=1 ; y=2"

Executions for behaviour: "2:R1=2 ; 2:R2=2 ; 3:R1=1 ; 3:R2=0 ; x=1 ; y=2"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=0 ; 3:R2=1 ; x=1 ; y=2"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=1 ; 3:R2=1 ; x=1 ; y=2"

Executions for behaviour: "2:R1=2 ; 2:R2=0 ; 3:R1=2 ; 3:R2=2 ; x=1 ; y=2"

ARM 2+2W+dmbs+reads ()
"2+2W+dmbs+reads"
{
P0:R5=x ; P0:R6=y ; P0:R1=1 ;P0:R2=2;
P1:R5=x ; P1:R6=y ; P1:R1=1 ;P1:R2=2;
P2:R5=x ;
P3:R6=y ;

}
P0        |P1        |P2        |P3           ;
str R2,R5 |str R2,R6 |ldr R1,R5 |ldr R1,R6 ;
dmb       |dmb       |          |             ;
str R1,R6 |str R1,R5 |ldr R2,R5 |ldr R2,R6 ;
Observed
    2:R1=2; 2:R2=0; 3:R1=0; 3:R2=0; x=1; y=1;
and 2:R1=1; 2:R2=2; 3:R1=0; 3:R2=0; x=1; y=1;
and 2:R1=0; 2:R2=0; 3:R1=2; 3:R2=0; x=1; y=1;
and 2:R1=1; 2:R2=1; 3:R1=2; 3:R2=0; x=1; y=1;
and 2:R1=2; 2:R2=2; 3:R1=2; 3:R2=0; x=1; y=1;
and 2:R1=2; 2:R2=0; 3:R1=1; 3:R2=1; x=1; y=1;
and 2:R1=1; 2:R2=2; 3:R1=1; 3:R2=1; x=1; y=1;
and 2:R1=1; 2:R2=1; 3:R1=1; 3:R2=2; x=1; y=1;
and 2:R1=2; 2:R2=2; 3:R1=1; 3:R2=2; x=1; y=1;
and 2:R1=2; 2:R2=0; 3:R1=2; 3:R2=2; x=1; y=1;
and 2:R1=1; 2:R2=2; 3:R1=2; 3:R2=2; x=1; y=1;
and 2:R1=1; 2:R2=0; 3:R1=0; 3:R2=0; x=2; y=1;
and 2:R1=0; 2:R2=0; 3:R1=2; 3:R2=0; x=2; y=1;
and 2:R1=0; 2:R2=1; 3:R1=2; 3:R2=0; x=2; y=1;
and 2:R1=1; 2:R2=1; 3:R1=2; 3:R2=0; x=2; y=1;
and 2:R1=2; 2:R2=2; 3:R1=2; 3:R2=0; x=2; y=1;
and 2:R1=1; 2:R2=0; 3:R1=1; 3:R2=1; x=2; y=1;
and 2:R1=1; 2:R2=0; 3:R1=2; 3:R2=2; x=2; y=1;
and 2:R1=2; 2:R2=0; 3:R1=0; 3:R2=0; x=1; y=2;
and 2:R1=1; 2:R2=1; 3:R1=1; 3:R2=0; x=1; y=2;
and 2:R1=2; 2:R2=2; 3:R1=1; 3:R2=0; x=1; y=2;
and 2:R1=2; 2:R2=0; 3:R1=0; 3:R2=1; x=1; y=2;
and 2:R1=2; 2:R2=0; 3:R1=1; 3:R2=1; x=1; y=2;
and 2:R1=2; 2:R2=0; 3:R1=2; 3:R2=2; x=1; y=2;