AArch64 coWWExp-TLBI-NExp+VMALL 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 ; STR X2,[X1] ; DSB ISH ; TLBI VMALLE1IS ; DSB ISH ; MOV W3,#1 ; STR W3,[X4] ; exists ([PTE(x)]=(oa:PA(y), dbm:1, db:0) /\ [x]=1)