include "barriers.cat"
(* For each instruction, for each read performed by the translation
table walk ASL code, we generate one translate-read (T) event. If
the translation finds an invalid entry, the translate-read event
will additionally belong to T_f. *)
set T
set T_f
(* T events which are part of a Stage 1 or 2 walk *)
set Stage1
set Stage2
set read_VMID
set read_ASID
relation same-translation
(* A write of an invalid descriptor (an even value) is in W_invalid *)
set W_invalid
(* A write of a valid descriptor (an odd value) is in W_valid *)
set W_valid
(* initial writes *)
set is_IW
(* trf is the translate analogue of rf, such that writes are
trf-related to translates that read them. trf1 is trf
restricted to stage 1 reads, and trf2 for stage 2 reads *)
relation trf
relation trf1
relation trf2
relation wco
relation iio
relation instruction-order
(* e1 speculative e2
* iff e2 was conditionally executed based on the value of e1
*)
let speculative =
ctrl
| addr; po
| [T] ; instruction-order
(* po-pa relates all events from instructions in instruction-order to the same PA *)
let po-pa = instruction-order & loc
let trfi = trf & int
let trfe = trf \ trfi
(* likewise, tfr is the translate analogue of fr *)
(* we use overlap-loc not loc here to handle the case where
* multiple translations get merged into a single event *)
relation overlap-loc
let tfr1 = (((trf1^-1); co) \ id) & overlap-loc
let tfr2 = (((trf2^-1); co) \ id) & overlap-loc
let tfr = tfr1 | tfr2
let tfri = tfr & int
let tfre = tfr \ tfri
(* translate and TLBI events with VAs within the same 4K region
* are related by same-va-page, similarly for IPAs and same-ipa-page *)
relation same-va-page
relation same-ipa-page
relation same-asid-internal
relation same-vmid-internal
relation tlbi-to-asid-read
relation tlbi-to-vmid-read
(* for convenience, derive some handy embeddings of program-order into
* some subset of the events *)
(*
* THESE ARE GENERATED BY ISLA
let instruction-order = iio^-1 ; fpo ; iio
let po = [M|F|C] ; instruction-order ; [M|F|C]
let tpo = [T] ; instruction-order ; [T]
*)
(* addr is now derived from the data dependency into the translate-reads
* if a translation exists *)
(*
* THIS IS GENERATED BY ISLA
let _addr =
tdata ; [M]
| tdata ; iio+ ; [R|W]
| tdata ; [T_f]
*)
(* CSEs are context-synchronization-events
* that is an ISB, and taking/returning from an exception *)
(*
let CSE = ISB | TE | ERET
*)
(* Context changing operations
* are those that write to system registers
*)
let ContextChange = MSR | TE | ERET
(* fault events come from reads or writes *)
let Fault = TE (* TakeException, this is overly general *)
let IsTranslationFault = Fault
let IsPermissionFault = Fault
set IsFromR (* events originating from an Arm LDR instruction *)
set IsFromW (* events originating from an Arm STR instruction *)
set IsFromReleaseW (* events originating from an Arm STLR instruction *)
(* Currently we only use same-vmid/same-asid between TLBIs and
* translates, so this relation defines them in a minimal way.
*)
let same-vmid = tlbi-to-vmid-read; [read_VMID]; same-translation
let same-asid = tlbi-to-asid-read; [read_ASID]; same-translation
(* A TLBI barriers some writes, making them unobservable to "future" reads from a translation table walk.
*
* tseq1 relates writes with TLBIs that ensure their visibility
* e.g. `a: Wpte(x) ; b: Wpte(x) ; c: Wpte(x) ; d: TLBI x`
* then `c ; tseq1 ; d`
* as a, b are no longer visible to translation table walks
*)
let tlb_might_affect =
[ TLBI-S1 & ~TLBI-S2 & TLBI-VA & TLBI-ASID & TLBI-VMID] ; (same-va-page & same-asid & same-vmid) ; [T & Stage1]
| [ TLBI-S1 & ~TLBI-S2 & ~TLBI-VA & TLBI-ASID & TLBI-VMID] ; (same-asid & same-vmid) ; [T & Stage1]
| [ TLBI-S1 & ~TLBI-S2 & ~TLBI-VA & ~TLBI-ASID & TLBI-VMID] ; same-vmid ; [T & Stage1]
| [~TLBI-S1 & TLBI-S2 & TLBI-IPA & ~TLBI-ASID & TLBI-VMID] ; (same-ipa-page & same-vmid) ; [T & Stage2]
| [~TLBI-S1 & TLBI-S2 & ~TLBI-IPA & ~TLBI-ASID & TLBI-VMID] ; same-vmid ; [T & Stage2]
| [ TLBI-S1 & TLBI-S2 & ~TLBI-IPA & ~TLBI-ASID & TLBI-VMID] ; same-vmid ; [T]
| ( TLBI-S1 & ~TLBI-IPA & ~TLBI-ASID & ~TLBI-VMID) * (T & Stage1)
| ( TLBI-S2 & ~TLBI-IPA & ~TLBI-ASID & ~TLBI-VMID) * (T & Stage2)
(* | (TLBI-ALL * T) *)
let tlb-affects =
[TLBI-IS] ; tlb_might_affect
| ([~TLBI-IS] ; tlb_might_affect) & int
(* [T] -> [TLBI] where the T reads-from a write before the TLBI and the TLBI is to the same addr
* this doesn't mean the T happened before the TLBI, but it does mean there could have been a cached version
* which the TLBI threw away
*)
let maybe_TLB_cached =
([T] ; trf^-1 ; wco ; [TLBI-S1]) & tlb-affects^-1
(* translation-ordered-before *)
let tob =
(* a faulting translation must read from flat memory or newer *)
[T_f] ; tfre
(* cannot forward past a DSB *)
| ([T_f] ; tfri ; [W]) & (po ; [dsbst] ; instruction-order)^-1
(* no forwarding from speculative writes *)
| speculative ; trfi
let tlb_barriered =
([T] ; tfr ; wco ; [TLBI]) & tlb-affects^-1
let obtlbi_translate =
(* A S1 translation must read from TLB/memory before the TLBI which
* invalidates that entry happens *)
[T & Stage1] ; tlb_barriered ; [TLBI-S1]
(* if the S2 translation is ordered before some S2 write
* then the S1 translation has to be ordered before the subsequent
* S1 invalidate which would force the S2 write to be visible
*
* this applies to S2 translations during a S1 walk as well
* here the Stage2 translation is only complete once the TLBI VA which
* invalidates previous translation-table-walks have been complete *)
(* if the S1 translation is from after the TLBI VA
* then the S2 translation is only ordered after the TLBI IPA
*)
| ([T & Stage2] ; tlb_barriered ; [TLBI-S2])
& (same-translation ; [T & Stage1] ; trf^-1 ; wco^-1)
(* if the S1 translation is from before the TLBI VA,
* then the S2 translation is ordered after the TLBI VA
*)
| (([T & Stage2] ; tlb_barriered ; [TLBI-S2]) ; wco? ; [TLBI-S1])
& (same-translation ; [T & Stage1] ; maybe_TLB_cached)
(* ordered-before-TLBI *)
let obtlbi =
obtlbi_translate
(*
* a TLBI ensures all instructions that use the old translation
* and their respective memory events
* are ordered before the TLBI.
*)
| [R|W|Fault] ; iio^-1 ; (obtlbi_translate & ext) ; [TLBI]
(* context-change ordered-before *)
(* note that this is under-approximate and future work is needed
* on exceptions and context-changing operations in general *)
let ctxob =
(* no speculating past context-changing operations *)
speculative ; [MSR]
(* context-synchronization orders everything po-after with the synchronization point *)
| [CSE] ; instruction-order
(* context-synchronization acts as a barrier for context-changing operations *)
| [ContextChange] ; po ; [CSE]
(* context-synchronization-events cannot happen speculatively *)
| speculative ; [CSE]
(* ordered-before a translation fault *)
let obfault =
data ; [Fault & IsFromW]
| speculative ; [Fault & IsFromW]
| [dmbst] ; po ; [Fault & IsFromW]
| [dmbld] ; po ; [Fault & (IsFromW | IsFromR)]
| [A|Q] ; po ; [Fault & (IsFromW | IsFromR)]
| [R|W] ; po ; [Fault & IsFromW & IsFromReleaseW]
(* ETS-ordered-before *)
(* if FEAT_ETS then if E1 is ordered-before some Fault
* then E1 is ordered-before the translation-table-walk read which generated that fault
* (but not *every* read from the walk, only the one that directly led to the translation fault)
*
* Additionally, if ETS then TLBIs are guaranteed completed after DSBs
* hence po-later translations must be ordered after the TLBI (D5.10.2)
*)
let obETS =
(obfault ; [Fault]) ; iio^-1 ; [T_f]
| ([TLBI] ; po ; [dsb] ; instruction-order ; [T]) & tlb-affects
include "shows.cat"