Skip to content

Commit 7880198

Browse files
febyejifebyeji
committed
Clean-up promise-first codes
1 parent 80b7aad commit 7880198

File tree

5 files changed

+18
-155
lines changed

5 files changed

+18
-155
lines changed

‎ArchSem/GenPromising.v‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -380,7 +380,7 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
380380
promise ← mchoosel (enum bool);
381381
if (promise : bool) then cpromise_tid fuel tid else run_tid isem prom tid.
382382

383-
(** Computational evaluate all the possible allowed final states according
383+
(** Computationally evaluate all the possible allowed final states according
384384
to the promising model prom starting from st *)
385385
Fixpoint run (fuel : nat) : Exec.t t string final :=
386386
st ← mGet;
@@ -416,12 +416,13 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
416416

417417
(* Non-deterministically choose the next promise and the tid for pruning *)
418418
let promises_all := List.concat executions.*1 in
419-
if is_emptyb promises_all then
420-
mret (new_finals ++ finals)
421-
else
419+
promise ← mchoosel (enum bool);
420+
if (promise : bool) then
422421
'(next_ev, tid) ← mchoosel promises_all;
423422
mSet (λ st, promise_tid prom st tid next_ev);;
424423
prune_promises_and_states fuel_per_tid fuel (new_finals ++ finals)
424+
else
425+
mret (new_finals ++ finals)
425426
else mret finals.
426427

427428
(** Computational evaluate all the possible allowed final states according
@@ -445,7 +446,7 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
445446
<$> CPState.run isem prom term fuel.
446447

447448
(** Create a computational model from an ISA model and promising model
448-
with promise-free optimization *)
449+
with promise-first optimization *)
449450
Definition Promising_to_Modelc_pf (isem : iMon ()) (prom : BasicExecutablePM)
450451
(fuel : nat) : archModel.c ∅ :=
451452
λ n term (initMs : archState n),

‎ArchSemArm/UMPromising.v‎

Lines changed: 8 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -462,11 +462,11 @@ Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
462462
let msg := Msg.make tid loc data in
463463
let is_release := is_rel_acq macc in
464464
ts ← mGet;
465-
'(time, mem, new_promise) ←
465+
let '(time, mem, new_promise) :=
466466
match Memory.fulfill msg (TState.prom ts) mem with
467-
| Some t => mret (t, mem, false)
468-
| None => mret (Memory.promise msg mem, true)
469-
end;
467+
| Some t => (t, mem, false)
468+
| None => (Memory.promise msg mem, true)
469+
end in
470470
let vbob :=
471471
ts.(TState.vdmbst) ⊔ ts.(TState.vdmb) ⊔ ts.(TState.visb) ⊔ ts.(TState.vacq)
472472
⊔ view_if is_release (ts.(TState.vrd) ⊔ ts.(TState.vwr)) in
@@ -476,7 +476,7 @@ Definition write_mem (tid : nat) (loc : Loc.t) (vdata : view)
476476
mSet $ TState.update_coh loc time;;
477477
mSet $ TState.update TState.vwr time;;
478478
mSet $ TState.update TState.vrel (view_if is_release time);;
479-
mret $ if (new_promise : bool) then (mem, time, Some vpre) else (mem, time, None).
479+
mret (mem, time, (if new_promise then Some vpre else None)).
480480

481481
(** Tries to perform a memory write.
482482
@@ -531,8 +531,7 @@ End IIS.
531531
and computation. This can mutate memory because it will append a write at
532532
the end of memory the corresponding event was not already promised. *)
533533
Section RunOutcome.
534-
Context (tid : nat).
535-
Context (initmem : memoryMap).
534+
Context (tid : nat) (initmem : memoryMap).
536535

537536
Equations run_outcome (out : outcome) :
538537
Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out * option view) :=
@@ -613,6 +612,7 @@ Section RunOutcome.
613612
Definition run_outcome' (out : outcome) :
614613
Exec.t (PPState.t TState.t Msg.t IIS.t) string (eff_ret out) :=
615614
run_outcome out |$> fst.
615+
616616
End RunOutcome.
617617

