AArch64 LDCLRptex-STRx+db+BIS 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] ; (* Final pte_x value with db:1 and valid:0, while 0:X6 has db:0 *) exists (0:X6=(oa:PA(x), dbm:1) /\ [PTE(x)]=(oa:PA(x), valid:0, dbm:1) /\ [x]=1 /\ ~fault(P0:L0,x))