Introduced extended specs to allow wrapping command sequences

The motivating use case is to make it nicer to test commands that perform
effects.

CHANGES.md

@@ -3,6 +3,7 @@
 ## NEXT RELEASE
 
 - #509: Change/Fix to use a symmetric barrier to synchronize domains
+- #511: Introduce extended specs to allow wrapping command sequences
 
 ## 0.6
 

lib/STM.ml

@@ -108,6 +108,19 @@ sig
       Note: [s] is in this case the model's state prior to command execution. *)
 end
 
+module type SpecExt =
+sig
+  include Spec
+
+  val wrap_cmd_seq : (unit -> 'a) -> 'a
+end
+
+module SpecDefaults =
+struct
+  let cleanup = ignore
+  let precond _ _ = true
+  let wrap_cmd_seq th = th ()
+end
 
 module Internal =
 struct

lib/STM.mli

@@ -75,7 +75,9 @@ type res =
 val show_res : res -> string
 
 
-(** The specification of a state machine. *)
+(** The specification of a state machine.
+
+    See also {!SpecExt} and {!SpecDefaults}. *)
 module type Spec =
 sig
   type cmd
@@ -126,6 +128,50 @@ sig
       This is helpful to model, e.g., a [remove] [cmd] that returns the removed element. *)
 end
 
+module type SpecExt =
+sig
+  (** Extended specification of a state machine.
+
+      This signature may be extended in the future with new specifications that
+      can be given defaults via {!SpecDefaults}. *)
+
+  include Spec
+
+  val wrap_cmd_seq : (unit -> 'a) -> 'a
+  (** [wrap_cmd_seq thunk] must call [thunk ()] and return or raise whatever
+      [thunk ()] returned or raised.  [wrap_cmd_seq] is used to wrap the
+      execution of the generated command sequences.  [wrap_cmd_seq] is useful,
+      e.g., to handle effects performed by blocking primitives. *)
+end
+
+module SpecDefaults :
+sig
+  (** Default implementations for state machine specifications that can be given
+      useful defaults.
+
+      The intention is that extended spec modules would [include] the defaults:
+
+      {[
+        module MySpec = struct
+          include SpecDefaults
+
+          (* ... *)
+        end
+      ]}
+
+      This way the spec module can usually just continue working after new
+      specifications have been added to {!SpecExt} with defaults in
+      {!SpecDefaults}. *)
+
+  val cleanup : 'sut -> unit
+  (** [cleanup sut] just return [()]. *)
+
+  val precond : 'cmd -> 'state -> bool
+  (** [precond cmd state] just returns [true]. *)
+
+  val wrap_cmd_seq : (unit -> 'a) -> 'a
+  (** [wrap_cmd_seq thunk] is equivalent to [thunk ()]. *)
+end
 
 module Internal : sig
 open QCheck

lib/STM_domain.ml

@@ -1,6 +1,6 @@
 open STM
 
-module Make (Spec: Spec) = struct
+module MakeExt (Spec: SpecExt) = struct
 
   open Util
   open QCheck
@@ -24,9 +24,10 @@ module Make (Spec: Spec) = struct
 
   let run_par seq_pref cmds1 cmds2 =
     let sut = Spec.init_sut () in
-    let pref_obs = interp_sut_res sut seq_pref in
+    let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in
     let barrier = Atomic.make 2 in
     let main cmds () =
+      Spec.wrap_cmd_seq @@ fun () ->
       Atomic.decr barrier;
       while Atomic.get barrier <> 0 do Domain.cpu_relax() done;
       try Ok (interp_sut_res sut cmds) with exn -> Error exn
@@ -54,17 +55,20 @@ module Make (Spec: Spec) = struct
 
   let agree_prop_par_asym (seq_pref, cmds1, cmds2) =
     let sut = Spec.init_sut () in
-    let pref_obs = interp_sut_res sut seq_pref in
+    let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in
     let wait = Atomic.make 2 in
     let child_dom =
       Domain.spawn (fun () ->
+          Spec.wrap_cmd_seq @@ fun () ->
           Atomic.decr wait;
           while Atomic.get wait <> 0 do Domain.cpu_relax() done;
           try Ok (interp_sut_res sut cmds2) with exn -> Error exn)
     in
-    Atomic.decr wait;
-    while Atomic.get wait <> 0 do Domain.cpu_relax() done;
-    let parent_obs = try Ok (interp_sut_res sut cmds1) with exn -> Error exn in
+    let parent_obs =
+      Spec.wrap_cmd_seq @@ fun () ->
+      Atomic.decr wait;
+      while Atomic.get wait <> 0 do Domain.cpu_relax() done;
+      try Ok (interp_sut_res sut cmds1) with exn -> Error exn in
     let child_obs = Domain.join child_dom in
     let () = Spec.cleanup sut in
     let parent_obs = match parent_obs with Ok v -> v | Error exn -> raise exn in
@@ -125,3 +129,9 @@ module Make (Spec: Spec) = struct
          assume (all_interleavings_ok triple);
          repeat rep_count agree_prop_par_asym triple) (* 25 times each, then 25 * 10 times when shrinking *)
 end
+
+module Make (Spec: Spec) =
+  MakeExt (struct
+    include SpecDefaults
+    include Spec
+  end)

lib/STM_domain.mli

@@ -96,3 +96,6 @@ module Make : functor (Spec : STM.Spec) ->
         interleaving search like {!agree_test_par} and {!neg_agree_test_par}. *)
 
  end
