AArch64 CASAL+FAIL
Variant=skip
{
int x;
int y;
0:X1=(oa:PA(x),db:0);
0:X2=y; 0:X4=PTE(x);
1:X2=y; 1:X4=x;
}
P0 | P1 ;
MOV W3,#1 | MOV W1,#0 ;
STR W3,[X2] | MOV W3,#1 ;
DSB ISH |L0: ;
STR X1,[X4] | CASAL W1,w3,[X4] ;
| LDR W5,[X2] ;
exists (1:X5=0 /\ fault(P1:L0,x,MMU:Permission))