Test CO-MP+dmb+po

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

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

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

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

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

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

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

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

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

ARM CO-MP+dmb+po

{0:R2=x; 1:R2=x;}

 P0          | P1          ;
 MOV R0,#1   | LDR R0,[R2] ;
 STR R0,[R2] | LDR R1,[R2] ;
 DMB         |             ;
 MOV R1,#2   |             ;
 STR R1,[R2] |             ;
exists (1:R0=0 /\ 1:R1=0) \/ (1:R0=0 /\ 1:R1=1) \/ (1:R0=0 /\ 1:R1=2) \/ (1:R0=1 /\ 1:R1=0) \/ (1:R0=1 /\ 1:R1=1) \/ (1:R0=1 /\ 1:R1=2) \/ (1:R0=2 /\ 1:R1=0) \/ (1:R0=2 /\ 1:R1=1) \/ (1:R0=2 /\ 1:R1=2)