AArch64 coRRNExpNExpExp+DSB5 TTHM=HA HD { 0:X0=x; 0:X1=1; 1:X6=(oa:phy_x,db:0,dbm:1); 1:X0=x; 1:X2=pte_x; pte_x=(db:0,dbm:1); } P0 | P1 ; STR W1, [X0] | LDR W1, [X0]; | DSB SY ; | LDR X3, [X2]; | CMP X3,X6 ; | CSET W5,EQ ; exists (1:X1=1 /\ 1:X5=1)