AArch64 coRmwWExpNExp TTHM=HD { int x; int y; 0:X1=pte_x; pte_x=(oa:phy_x,db:0,dbm:1,valid:1); 0:X2=(oa:phy_y,db:0,dbm:1,valid:1); 0:X4=x; } P0 ; SWP X2,X9,[X1]; MOV W3,#1 ; STR W3,[X4] ; exists ([PTE(x)]=(oa:PA(y), dbm:1, db:0) /\ [x]=1)