AArch64 LDCLRptex-STRx+db TTHM=HA HD { int x=0; 0:X2=x; 0:X4=pte_x; pte_x=(af:0,db:0,dbm:1); } P0 ; MOV X9,#1 ; LDCLR X9,X6,[X4] ; MOV W1,#1 ; L0: ; STR W1,[X2] ; exists (0:X6=(oa:PA(x), dbm:1) /\ [PTE(x)]=(oa:PA(x), valid:0, dbm:1) /\ [x]=1 /\ ~fault(P0:L0,x))