…
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))