Skip to content

Commit 533182a

Browse files
febyejifebyeji
committed
Apply code reviews
1 parent 7880198 commit 533182a

File tree

5 files changed

+74
-116
lines changed

5 files changed

+74
-116
lines changed

‎ArchSem/GenPromising.v‎

Lines changed: 22 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -391,46 +391,41 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
391391
run fuel
392392
else mthrow "Could not finish running within the size of the fuel".
393393

394-
(** Explore all possible promise-based executions across all threads. *)
395-
Fixpoint prune_promises_and_states (fuel_per_tid fuel : nat)
396-
(finals : list final) : Exec.t t string (list final) :=
394+
(** Computationally evaluate all the possible allowed final states according
395+
to the promising model prom starting from st with promise-first optimization.
396+
The size of fuel should be at least (# of promises) + max(# of instructions) + 1 *)
397+
Fixpoint run_promise_first (fuel : nat) : Exec.t t string final :=
397398
if fuel is S fuel then
398399
st ← mGet;
399400
(* Find out next possible promises or terminating states at the current thread *)
400401
executions ←
401402
vmapM (λ '(tid, ts),
402403
'(promises_per_tid, tstates_per_tid) ←
403404
mlift $ prom.(enumerate_promises_and_terminal_states)
404-
fuel_per_tid (fin_to_nat tid) (term tid) (initmem st) ts (events st);
405+
fuel (fin_to_nat tid) (term tid) (initmem st) ts (events st);
405406
mret (map (.,tid) promises_per_tid, tstates_per_tid)
406407
) (venumerate (tstates st));
407-
(* Compute cartesian products of the possible thread states *)
408-
let tstates_all := cprodn (vmap snd executions) in
409-
let new_finals :=
410-
omap (λ tstates,
411-
let st := Make tstates st.(PState.initmem) st.(PState.events) in
412-
if decide $ terminated prom term st is left pt
413-
then Some (make_final st pt)
414-
else None
415-
) tstates_all in
416-
417-
(* Non-deterministically choose the next promise and the tid for pruning *)
418-
let promises_all := List.concat executions.*1 in
408+
419409
promise ← mchoosel (enum bool);
420410
if (promise : bool) then
411+
(* Non-deterministically choose the next promise and the tid for pruning *)
412+
let promises_all := List.concat (vmap fst executions) in
421413
'(next_ev, tid) ← mchoosel promises_all;
422414
mSet (λ st, promise_tid prom st tid next_ev);;
423-
prune_promises_and_states fuel_per_tid fuel (new_finals ++ finals)
415+
run_promise_first fuel
424416
else
425-
mret (new_finals ++ finals)
426-
else mret finals.
427-
428-
(** Computational evaluate all the possible allowed final states according
429-
to the promising model prom starting from st
430-
with promise-first optimization *)
431-
Definition run_promise_first (fuel : nat) : Exec.t t string final :=
432-
finals ← prune_promises_and_states fuel fuel [];
433-
mchoosel finals.
417+
(* Compute cartesian products of the possible thread states *)
418+
let tstates_all := cprodn (vmap snd executions) in
419+
let new_finals :=
420+
omap (λ tstates,
421+
let st := Make tstates st.(PState.initmem) st.(PState.events) in
422+
if decide $ terminated prom term st is left pt
423+
then Some (make_final st pt)
424+
else None
425+
) tstates_all in
426+
mchoosel new_finals
427+
else
428+
mthrow "Could not finish running within the size of the fuel".
434429

435430
End CPS.
436431
Arguments to_final_archState {_ _ _}.
@@ -439,27 +434,14 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
439434
(** Create a computational model from an ISA model and promising model *)
440435
Definition Promising_to_Modelc (isem : iMon ()) (prom : BasicExecutablePM)
441436
(fuel : nat) : archModel.c ∅ :=
442-
λ n term (initMs : archState n),
443-
PState.from_archState prom initMs |>
444-
archModel.Res.from_exec
445-
$ CPState.to_final_archState
446-
<$> CPState.run isem prom term fuel.
447-
448-
(** Create a computational model from an ISA model and promising model
449-
with promise-first optimization *)
450-
Definition Promising_to_Modelc_pf (isem : iMon ()) (prom : BasicExecutablePM)
451-
(fuel : nat) : archModel.c ∅ :=
452437
λ n term (initMs : archState n),
453438
PState.from_archState prom initMs |>
454439
archModel.Res.from_exec
455440
$ CPState.to_final_archState
456441
<$> CPState.run_promise_first prom term fuel.
457442

458-
(* TODO state some soundness lemma between Promising_to_Modelnc and
459-
Promising_Modelc *)
460-
461443
End GenPromising.
462444

463445
Module Type GenPromisingT (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
464446
Include GenPromising IWA TM.
465-
End GenPromisingT.
447+
End GenPromisingT.

‎ArchSemArm/UMPromising.v‎

Lines changed: 6 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -659,7 +659,7 @@ Section ComputeProm.
659659
else
660660
mret res.
661661

662-
(* Run the thread state until termination, collecting certifiable promises.
662+
(* Run the thread state until termination, collecting certified promises.
663663
Returns true if termination occurs within the given fuel,
664664
false otherwise. *)
665665
Fixpoint run_to_termination_promise
@@ -681,19 +681,7 @@ Section ComputeProm.
681681
run_to_termination_promise isem fuel base
682682
end.
683683

684-
Definition run_to_termination (isem : iMon ())
685-
(fuel : nat)
686-
(ts : TState.t)
687-
(mem : Memory.t) :
688-
result string (list Msg.t * list TState.t) :=
689-
let base := List.length mem in
690-
let res := Exec.results $
691-
run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
692-
guard_or ("Could not finish promises within the size of the fuel")%string
693-
(∀ r ∈ res, r.2 = true);;
694-
mret $ (CProm.proms (union_list res.*1.*1), []).
695-
696-
Definition run_to_termination_pf (isem : iMon ())
684+
Definition run_to_termination (isem : iMon ())
697685
(fuel : nat)
698686
(ts : TState.t)
699687
(mem : Memory.t)
@@ -782,17 +770,17 @@ Definition UMPromising_cert_nc isem :=
782770

783771
(** Implement the Executable Promising Model (Promise-Free) *)
784772

785-
Program Definition UMPromising_exe_pf' (isem : iMon ())
773+
Program Definition UMPromising_exe' (isem : iMon ())
786774
: BasicExecutablePM :=
787775
{|pModel := UMPromising_cert' isem;
788776
enumerate_promises_and_terminal_states :=
789777
λ fuel tid term initmem ts mem,
790-
run_to_termination_pf tid initmem term isem fuel ts mem
778+
run_to_termination tid initmem term isem fuel ts mem
791779
|}.
792780
Next Obligation. Admitted.
793781
Next Obligation. Admitted.
794782
Next Obligation. Admitted.
795783
Next Obligation. Admitted.
796784

797-
Definition UMPromising_cert_c_pf isem fuel :=
798-
Promising_to_Modelc_pf isem (UMPromising_exe_pf' isem) fuel.
785+
Definition UMPromising_cert_c isem fuel :=
786+
Promising_to_Modelc isem (UMPromising_exe' isem) fuel.

‎ArchSemArm/VMPromising.v‎

Lines changed: 6 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1942,7 +1942,7 @@ Section ComputeProm.
19421942
else
19431943
mret res.
19441944

1945-
(* Run the thread state until termination, collecting certifiable promises.
1945+
(* Run the thread state until termination, collecting certified promises.
19461946
Returns true if termination occurs within the given fuel,
19471947
false otherwise. *)
19481948
Fixpoint run_to_termination_promise
@@ -1964,19 +1964,7 @@ Section ComputeProm.
19641964
run_to_termination_promise isem fuel base
19651965
end.
19661966

1967-
Definition run_to_termination (isem : iMon ())
1968-
(fuel : nat)
1969-
(ts : TState.t)
1970-
(mem : Memory.t) :
1971-
result string (list Ev.t * list TState.t) :=
1972-
let base := List.length mem in
1973-
let res := Exec.results $
1974-
run_to_termination_promise isem fuel base (CProm.init, PPState.Make ts mem IIS.init) in
1975-
guard_or ("Could not finish promises within the size of the fuel")%string
1976-
(∀ r ∈ res, r.2 = true);;
1977-
mret $ (CProm.proms (union_list res.*1.*1), []).
1978-
1979-
Definition run_to_termination_pf (isem : iMon ())
1967+
Definition run_to_termination (isem : iMon ())
19801968
(fuel : nat)
19811969
(ts : TState.t)
19821970
(mem : Memory.t)
@@ -2059,17 +2047,17 @@ Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
20592047

20602048
(** Implement the Executable Promising Model (Promise-Free) *)
20612049

2062-
Program Definition VMPromising_exe_pf' (isem : iMon ())
2050+
Program Definition VMPromising_exe' (isem : iMon ())
20632051
: BasicExecutablePM :=
20642052
{|pModel := VMPromising_cert' isem;
20652053
enumerate_promises_and_terminal_states :=
20662054
λ fuel tid term initmem ts mem,
2067-
run_to_termination_pf tid initmem term isem fuel ts mem
2055+
run_to_termination tid initmem term isem fuel ts mem
20682056
|}.
20692057
Next Obligation. Admitted.
20702058
Next Obligation. Admitted.
20712059
Next Obligation. Admitted.
20722060
Next Obligation. Admitted.
20732061

2074-
Definition VMPromising_cert_c_pf isem fuel :=
2075-
Promising_to_Modelc_pf isem (VMPromising_exe_pf' isem) fuel.
2062+
Definition VMPromising_cert_c isem fuel :=
2063+
Promising_to_Modelc isem (VMPromising_exe' isem) fuel.

‎ArchSemArm/tests/UMPromisingTest.v‎

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -116,10 +116,10 @@ Module EOR.
116116

117117
Definition fuel := 2%nat.
118118

119-
Definition test_results_pf :=
120-
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
119+
Definition test_results :=
120+
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
121121

122-
Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
122+
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x110%Z].
123123
vm_compute (_ <$> _).
124124
reflexivity.
125125
Qed.
@@ -151,10 +151,10 @@ Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
151151

152152
Definition fuel := 2%nat.
153153

154-
Definition test_results_pf :=
155-
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
154+
Definition test_results :=
155+
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
156156

157-
Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x2a%Z].
157+
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x2a%Z].
158158
vm_compute (_ <$> _).
159159
reflexivity.
160160
Qed.
@@ -186,12 +186,12 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
186186
archState.regs := [# init_reg];
187187
archState.address_space := PAS_NonSecure |}.
188188

189-
Definition fuel := 3%nat.
189+
Definition fuel := 4%nat.
190190

191-
Definition test_results_pf :=
192-
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
191+
Definition test_results :=
192+
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
193193

194-
Goal reg_extract R0 0%fin <$> test_results_pf ≡ Listset [Ok 0x2a%Z].
194+
Goal reg_extract R0 0%fin <$> test_results ≡ Listset [Ok 0x2a%Z].
195195
vm_compute (_ <$> _).
196196
set_solver.
197197
Qed.
@@ -257,10 +257,10 @@ Module MP.
257257

258258
Definition fuel := 6%nat.
259259

260-
Definition test_results_pf :=
261-
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
260+
Definition test_results :=
261+
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
262262

263-
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
263+
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
264264
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
265265
Proof.
266266
vm_compute (elements _).
@@ -327,12 +327,12 @@ Module MPDMBS.
327327
archState.regs := [# init_reg_t1; init_reg_t2];
328328
archState.address_space := PAS_NonSecure |}.
329329

330-
Definition fuel := 8%nat.
330+
Definition fuel := 9%nat.
331331

332-
Definition test_results_pf :=
333-
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
332+
Definition test_results :=
333+
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
334334

335-
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
335+
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
336336
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
337337
Proof.
338338
vm_compute (elements _).

‎ArchSemArm/tests/VMPromisingTest.v‎

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -126,10 +126,10 @@ Module EORMMUOFF.
126126

127127
Definition fuel := 2%nat.
128128

129-
Definition test_results_pf :=
130-
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
129+
Definition test_results :=
130+
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
131131

132-
Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
132+
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x110%Z].
133133
vm_compute (_ <$> _).
134134
reflexivity.
135135
Qed.
@@ -192,10 +192,10 @@ Module EOR.
192192

193193
Definition fuel := 2%nat.
194194

195-
Definition test_results_pf :=
196-
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
195+
Definition test_results :=
196+
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
197197

198-
Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x110%Z].
198+
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x110%Z].
199199
vm_compute (_ <$> _).
200200
reflexivity.
201201
Qed.
@@ -245,10 +245,10 @@ Module LDR.
245245

246246
Definition fuel := 2%nat.
247247

248-
Definition test_results_pf :=
249-
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
248+
Definition test_results :=
249+
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
250250

251-
Goal reg_extract R0 0%fin <$> test_results_pf = Listset [Ok 0x2a%Z].
251+
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x2a%Z].
252252
vm_compute (_ <$> _).
253253
reflexivity.
254254
Qed.
@@ -297,10 +297,10 @@ Module STRLDR.
297297

298298
Definition fuel := 4%nat.
299299

300-
Definition test_results_pf :=
301-
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
300+
Definition test_results :=
301+
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
302302

303-
Goal reg_extract R0 0%fin <$> test_results_pf ≡ Listset [Ok 0x2a%Z].
303+
Goal reg_extract R0 0%fin <$> test_results ≡ Listset [Ok 0x2a%Z].
304304
vm_compute (_ <$> _).
305305
set_solver.
306306
Qed.
@@ -364,13 +364,13 @@ Module LDRPT.
364364
archState.regs := [# init_reg];
365365
archState.address_space := PAS_NonSecure |}.
366366

367-
Definition fuel := 4%nat.
367+
Definition fuel := 5%nat.
368368

369-
Definition test_results_pf :=
370-
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
369+
Definition test_results :=
370+
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
371371

372372
(* R0 should be 0x2a (from old mapping), R4 should be 0x42 (from new mapping) *)
373-
Goal elements (regs_extract [(0%fin, R0); (0%fin, R4)] <$> test_results_pf) ≡ₚ
373+
Goal elements (regs_extract [(0%fin, R0); (0%fin, R4)] <$> test_results) ≡ₚ
374374
[Ok [0x2a%Z; 0x2a%Z]; Ok [0x2a%Z; 0x42%Z]].
375375
Proof.
376376
vm_compute (elements _).
@@ -457,12 +457,12 @@ Module MP.
457457
archState.regs := [# init_reg_t1; init_reg_t2];
458458
archState.address_space := PAS_NonSecure |}.
459459

460-
Definition fuel := 6%nat.
460+
Definition fuel := 8%nat.
461461

462-
Definition test_results_pf :=
463-
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
462+
Definition test_results :=
463+
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
464464

465-
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
465+
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
466466
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
467467
Proof.
468468
vm_compute (elements _).
@@ -551,11 +551,11 @@ Module MPDMBS.
551551

552552
Definition fuel := 8%nat.
553553

554-
Definition test_results_pf :=
555-
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
554+
Definition test_results :=
555+
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
556556

557557
(** The test is fenced enough, the 0x1; 0x0 outcome is impossible*)
558-
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
558+
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
559559
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
560560
Proof.
561561
vm_compute (elements _).

0 commit comments

Comments
 (0)