+
+module MakeExt : functor (Spec : STM.SpecExt) ->
+  module type of Make (Spec)

lib/STM_sequential.ml

@@ -1,6 +1,6 @@
 open STM
 
-module Make (Spec: Spec) = struct
+module MakeExt (Spec: SpecExt) = struct
 
   open QCheck
   open Internal.Make(Spec)
@@ -18,7 +18,7 @@ module Make (Spec: Spec) = struct
   let agree_prop cs =
     assume (cmds_ok Spec.init_state cs);
     let sut = Spec.init_sut () in (* reset system's state *)
-    let res = try Ok (check_disagree Spec.init_state sut cs) with exn -> Error exn in
+    let res = try Ok (Spec.wrap_cmd_seq @@ fun () -> check_disagree Spec.init_state sut cs) with exn -> Error exn in
     let ()  = Spec.cleanup sut in
     let res = match res with Ok res -> res | Error exn -> raise exn in
     match res with
@@ -34,3 +34,9 @@ module Make (Spec: Spec) = struct
     Test.make_neg ~name ~count (arb_cmds Spec.init_state) agree_prop
 
   end
+
+module Make (Spec : Spec) =
+  MakeExt (struct
+    include SpecDefaults
+    include Spec
+  end)

lib/STM_sequential.mli

@@ -25,3 +25,6 @@ module Make : functor (Spec : STM.Spec) ->
     (** A negative agreement test (for convenience). Accepts two labeled parameters:
         [count] is the test count and [name] is the printed test name. *)
   end
+
+module MakeExt : functor (Spec : STM.SpecExt) ->
+  module type of Make (Spec)

lib/STM_thread.ml

@@ -1,6 +1,6 @@
 open STM
 
-module Make (Spec: Spec) = struct
+module MakeExt (Spec: SpecExt) = struct
 
   open Util
   open QCheck
@@ -23,10 +23,10 @@ module Make (Spec: Spec) = struct
   let agree_prop_conc (seq_pref,cmds1,cmds2) =
     let sut = Spec.init_sut () in
     let obs1,obs2 = ref (Error ThreadNotFinished), ref (Error ThreadNotFinished) in
-    let pref_obs = interp_sut_res sut seq_pref in
+    let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in
     let wait = ref true in
-    let th1 = Thread.create (fun () -> while !wait do Thread.yield () done; obs1 := try Ok (interp_sut_res sut cmds1) with exn -> Error exn) () in
-    let th2 = Thread.create (fun () -> wait := false; obs2 := try Ok (interp_sut_res sut cmds2) with exn -> Error exn) () in
+    let th1 = Thread.create (fun () -> Spec.wrap_cmd_seq @@ fun () -> while !wait do Thread.yield () done; obs1 := try Ok (interp_sut_res sut cmds1) with exn -> Error exn) () in
+    let th2 = Thread.create (fun () -> Spec.wrap_cmd_seq @@ fun () -> wait := false; obs2 := try Ok (interp_sut_res sut cmds2) with exn -> Error exn) () in
     let ()   = Thread.join th1 in
     let ()   = Thread.join th2 in
     let ()   = Spec.cleanup sut in
@@ -59,3 +59,9 @@ module Make (Spec: Spec) = struct
          assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
          repeat rep_count agree_prop_conc triple) (* 100 times each, then 100 * 15 times when shrinking *)
   end
+
+module Make (Spec: Spec) =
+  MakeExt (struct
+    include SpecDefaults
+    include Spec
+  end)

lib/STM_thread.mli

@@ -27,3 +27,7 @@ module Make : functor (Spec : STM.Spec) ->
 
   end
   [@@alert experimental "This module is experimental: It may fail to trigger concurrency issues that are present."]
+
+module MakeExt : functor (Spec : STM.SpecExt) ->
+  module type of Make (Spec) [@@alert "-experimental"]
+  [@@alert experimental "This module is experimental: It may fail to trigger concurrency issues that are present."]