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