618618
Module CProm.
@@ -780,19 +780,7 @@ Definition UMPromising_cert' (isem : iMon ()) : PromisingModel :=
780780
Definition UMPromising_cert_nc isem :=
781781
Promising_to_Modelnc isem (UMPromising_cert' isem).
782782

783-
(** Implement the Executable Promising Model *)
784-
785-
Program Definition UMPromising_exe' (isem : iMon ())
786-
: BasicExecutablePM :=
787-
{|pModel := UMPromising_cert' isem;
788-
enumerate_promises_and_terminal_states :=
789-
λ fuel tid term initmem ts mem,
790-
run_to_termination tid initmem term isem fuel ts mem
791-
|}.
792-
Next Obligation. Admitted.
793-
Next Obligation. Admitted.
794-
Next Obligation. Admitted.
795-
Next Obligation. Admitted.
783+
(** Implement the Executable Promising Model (Promise-Free) *)
796784

797785
Program Definition UMPromising_exe_pf' (isem : iMon ())
798786
: BasicExecutablePM :=
@@ -806,8 +794,5 @@ Next Obligation. Admitted.
806794
Next Obligation. Admitted.
807795
Next Obligation. Admitted.
808796

809-
Definition UMPromising_cert_c isem fuel :=
810-
Promising_to_Modelc isem (UMPromising_exe' isem) fuel.
811-
812797
Definition UMPromising_cert_c_pf isem fuel :=
813798
Promising_to_Modelc_pf isem (UMPromising_exe_pf' isem) fuel.

‎ArchSemArm/VMPromising.v‎

Lines changed: 4 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1585,7 +1585,7 @@ Definition write_mem (tid : nat) (loc : Loc.t) (viio : view)
15851585
mset fst $ TState.update_coh loc time;;
15861586
mset fst $ TState.update TState.vwr time;;
15871587
mset fst $ TState.update TState.vrel (view_if is_release time);;
1588-
mret $ if (new_promise : bool) then (time, Some vpre) else (time, None).
1588+
mret (time, if (new_promise : bool) then Some vpre else None).
15891589

15901590
(** Tries to perform a memory write.
15911591
@@ -1828,8 +1828,7 @@ Definition run_take_exception (fault : exn) (vmax_t : view) :
18281828

18291829
(** Runs an outcome. *)
18301830
Section RunOutcome.
1831-
Context (tid : nat).
1832-
Context (initmem : memoryMap).
1831+
Context (tid : nat) (initmem : memoryMap).
18331832

18341833
Equations run_outcome (out : outcome) :
18351834
Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out * option view) :=
@@ -1896,6 +1895,7 @@ Section RunOutcome.
18961895
Definition run_outcome' (out : outcome) :
18971896
Exec.t (PPState.t TState.t Ev.t IIS.t) string (eff_ret out) :=
18981897
run_outcome out |$> fst.
1898+
18991899
End RunOutcome.
19001900

19011901
Module CProm.
@@ -2057,19 +2057,7 @@ Definition VMPromising_cert' (isem : iMon ()) : PromisingModel :=
20572057
λ initmem, Memory.to_memMap (Memory.initial_from_memMap initmem);
20582058
|}.
20592059

2060-
(** Implement the Executable Promising Model *)
2061-
2062-
Program Definition VMPromising_exe' (isem : iMon ())
2063-
: BasicExecutablePM :=
2064-
{|pModel := VMPromising_cert' isem;
2065-
enumerate_promises_and_terminal_states :=
2066-
λ fuel tid term initmem ts mem,
2067-
run_to_termination tid initmem term isem fuel ts mem
2068-
|}.
2069-
Next Obligation. Admitted.
2070-
Next Obligation. Admitted.
2071-
Next Obligation. Admitted.
2072-
Next Obligation. Admitted.
2060+
(** Implement the Executable Promising Model (Promise-Free) *)
20732061

20742062
Program Definition VMPromising_exe_pf' (isem : iMon ())
20752063
: BasicExecutablePM :=
@@ -2083,8 +2071,5 @@ Next Obligation. Admitted.
20832071
Next Obligation. Admitted.
20842072
Next Obligation. Admitted.
20852073

2086-
Definition VMPromising_cert_c isem fuel :=
2087-
Promising_to_Modelc isem (VMPromising_exe' isem) fuel.
2088-
20892074
Definition VMPromising_cert_c_pf isem fuel :=
20902075
Promising_to_Modelc_pf isem (VMPromising_exe_pf' isem) fuel.

‎ArchSemArm/tests/UMPromisingTest.v‎

Lines changed: 0 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -116,14 +116,6 @@ Module EOR.
116116

117117
Definition fuel := 2%nat.
118118

119-
Definition test_results :=
120-
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
121-
122-
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x110%Z].
123-
vm_compute (_ <$> _).
124-
reflexivity.
125-
Qed.
126-
127119
Definition test_results_pf :=
128120
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
129121

@@ -159,14 +151,6 @@ Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
159151

160152
Definition fuel := 2%nat.
161153

162-
Definition test_results :=
163-
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
164-
165-
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x2a%Z].
166-
vm_compute (_ <$> _).
167-
reflexivity.
168-
Qed.
169-
170154
Definition test_results_pf :=
171155
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
172156

@@ -204,14 +188,6 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
204188

205189
Definition fuel := 3%nat.
206190

207-
Definition test_results :=
208-
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
209-
210-
Goal reg_extract R0 0%fin <$> test_results ≡ Listset [Ok 0x2a%Z].
211-
vm_compute (_ <$> _).
212-
set_solver.
213-
Qed.
214-
215191
Definition test_results_pf :=
216192
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
217193

@@ -281,16 +257,6 @@ Module MP.
281257

282258
Definition fuel := 6%nat.
283259

284-
Definition test_results :=
285-
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
286-
287-
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
288-
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
289-
Proof.
290-
vm_compute (elements _).
291-
apply NoDup_Permutation; try solve_NoDup; set_solver.
292-
Qed.
293-
294260
Definition test_results_pf :=
295261
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
296262

@@ -363,16 +329,6 @@ Module MPDMBS.
363329

364330
Definition fuel := 8%nat.
365331

366-
Definition test_results :=
367-
UMPromising_cert_c arm_sem fuel n_threads termCond initState.
368-
369-
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
370-
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
371-
Proof.
372-
vm_compute (elements _).
373-
apply NoDup_Permutation; try solve_NoDup; set_solver.
374-
Qed.
375-
376332
Definition test_results_pf :=
377333
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
378334

‎ArchSemArm/tests/VMPromisingTest.v‎

Lines changed: 0 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -126,14 +126,6 @@ Module EORMMUOFF.
126126

127127
Definition fuel := 2%nat.
128128

129-
Definition test_results :=
130-
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
131-
132-
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x110%Z].
133-
vm_compute (_ <$> _).
134-
reflexivity.
135-
Qed.
136-
137129
Definition test_results_pf :=
138130
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
139131

@@ -200,14 +192,6 @@ Module EOR.
200192

201193
Definition fuel := 2%nat.
202194

203-
Definition test_results :=
204-
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
205-
206-
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x110%Z].
207-
vm_compute (_ <$> _).
208-
reflexivity.
209-
Qed.
210-
211195
Definition test_results_pf :=
212196
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
213197

