Library ArchSemArm.VMSA22Arm
From ASCommon Require Import Options.
From ASCommon Require Import Common GRel FMon.
Require Import ArmInst.
Require Import GenAxiomaticArm.
This file define the VMSA model from the ESOP 22 paper by Ben Simner et al.
The reference implementation is at: TODO
Section VMSAArm.
Import Candidate.
Context (regs_whitelist : gset reg).
Context {nmth : nat}.
Context (cd : Candidate.t NMS nmth).
Notation pe := (pre_exec cd).
Notation int := (same_thread pe).
Notation si := (same_instruction_instance cd).
Notation sca := (same_access cd).
Notation instruction_order := (instruction_order pe).
Notation full_instruction_order := (full_instruction_order pe).
Notation iio := (iio pe).
Notation int := (same_thread pe).
Notation si := (same_instruction_instance cd).
Notation sca := (same_access cd).
Notation instruction_order := (instruction_order pe).
Notation full_instruction_order := (full_instruction_order pe).
Notation iio := (iio pe).
Notation RR := (reg_reads pe).
Notation RW := (reg_writes pe).
Notation RE := (RE cd).
Notation rrf := (reg_reads_from cd).
Notation rfr := (reg_from_reads cd).
Notation MSR := (MSR cd).
Notation MRS := (MRS cd).
Notation RW := (reg_writes pe).
Notation RE := (RE cd).
Notation rrf := (reg_reads_from cd).
Notation rfr := (reg_from_reads cd).
Notation MSR := (MSR cd).
Notation MRS := (MRS cd).
Notation W := (explicit_writes pe).
Notation R := (explicit_reads pe).
Notation M := (mem_explicit pe).
Notation Wx := (exclusive_writes pe).
Notation Rx := (exclusive_writes pe).
Notation L := (rel_acq_rcsc_writes pe).
Notation A := (rel_acq_rcsc_reads pe).
Notation Q := (rel_acq_rcpc_reads pe).
Notation T := (ttw_reads pe).
Notation IF := (ifetch_reads pe).
Notation IR := (init_mem_reads cd).
Notation lxsx := (lxsx cd).
Notation amo := (atomic_update cd).
Notation rmw := (rmw cd).
Notation co := (co cd).
Notation coi := (coi cd).
Notation coe := (coe cd).
Notation rf := (rf cd).
Notation rfi := (rfi cd).
Notation rfe := (rfe cd).
Notation fr := (fr cd).
Notation fri := (fri cd).
Notation fre := (fre cd).
Notation frf := (frf cd).
Notation frfi := (frfi cd).
Notation trf := (trf cd).
Notation trfi := (trfi cd).
Notation trfe := (trfe cd).
Notation tfr := (tfr cd).
Notation tfri := (tfri cd).
Notation tfre := (tfre cd).
Notation irf := (irf cd).
Notation irfi := (irfi cd).
Notation irfe := (irfe cd).
Notation ifr := (ifr cd).
Notation ifri := (ifri cd).
Notation ifre := (ifre cd).
Notation R := (explicit_reads pe).
Notation M := (mem_explicit pe).
Notation Wx := (exclusive_writes pe).
Notation Rx := (exclusive_writes pe).
Notation L := (rel_acq_rcsc_writes pe).
Notation A := (rel_acq_rcsc_reads pe).
Notation Q := (rel_acq_rcpc_reads pe).
Notation T := (ttw_reads pe).
Notation IF := (ifetch_reads pe).
Notation IR := (init_mem_reads cd).
Notation lxsx := (lxsx cd).
Notation amo := (atomic_update cd).
Notation rmw := (rmw cd).
Notation co := (co cd).
Notation coi := (coi cd).
Notation coe := (coe cd).
Notation rf := (rf cd).
Notation rfi := (rfi cd).
Notation rfe := (rfe cd).
Notation fr := (fr cd).
Notation fri := (fri cd).
Notation fre := (fre cd).
Notation frf := (frf cd).
Notation frfi := (frfi cd).
Notation trf := (trf cd).
Notation trfi := (trfi cd).
Notation trfe := (trfe cd).
Notation tfr := (tfr cd).
Notation tfri := (tfri cd).
Notation tfre := (tfre cd).
Notation irf := (irf cd).
Notation irfi := (irfi cd).
Notation irfe := (irfe cd).
Notation ifr := (ifr cd).
Notation ifri := (ifri cd).
Notation ifre := (ifre cd).
Registers
Definition is_illegal_reg_write (regs : gset reg) :=
is_reg_writeP (λ reg acc _, reg ∉ regs ∨ acc ≠ None).
#[export] Instance is_illegal_reg_write_dec regs ev :
Decision (is_illegal_reg_write regs ev).
Proof. unfold_decide. Defined.
Definition Illegal_RW := collect_all (λ _, is_illegal_reg_write regs_whitelist) cd.
Notation "'id'" := ⦗valid_eids cd⦘.
Definition valid_eids_rc r := r ∪ id.
Definition valid_eids_compl a := (valid_eids cd) ∖ a.
Notation "a ?" := (valid_eids_rc a) (at level 1, format "a ?") : stdpp_scope.
Notation "'~~' a" := (valid_eids_compl a)
(at level 1, format "~~ a") : stdpp_scope.
Explicit memory
- Explicit
- TTW
- IFetch
Definition wco := (coherence cd).
#[local] Hint Extern 10 (Decision (?x _)) ⇒ unfold x : typeclass_instances.
#[local] Hint Extern 10 (Decision (?x _ _)) ⇒ unfold x : typeclass_instances.
#[local] Hint Extern 10 (Decision (?x _ _ _)) ⇒ unfold x : typeclass_instances.
Definition is_tlbi_op (tlbiop : TLBIOp) (tlbop : TLBIInfo) :=
tlbop.(TLBIInfo_rec).(TLBIRecord_op) = tlbiop.
Definition has_tlbi_op (event : iEvent) (tlbiop : TLBIOp) :=
is_tlbopP (is_tlbi_op tlbiop) event.
Definition TLBI_ASID :=
collect_all (λ _ event, has_tlbi_op event TLBIOp_ASID
∨ has_tlbi_op event TLBIOp_VA
∨ has_tlbi_op event TLBIOp_VAA) cd.
Definition TLBI_S1 :=
collect_all (λ _ event, has_tlbi_op event TLBIOp_VA
∨ has_tlbi_op event TLBIOp_VMALLS12
∨ has_tlbi_op event TLBIOp_VMALL
∨ has_tlbi_op event TLBIOp_ALL
∨ has_tlbi_op event TLBIOp_ASID) cd.
Definition TLBI_S2 :=
collect_all (λ _ event, has_tlbi_op event TLBIOp_IPAS2
∨ has_tlbi_op event TLBIOp_VMALLS12
∨ has_tlbi_op event TLBIOp_VMALL
∨ has_tlbi_op event TLBIOp_ALL
∨ has_tlbi_op event TLBIOp_ASID) cd.
Definition TLBI_VMID :=
collect_all (λ _ event, has_tlbi_op event TLBIOp_VA
∨ has_tlbi_op event TLBIOp_VAA
∨ has_tlbi_op event TLBIOp_IPAS2
∨ has_tlbi_op event TLBIOp_VMALLS12
∨ has_tlbi_op event TLBIOp_VMALL
∨ has_tlbi_op event TLBIOp_ASID) cd.
Definition TLBI_VA :=
collect_all (λ _ event, has_tlbi_op event TLBIOp_VA) cd.
Definition TLBI_IPA :=
collect_all (λ _ event, has_tlbi_op event TLBIOp_IPAS2) cd.
regime
Definition is_tlbi_regime (reg : Regime) (tlbop : TLBIInfo) :=
tlbop.(TLBIInfo_rec).(TLBIRecord_regime) = reg.
Definition has_tlbi_regime (event : iEvent) (reg : Regime) :=
is_tlbopP (is_tlbi_regime reg) event.
Definition TLBI_EL1 :=
collect_all (λ _ event, has_tlbi_regime event Regime_EL10) cd.
Definition TLBI_EL2 :=
collect_all (λ _ event, has_tlbi_regime event Regime_EL2) cd.
tlbop.(TLBIInfo_rec).(TLBIRecord_regime) = reg.
Definition has_tlbi_regime (event : iEvent) (reg : Regime) :=
is_tlbopP (is_tlbi_regime reg) event.
Definition TLBI_EL1 :=
collect_all (λ _ event, has_tlbi_regime event Regime_EL10) cd.
Definition TLBI_EL2 :=
collect_all (λ _ event, has_tlbi_regime event Regime_EL2) cd.
shareability
Definition is_tlbi_shareability (share : Shareability)
(tlbop : TLBIInfo) :=
tlbop.(TLBIInfo_shareability) = share.
Definition has_tlbi_shareability (event : iEvent) (share : Shareability) :=
is_tlbopP (is_tlbi_shareability share) event.
Definition TLBI_IS :=
collect_all (λ _ event, has_tlbi_shareability event Shareability_ISH
∨ has_tlbi_shareability event Shareability_OSH) cd.
Definition same_translation : grel EID.t := same_instruction_instance cd.
Definition get_translation_start (eid : EID.t) : option trans_start :=
'(instr_trace, _) ← lookup_instruction cd eid.(EID.tid) eid.(EID.iid);
let trace_before := take eid.(EID.ieid) instr_trace in
last $ omap get_trans_start trace_before.
Definition get_vmid (eid : EID.t) (event : iEvent) :=
if event is TlbOp tlbop &→ _
then Some tlbop.(TLBIInfo_rec).(TLBIRecord_asid)
else
ts ← get_translation_start eid;
Some ts.(TranslationStartInfo_asid).
Definition same_vmid := same_key get_vmid cd.
Definition get_asid (eid : EID.t) (event : iEvent) :=
if event is TlbOp tlbop &→ _
then Some tlbop.(TLBIInfo_rec).(TLBIRecord_asid)
else
ts ← get_translation_start eid;
Some ts.(TranslationStartInfo_asid).
Definition same_asid := same_key get_asid cd.
Definition tlbi_translate_same_asid : grel EID.t :=
(TLBI_ASID × T) ∩ same_asid.
Definition tlbi_translate_same_vmid : grel EID.t :=
(TLBI_VMID × T) ∩ same_vmid.
Definition page_of_addr (ad: bits 64): bits 36 := bv_extract 12 36 ad.
Inductive TLBI_addr_kind :=
| TLBI_ak_unsupported
| TLBI_ak_no
| TLBI_ak_va
| TLBI_ak_ipa.
(tlbop : TLBIInfo) :=
tlbop.(TLBIInfo_shareability) = share.
Definition has_tlbi_shareability (event : iEvent) (share : Shareability) :=
is_tlbopP (is_tlbi_shareability share) event.
Definition TLBI_IS :=
collect_all (λ _ event, has_tlbi_shareability event Shareability_ISH
∨ has_tlbi_shareability event Shareability_OSH) cd.
Definition same_translation : grel EID.t := same_instruction_instance cd.
Definition get_translation_start (eid : EID.t) : option trans_start :=
'(instr_trace, _) ← lookup_instruction cd eid.(EID.tid) eid.(EID.iid);
let trace_before := take eid.(EID.ieid) instr_trace in
last $ omap get_trans_start trace_before.
Definition get_vmid (eid : EID.t) (event : iEvent) :=
if event is TlbOp tlbop &→ _
then Some tlbop.(TLBIInfo_rec).(TLBIRecord_asid)
else
ts ← get_translation_start eid;
Some ts.(TranslationStartInfo_asid).
Definition same_vmid := same_key get_vmid cd.
Definition get_asid (eid : EID.t) (event : iEvent) :=
if event is TlbOp tlbop &→ _
then Some tlbop.(TLBIInfo_rec).(TLBIRecord_asid)
else
ts ← get_translation_start eid;
Some ts.(TranslationStartInfo_asid).
Definition same_asid := same_key get_asid cd.
Definition tlbi_translate_same_asid : grel EID.t :=
(TLBI_ASID × T) ∩ same_asid.
Definition tlbi_translate_same_vmid : grel EID.t :=
(TLBI_VMID × T) ∩ same_vmid.
Definition page_of_addr (ad: bits 64): bits 36 := bv_extract 12 36 ad.
Inductive TLBI_addr_kind :=
| TLBI_ak_unsupported
| TLBI_ak_no
| TLBI_ak_va
| TLBI_ak_ipa.
Classifies the use of the TLBI address field (TLBIRecord_address).
The results can be:
TODO write this function in Sail so other sail backends can use it?
- This TLBI is unsupported (because Aarch32, VMSA128, or GPT/RME)
- doesn't use an address, thus this field is unused
- use the address as a virtual address (VA)
- use the address as a intermediate physical address (IPA)
Definition get_TLBI_addr_kind (top : TLBIOp) : TLBI_addr_kind :=
match top with
| TLBIOp_ALL ⇒ TLBI_ak_no
| TLBIOp_ASID ⇒ TLBI_ak_no
| TLBIOp_IPAS2 ⇒ TLBI_ak_ipa
| TLBIOp_VAA ⇒ TLBI_ak_va
| TLBIOp_VA ⇒ TLBI_ak_va
| TLBIOp_VMALL ⇒ TLBI_ak_no
| TLBIOp_VMALLS12 ⇒ TLBI_ak_no
| TLBIOp_RIPAS2 ⇒ TLBI_ak_ipa
| TLBIOp_RVAA ⇒ TLBI_ak_va
| TLBIOp_RVA ⇒ TLBI_ak_va
| _ ⇒ TLBI_ak_unsupported
end.
Definition get_va_page (eid : EID.t) (event : iEvent) :=
if event is TlbOp tlbop &→ _
then
guard (get_TLBI_addr_kind tlbop.(TLBIInfo_rec).(TLBIRecord_op) = TLBI_ak_va);;
Some $ page_of_addr tlbop.(TLBIInfo_rec).(TLBIRecord_address)
else
ts ← get_translation_start eid;
Some $ page_of_addr ts.(TranslationStartInfo_va).
Definition va_page_overlap :=
same_key get_va_page cd.
Definition get_ipa_page (eid : EID.t) (event : iEvent) :=
if event is TlbOp tlbop &→ _
then
guard (get_TLBI_addr_kind tlbop.(TLBIInfo_rec).(TLBIRecord_op) = TLBI_ak_ipa);;
Some $ page_of_addr tlbop.(TLBIInfo_rec).(TLBIRecord_address)
else
ts ← get_translation_start eid;
guard (ts.(TranslationStartInfo_regime) = Regime_EL10);;
Some $ page_of_addr ts.(TranslationStartInfo_va).
Definition ipa_page_overlap :=
same_key get_ipa_page cd.
Definition tlbi_translate_same_va_page : grel EID.t :=
(TLBI_VA × T) ∩ va_page_overlap.
Definition tlbi_translate_same_ipa_page : grel EID.t :=
(TLBI_IPA × T) ∩ ipa_page_overlap.
Section isFault.
Context (P : FaultRecord → Prop).
Implicit Type ev : iEvent.
Definition is_faultP :=
is_take_exceptionP (λ e, if e is Some f then P f else False).
Typeclasses Opaque is_faultP.
Definition is_faultP_spec ev:
is_faultP ev ↔
∃ flt, ev = TakeException (Some flt) &→ () ∧ P flt.
Proof.
clear - P ev.
destruct ev as [[] fret];
split; cdestruct |- ? #CDestrMatch; destruct fret; sauto lq:on dep:on.
Qed.
Context `{Pdec: ∀ c, Decision (P c)}.
#[global] Instance is_faultP_dec ev: Decision (is_faultP ev).
Proof using Pdec. unfold is_faultP. solve_decision. Defined.
End isFault.
Notation is_fault := (is_faultP (λ _, True)).
Definition Fault := collect_all (λ _ event, is_fault event) cd.
Definition Fault_T :=
collect_all
(λ _ event,
is_faultP
(λ fault, fault.(FaultRecord_statuscode) = Fault_Translation) event) cd.
Definition Fault_P :=
collect_all
(λ _ event,
is_faultP
(λ fault, fault.(FaultRecord_statuscode) = Fault_Permission) event) cd.
Definition FaultFromR :=
collect_all
(λ _ event,
is_faultP (λ fault, fault.(FaultRecord_write) = false) event) cd.
Definition FaultFromW :=
collect_all
(λ _ event,
is_faultP (λ fault, fault.(FaultRecord_write) = true) event) cd.
Definition FaultFromAquireR :=
collect_all
(λ _ event,
is_faultP
(λ fault, fault.(FaultRecord_write) = false
∧ fault.(FaultRecord_access).(AccessDescriptor_acqsc)) event) cd.
Definition FaultFromReleaseW :=
collect_all
(λ _ event,
is_faultP
(λ fault, fault.(FaultRecord_write) = true
∧ fault.(FaultRecord_access).(AccessDescriptor_relsc)) event) cd.
Notation T_f := (T_f cd).
match top with
| TLBIOp_ALL ⇒ TLBI_ak_no
| TLBIOp_ASID ⇒ TLBI_ak_no
| TLBIOp_IPAS2 ⇒ TLBI_ak_ipa
| TLBIOp_VAA ⇒ TLBI_ak_va
| TLBIOp_VA ⇒ TLBI_ak_va
| TLBIOp_VMALL ⇒ TLBI_ak_no
| TLBIOp_VMALLS12 ⇒ TLBI_ak_no
| TLBIOp_RIPAS2 ⇒ TLBI_ak_ipa
| TLBIOp_RVAA ⇒ TLBI_ak_va
| TLBIOp_RVA ⇒ TLBI_ak_va
| _ ⇒ TLBI_ak_unsupported
end.
Definition get_va_page (eid : EID.t) (event : iEvent) :=
if event is TlbOp tlbop &→ _
then
guard (get_TLBI_addr_kind tlbop.(TLBIInfo_rec).(TLBIRecord_op) = TLBI_ak_va);;
Some $ page_of_addr tlbop.(TLBIInfo_rec).(TLBIRecord_address)
else
ts ← get_translation_start eid;
Some $ page_of_addr ts.(TranslationStartInfo_va).
Definition va_page_overlap :=
same_key get_va_page cd.
Definition get_ipa_page (eid : EID.t) (event : iEvent) :=
if event is TlbOp tlbop &→ _
then
guard (get_TLBI_addr_kind tlbop.(TLBIInfo_rec).(TLBIRecord_op) = TLBI_ak_ipa);;
Some $ page_of_addr tlbop.(TLBIInfo_rec).(TLBIRecord_address)
else
ts ← get_translation_start eid;
guard (ts.(TranslationStartInfo_regime) = Regime_EL10);;
Some $ page_of_addr ts.(TranslationStartInfo_va).
Definition ipa_page_overlap :=
same_key get_ipa_page cd.
Definition tlbi_translate_same_va_page : grel EID.t :=
(TLBI_VA × T) ∩ va_page_overlap.
Definition tlbi_translate_same_ipa_page : grel EID.t :=
(TLBI_IPA × T) ∩ ipa_page_overlap.
Section isFault.
Context (P : FaultRecord → Prop).
Implicit Type ev : iEvent.
Definition is_faultP :=
is_take_exceptionP (λ e, if e is Some f then P f else False).
Typeclasses Opaque is_faultP.
Definition is_faultP_spec ev:
is_faultP ev ↔
∃ flt, ev = TakeException (Some flt) &→ () ∧ P flt.
Proof.
clear - P ev.
destruct ev as [[] fret];
split; cdestruct |- ? #CDestrMatch; destruct fret; sauto lq:on dep:on.
Qed.
Context `{Pdec: ∀ c, Decision (P c)}.
#[global] Instance is_faultP_dec ev: Decision (is_faultP ev).
Proof using Pdec. unfold is_faultP. solve_decision. Defined.
End isFault.
Notation is_fault := (is_faultP (λ _, True)).
Definition Fault := collect_all (λ _ event, is_fault event) cd.
Definition Fault_T :=
collect_all
(λ _ event,
is_faultP
(λ fault, fault.(FaultRecord_statuscode) = Fault_Translation) event) cd.
Definition Fault_P :=
collect_all
(λ _ event,
is_faultP
(λ fault, fault.(FaultRecord_statuscode) = Fault_Permission) event) cd.
Definition FaultFromR :=
collect_all
(λ _ event,
is_faultP (λ fault, fault.(FaultRecord_write) = false) event) cd.
Definition FaultFromW :=
collect_all
(λ _ event,
is_faultP (λ fault, fault.(FaultRecord_write) = true) event) cd.
Definition FaultFromAquireR :=
collect_all
(λ _ event,
is_faultP
(λ fault, fault.(FaultRecord_write) = false
∧ fault.(FaultRecord_access).(AccessDescriptor_acqsc)) event) cd.
Definition FaultFromReleaseW :=
collect_all
(λ _ event,
is_faultP
(λ fault, fault.(FaultRecord_write) = true
∧ fault.(FaultRecord_access).(AccessDescriptor_relsc)) event) cd.
Notation T_f := (T_f cd).
Stage 2 is temporarily disabled because the current Arm instantiation in
translation start/end doesn't support it
Definition Stage1 := T. Definition Stage2 : gset EID.t:= ∅.
Definition speculative := ctrl ∪ (addr⨾po).
Definition ContextChange := MSR ∪ TE ∪ ERET.
Definition CSE := ISB ∪ TE ∪ ERET.
Definition tlb_might_affect :=
(⦗TLBI_S1 ∩ ~~TLBI_S2 ∩ TLBI_VA ∩ TLBI_ASID⦘⨾
(tlbi_translate_same_va_page ∩ tlbi_translate_same_asid
∩ tlbi_translate_same_vmid)⨾⦗T ∩ Stage1⦘)
∪ (⦗TLBI_S1 ∩ ~~TLBI_S2 ∩ TLBI_VA ∩ TLBI_ASID ∩ ~~TLBI_VMID⦘
⨾(tlbi_translate_same_va_page ∩ tlbi_translate_same_asid)⨾⦗T ∩ Stage1⦘)
∪ (⦗TLBI_S1 ∩ ~~TLBI_S2 ∩ ~~TLBI_VA ∩ TLBI_ASID ∩ TLBI_VMID⦘
⨾(tlbi_translate_same_asid ∩ tlbi_translate_same_vmid)⨾⦗T ∩ Stage1⦘)
∪ (⦗TLBI_S1 ∩ ~~TLBI_S2 ∩ ~~TLBI_VA ∩ ~~TLBI_ASID ∩ TLBI_VMID⦘
⨾tlbi_translate_same_vmid⨾⦗T ∩ Stage1⦘)
∪ (⦗~~TLBI_S1 ∩ TLBI_S2 ∩ TLBI_IPA ∩ ~~TLBI_ASID ∩ TLBI_VMID⦘
⨾(tlbi_translate_same_ipa_page ∩ tlbi_translate_same_vmid)⨾⦗T ∩ Stage2⦘)
∪ (⦗~~TLBI_S1 ∩ TLBI_S2 ∩ ~~TLBI_IPA ∩ ~~TLBI_ASID ∩ TLBI_VMID⦘⨾
tlbi_translate_same_vmid⨾⦗T ∩ Stage2⦘)
∪ (⦗TLBI_S1 ∩ TLBI_S2 ∩ ~~TLBI_IPA ∩ ~~TLBI_ASID ∩ TLBI_VMID⦘⨾
tlbi_translate_same_vmid⨾⦗T⦘)
∪ (TLBI_S1 ∩ ~~TLBI_IPA ∩ ~~TLBI_ASID ∩ ~~TLBI_VMID) × (T ∩ Stage1)
∪ (TLBI_S2 ∩ ~~TLBI_IPA ∩ ~~TLBI_ASID ∩ ~~TLBI_VMID) × (T ∩ Stage2).
Definition tlb_affects :=
(⦗TLBI_IS⦘⨾tlb_might_affect)
∪ (⦗~~TLBI_IS⦘⨾tlb_might_affect) ∩ int.
Definition maybe_TLB_cached :=
((⦗T⦘⨾trf⁻¹⨾wco⨾⦗TLBI_S1⦘) ∪
((T ∖ grel_rng trf) × (TLBI_S1 ∩ (grel_dom wco ∖ grel_rng wco)))
) ∩ tlb_affects⁻¹.
Definition tob :=
(⦗T_f⦘⨾tfr) ∪ (speculative⨾trfi).
Definition tlb_barriered :=
(⦗T⦘⨾tfr⨾wco⨾⦗TLBI⦘) ∩ tlb_affects⁻¹.
Definition obtlbi_translate :=
(⦗T ∩ Stage1⦘⨾tlb_barriered⨾⦗TLBI_S1⦘)
∪ ((⦗T ∩ Stage2⦘⨾tlb_barriered⨾⦗TLBI_S2⦘)
∩ (same_translation⨾⦗T ∩ Stage1⦘⨾trf⁻¹⨾wco⁻¹))
∪ (((⦗T ∩ Stage2⦘⨾tlb_barriered⨾⦗TLBI_S2⦘)⨾(wco ?)⨾⦗TLBI_S1⦘)
∩ (same_translation⨾⦗T ∩ Stage1⦘⨾maybe_TLB_cached)).
Definition obtlbi :=
obtlbi_translate
∪ (⦗R ∪ W ∪ Fault⦘⨾iio⁻¹⨾(obtlbi_translate ∖ int)⨾⦗TLBI⦘).
Definition ctxob :=
(speculative⨾⦗MSR⦘)
∪ (⦗CSE⦘⨾instruction_order)
∪ (⦗ContextChange⦘⨾po⨾⦗CSE⦘)
∪ (speculative⨾⦗CSE⦘).
Definition obfault :=
data⨾⦗Fault_T ∩ FaultFromW⦘
∪ speculative⨾⦗Fault_T ∩ FaultFromW⦘
∪ ⦗dmb_store cd⦘⨾po⨾⦗Fault_T ∩ FaultFromW⦘
∪ ⦗dmb_load cd⦘⨾po⨾⦗Fault_T ∩ (FaultFromW ∪ FaultFromR)⦘
∪ ⦗A ∪ Q⦘⨾po⨾⦗Fault_T ∩ (FaultFromW ∪ FaultFromR)⦘
∪ ⦗R ∪ W⦘⨾po⨾⦗Fault_T ∩ FaultFromW ∩ FaultFromReleaseW⦘.
Definition obETS :=
((obfault⨾⦗Fault_T⦘)⨾iio⁻¹⨾⦗T_f⦘)
∪ ((⦗TLBI⦘⨾po⨾⦗dsbsy cd⦘⨾instruction_order⨾⦗T⦘) ∩ tlb_affects).
Definition obETS2 :=
⦗M⦘⨾po⨾⦗T_f⦘
∪ ⦗dsbsy cd⦘⨾instruction_order⨾⦗IF⦘⨾iio⨾⦗T⦘.
Definition obs := rfe ∪ fr ∪ wco ∪ trfe.
Definition dob :=
addr ∪ data
∪ (speculative⨾⦗W⦘)
∪ ((addr ∪ data)⨾rfi)
∪ ((addr ∪ data)⨾trfi).
Definition aob :=
rmw
∪ (⦗grel_rng rmw⦘⨾rfi⨾(⦗A⦘∪⦗Q⦘)).
Definition bob :=
(⦗R⦘⨾po⨾⦗dmb_load cd⦘)
∪ (⦗W⦘⨾po⨾⦗dmb_store cd⦘)
∪ (⦗dmb cd⦘⨾po⨾⦗W⦘)
∪ (⦗dmb_load cd⦘⨾po⨾⦗R⦘)
∪ (⦗grel_rng (⦗A⦘⨾amo⨾⦗L⦘)⦘⨾po⨾⦗M⦘)
∪ (⦗L⦘⨾po⨾⦗A⦘)
∪ (⦗A ∪ Q⦘⨾po⨾⦗M⦘)
∪ (⦗M⦘⨾po⨾⦗L⦘)
∪ (⦗dsb cd⦘⨾po⨾⦗MSR ∪ M ∪ F ∪ C ∪ TE ∪ ERET⦘)
∪ (⦗ISB⦘⨾ instruction_order).
Definition ob1 := obs ∪ dob ∪ aob ∪ bob ∪ iio ∪ tob ∪ obtlbi ∪ ctxob
∪ obfault ∪ obETS.
Definition ob := ob1⁺.
Record consistent := {
internal :> exp_internal cd;
reg_internal' :> reg_internal cd;
translation_internal : trfi ⊆ not_after cd;
external : grel_irreflexive ob;
atomic : (rmw ∩ (fre⨾ coe)) = ∅;
co_contains_TBLI_writes:
∀ weid ∈ mem_writes cd, ∀ teid ∈ TLBI,
(weid, teid) ∈ coherence cd ∨ (teid, weid) ∈ coherence cd
}.
#[export] Instance consistent_dec : Decision consistent := ltac:(decide_record).
Record not_UB := {
initial_reads : IF ⊆ IR;
initial_reads_not_delayed : IF ## grel_rng (coherence cd);
register_write_permitted : Illegal_RW = ∅;
memory_events_permitted : (mem_events cd) ⊆ M ∪ T ∪ IF;
is_nms' : is_nms cd;
no_cacheop : ICDC = ∅;
}.
#[export] Instance not_UB_dec : Decision not_UB := ltac:(decide_record).
Definition consistent_ok := consistent ∧ not_UB.
Instance consistent_ok_dec : Decision consistent_ok := ltac:(unfold_decide).
End VMSAArm.
The VMSA22 Arm axiomatic model
Definition axmodel regs_whitelist : Ax.t Candidate.NMS ∅ :=
λ _ cd, if decide (consistent cd) then
if decide (not_UB regs_whitelist cd) then Ok Ax.Allowed
else Error ""
else Ok Ax.Rejected.
λ _ cd, if decide (consistent cd) then
if decide (not_UB regs_whitelist cd) then Ok Ax.Allowed
else Error ""
else Ok Ax.Rejected.
The VMSA22 Arm architecture model
Definition archmodel regs_whitelist isem : archModel.nc ∅ :=
Ax.to_archModel_nc isem (axmodel regs_whitelist).
Ax.to_archModel_nc isem (axmodel regs_whitelist).