refactor: Make termination condition be breakpoints lists

ArchSem/GenPromising.v

@@ -170,9 +170,15 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
       (** Initialize the model thread state from architectural state *)
       tState_init : (* tid *) nat → memoryMap → registerMap →
                     result string tState;
-      (** Get a register map out of a thread state to test the termination
-          condition and compute a final state *)
+      (** Get a register map out of a thread state to compute a final state.
+          This is only used once per execution *)
       tState_regs : tState → registerMap;
+      (** Get the PC out of a thread state. This is on the hot path: it is
+          called at every step to test the termination condition *)
+      tState_pc : tState → option (reg_type pc_reg);
+      (** [tState_pc] must agree with [tState_regs] *)
+      tState_pc_spec :
+        ∀ ts, tState_pc ts = reg_lookup pc_reg (tState_regs ts);
       (** Check if a thread state has no pending promises, which means that it
           can be explained with the current memory state *)
       tState_nopromises : tState → bool;
@@ -247,9 +253,13 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
       Local Notation mEvent := prom.(mEvent).
       Local Notation t := (t tState mEvent n).
 
+      (** Check if a thread state has reached one of its breakpoints *)
+      Definition terminated_ts (bps : list (reg_type pc_reg)) (ts : tState) :=
+        pc_terminated bps (prom.(tState_pc) ts).
+
       (** Check if a thread has finished according to term *)
       Definition terminated_tid (term : terminationCondition n) (ps : t)
-        (tid : fin n) := ps |> tstate tid |> prom.(tState_regs) |> term tid.
+        (tid : fin n) := ps |> tstate tid |> terminated_ts (term !!! tid).
 
       (** Check if all thread have finished according to term *)
       Definition terminated (term : terminationCondition n) (ps : t) :=
@@ -325,6 +335,33 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
         {|archState.regs := vmap (prom.(tState_regs)) ps.(tstates);
           archState.memory := prom.(memory_snapshot) ps.(initmem) ps.(events);
           archState.address_space := prom.(address_space) |}.
+
+      Lemma terminated_ts_regs (bps : list (reg_type pc_reg)) (ts : tState) :
+        terminated_ts bps ts = regs_terminated bps (prom.(tState_regs) ts).
+      Proof using.
+        unfold terminated_ts, regs_terminated.
+        by rewrite prom.(tState_pc_spec).
+      Qed.
+
+      Lemma terminated_tid_archState (term : terminationCondition n) (ps : t)
+          (tid : fin n) :
+        terminated_tid term ps tid =
+          regs_terminated (term !!! tid)
+            ((to_archState ps).(archState.regs) !!! tid).
+      Proof using.
+        unfold terminated_tid, to_archState.
+        cbn.
+        rewrite vlookup_map.
+        apply terminated_ts_regs.
+      Qed.
+
+      Lemma terminated_to_archState (term : terminationCondition n) (ps : t) :
+        terminated term ps → archState.is_terminated term (to_archState ps).
+      Proof using.
+        unfold terminated, archState.is_terminated.
+        setoid_rewrite <- terminated_tid_archState.
+        by bool_unfold.
+      Qed.
     End PSProm.
 
 
@@ -401,11 +438,10 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
         mthrow err.
 
     (** Convert a final promising state to a generic final state *)
-    Program Definition to_final_archState (f : final) :
+    Definition to_final_archState (f : final) :
         {s & archState.is_terminated term s} :=
-      existT (to_archState prom f) _.
-    Solve All Obligations with
-      hauto unfold:terminated unfold:archState.is_terminated l:on db:vec, brefl.
+      existT (to_archState prom (proj1_sig f))
+        (terminated_to_archState prom term (proj1_sig f) (proj2_sig f)).
 
 
     Section EnumerateResult.
@@ -433,7 +469,7 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
       Fixpoint run_to_termination (fuel : nat) (base : nat) :
           Exec.t (list mEvent * PPState.t tState mEvent iis) string bool :=
         ts ← mget (PPState.state ∘ snd);
-        if term tid (prom.(tState_regs) ts) then
+        if terminated_ts prom (term !!! tid) ts then
           mret true
         else
           match fuel with

ArchSem/TermModels.v

