Skip to content

Commit 67dd3e1

Browse files
febyejifebyeji
committed
TLB invalidation from all the active ASIDs and small optimizations
1 parent 8341625 commit 67dd3e1

File tree

1 file changed

+69
-56
lines changed

1 file changed

+69
-56
lines changed

‎ArchSemArm/VMPromising.v‎

Lines changed: 69 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -830,6 +830,9 @@ Module TLB.
830830
Definition singleton (ctxt : Ctxt.t) (entry : Entry.t (Ctxt.lvl ctxt)) : t :=
831831
hset (Ctxt.lvl ctxt) {[(Ctxt.nd ctxt) := {[ entry ]}]} init.
832832

833+
Definition setFEs (ctxt : Ctxt.t) (entries : gset (Entry.t (Ctxt.lvl ctxt))) (vatlb : t) : t :=
834+
hset (Ctxt.lvl ctxt) {[(Ctxt.nd ctxt) := entries]} vatlb.
835+
833836
#[global] Instance empty : Empty t := VATLB.init.
834837
#[global] Instance union : Union t := fun x y => hmap2 (fun _ => (∪ₘ)) x y.
835838
End VATLB.
@@ -993,23 +996,6 @@ Module TLB.
993996

994997
(** ** TLB invalidation *)
995998

996-
Definition affects_va (asid : bv 16) (va : bv 36) (last : bool)
997-
(ctxt : Ctxt.t)
998-
(te : Entry.t (Ctxt.lvl ctxt)) : Prop :=
999-
let '(te_lvl, te_va, te_asid, te_val) :=
1000-
(Ctxt.lvl ctxt, Ctxt.va ctxt, Ctxt.asid ctxt, Entry.pte te) in
1001-
(match_prefix_at te_lvl te_va va)
1002-
∧ (match te_asid with
1003-
| Some te_asid => asid = te_asid
1004-
| None => True
1005-
end)
1006-
∧ (if last then is_final te_lvl te_val else True).
1007-
Instance Decision_affects_va (asid : bv 16) (va : bv 36) (last : bool)
1008-
(ctxt : Ctxt.t)
1009-
(te : Entry.t (Ctxt.lvl ctxt)) :
1010-
Decision (affects_va asid va last ctxt te).
1011-
Proof. unfold_decide. Defined.
1012-
1013999
Definition affects_asid (asid : bv 16)
10141000
(ctxt : Ctxt.t)
10151001
(te : Entry.t (Ctxt.lvl ctxt)) : Prop :=
@@ -1040,7 +1026,8 @@ Module TLB.
10401026
(te : Entry.t (Ctxt.lvl ctxt)) : Prop :=
10411027
match tlbi with
10421028
| TLBI.All tid => True
1043-
| TLBI.Va tid asid va last => affects_va asid va last ctxt te
1029+
| TLBI.Va tid asid va last =>
1030+
affects_asid asid ctxt te ∧ affects_vaa va last ctxt te
10441031
| TLBI.Asid tid asid => affects_asid asid ctxt te
10451032
| TLBI.Vaa tid va last => affects_vaa va last ctxt te
10461033
end.
@@ -1055,52 +1042,76 @@ Module TLB.
10551042
(tlbi : TLBI.t)
10561043
(lvl : Level)
10571044
(va : bv 64)
1058-
(asid : option (bv 16)) : t :=
1059-
let ndctxt := NDCtxt.make (level_prefix va lvl) asid in
1060-
let ctxt := existT lvl ndctxt in
1061-
VATLB.get ctxt tlb.(vatlb)
1062-
|> filter (λ te, ¬(affects tlbi ctxt te))
1063-
|> λ tes,
1064-
TLB.make $ hset (Ctxt.lvl ctxt) {[(Ctxt.nd ctxt) := tes]} tlb.(vatlb).
1045+
(ttbr : reg) : result string t :=
1046+
sregs ← othrow "TTBR should exist in initial state"
1047+
$ TState.read_sreg_at ts ttbr time;
1048+
active_vatlbs ←
1049+
for sreg in sregs do
1050+
val_ttbr ← othrow "TTBR should be a 64 bit value"
1051+
$ regval_to_val ttbr sreg.1;
1052+
let asid := bv_extract 48 16 val_ttbr in
1053+
let ndctxt_asid := NDCtxt.make (level_prefix va lvl) (Some asid) in
1054+
let ndctxt_global := NDCtxt.make (level_prefix va lvl) None in
1055+
vatlbs ←
1056+
for ndctxt in [ndctxt_asid; ndctxt_global] do
1057+
let ctxt := existT lvl ndctxt in
1058+
let tes := VATLB.get ctxt tlb.(vatlb)
1059+
|> filter (λ te, ¬(affects tlbi ctxt te)) in
1060+
Ok $ VATLB.setFEs ctxt tes tlb.(vatlb)
1061+
end;
1062+
Ok $ (union_list vatlbs)
1063+
end;
1064+
Ok $ TLB.make (union_list active_vatlbs).
10651065

