Skip to content

Commit b898dc2

Browse files
febyejifebyeji
committed
Pass MP, MPDMBS tests with address translation
1 parent 9f1336c commit b898dc2

File tree

4 files changed

+117
-29
lines changed

4 files changed

+117
-29
lines changed

‎ArchSem/GenPromising.v‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,6 @@ Require Import ASCommon.Common.
5353
Require Import ASCommon.Exec.
5454
Require Import ASCommon.Effects.
5555
Require Import ASCommon.FMon.
56-
Require Import ASCommon.HVec.
5756
Require Import ASCommon.StateT.
5857

5958
Require Import Relations.

‎ArchSemArm/VMPromising.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2117,4 +2117,4 @@ Definition VMPromising_cert_c isem fuel :=
21172117
Promising_to_Modelc isem (VMPromising_exe' isem) fuel.
21182118

21192119
Definition VMPromising_cert_c_pf isem fuel :=
2120-
Promising_to_Modelc isem (VMPromising_exe' isem) fuel.
2120+
Promising_to_Modelc_pf isem (VMPromising_exe' isem) fuel.

‎ArchSemArm/tests/UMPromisingTest.v‎

Lines changed: 84 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -288,7 +288,7 @@ Module MP.
288288
Goal elements (regs_extract [(1%fin, R5); (1%fin, R2)] <$> test_results) ≡ₚ
289289
[Ok [0x0%Z;0x2a%Z]; Ok [0x0%Z;0x0%Z]; Ok [0x1%Z; 0x2a%Z]; Ok [0x1%Z; 0x0%Z]].
290290
Proof.
291-
Time vm_compute (elements _).
291+
vm_compute (elements _).
292292
apply NoDup_Permutation; try solve_NoDup; set_solver.
293293
Qed.
294294

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

‎ArchSemArm/tests/VMPromisingTest.v‎

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

425-
(* Module MP.
425+
Module MP.
426426
(* A classic MP litmus test with address translation
427427
Thread 1: STR X2, [X1, X0]; STR X5, [X4, X3]
428428
Thread 2: LDR X5, [X4, X3]; LDR X2, [X1, X0]
@@ -477,15 +477,15 @@ End LDRPT.
477477
|> mem_insert 0x1100 8 0x0
478478
|> mem_insert 0x1200 8 0x0
479479
(* L0[1] -> L1 (for VA with L0 index = 1) *)
480-
|> mem_insert 0x80008 8 0x81003
480+
|> mem_insert 0x80008 8 0x81803
481481
(* L1[0] -> L2 *)
482-
|> mem_insert 0x81000 8 0x82003
482+
|> mem_insert 0x81000 8 0x82803
483483
(* L2[0] -> L3 *)
484-
|> mem_insert 0x82000 8 0x83003
484+
|> mem_insert 0x82000 8 0x83803
485485
(* L3[0] : map VA page 0x8000000000 -> PA page 0x0000 (executable) *)
486-
|> mem_insert 0x83000 8 0x3
486+
|> mem_insert 0x83000 8 0x403
487487
(* L3[1] : map VA page 0x8000001000 -> PA page 0x1000 (data) *)
488-
|> mem_insert 0x83008 8 0x1003.
488+
|> mem_insert 0x83008 8 0x1443.
489489

490490
Definition n_threads := 2%nat.
491491

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

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

506504
Definition fuel := 6%nat.
507505

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

518516
Definition test_results_pf :=
519517
VMPromising_cert_c_pf arm_sem fuel n_threads termCond initState.
@@ -524,9 +522,9 @@ End LDRPT.
524522
vm_compute (elements _).
525523
apply NoDup_Permutation; try solve_NoDup; set_solver.
526524
Qed.
527-
End MP. *)
525+
End MP.
528526

529-
(* Module MPDMBS.
527+
Module MPDMBS.
530528
(* A classic MP litmus test with address translation
531529
Thread 1: STR X2, [X1, X0]; DMB SY; STR X5, [X4, X3]
532530
Thread 2: LDR X5, [X4, X3]; DMB SY; LDR X2, [X1, X0]
@@ -588,9 +586,9 @@ End MP. *)
588586
(* L2[0] -> L3 *)
589587
|> mem_insert 0x82000 8 0x83003
590588
(* L3[0] : map VA page 0x8000000000 -> PA page 0x0000 (executable) *)
591-
|> mem_insert 0x83000 8 0x3
589+
|> mem_insert 0x83000 8 0x403
592590
(* L3[1] : map VA page 0x8000001000 -> PA page 0x1000 (data) *)
593-
|> mem_insert 0x83008 8 0x1003.
591+
|> mem_insert 0x83008 8 0x60000000001443.
594592

595593
Definition n_threads := 2%nat.
596594

@@ -601,22 +599,31 @@ End MP. *)
601599
(λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).
602600

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

610606
Definition fuel := 8%nat.
611607

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

0 commit comments

Comments
 (0)