refactor: Allow op and model initialisation to fail, and promises

ArchSem/GenPromising.v

@@ -168,7 +168,8 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
       (** The thread state of the model *)
       tState : Type;
       (** Initialize the model thread state from architectural state *)
-      tState_init : (* tid *) nat → memoryMap → registerMap → tState;
+      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 *)
       tState_regs : tState → registerMap;
@@ -199,15 +200,14 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
                   ∀ out : outcome,
                   Exec.t (PPState.t tState mEvent iis) string
                          (eff_ret out * option nat);
-      (** Update a thread state after emission of a promise. This is called
+      (** Updates a thread state after emission of a promise. This is called
           once for every thread of the machine, with [tid] being the tid of the
-          thread being updated; the thread that made the promise is
-          [mEvent_tid] of the event. The new promise has already been added to
-          the memory when calling that function. I'm not considering that
-          emit_promise can fail or have a non-deterministic behaviour.
-          TODO: Add support for failure *)
+          thread being updated; the thread that made the promise is [mEvent_tid]
+          of the event. The new promise has already been added to the memory
+          when calling that function. *)
       emit_promise : (* updated thread tid *) nat → memoryMap →
-                     PromMemory.t mEvent → mEvent → tState → tState;
+                     PromMemory.t mEvent → mEvent → tState →
+                     result string tState;
       (** Hook for extra UB checks to be done before returning a final state,
           e.g. BBM checks. Any returned string is an error, [[]] is success. *)
       check_valid_end : (* tid *) nat → memoryMap → tState →
@@ -290,37 +290,34 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
 
       (** Emit a promise, updating every thread state. The thread that made
           the promise is [prom.(mEvent_tid) event] *)
-      Definition promise (event : mEvent) (st : t) :=
+      Definition promise (event : mEvent) (st : t) : result string t :=
         let st := set events (event ::.) st in
