"VMSA strong"
include "cos.cat"
include "barriers.cat"
include "aarch64_mmu_common.cat"
(* observed by *)
let obs = rfe | fr | wco
(* observing a write through a fetch or translate
* means the write is now visible to the rest of the system
* aka {instruction, translation}->data coherence *)
| trfe
(* dependency-ordered-before *)
let dob =
addr | data
| speculative ; [W]
| addr; po; [W]
| (addr | data); rfi
| (addr | data); trfi
(* atomic-ordered-before *)
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
(* Ordered-before *)
let _ob = obs | dob | aob | bob | iio | tob | obtlbi | ctxob | obfault
let ob = _ob^+
(* 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
(* No translations interposing well-bracketed take/return exceptions *)
(* empty take-to-return & ((ob & int) ; [T] ; (ob & higher-EL)) *)