Skip to content

Commit 6b64446

Browse files
febyejifebyeji
committed
Add mem_strict in computational model in VMPromising to distinguish va-fill and traverse
1 parent 84f4179 commit 6b64446

File tree

2 files changed

+142
-126
lines changed

2 files changed

+142
-126
lines changed

‎ArchSemArm/VMPromising.v‎

Lines changed: 74 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -985,24 +985,27 @@ Module TLB.
985985
(time : nat)
986986
(va : prefix root_lvl)
987987
(ttbr : reg)
988-
(val_ttbrs : list (bv 64)) : result string (VATLB.t * bool) :=
988+
(val_ttbrs : list (bv 64))
989+
(mem_strict : bool) : result string (VATLB.t * bool) :=
989990
is_upper ← othrow "The register is not TTBR" (is_upper_ttbr ttbr);
990991
foldlM (λ '(vatlb, is_changed) val_ttbr,
991992
let entry_addr := next_entry_addr val_ttbr va in
992993
let loc := Loc.from_addr_in entry_addr in
993-
'(memval, _) ← othrow "Memory read failed"
994-
$ Memory.read_at loc init mem time;
995-
if decide (is_table root_lvl memval) then
996-
let asid := bv_extract 48 16 val_ttbr in
997-
let ndctxt := NDCtxt.make is_upper va (Some asid) in
998-
let ctxt := existT root_lvl ndctxt in
999-
let entry : Entry.t (Ctxt.lvl ctxt) :=
1000-
Entry.make _ val_ttbr ([#memval] : vec val (S root_lvl)) in
1001-
(* add the entry to vatlb only when it is not in the original vatlb *)
1002-
if decide (entry ∉ (VATLB.get ctxt vatlb)) then
1003-
Ok (VATLB.insert ctxt entry vatlb, true)
994+
if Memory.read_at loc init mem time is Some (memval, _) then
995+
if decide (is_table root_lvl memval) then
996+
let asid := bv_extract 48 16 val_ttbr in
997+
let ndctxt := NDCtxt.make is_upper va (Some asid) in
998+
let ctxt := existT root_lvl ndctxt in
999+
let entry : Entry.t (Ctxt.lvl ctxt) :=
1000+
Entry.make _ val_ttbr ([#memval] : vec val (S root_lvl)) in
1001+
(* add the entry to vatlb only when it is not in the original vatlb *)
1002+
if decide (entry ∉ (VATLB.get ctxt vatlb)) then
1003+
Ok (VATLB.insert ctxt entry vatlb, true)
1004+
else Ok (vatlb, is_changed)
10041005
else Ok (vatlb, is_changed)
1005-
else Ok (vatlb, is_changed)
1006+
else
1007+
guard_or ("Memory read failed at " ++ (pretty entry_addr))%string (negb mem_strict);;
1008+
Ok (vatlb, is_changed)
10061009
) (vatlb, false) val_ttbrs.
10071010

10081011
(** Extend one level down from a parent table entry [te].
@@ -1017,30 +1020,33 @@ Module TLB.
10171020
(ctxt : Ctxt.t)
10181021
(te : Entry.t (Ctxt.lvl ctxt))
10191022
(index : bv 9)
1020-
(ttbr : reg) : result string (VATLB.t * bool) :=
1023+
(ttbr : reg)
1024+
(mem_strict : bool) : result string (VATLB.t * bool) :=
10211025
let plvl := Ctxt.lvl ctxt in
10221026
if decide (¬is_table plvl (Entry.pte te)) then Ok (vatlb, false)
10231027
else
10241028
let entry_addr := next_entry_addr (Entry.pte te) index in
10251029
let loc := Loc.from_addr_in entry_addr in
1026-
'(next_pte, _) ← othrow "The location of the next level address should be read"
1027-
$ Memory.read_at loc init mem time;
1028-
if decide (is_valid next_pte) then
1029-
match inspect $ child_lvl (Ctxt.lvl ctxt) with
1030-
| Some clvl eq:e =>
1031-
let va := next_va ctxt index (child_lvl_add_one _ _ e) in
1032-
let asid := if bool_decide (is_global clvl next_pte) then None
1033-
else Ctxt.asid ctxt in
1034-
let ndctxt := NDCtxt.make (Ctxt.is_upper ctxt) va asid in
1035-
let ctxt := existT clvl ndctxt in
1036-
let entry := Entry.append te next_pte (child_lvl_add_one _ _ e) in
1037-
(* add the entry to vatlb only when it is not in the original vatlb *)
1038-
if decide (entry ∉ (VATLB.get ctxt vatlb)) then
1039-
Ok (VATLB.insert ctxt entry vatlb, true)
1040-
else Ok (vatlb, false)
1041-
| None eq:_ => mthrow "An intermediate level should have a child level"
1042-
end
1030+
if (Memory.read_at loc init mem time) is Some (next_pte, _) then
1031+
if decide (is_valid next_pte) then
1032+
match inspect $ child_lvl (Ctxt.lvl ctxt) with
1033+
| Some clvl eq:e =>
1034+
let va := next_va ctxt index (child_lvl_add_one _ _ e) in
1035+
let asid := if bool_decide (is_global clvl next_pte) then None
1036+
else Ctxt.asid ctxt in
1037+
let ndctxt := NDCtxt.make (Ctxt.is_upper ctxt) va asid in
1038+
let ctxt := existT clvl ndctxt in
1039+
let entry := Entry.append te next_pte (child_lvl_add_one _ _ e) in
1040+
(* add the entry to vatlb only when it is not in the original vatlb *)
1041+
if decide (entry ∉ (VATLB.get ctxt vatlb)) then
1042+
Ok (VATLB.insert ctxt entry vatlb, true)
1043+
else Ok (vatlb, false)
1044+
| None eq:_ => mthrow "An intermediate level should have a child level"
1045+
end
1046+
else
1047+
Ok (vatlb, false)
10431048
else
1049+
guard_or ("The location of the next level address should be read: " ++ (pretty loc))%string (negb mem_strict);;
10441050
Ok (vatlb, false).
10451051

10461052
(** Make [tlb] containing entries for [va] at [lvl].
@@ -1058,7 +1064,7 @@ Module TLB.
10581064
'(vatlb_new, is_changed) ←
10591065
match parent_lvl lvl with
10601066
| None =>
1061-
va_fill_root tlb.(vatlb) ts init mem time (level_index va root_lvl) ttbr val_ttbrs
1067+
va_fill_root tlb.(vatlb) ts init mem time (level_index va root_lvl) ttbr val_ttbrs true
10621068
| Some plvl =>
10631069
let pva := level_prefix va plvl in
10641070
let index := level_index va lvl in
@@ -1071,7 +1077,7 @@ Module TLB.
10711077
let tes := elements (VATLB.get ctxt tlb.(vatlb)) in
10721078
foldlM (λ '(vatlb_prev, is_changed_prev) te,
10731079
'(vatlb_lvl, is_changed_lvl) ←
1074-
va_fill_lvl vatlb_prev ts init mem time ctxt te index ttbr;
1080+
va_fill_lvl vatlb_prev ts init mem time ctxt te index ttbr true;
10751081
mret (vatlb_lvl, is_changed_lvl || is_changed_prev)
10761082
) prev tes
10771083
) (tlb.(vatlb), false) val_ttbrs
@@ -1101,10 +1107,11 @@ Module TLB.
11011107
(mem : Memory.t)
11021108
(time : nat)
11031109
(ttbr : reg)
1104-
(val_ttbrs : list (bv 64)) : result string (VATLB.t * bool) :=
1110+
(val_ttbrs : list (bv 64))
1111+
(mem_strict : bool) : result string (VATLB.t * bool) :=
11051112
foldlM (λ '(vatlb_prev, is_changed_prev) index,
11061113
'(vatlb_new, is_changed) ←
1107-
va_fill_root vatlb_prev ts init mem time index ttbr val_ttbrs;
1114+
va_fill_root vatlb_prev ts init mem time index ttbr val_ttbrs mem_strict;
11081115
mret (vatlb_new, is_changed || is_changed_prev)
11091116
) (vatlb, false) (enum (bv 9)).
11101117

@@ -1113,10 +1120,11 @@ Module TLB.
11131120
(mem : Memory.t)
11141121
(time : nat)
11151122
(fe : FE.t)
1116-
(ttbr : reg) : result string (VATLB.t * bool) :=
1123+
(ttbr : reg)
1124+
(mem_strict : bool) : result string (VATLB.t * bool) :=
11171125
foldlM (λ '(vatlb_prev, is_changed_prev) index,
11181126
'(vatlb_new, is_changed_new) ←
1119-
va_fill_lvl vatlb_prev ts init mem time (FE.ctxt fe) (projT2 fe) index ttbr;
1127+
va_fill_lvl vatlb_prev ts init mem time (FE.ctxt fe) (projT2 fe) index ttbr mem_strict;
11201128
mret (vatlb_new, is_changed_new || is_changed_prev)
11211129
) (vatlb, false) (enum (bv 9)).
11221130

@@ -1129,11 +1137,12 @@ Module TLB.
11291137
(time : nat)
11301138
(lvl : Level)
11311139
(ttbr : reg)
1132-
(val_ttbrs : list (bv 64)) : result string (t * bool) :=
1140+
(val_ttbrs : list (bv 64))
1141+
(mem_strict : bool) : result string (t * bool) :=
11331142
'(vatlb_new, is_changed) ←
11341143
match parent_lvl lvl with
11351144
| None =>
1136-
traverse_root tlb.(vatlb) ts init mem time ttbr val_ttbrs
1145+
traverse_root tlb.(vatlb) ts init mem time ttbr val_ttbrs mem_strict
11371146
| Some plvl =>
11381147
let fes :=
11391148
omap (λ fe,
@@ -1142,7 +1151,7 @@ Module TLB.
11421151
else None) (elements tlb.(vatlb)) in
11431152
foldlM (λ '(vatlb, is_changed_prev) fe,
11441153
'(vatlb_new, is_changed) ←
1145-
traverse_lvl vatlb ts init mem time fe ttbr;
1154+
traverse_lvl vatlb ts init mem time fe ttbr mem_strict;
11461155
mret (vatlb_new, is_changed || is_changed_prev)
11471156
) (tlb.(vatlb), false) fes
11481157
end;
@@ -1155,12 +1164,14 @@ Module TLB.
11551164
(init : Memory.initial)
11561165
(mem : Memory.t)
11571166
(time : nat)
1158-
(ttbr : reg) : result string (t * bool) :=
1167+
(ttbr : reg)
1168+
(mem_strict : bool) : result string (t * bool) :=
11591169
sregs ← othrow "TTBR should exist in initial state"
11601170
$ TState.read_sreg_at ts ttbr time;
11611171
let val_ttbrs := omap (λ sreg, regval_to_val ttbr sreg.1) sregs in
11621172
foldlM (λ '(tlb_prev, is_changed_prev) lvl,
1163-
'(tlb_new, is_changed) ← traverse tlb_prev ts init mem time lvl ttbr val_ttbrs;
1173+
'(tlb_new, is_changed) ←
1174+
traverse tlb_prev ts init mem time lvl ttbr val_ttbrs mem_strict;
11641175
mret (tlb_new, is_changed || is_changed_prev)
11651176
) (tlb, false) (enum Level).
11661177

@@ -1266,7 +1277,8 @@ Module TLB.
12661277
(tlb_prev : t)
12671278
(time_prev cnt : nat)
12681279
(ttbr : reg)
1269-
(acc : list (t * nat)) :
1280+
(acc : list (t * nat))
1281+
(mem_strict : bool) :
12701282
result string (list (t * nat)) :=
12711283
match cnt with
12721284
| O => mret acc
@@ -1281,14 +1293,14 @@ Module TLB.
12811293
then (tlbi_apply tlbi tlb_prev, true)
12821294
else (tlb_prev, false)
12831295
in
1284-
'(tlb, is_changed) ← update_all tlb_inv ts mem_init mem time_cur ttbr;
1296+
'(tlb, is_changed) ← update_all tlb_inv ts mem_init mem time_cur ttbr mem_strict;
12851297
mret (tlb, is_changed || is_changed_by_tlbi)
12861298
| None => mret (init, false)
12871299
end;
12881300
let acc :=
12891301
if (is_changed : bool) then (tlb, time_cur) :: acc else acc in
12901302
unique_snapshots_between
1291-
ts mem_init mem tlb time_cur ccnt ttbr acc
1303+
ts mem_init mem tlb time_cur ccnt ttbr acc mem_strict
12921304
end.
12931305

12941306
(** Get the TLB states for all possible vas up until the timestamp [time]
@@ -1299,9 +1311,10 @@ Module TLB.
12991311
(mem_init : Memory.initial)
13001312
(mem : Memory.t)
13011313
(time : nat)
1302-
(ttbr : reg) : result string (list (t * nat)) :=
1303-
'(tlb, _) ← update_all init ts mem_init mem 0 ttbr;
1304-
unique_snapshots_between ts mem_init mem tlb 0 time ttbr [(tlb, 0)].
1314+
(ttbr : reg)
1315+
(mem_strict : bool) : result string (list (t * nat)) :=
1316+
'(tlb, _) ← update_all init ts mem_init mem 0 ttbr mem_strict;
1317+
unique_snapshots_between ts mem_init mem tlb 0 time ttbr [(tlb, 0)] mem_strict.
13051318

13061319
Definition is_te_invalidated_by_tlbi
13071320
(tlbi : TLBI.t)
@@ -1688,8 +1701,8 @@ Section BBM.
16881701
) (elements (tes × tes))
16891702
) ctxts.
16901703

1691-
Definition check_bbm_violation (ts : TState.t) (mem : Memory.t) :
1692-
result string bool :=
1704+
Definition check_bbm_violation (ts : TState.t)
1705+
(mem : Memory.t) (mem_strict : bool) : result string bool :=
16931706
mmu_enabled ← is_mmu_enabled ts;
16941707
if (mmu_enabled : bool) then
16951708
let initmem := Memory.initial_from_memMap initmem in
@@ -1701,7 +1714,7 @@ Section BBM.
17011714
foldlM (λ violated ttbr,
17021715
if (violated : bool) then mret true (* early return *)
17031716
else
1704-
snapshots ← TLB.unique_snapshots_until ts initmem mem max_t ttbr;
1717+
snapshots ← TLB.unique_snapshots_until ts initmem mem max_t ttbr mem_strict;
17051718
mret $
17061719
existsb (λ '(tlb, time),
17071720
if decide (time ∉ ts_to_check) then false
@@ -2313,9 +2326,11 @@ Section ComputeProm.
23132326
(ts : TState.t)
23142327
(mem : Memory.t)
23152328
(debug : bool)
2329+
(mem_strict : bool)
23162330
: result string (list Ev.t * list TState.t) :=
23172331
let base := List.length mem in
2318-
let exec := run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
2332+
let exec := run_to_termination_promise
2333+
isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
23192334
let errs := Exec.errors exec in
23202335
guard_or (String.concat ", " errs.*2) (negb debug || is_emptyb errs);;
23212336
let res_proms := Exec.results $ exec in
@@ -2324,7 +2339,7 @@ Section ComputeProm.
23242339

23252340
bbm_res ←
23262341
for st in res_proms.*1.*2 do
2327-
check_bbm_violation initmem (PPState.state st) (PPState.mem st)
2342+
check_bbm_violation initmem (PPState.state st) (PPState.mem st) mem_strict
23282343
end;
23292344
guard_or ("BBM check fails")%string (forallb (λ r, negb r) bbm_res);;
23302345

@@ -2401,20 +2416,20 @@ Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
24012416

24022417
(** Implement the Executable Promising Model *)
24032418

2404-
Program Definition VMPromising_exe' (isem : iMon ())
2419+
Program Definition VMPromising_exe' (isem : iMon ()) (debug : bool) (mem_strict : bool)
24052420
: BasicExecutablePM :=
24062421
{|pModel := VMPromising_cert' isem;
24072422
enumerate_promises_and_terminal_states :=
24082423
λ fuel tid term initmem ts mem,
2409-
run_to_termination tid initmem term isem fuel ts mem true
2424+
run_to_termination tid initmem term isem fuel ts mem debug mem_strict
24102425
|}.
24112426
Next Obligation. Admitted.
24122427
Next Obligation. Admitted.
24132428
Next Obligation. Admitted.
24142429
Next Obligation. Admitted.
24152430

2416-
Definition VMPromising_cert_c isem fuel :=
2417-
Promising_to_Modelc isem (VMPromising_exe' isem) fuel.
2431+
Definition VMPromising_cert_c isem fuel debug mem_strict :=
2432+
Promising_to_Modelc isem (VMPromising_exe' isem debug mem_strict) fuel.
24182433

2419-
Definition VMPromising_cert_c_pf isem fuel :=
2420-
Promising_to_Modelc_pf isem (VMPromising_exe' isem) fuel.
2434+
Definition VMPromising_cert_c_pf isem fuel debug mem_strict :=
2435+
Promising_to_Modelc_pf isem (VMPromising_exe' isem debug mem_strict) fuel.

0 commit comments

Comments
 (0)