Test C-Will02

AArch64 C-Will02
(* Test a particular case of linux atomic_add_return *)
{ ok=1;
0:X1=x; 0:X2=y; 0:X9=ok;
1:X2=y; 1:X1=x;
}
 P0               | P1           ;
 MOV W0,#1        | MOV W0,#2    ;
 STR W0,[X1]      | STR W0,[X2]  ;
 MOV W3,#1        | DMB ISH      ;
 LDXR W4,[X2]     | LDR W3,[X1]  ;
 ADD W3,W4,W3     |              ;
 STLXR W5,W3,[X2] |              ;
 CBNZ W5,Fail0    |              ;
 DMB ISH          |              ;
 B Exit0          |              ;
 Fail0:           |              ;
 MOV W8,#0        |              ;
 STR W8,[X9]      |              ;
 Exit0:           |              ;
locations [y;]
~exists (ok=1 /\ 0:X4=0 /\ 1:X3=0)