Test CO-MP+dmb+po

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

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

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

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=2 /\ (1:R1=1 \/ 1:R1=0) \/ 1:R0=1 /\ 1:R1=0