"VMSA weak"
include "cos.cat"
include "aarch64_mmu_common.cat"
include "barriers.cat"
let obs = rfe | fr | wco
let dob = addr | data
| ctrl; [W]
| (ctrl | (addr; po)); [ISB]
| addr; po; [W]
| (addr | data); rfi
| (addr | ctrl | data); trfi
let aob = rmw
| [range(rmw)]; rfi; [A | Q]
(* barrier-ordered-before *)
let bob = [R] ; po ; [dmbld]
| [W] ; po ; [dmbst]
| [dmbst]; po; [W]
| [dmbld]; po; [R|W]
| [L]; po; [A]
| [A | Q]; po; [R | W]
| [R | W]; po; [L]
| [F | C]; po; [dsbsy]
| [dsb] ; po
| [CSE] ; instruction-order
(* Ordered-before *)
let ob = (obs | dob | aob | bob | ctxob)^+
(* Internal visibility requirement *)
acyclic po-loc | fr | co | rf as internal
(* External visibility requirement *)
irreflexive ob as external
(* Atomic: Basic LDXR/STXR constraint to forbid intervening writes. *)
empty rmw & (fre; coe) as atomic
(* Writes cannot forward to po-future translations *)
acyclic (po-pa | trfi) as translation-internal
(* break-before-make S1 *)
empty
([is_IW | W_invalid] ; co ; [W_valid] ; ob ; [CSE] ; instruction-order ; [T & Stage1])
& (ob ; [dsbsy] ; po ; ([TLBI-S1] ; po ; [dsbsy] ; ob ; [CSE] ; instruction-order ; [T]) & tlb-affects)
& trf & loc
as bbm
(* break S1 *)
empty ([is_IW | W] ; co ; [W_invalid] ; ob ; [dsbsy] ; po
; ([TLBI-S1] ; po ; [dsbsy] ; ob ; [M]; iio^-1; [T]) & tlb-affects & ext
) & trf & loc
as brk1
empty ([is_IW | W] ; co ; [W_invalid] ; ob ; [dsbsy] ; po
; ([TLBI-S1] ; po ; [dsbsy] ; ob ; [CSE] ; instruction-order ; [T]) & tlb-affects
) & trf & loc
as brk2
(* break-before-make S2 *)
empty
([is_IW | W_invalid] ; co ; [W_valid] ; ob ; [CSE] ; instruction-order ; [T & Stage2])
& (ob ; [dsbsy] ; po
; ([TLBI-S2] ; po ; [dsbsy] ; po ;
; ([TLBI-S1] ; po ; [dsbsy] ; ob ; [CSE]; instruction-order; [T]) & tlb-affects
; iio ; [T]) & tlb-affects)
& trf & loc
as bbms2
(* break S2 *)
empty ([is_IW | W] ; co ; [W_invalid] ; ob ; [dsbsy] ; po
; ([TLBI-S2] ; po ; [dsbsy] ; po ; ([TLBI-S1] ; po ; [dsbsy] ; ob ; [M]; iio^-1; [T]) & tlb-affects & ext
; iio ; [T]) & tlb-affects & ext
) & trf & loc
as brk1s2
empty ([is_IW | W] ; co ; [W_invalid] ; ob ; [dsbsy] ; po
; ([TLBI-S2] ; po ; [dsbsy] ; po ; ([TLBI-S1] ; po ; [dsbsy] ; ob ; [CSE]; instruction-order; [T]) & tlb-affects
; iio ; [T]) & tlb-affects
) & trf & loc
as brk2s2