@@ -261,14 +245,6 @@ Module LDR.
261245

262246
Definition fuel := 2%nat.
263247

264-
Definition test_results :=
265-
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
266-
267-
Goal reg_extract R0 0%fin <$> test_results = Listset [Ok 0x2a%Z].
268-
vm_compute (_ <$> _).
269-
reflexivity.
270-
Qed.
271-
272248
Definition test_results_pf :=
273249
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
274250

@@ -321,14 +297,6 @@ Module STRLDR.
321297

322298
Definition fuel := 4%nat.
323299

324-
Definition test_results :=
325-
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
326-
327-
Goal reg_extract R0 0%fin <$> test_results ≡ Listset [Ok 0x2a%Z].
328-
vm_compute (_ <$> _).
329-
set_solver.
330-
Qed.
331-
332300
Definition test_results_pf :=
333301
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
334302

@@ -398,17 +366,6 @@ Module LDRPT.
398366

399367
Definition fuel := 4%nat.
400368

401-
Definition test_results :=
402-
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
403-
404-
(* R0 should be 0x2a (from old mapping), R4 should be 0x42 (from new mapping) *)
405-
Goal elements (regs_extract [(0%fin, R0); (0%fin, R4)] <$> test_results) ≡ₚ
406-
[Ok [0x2a%Z; 0x2a%Z]; Ok [0x2a%Z; 0x42%Z]].
407-
Proof.
408-
vm_compute (elements _).
409-
apply NoDup_Permutation; try solve_NoDup; set_solver.
410-
Qed.
411-
412369
Definition test_results_pf :=
413370
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
414371

@@ -502,16 +459,6 @@ Module MP.
502459

503460
Definition fuel := 6%nat.
504461

505-
(* Definition test_results :=
506-
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
507-
508-
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
509-
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
510-
Proof.
511-
vm_compute (elements _).
512-
apply NoDup_Permutation; try solve_NoDup; set_solver.
513-
Qed. *)
514-
515462
Definition test_results_pf :=
516463
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
517464

@@ -604,17 +551,6 @@ Module MPDMBS.
604551

605552
Definition fuel := 8%nat.
606553

607-
(* Definition test_results :=
608-
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
609-
610-
(** The test is fenced enough, the 0x1; 0x0 outcome is impossible*)
611-
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
612-
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
613-
Proof.
614-
vm_compute (elements _).
615-
apply NoDup_Permutation; try solve_NoDup; set_solver.
616-
Qed. *)
617-
618554
Definition test_results_pf :=
619555
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
620556

0 commit comments

Comments
 (0)