Make Arm UMPromising model executable

Also:
- Add tests: same as seq model + dual-core MP
- Add support for initial memory instruction fetching (otherwise it wouldn't run)

Co-authored-by: Thibaut Pérami <[email protected]>

Author: febyeji

ArchSem/GenPromising.v

@@ -189,24 +189,24 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
           failing, promise_select effectively computes the allowed_promises
           set.*)
       promise_select :
-        (* fuel *) nat -> (* tid *) nat → memoryMap → pModel.(tState) →
-        PromMemory.t pModel.(mEvent) → Exec.res string pModel.(mEvent);
+        (* fuel *) nat → (* tid *) nat →
+        (* termination condition *) (registerMap → bool) →
+        memoryMap → pModel.(tState) → PromMemory.t pModel.(mEvent) →
+        Exec.res string pModel.(mEvent);
 
       promise_select_sound :
-      ∀ n tid initMem ts mem,
-        ∀ ev ∈ (promise_select n tid initMem ts mem),
+      ∀ fuel tid term initMem ts mem,
+        ∀ ev ∈ (promise_select fuel tid term initMem ts mem),
           ev ∈ pModel.(allowed_promises) tid initMem ts mem;
       promise_select_complete :
-      ∀ n tid initMem ts mem,
-        ¬ Exec.has_error (promise_select n tid initMem ts mem) →
+      ∀ fuel tid term initMem ts mem,
+        ¬ Exec.has_error (promise_select fuel tid term initMem ts mem) →
         ∀ ev ∈ pModel.(allowed_promises) tid initMem ts mem,
-          ev ∈ promise_select n tid initMem ts mem
+          ev ∈ promise_select fuel tid term initMem ts mem
     }.
   Arguments BasicExecutablePM : clear implicits.
 
-
   Module PState. (* namespace *)
-
     Section PS.
       Context {tState : Type}.
       Context {mEvent : Type}.
@@ -226,7 +226,6 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
     End PS.
     Arguments t : clear implicits.
 
-
     Section PSProm.
       Context (isem : iMon ()).
       Context (prom : PromisingModel).
@@ -345,7 +344,7 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
     (** Get a list of possible promises for a thread by tid *)
     Definition promise_select_tid (fuel : nat) (st : t)
         (tid : fin n) : Exec.res string mEvent :=
-      prom.(promise_select) n tid (initmem st) (tstate tid st) (events st).
+      prom.(promise_select) fuel tid (term tid) (initmem st) (tstate tid st) (events st).
 
     (** Take any promising step for that tid and promise it *)
     Definition cpromise_tid (fuel : nat) (tid : fin n)
@@ -361,7 +360,6 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
         search but it is obviously correct. If a thread has reached termination
         no progress is made in the thread (either instruction running or
         promises *)
-    (* TODO: Make if/then/else syntax only work on bool *)
     Definition run_step (fuel : nat) : Exec.t t string () :=
       st ← mGet;
       tid ← mchoose n;
@@ -387,17 +385,14 @@ Module GenPromising (IWA : InterfaceWithArch) (TM : TermModelsT IWA).
 
     (** Computational evaluate all the possible allowed final states according
         to the promising model prom starting from st *)
-    Program Fixpoint run (fuel : nat) : Exec.t t string final :=
-      match fuel with
-      | 0%nat => mthrow "not enough fuel"
-      | S fuel =>
-          st ← mGet;
-          if dec $ terminated prom term st then mret (make_final st _)
-          else
-            run_step fuel;;
-            run fuel
-      end.
-    Solve All Obligations with naive_solver.
+    Fixpoint run (fuel : nat) : Exec.t t string final :=
+      st ← mGet;
+      if decide $ terminated prom term st is left pt then mret (make_final st pt)
+      else
+        if fuel is S fuel then
+          run_step (S fuel);;
+          run fuel
+        else mthrow "Could not finish running within the size of the fuel".
     End CPS.
     Arguments to_final_MState {_ _ _}.
   End CPState.