AArch64 2+2WNExpExp+NExpNExp+DMBST+DMBST+SHOW
TTHM=HD
{
int z;
0:X2=x; 1:X4=pte_x;
0:X3=y; 1:X6=pte_y;
1:X5=(oa:phy_z,db:0,dbm:1);
1:X7=(oa:phy_y,db:0,dbm:1);
pte_x=(oa:phy_x,db:0,dbm:1);
pte_y=(oa:phy_y,db:1,dbm:1);
}
P0 | P1 ;
MOV W8,#1 | STR X5,[X4];
LY: | DMB ST ;
STR W8,[X3] | STR X7,[X6];
DMB ST | ;
MOV W9,#1 | ;
LX: | ;
STR W9,[X2] | ;
exists ([PTE(x)]=(oa:PA(z), dbm:1, db:0) /\ [PTE(y)]=(oa:PA(y), dbm:1) /\ [x]=1 /\ [y]=1 /\ [z]=0 /\ ~fault(P0:LX,x) /\ ~fault(P0:LY,y))