10661066
Definition tlbi_apply (tlb : t) (ts : TState.t)
10671067
(init : Memory.initial) (mem : Memory.t)
10681068
(time : nat)
10691069
(tlbi : TLBI.t)
10701070
(va : bv 64)
1071-
(asid : option (bv 16)) : t :=
1072-
let tlb0 := tlbi_apply_lvl tlb ts init mem time tlbi root_lvl va asid in
1073-
let tlb1 := tlbi_apply_lvl tlb0 ts init mem time tlbi 1%fin va asid in
1074-
let tlb2 := tlbi_apply_lvl tlb1 ts init mem time tlbi 2%fin va asid in
1075-
tlbi_apply_lvl tlb2 ts init mem time tlbi 3%fin va asid.
1076-
1077-
(** Get the TLB state at a certain timestamp *)
1078-
Fixpoint at_timestamp (ts : TState.t) (mem_init : Memory.initial) (mem : Memory.t)
1079-
(time : nat)
1071+
(ttbr : reg) : result string t :=
1072+
tlb0 ← tlbi_apply_lvl tlb ts init mem time tlbi root_lvl va ttbr;
1073+
tlb1 ← tlbi_apply_lvl tlb0 ts init mem time tlbi 1%fin va ttbr;
1074+
tlb2 ← tlbi_apply_lvl tlb1 ts init mem time tlbi 2%fin va ttbr;
1075+
tlbi_apply_lvl tlb2 ts init mem time tlbi 3%fin va ttbr.
1076+
1077+
(** Get the TLB state at a timestamp (time_prev + cnt) *)
1078+
Fixpoint at_timestamp_from (ts : TState.t) (mem_init : Memory.initial) (mem : Memory.t)
1079+
(tlb_prev : t)
1080+
(time_prev cnt : nat)
10801081
(va : bv 64)
1081-
(asid : option (bv 16))
10821082
(ttbr : reg)
1083-
{struct time} : result string t :=
1084-
match time with
1085-
| O => update init ts mem_init mem 0 va ttbr
1086-
| S ptime =>
1087-
tlb ← at_timestamp ts mem_init mem ptime va asid ttbr;
1088-
match mem !! time with
1089-
| Some ev =>
1090-
match Ev.get_tlbi ev with
1091-
| Some tlbi => mret $ tlbi_apply tlb ts mem_init mem time tlbi va asid
1092-
| None => update tlb ts mem_init mem time va ttbr
1093-
end
1094-
| None => mret init
1095-
end
1083+
{struct cnt} : result string t :=
1084+
match cnt with
1085+
| O => mret tlb_prev
1086+
| S ccnt =>
1087+
let time_cur := time_prev + 1 in
1088+
tlb ←
1089+
match mem !! time_cur with
1090+
| Some ev =>
1091+
match Ev.get_tlbi ev with
1092+
| Some tlbi => tlbi_apply tlb_prev ts mem_init mem time_cur tlbi va ttbr
1093+
| None => update tlb_prev ts mem_init mem time_cur va ttbr
1094+
end
1095+
| None => mret init
1096+
end;
1097+
at_timestamp_from ts mem_init mem tlb time_cur ccnt va ttbr
10961098
end.
10971099