-        set tstates
-          (vimap
-             (λ tid, prom.(emit_promise) tid st.(initmem) st.(events) event))
-          st.
+        nts ←
+          vimapM
+            (λ tid ts,
+               prom.(emit_promise) tid st.(initmem) st.(events) event ts)
+            st.(tstates);
+        mret (setv tstates nts st).
 
       (** The inductive stepping relation of the non-certified promising model
           (non_executable) *)
       Inductive non_cert_step (ps : t) : (t) -> Prop :=
       | SRun (tid : fin n) (ps' : t) :
         (ps', ()) ∈ (run_tid tid ps) → non_cert_step ps ps'
-      | SPromise (event : mEvent) :
+      | SPromise (event : mEvent) (ps' : t) :
         prom.(mEvent_tid) event < n →
-        non_cert_step ps (promise event ps).
-
-      Lemma non_cert_step_promise  (ps ps' : t) (event : mEvent) :
-        prom.(mEvent_tid) event < n →
-        ps' = promise event ps →
+        promise event ps = Ok ps' →
         non_cert_step ps ps'.
-      Proof using. sauto l:on. Qed.
 
       (** Create an initial promising state from a generic machine state *)
-      Definition from_archState (ms: archState n) : t :=
-        {|tstates :=
-            fun_to_vec
-              (λ tid,
-                 prom.(tState_init) tid ms.(archState.memory)
-                                                  $ ms.(archState.regs) !!! tid);
-          initmem := ms.(archState.memory);
-          events := []|}.
+      Definition from_archState (ms: archState n) : result string t :=
+        nts ←
+          vimapM
+            (λ tid rm, prom.(tState_init) tid ms.(archState.memory) rm)
+            ms.(archState.regs);
+        mret {|tstates := nts;
+               initmem := ms.(archState.memory);
+               events := []|}.
 
       (** Convert a promising state to a generic machine state.
           This is a lossy conversion *)
@@ -333,27 +330,40 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
 
   End PState.
 
-  (** Create a non-computational model from an ISA model and promising model *)
+  (** Create a non-computational non-certified model from an ISA model and
+      promising model
+
+      This model will create a lot of spurious error but is only intended as a
+      proof tool. The goal is that any non-error trace of that model can be
+      reproduced in the certified promising model. *)
   Definition Promising_to_Modelnc (prom : Promising.Model) (isem : iMon ()) :
       archModel.nc ∅ :=
     λ n term (initMs : archState n),
       {[ mr : archModel.res ∅ n term |
-         let initPs := PState.from_archState prom initMs in
-         match mr with
-         | archModel.Res.FinalState fs _ =>
-             ∃ finPs, rtc (PState.non_cert_step isem prom) initPs finPs ∧
-                        PState.to_archState prom finPs = fs ∧
-                        PState.nopromises prom finPs ∧
-                        PState.check_valid_end prom finPs = []
-         | archModel.Res.Error s =>
-             ∃ finPs,
-              rtc (PState.non_cert_step isem prom) initPs finPs ∧
-                ((∃ tid, Error s ∈ PState.run_tid isem prom tid finPs)
-                  ∨
-                 (PState.terminated prom term finPs ∧
-                  PState.nopromises prom finPs ∧
-                  s ∈ PState.check_valid_end prom finPs))
-         | _ => False
+         match PState.from_archState prom initMs with
+         | Error s => mr = archModel.Res.Error s
+         | Ok initPs =>
+             match mr with
+             | archModel.Res.FinalState fs _ =>
+                 ∃ finPs, rtc (PState.non_cert_step isem prom) initPs finPs ∧
+                            PState.to_archState prom finPs = fs ∧
+                            PState.nopromises prom finPs ∧
+                            PState.check_valid_end prom finPs = []
+             | archModel.Res.Error s =>
+                 ∃ finPs,
+                  rtc (PState.non_cert_step isem prom) initPs finPs ∧
+                    ((∃ tid, Error s ∈ PState.run_tid isem prom tid finPs)
+                      ∨
+                     (∃ ev,
+                         (* This is way too trigger happy *)
+                         prom.(Promising.mEvent_tid) ev < n →
+                         PState.promise prom ev finPs = Error s)
+                      ∨
+                     (PState.terminated prom term finPs ∧
+                      PState.nopromises prom finPs ∧
+                      s ∈ PState.check_valid_end prom finPs))
+             | _ => False
+             end
          end]}.
 
   (** Computational promising state. Right now it the same type as PState.t but
@@ -491,7 +501,8 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
     Definition cpromise_tid (fuel : nat) (tid : fin n) : Exec.t t string () :=
       st ← mGet;
       ev ← mlift (promise_select_tid fuel st tid);
-      mSetv (promise prom ev st).
+      nst ← mlift (promise prom ev st);
+      mSetv nst.
 
     (** Run any possible step, this is the most exhaustive and expensive kind of
         search but it is obviously correct. If a thread has reached termination
@@ -545,7 +556,8 @@ Module GenPromising (Arch : Arch) (Inter : InterfaceT Arch)
       | 0 =>
         tid ← mchoosef (fin n);
         next_ev ← mchoosel (execution_results !!! tid).(promises);
-        mSet (promise prom next_ev);;
+        nst ← mlift (promise prom next_ev st);
+        mSetv nst;;
         mret None
       | 1 =>
         (* Compute cartesian products of the possible thread states *)

ArchSem/SeqModel.v

@@ -156,7 +156,7 @@ Module SequentialModel (Arch : Arch) (Inter : InterfaceT Arch)
         transition per instruction, but one could easily make one that does one
         transition per outcome *)
     Definition sequential_opmodel (isem : iMon ()) : opModel 1 :=
-      let init _ initSt := {| sst := initSt; written := ∅ |} in
+      let init _ initSt := mret {| sst := initSt; written := ∅ |} in
       let step term _ _ :=
         st ← mget sst;
         if decide (archState.is_terminated term st) is left p

ArchSem/TermModels.v

@@ -399,7 +399,10 @@ Module TermModels (Arch : Arch) (Inter : InterfaceT Arch). (* to be imported *)
     Record t {nth : nat} :=
       Make {
           state : Type;
-          init : terminationCondition nth → archState nth → state;
+          (** Build the initial model state. Returning an [Error] aborts the
+              run with that message *)
+          init : terminationCondition nth → archState nth →
+                 result string state;
           step : ∀ term : terminationCondition nth,
             (* Initial state again *) archState nth → (* fuel *) nat →
             (* Returning None means this is not a final transition *)
@@ -421,17 +424,20 @@ Module TermModels (Arch : Arch) (Inter : InterfaceT Arch). (* to be imported *)
     Definition to_archModel (opmod : ∀ nth, t nth) (fuel : nat) : archModel.c ∅ :=
       λ nth term (initSt : archState nth),
         let opmod := opmod nth in
-        opmod.(init) term initSt |>
-          archModel.Res.from_exec
-            $ run opmod fuel term initSt.
+        match opmod.(init) term initSt with
+        | Error s => mret (archModel.Res.Error s)
+        | Ok st => archModel.Res.from_exec (run opmod fuel term initSt) st
+        end.
 
     (** Convert a single-core operational model to a architectural model *)
     Definition to_archModel1 (opmod : t 1) (fuel : nat) : archModel.c ∅ :=
       λ nth,
         match nth with
         | 1 => λ term initSt,
-            opmod.(init) term initSt
-            |> archModel.Res.from_exec (run opmod fuel term initSt)
+            match opmod.(init) term initSt with
+            | Error s => mret (archModel.Res.Error s)
+            | Ok st => archModel.Res.from_exec (run opmod fuel term initSt) st
+            end
         | _ => λ _ _, mret (archModel.Res.Error "Expected one thread")
         end.
 

ArchSemArm/UMPromising.v

@@ -601,7 +601,7 @@ Import Promising.
 
 Definition UMPromising : Promising.Model :=
   {|tState := TState.t;
-    tState_init := λ tid, TState.init;
+    tState_init := λ tid mem regs, mret (TState.init mem regs);
     tState_regs := TState.reg_map;
     tState_nopromises := is_emptyb ∘ TState.prom;
     iis := IIS.t;
@@ -612,8 +612,9 @@ Definition UMPromising : Promising.Model :=
     filter_promises := λ _ _ _ promises, promises;
     handle_outcome := λ _ tid initmem, run_outcome tid initmem;
     emit_promise := λ tid initmem mem msg ts,
-      if bool_decide (Msg.tid msg = tid) then TState.promise (length mem) ts
-      else ts;
+      mret $
+        if bool_decide (Msg.tid msg = tid) then TState.promise (length mem) ts
+        else ts;
     check_valid_end := λ _ _ _ _, [];
     memory_snapshot := Memory.to_memMap;
   |}.

ArchSemArm/VMPromising.v

@@ -2854,11 +2854,12 @@ End BBM.
 Import Promising.
 
 Definition emit_promise' (tid : nat) (initmem : memoryMap) (mem : Memory.t)
-    (ev : Ev.t) (ts : TState.t) : TState.t :=
-  if bool_decide (Ev.tid ev = tid) then
-    if ev is Ev.Msg _ then TState.promise_write (length mem) ts
-    else TState.promise_tlbi (length mem) ts
-  else ts.
+    (ev : Ev.t) (ts : TState.t) : result string TState.t :=
+  mret $
+    if bool_decide (Ev.tid ev = tid) then
+      if ev is Ev.Msg _ then TState.promise_write (length mem) ts
+      else TState.promise_tlbi (length mem) ts
+    else ts.
 
 (** Avoid exploring duplicate TLBI promise orders.  During one enumeration run,
     we keep TLBI recipients in nondecreasing order, comparing each candidate
@@ -2880,7 +2881,7 @@ Definition filter_tlbi_promises
 
 Definition VMPromising (bbm_param : BBM.param) : Promising.Model :=
   {|tState := TState.t;
-    tState_init := λ tid, TState.init;
+    tState_init := λ tid mem regs, mret (TState.init mem regs);
     tState_regs := TState.reg_map;
     tState_nopromises := (λ ts, is_emptyb (TState.prom_wr ts ++ TState.prom_tlbi ts));
     iis := IIS.t;

ArchSemX86/OperationalX86TSO.v

@@ -450,20 +450,21 @@ Section Model.
       transitions. Need [fuel] for all instruction + all flushed writes + 1 for the
       terminating step *)
   Definition x86_tso_opmodel : opModel threads :=
+    let init term initSt := mret (from_archState term initSt) in
     let opstep term _ _ :=
       fstate ← mget (to_terminated_archState term);
       if fstate is Some fs then mret (Some fs) else
         step term;;
         mret None
     in
-    opModel.Make threads mstate from_archState opstep.
+    opModel.Make threads mstate init opstep.
 
 
   (** The X86-TSO model with eager steps. The fuel of of the previous model plus
       one is guaranteed to be sufficient but some lower fuel might work
       depending on the interleaving of eager and non-eager steps. *)
   Definition x86_tso_opmodel_eager : opModel threads :=
-    let init term initSt := (from_archState term initSt, true) in
+    let init term initSt := mret (from_archState term initSt, true) in
     let step term _ fuel :=
       fstate ← mget (to_terminated_archState term ∘ fst);
       if fstate is Some fs then mret (Some fs)

Common/CExtraction.v

@@ -401,6 +401,7 @@ Extract Inlined Constant vec_to_list => "(fun x -> x)".
 
 Extraction Implicit cprodn [A n].
 Extraction Implicit vmapM [A B n].
+Extraction Implicit vimapM [A B n].
 
 Extraction Implicit vec_dec [A n].
 Extract Inlined Constant vec_dec => "List.equal".

Common/CVec.v

@@ -259,6 +259,19 @@ Fixpoint vmapM {A B} `{MBind M, MRet M} (f : A → M B) {n} (v : vec A n) :
 Definition vimap {A B n} (f : fin n → A → B) (v : vec A n) : vec B n :=
   fun_to_vec (λ i, f i (v !!! i)).
 
+(** * vimapM *)
+
+Fixpoint vimapM {A B} `{MBind M, MRet M} {n} (f : fin n → A → M B)
+    (v : vec A n) : M (vec B n) :=
+  match v in vec _ n return (fin n → A → M B) → M (vec B n) with
+  | [#] => λ _, mret [#]
+  | hd ::: tl =>
+      λ f,
+        nhd ← f 0%fin hd;
+        ntl ← vimapM (f ∘ FS) tl;
+        mret (nhd ::: ntl)
+  end f.
+
 (** * venumerate *)
 Definition venumerate {A n} (v : vec A n) : vec ((fin n) * A) n :=
   fun_to_vec (λ i, (i, v !!! i)).

Extraction/arch.mli

@@ -176,7 +176,9 @@ module type Arch = sig
       (** The internal state of the model *)
       type state
 
-      val init : t -> termCond -> ArchState.t -> state
+      (** Build the initial model state, or return the error message with
+          which the model rejected the initial architectural state *)
+      val init : t -> termCond -> ArchState.t -> (state, string) result
 
       (** [step model term initSt ~fuel st] takes one transition from [st].
           [initSt] is the initial architectural state and [fuel] the amount of

Extraction/archBuild.ml

@@ -218,7 +218,7 @@ module Build (ArchReq : ArchRequired) = struct
 
       type state
 
-      val init : t -> termCond -> ArchState.t -> state
+      val init : t -> termCond -> ArchState.t -> (state, string) result
 
       val step :
          t ->

cli/lib/litmus/driver.ml

@@ -69,7 +69,10 @@ module Make (A : Archsem.Arch) (M : A.OpModel.S) = struct
           in
           loop finals errors rest
     in
-    let (finals, errors) = loop [] [] [(M.init m term initSt, fuel)] in
-    List.rev_map (fun fs -> A.ArchModel.Res.FinalState fs) finals
-    @ List.rev_map (fun e -> A.ArchModel.Res.Error e) errors
+    match M.init m term initSt with
+    | Error e -> [A.ArchModel.Res.Error e]
+    | Ok st ->
+        let (finals, errors) = loop [] [] [(st, fuel)] in
+        List.rev_map (fun fs -> A.ArchModel.Res.FinalState fs) finals
+        @ List.rev_map (fun e -> A.ArchModel.Res.Error e) errors
 end