AArch64 STRx+2LDSETptex+db3 TTHM=HA HD { pte_x=(db:0,dbm:1); 0:X2=x; 1:X4=pte_x; 1:X6=(oa:phy_x,db:0,dbm:1); xs} P0 | P1 ; MOV W1,#1 | MOV X6,#1 ; L0: | LSL X6,X6,#7 ; STR W1,[X2] | LDSET X6,X0,[X4] ; | LDSET X6,X1,[X4] ; exists (1:X0=(oa:PA(x), dbm:1) /\ 1:X1=(oa:PA(x), dbm:1, db:0) /\ [PTE(x)]=(oa:PA(x), dbm:1) /\ [x]=1) \/ (1:X0=(oa:PA(x), dbm:1, db:0) /\ 1:X1=(oa:PA(x), dbm:1) /\ [PTE(x)]=(oa:PA(x), dbm:1) /\ [x]=1)