Skip to content

Add two ARM UMPromising tests #41

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Add two ARM UMPromising tests #41

Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ab7b90d
Add ARM UMPromising LB litmus test
Chris-F5 Nov 20, 2025
c3a7bf5
Add ARM UMPromising LBDMBS litmus test
Chris-F5 Nov 20, 2025
b2391dc
Initialize ARM UBPromising LB/LBDMBS test backing memory to zero
Chris-F5 Dec 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
136 changes: 136 additions & 0 deletions ArchSemArm/tests/UMPromisingTest.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -341,3 +341,139 @@ Module MPDMBS.
apply NoDup_Permutation; try solve_NoDup; set_solver.
Qed.
End MPDMBS.


Module LB.
(*
Thread 1 (X1=x, X2=#1, X3=y): LDR X0, [X1, X4]; STR X2, [X3, X4]
Thread 2 (X1=y, X2=#1, X3=x): LDR X0, [X1, X4]; STR X2, [X3, X4]
*)

Definition init_reg_t1 : registerMap :=
∅
|> reg_insert _PC 0x500
|> reg_insert R0 0x0
|> reg_insert R1 0x1000
|> reg_insert R2 0x1
|> reg_insert R3 0x2000
|> reg_insert R4 0x0
|> reg_insert SCTLR_EL1 0x0
|> reg_insert PSTATE (init_pstate 0%bv 0%bv).

Definition init_reg_t2 : registerMap :=
∅
|> reg_insert _PC 0x600
|> reg_insert R0 0x0
|> reg_insert R1 0x2000
|> reg_insert R2 0x1
|> reg_insert R3 0x1000
|> reg_insert R4 0x0
|> reg_insert SCTLR_EL1 0x0
|> reg_insert PSTATE (init_pstate 0%bv 0%bv).

Definition init_mem : memoryMap :=
∅
(* Thread 1 @ 0x500 *)
|> mem_insert 0x500 4 0xf8646820 (* LDR X0, [X1, X4] *)
|> mem_insert 0x504 4 0xf8246862 (* STR X2, [X3, X4] *)
(* Thread 2 @ 0x600 *)
|> mem_insert 0x600 4 0xf8646820 (* LDR X0, [X1, X4] *)
|> mem_insert 0x604 4 0xf8246862 (* STR X2, [X3, X4] *)
(* Backing memory *)
|> mem_insert 0x1000 8 0x1a
|> mem_insert 0x2000 8 0x2a.
Copy link
Collaborator

@tperami tperami Dec 1, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry for the nitpick, but standard litmus test convention it to initialize those to 0, so could you do that, otherwise it field weird for people that are used to those litmus tests

Copy link
Collaborator Author

@Chris-F5 Chris-F5 Dec 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is a bad convention because now you cant tell the difference between the zero from memory address 0x1000 and the zero from memory address 0x2000. Both types of zeros appear in the test expected results so they could be confused.

But a bad convention is better than no convention at all, so I have made the change.


Definition n_threads := 2%nat.

Definition terminate_at := [# Some (0x508 : bv 64); Some (0x608 : bv 64)].

(* Each thread’s PC must reach the end of its instructions *)
Definition termCond : terminationCondition n_threads :=
(λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).

Definition initState :=
{|archState.memory := init_mem;
archState.regs := [# init_reg_t1; init_reg_t2];
archState.address_space := PAS_NonSecure |}.

Definition fuel := 8%nat.

Definition test_results :=
UMPromising_cert_c arm_sem fuel n_threads termCond initState.

Goal elements (regs_extract [(0%fin, R0); (1%fin, R0)] <$> test_results) ≡ₚ
[Ok [0x01%Z; 0x01%Z]; Ok [0x1a%Z; 0x01%Z]; Ok [0x01%Z; 0x2a%Z]; Ok [0x1a%Z; 0x2a%Z]].
Proof.
vm_compute (elements _).
apply NoDup_Permutation; try solve_NoDup; set_solver.
Qed.
End LB.

Module LBDMBS.
(*
Thread 1 (X1=x, X2=#1, X3=y): LDR X0, [X1, X4]; DMB SY; STR X2, [X3, X4]
Thread 2 (X1=y, X2=#1, X3=x): LDR X0, [X1, X4]; DMB SY; STR X2, [X3, X4]
*)

Definition init_reg_t1 : registerMap :=
∅
|> reg_insert _PC 0x500
|> reg_insert R0 0x0
|> reg_insert R1 0x1000
|> reg_insert R2 0x1
|> reg_insert R3 0x2000
|> reg_insert R4 0x0
|> reg_insert SCTLR_EL1 0x0
|> reg_insert PSTATE (init_pstate 0%bv 0%bv).

Definition init_reg_t2 : registerMap :=
∅
|> reg_insert _PC 0x600
|> reg_insert R0 0x0
|> reg_insert R1 0x2000
|> reg_insert R2 0x1
|> reg_insert R3 0x1000
|> reg_insert R4 0x0
|> reg_insert SCTLR_EL1 0x0
|> reg_insert PSTATE (init_pstate 0%bv 0%bv).

Definition init_mem : memoryMap :=
∅
(* Thread 1 @ 0x500 *)
|> mem_insert 0x500 4 0xf8646820 (* LDR X0, [X1, X4] *)
|> mem_insert 0x504 4 0xd5033fbf (* DMB SY *)
|> mem_insert 0x508 4 0xf8246862 (* STR X2, [X3, X4] *)
(* Thread 2 @ 0x600 *)
|> mem_insert 0x600 4 0xf8646820 (* LDR X0, [X1, X4] *)
|> mem_insert 0x604 4 0xd5033fbf (* DMB SY *)
|> mem_insert 0x608 4 0xf8246862 (* STR X2, [X3, X4] *)
(* Backing memory *)
|> mem_insert 0x1000 8 0x1a
|> mem_insert 0x2000 8 0x2a.

Definition n_threads := 2%nat.

Definition terminate_at := [# Some (0x50c : bv 64); Some (0x60c : bv 64)].

(* Each thread’s PC must reach the end of its instructions *)
Definition termCond : terminationCondition n_threads :=
(λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).

Definition initState :=
{|archState.memory := init_mem;
archState.regs := [# init_reg_t1; init_reg_t2];
archState.address_space := PAS_NonSecure |}.

Definition fuel := 8%nat.

Definition test_results :=
UMPromising_cert_c arm_sem fuel n_threads termCond initState.

(* The (1, 1) result is now impossible due the barriers. *)
Goal elements (regs_extract [(0%fin, R0); (1%fin, R0)] <$> test_results) ≡ₚ
[Ok [0x1a%Z; 0x01%Z]; Ok [0x01%Z; 0x2a%Z]; Ok [0x1a%Z; 0x2a%Z]].
Proof.
vm_compute (elements _).
apply NoDup_Permutation; try solve_NoDup; set_solver.
Qed.
End LBDMBS.