@@ -136,10 +136,23 @@ Module TermModels (Arch : Arch) (Inter : InterfaceT Arch). (* to be imported *)
   Definition reg_delete (r : reg) : registerMap → registerMap := dmap_delete r.
 
   (** A termination condition that define when each thread should stop.
-
-      We expect this will be restricted to only being about the PC (RIP on x86)
-      soon (maybe also the privilege level) *)
-  Definition terminationCondition (n : nat) := fin n → registerMap → bool.
+      Each has a list of breakpoint at which it stops.
+      This is deliberately restricted to support Flat-like models.
+      This may later be extended with the privilege level. *)
+  Definition terminationCondition (n : nat) := vec (list (reg_type pc_reg)) n.
+  #[global] Typeclasses Transparent terminationCondition.
+
+  (** Test a thread's breakpoint list against a PC value from a register map. To
+      avoid complexifing the error path, a thread whose PC is unset is never
+      terminated. Such a thing should never happen in practice. *)
+  Definition pc_terminated (bps : list (reg_type pc_reg))
+      (pc : option (reg_type pc_reg)) : bool :=
+    if pc is Some pc then bool_decide (pc ∈ bps) else false.
+
+  (** Test a thread's breakpoint list against a full register map *)
+  Definition regs_terminated (bps : list (reg_type pc_reg))
+      (rm : registerMap) : bool :=
+    pc_terminated bps (reg_lookup pc_reg rm).
 
   (** ** Architectural state
 
@@ -168,7 +181,7 @@ Module TermModels (Arch : Arch) (Inter : InterfaceT Arch). (* to be imported *)
     Arguments t : clear implicits.
 
     Definition is_terminated `(termCond : terminationCondition n) (s : t n) :=
-      ∀ tid, termCond tid (s.(regs) !!! tid).
+      ∀ tid, regs_terminated (termCond !!! tid) (s.(regs) !!! tid).
 
     #[export] Instance is_terminated_dec n term s :
       Decision (@is_terminated n term s).

ArchSemArm/UMPromising.v

@@ -245,12 +245,18 @@ Module TState.
       xclb := None
     |})%nat.
 
-  (** Extracts a plain register map from the thread state without views.
-      This is used to decide if a thread has terminated, and to observe the
-      results of the model *)
+  (** Extracts a plain register map from the thread state without views. *)
   Definition reg_map (ts : t) : registerMap :=
     dmap_map (λ _, fst) ts.(regs).
 
+  (** Extract the PC from the thread state, without rebuilding a full register
+      map. This is used to decide if a thread has terminated on every step *)
+  Definition pc (ts : t) : option (reg_type pc_reg) :=
+    fst <$> dmap_lookup pc_reg ts.(regs).
+
+  Lemma pc_reg_map (ts : t) : pc ts = reg_lookup pc_reg (reg_map ts).
+  Proof. unfold pc, reg_map, reg_lookup. by rewrite dmap_lookup_map. Qed.
+
   (** Sets the value of a register *)
   Definition set_reg (reg : reg) (rv : reg_type reg * view) (ts : t) : option t :=
     if decide (is_Some (dmap_lookup reg ts.(regs))) then
@@ -603,6 +609,8 @@ Definition UMPromising : Promising.Model :=
   {|tState := TState.t;
     tState_init := λ tid mem regs, mret (TState.init mem regs);
     tState_regs := TState.reg_map;
+    tState_pc := TState.pc;
+    tState_pc_spec := TState.pc_reg_map;
     tState_nopromises := is_emptyb ∘ TState.prom;
     iis := IIS.t;
     iis_init := IIS.init;

ArchSemArm/VMPromising.v

@@ -596,9 +596,7 @@ Module TState.
       read_sreg_direct ts r
     else dmap_lookup r ts.(regs).
 
-  (** Extract a plain register map from the thread state without views.
-      This is used to decide if a thread has terminated, and to observe the
-      results of the model *)
+  (** Extract a plain register map from the thread state without views. *)
   Definition reg_map (ts : t) : registerMap :=
     dmap_map
       (λ r rv,
@@ -607,6 +605,14 @@ Module TState.
         else rv.1)
       ts.(regs).
 
+  (** Extract the PC from the thread state, without rebuilding a full register
+      map. This is used to decide if a thread has terminated on every step *)
+  Definition pc (ts : t) : option (reg_type pc_reg) :=
+    fst <$> dmap_lookup pc_reg ts.(regs).
+
+  Lemma pc_reg_map (ts : t) : pc ts = reg_lookup pc_reg (reg_map ts).
+  Proof. unfold pc, reg_map, reg_lookup. by rewrite dmap_lookup_map. Qed.
+
   (** Sets the value of a register *)
   Definition set_reg (reg : reg) (rv : reg_type reg * view) (ts : t) : option t :=
     if decide (is_Some (dmap_lookup reg ts.(regs))) then
@@ -2883,6 +2889,8 @@ Definition VMPromising (bbm_param : BBM.param) : Promising.Model :=
   {|tState := TState.t;
     tState_init := λ tid mem regs, mret (TState.init mem regs);
     tState_regs := TState.reg_map;
+    tState_pc := TState.pc;
+    tState_pc_spec := TState.pc_reg_map;
     tState_nopromises := (λ ts, is_emptyb (TState.prom_wr ts ++ TState.prom_tlbi ts));
     iis := IIS.t;
     iis_init := IIS.init;

ArchSemArm/tests/ArmSeqModelTest.v

@@ -80,7 +80,7 @@ Definition init_mem : memoryMap:=
   |> mem_insert 0x500 4 0xca020020. (* EOR X0, X1, X2 *)
 
 Definition termCond : terminationCondition 1 :=
-  (λ tid rm, reg_lookup _PC rm =? Some (0x504 : bv 64)).
+  [# [(0x504 : bv 64)]].
 
 Definition initState :=
   {|archState.memory := init_mem;
@@ -111,7 +111,7 @@ Definition init_mem : memoryMap:=
   |> mem_insert 0x1000 8 0x2a. (* data to be read *)
 
 Definition termCond : terminationCondition 1 :=
-  (λ tid rm, reg_lookup _PC rm =? Some (0x504 : bv 64)).
+  [# [(0x504 : bv 64)]].
 
 Definition initState :=
   {|archState.memory := init_mem;
@@ -143,7 +143,7 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
     |> mem_insert 0x1100 8 0x0. (* Memory need to exists to be written to *)
 
   Definition termCond : terminationCondition 1 :=
-    (λ tid rm, reg_lookup _PC rm =? Some (0x508 : bv 64)).
+    [# [(0x508 : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;

ArchSemArm/tests/UMPromisingTest.v

@@ -97,7 +97,7 @@ Module EOR.
   Definition n_threads := 1%nat.
 
   Definition termCond : terminationCondition n_threads :=
-    (λ tid rm, reg_lookup _PC rm =? Some (0x504 : bv 64)).
+    [# [(0x504 : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;
@@ -140,7 +140,7 @@ Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
   Definition n_threads := 1%nat.
 
   Definition termCond : terminationCondition n_threads :=
-    (λ tid rm, reg_lookup _PC rm =? Some (0x504 : bv 64)).
+    [# [(0x504 : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;
@@ -185,7 +185,7 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
   Definition n_threads := 1%nat.
 
   Definition termCond : terminationCondition n_threads :=
-    (λ tid rm, reg_lookup _PC rm =? Some (0x508 : bv 64)).
+    [# [(0x508 : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;
@@ -258,11 +258,10 @@ Module MP.
 
   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 two instructions *)
   Definition termCond : terminationCondition n_threads :=
-    (λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).
+    [# [(0x508 : bv 64)]; [(0x608 : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;
@@ -341,11 +340,10 @@ Module MPDMBS.
 
   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 three instructions *)
   Definition termCond : terminationCondition n_threads :=
-    (λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).
+    [# [(0x50c : bv 64)]; [(0x60c : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;
@@ -420,11 +418,10 @@ Module LB.
 
   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).
+    [# [(0x508 : bv 64)]; [(0x608 : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;
@@ -498,11 +495,10 @@ Module LBDMBS.
 
   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).
+    [# [(0x50c : bv 64)]; [(0x60c : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;
@@ -555,7 +551,7 @@ Module STRW_LDRX. (* STR W2, [X1, X0]; LDR X0, [X1, X0] — 4-byte write, 8-byte
   Definition n_threads := 1%nat.
 
   Definition termCond : terminationCondition n_threads :=
-    (λ tid rm, reg_lookup _PC rm =? Some (0x508 : bv 64)).
+    [# [(0x508 : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;
@@ -611,10 +607,9 @@ Module CoWWRmixed.
 
   Definition n_threads := 2%nat.
 
-  Definition terminate_at := [# Some (0x504 : bv 64); Some (0x608 : bv 64)].
 
   Definition termCond : terminationCondition n_threads :=
-    (λ tid rm, reg_lookup _PC rm =? terminate_at !!! tid).
+    [# [(0x504 : bv 64)]; [(0x608 : bv 64)]].
 
   Definition initState :=
     {|archState.memory := init_mem;