1100+
1101+
(** Get the TLB state at a timestamp `time` *)
1102+
Definition at_timestamp (ts : TState.t) (mem_init : Memory.initial) (mem : Memory.t)
1103+
(time : nat)
1104+
(va : bv 64)
1105+
(ttbr : reg) : result string t :=
1106+
tlb ← update init ts mem_init mem 0 va ttbr;
1107+
at_timestamp_from ts mem_init mem tlb 0 time va ttbr.
1108+
10981109
Definition is_te_invalidated_by_tlbi (tlb : t)
10991110
(tlbi : TLBI.t)
11001111
(tid : nat)
11011112
(ctxt : Ctxt.t)
11021113
(te : Entry.t (Ctxt.lvl ctxt)) : Prop :=
1103-
TLBI.tid tlbi <> tid ∧ te ∉ VATLB.get ctxt tlb.(vatlb).
1114+
TLBI.tid tlbi <> tid ∧ (affects tlbi ctxt te).
11041115
Instance Decision_is_te_invalidated_by_tlbi (tlb : t) (tlbi : TLBI.t) (tid : nat)
11051116
(ctxt : Ctxt.t) (te : Entry.t (Ctxt.lvl ctxt)) :
11061117
Decision (is_te_invalidated_by_tlbi tlb tlbi tid ctxt te).
@@ -1112,32 +1123,34 @@ Module TLB.
11121123
(ctxt : Ctxt.t)
11131124
(te : Entry.t (Ctxt.lvl ctxt))
11141125
(ttbr : reg)
1115-
(evs : list (Ev.t * nat)) : result string nat :=
1126+
(evs : list (Ev.t * nat))
1127+
(tlb_base : t) (time_base : nat) : result string nat :=
11161128
match evs with
11171129
| nil => mret 0
11181130
| (ev, t) :: tl =>
11191131
match ev with
11201132
| Ev.Tlbi tlbi =>
11211133
let va := Ctxt.va ctxt in
11221134
let asid := Ctxt.asid ctxt in
1123-
tlb ← at_timestamp ts init mem t (prefix_to_va va) asid ttbr;
1135+
tlb ← at_timestamp_from ts init mem tlb_base time_base (t - time_base) (prefix_to_va va) ttbr;
11241136
if decide (is_te_invalidated_by_tlbi tlb tlbi tid ctxt te) then
11251137
mret t
11261138
else
1127-
invalidation_time_from_evs ts init mem tid ctxt te ttbr tl
1128-
| _ => invalidation_time_from_evs ts init mem tid ctxt te ttbr tl
1139+
invalidation_time_from_evs ts init mem tid ctxt te ttbr tl tlb_base time_base
1140+
| _ => invalidation_time_from_evs ts init mem tid ctxt te ttbr tl tlb_base time_base
11291141
end
11301142
end.
11311143

11321144
(** Calculate the earliest future time at which a translation entry is effectively invalidated
11331145
in the TLB due to an TLBI event *)
11341146
Definition invalidation_time (ts : TState.t) (init : Memory.initial) (mem : Memory.t)
1135-
(tid : nat) (time : nat)
1147+
(tid : nat)
1148+
(tlb_base : t) (time_base : nat)
11361149
(ctxt : Ctxt.t)
11371150
(te : Entry.t (Ctxt.lvl ctxt))
11381151
(ttbr : reg) : result string nat :=
1139-
let evs := PromMemory.cut_after_with_timestamps time mem in
1140-
invalidation_time_from_evs ts init mem tid ctxt te ttbr evs.
1152+
let evs := PromMemory.cut_after_with_timestamps time_base mem in
1153+
invalidation_time_from_evs ts init mem tid ctxt te ttbr evs tlb_base time_base.
11411154
End TLB.
11421155

11431156
Module VATLB := TLB.VATLB.

0 commit comments

Comments
 (0)