Skip to content

Commit 7f3f7f9

Browse files
febyejifebyeji
committed
Pass MP, MPDMBS tests with address translation
1 parent 6137d35 commit 7f3f7f9

File tree

3 files changed

+127
-26
lines changed

3 files changed

+127
-26
lines changed

‎ArchSemArm/VMPromising.v‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2102,8 +2102,20 @@ Next Obligation. Admitted.
21022102
Next Obligation. Admitted.
21032103
Next Obligation. Admitted.
21042104

2105+
Program Definition VMPromising_exe_pf' (isem : iMon ())
2106+
: BasicExecutablePM :=
2107+
{|pModel := VMPromising_cert' isem;
2108+
enumerate_promises_and_terminal_states :=
2109+
λ fuel tid term initmem ts mem,
2110+
run_to_termination_pf tid initmem term isem fuel ts mem
2111+
|}.
2112+
Next Obligation. Admitted.
2113+
Next Obligation. Admitted.
2114+
Next Obligation. Admitted.
2115+
Next Obligation. Admitted.
2116+
21052117
Definition VMPromising_cert_c isem fuel :=
21062118
Promising_to_Modelc isem (VMPromising_exe' isem) fuel.
21072119

21082120
Definition VMPromising_cert_c_pf isem fuel :=
2109-
Promising_to_Modelc_pf isem (VMPromising_exe' isem) fuel.
2121+
Promising_to_Modelc_pf isem (VMPromising_exe_pf' isem) fuel.

‎ArchSemArm/tests/UMPromisingTest.v‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -301,3 +301,85 @@ Module MP.
301301
apply NoDup_Permutation; try solve_NoDup; set_solver.
302302
Qed.
303303
End MP.
304+
305+
Module MPDMBS.
306+
(* A classic MP litmus test
307+
Thread 1: STR X2, [X1, X0]; DMB SY; STR X5, [X4, X3]
308+
Thread 2: LDR X5, [X4, X3]; DMB SY; LDR X2, [X1, X0]
309+
Expected outcome of (R5, R2) at Thread 2:
310+
(0x1, 0x2a), (0x0, 0x2a), (0x0, 0x0)
311+
*)
312+
313+
Definition init_reg_t1 : registerMap :=
314+
∅
315+
|> reg_insert _PC 0x500
316+
|> reg_insert R0 0x1000
317+
|> reg_insert R1 0x100
318+
|> reg_insert R3 0x1000
319+
|> reg_insert R4 0x200
320+
|> reg_insert R2 0x2a
321+
|> reg_insert R5 0x1
322+
|> reg_insert SCTLR_EL1 0x0
323+
|> reg_insert PSTATE (init_pstate 0%bv 0%bv).
324+
325+
Definition init_reg_t2 : registerMap :=
326+
∅
327+
|> reg_insert _PC 0x600
328+
|> reg_insert R0 0x1000
329+
|> reg_insert R1 0x100
330+
|> reg_insert R3 0x1000
331+
|> reg_insert R4 0x200
332+
|> reg_insert R2 0x0
333+
|> reg_insert R5 0x0
334+
|> reg_insert SCTLR_EL1 0x0
335+
|> reg_insert PSTATE (init_pstate 0%bv 0%bv).
336+
337+
Definition init_mem : memoryMap :=
338+
∅
339+
(* Thread 1 @ 0x500 *)
340+
|> mem_insert 0x500 4 0xf8206822 (* STR X2, [X1, X0] *)
341+
|> mem_insert 0x504 4 0xd5033fbf (* DMB SY *)
342+
|> mem_insert 0x508 4 0xf8236885 (* STR X5, [X4, X3] *)
343+
(* Thread 2 @ 0x600 *)
344+
|> mem_insert 0x600 4 0xf8636885 (* LDR X5, [X4, X3] *)
345+
|> mem_insert 0x604 4 0xd5033fbf (* DMB SY *)
346+
|> mem_insert 0x608 4 0xf8606822 (* LDR X2, [X1, X0] *)
347+
(* Backing memory so the addresses exist *)
348+
|> mem_insert 0x1100 8 0x0
349+
|> mem_insert 0x1200 8 0x0.
350+
351+
Definition n_threads := 2%nat.
352+
353+
Definition terminate_at := [# Some (0x50c : bv 64); Some (0x60c : bv 64)].
354+
355+
(* Each thread’s PC must reach the end of its three instructions *)
356+
Definition termCond : terminationCondition n_threads :=
357+
(λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).
358+
359+
Definition initState :=
360+
{|archState.memory := init_mem;
361+
archState.regs := [# init_reg_t1; init_reg_t2];
362+
archState.address_space := PAS_NonSecure |}.
363+
364+
Definition fuel := 8%nat.
365+
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+
376+
Definition test_results_pf :=
377+
UMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
378+
379+
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
380+
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
381+
Proof.
382+
vm_compute (elements _).
383+
apply NoDup_Permutation; try solve_NoDup; set_solver.
384+
Qed.
385+
End MPDMBS.

‎ArchSemArm/tests/VMPromisingTest.v‎

Lines changed: 32 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -421,7 +421,7 @@ Module LDRPT.
421421
Qed.
422422
End LDRPT.
423423

424-
(* Module MP.
424+
Module MP.
425425
(* A classic MP litmus test with address translation
426426
Thread 1: STR X2, [X1, X0]; STR X5, [X4, X3]
427427
Thread 2: LDR X5, [X4, X3]; LDR X2, [X1, X0]
@@ -476,15 +476,15 @@ End LDRPT.
476476
|> mem_insert 0x1100 8 0x0
477477
|> mem_insert 0x1200 8 0x0
478478
(* L0[1] -> L1 (for VA with L0 index = 1) *)
479-
|> mem_insert 0x80008 8 0x81003
479+
|> mem_insert 0x80008 8 0x81803
480480
(* L1[0] -> L2 *)
481-
|> mem_insert 0x81000 8 0x82003
481+
|> mem_insert 0x81000 8 0x82803
482482
(* L2[0] -> L3 *)
483-
|> mem_insert 0x82000 8 0x83003
483+
|> mem_insert 0x82000 8 0x83803
484484
(* L3[0] : map VA page 0x8000000000 -> PA page 0x0000 (executable) *)
485-
|> mem_insert 0x83000 8 0x3
485+
|> mem_insert 0x83000 8 0x403
486486
(* L3[1] : map VA page 0x8000001000 -> PA page 0x1000 (data) *)
487-
|> mem_insert 0x83008 8 0x1003.
487+
|> mem_insert 0x83008 8 0x1443.
488488

489489
Definition n_threads := 2%nat.
490490

@@ -496,23 +496,21 @@ End LDRPT.
496496
(λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).
497497

498498
Definition initState :=
499-
{| MState.state :=
500-
{| MState.memory := init_mem;
501-
MState.regs := [# init_reg_t1; init_reg_t2];
502-
MState.address_space := PAS_NonSecure |};
503-
MState.termCond := termCond |}.
499+
{|archState.memory := init_mem;
500+
archState.regs := [# init_reg_t1; init_reg_t2];
501+
archState.address_space := PAS_NonSecure |}.
504502

505503
Definition fuel := 6%nat.
506504

507-
Definition test_results :=
505+
(* Definition test_results :=
508506
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
509507
510508
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
511509
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
512510
Proof.
513511
vm_compute (elements _).
514512
apply NoDup_Permutation; try solve_NoDup; set_solver.
515-
Qed.
513+
Qed. *)
516514

517515
Definition test_results_pf :=
518516
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
@@ -523,9 +521,9 @@ End LDRPT.
523521
vm_compute (elements _).
524522
apply NoDup_Permutation; try solve_NoDup; set_solver.
525523
Qed.
526-
End MP. *)
524+
End MP.
527525

528-
(* Module MPDMBS.
526+
Module MPDMBS.
529527
(* A classic MP litmus test with address translation
530528
Thread 1: STR X2, [X1, X0]; DMB SY; STR X5, [X4, X3]
531529
Thread 2: LDR X5, [X4, X3]; DMB SY; LDR X2, [X1, X0]
@@ -587,9 +585,9 @@ End MP. *)
587585
(* L2[0] -> L3 *)
588586
|> mem_insert 0x82000 8 0x83003
589587
(* L3[0] : map VA page 0x8000000000 -> PA page 0x0000 (executable) *)
590-
|> mem_insert 0x83000 8 0x3
588+
|> mem_insert 0x83000 8 0x403
591589
(* L3[1] : map VA page 0x8000001000 -> PA page 0x1000 (data) *)
592-
|> mem_insert 0x83008 8 0x1003.
590+
|> mem_insert 0x83008 8 0x60000000001443.
593591

594592
Definition n_threads := 2%nat.
595593

@@ -600,22 +598,31 @@ End MP. *)
600598
(λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).
601599

602600
Definition initState :=
603-
{| MState.state :=
604-
{| MState.memory := init_mem;
605-
MState.regs := [# init_reg_t1; init_reg_t2];
606-
MState.address_space := PAS_NonSecure |};
607-
MState.termCond := termCond |}.
601+
{|archState.memory := init_mem;
602+
archState.regs := [# init_reg_t1; init_reg_t2];
603+
archState.address_space := PAS_NonSecure |}.
608604

609605
Definition fuel := 8%nat.
610606

611-
Definition test_results :=
612-
VMPromising_cert_c arm_sem fuel n_threads initState.
607+
(* Definition test_results :=
608+
VMPromising_cert_c arm_sem fuel n_threads termCond initState.
613609
614610
(** The test is fenced enough, the 0x1; 0x0 outcome is impossible*)
615611
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
616612
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
617613
Proof.
618614
vm_compute (elements _).
619615
apply NoDup_Permutation; try solve_NoDup; set_solver.
616+
Qed. *)
617+
618+
Definition test_results_pf :=
619+
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
620+
621+
(** The test is fenced enough, the 0x1; 0x0 outcome is impossible*)
622+
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results_pf) ≡ₚ
623+
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]].
624+
Proof.
625+
vm_compute (elements _).
626+
apply NoDup_Permutation; try solve_NoDup; set_solver.
620627
Qed.
621-
End MPDMBS. *)
628+
End MPDMBS.

0 commit comments

Comments
 (0)