From 622111305e8d3810b5b39f308ad8e04019d56568 Mon Sep 17 00:00:00 2001
From: Olivier Nicole <olivier@chnik.fr>
Date: Sat, 20 Apr 2024 20:18:11 +0200
Subject: [PATCH 1/2] Specifications can be terser and safer through more type
 trickery

---
 lib/STM.ml              | 131 ++++++++++++++++++++++++++--------------
 lib/STM.mli             |  68 +++++++++++++++------
 lib/STM_domain.ml       |  50 +++++++++++++--
 lib/STM_domain.mli      |  50 ++++++++++++---
 lib/STM_sequential.ml   |  11 +++-
 lib/STM_sequential.mli  |  10 ++-
 lib/STM_thread.ml       |  15 ++++-
 lib/STM_thread.mli      |  12 +++-
 src/atomic/stm_tests.ml |  77 ++++++++++++-----------
 9 files changed, 300 insertions(+), 124 deletions(-)

diff --git a/lib/STM.ml b/lib/STM.ml
index ce25ba7c7..8cfdbab06 100644
--- a/lib/STM.ml
+++ b/lib/STM.ml
@@ -57,33 +57,34 @@ let seq spec =
 
 
 
-type res =
-    Res : 'a ty_show * 'a -> res
+type 'a res = 'a ty_show * 'a
 
-let show_res (Res ((_,show), v)) = show v
+let show_res ((_,show), v) = show v
 
 (** The specification of a state machine. *)
 module type Spec =
 sig
-  type cmd
+  type 'a cmd
   (** The type of commands *)
 
+  type packed_cmd = Pack_cmd : 'a cmd -> packed_cmd
+
   type state
   (** The type of the model's state *)
 
   type sut
   (** The type of the system under test *)
 
-  val arb_cmd : state -> cmd arbitrary
+  val arb_cmd : 'a. state -> packed_cmd arbitrary
   (** A command generator. Accepts a state parameter to enable state-dependent [cmd] generation. *)
 
   val init_state : state
   (** The model's initial state. *)
 
-  val show_cmd : cmd -> string
+  val show_cmd : 'a. 'a cmd -> string
   (** [show_cmd c] returns a string representing the command [c]. *)
 
-  val next_state : cmd -> state -> state
+  val next_state : 'a. 'a cmd -> state -> state
   (** Move the internal state machine to the next state. *)
 
   val init_sut : unit -> sut
@@ -93,15 +94,15 @@ sig
   (** Utility function to clean up the [sut] after each test instance,
       e.g., for closing sockets, files, or resetting global parameters*)
 
-  val precond : cmd -> state -> bool
+  val precond : 'a. 'a cmd -> state -> bool
   (** [precond c s] expresses preconditions for command [c].
       This is useful, e.g., to prevent the shrinker from breaking invariants when minimizing
       counterexamples. *)
 
-  val run : cmd -> sut -> res
+  val run : 'a. 'a cmd -> sut -> 'a res
   (** [run c i] should interpret the command [c] over the system under test (typically side-effecting). *)
 
-  val postcond : cmd -> state -> res -> bool
+  val postcond : 'a. 'a cmd -> state -> 'a -> bool
   (** [postcond c s res] checks whether [res] arising from interpreting the
       command [c] over the system under test with [run] agrees with the
       model's result.
@@ -113,20 +114,31 @@ module Internal =
 struct
   module Make(Spec : Spec) = struct
 
-    let rec gen_cmds arb s fuel =
+    type packed_res = Pack_res : 'a res -> packed_res [@@unboxed]
+
+    type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a res -> cmd_res
+
+    type arb_cmd_of_state = { arb_cmd_of_state : 'r. Spec.state -> 'r Spec.cmd arbitrary }
+
+    let rec gen_cmds
+      :  (Spec.state -> Spec.packed_cmd arbitrary)
+      -> Spec.state
+      -> int
+      -> Spec.packed_cmd list QCheck.Gen.t =
+      fun arb s fuel ->
       Gen.(if fuel = 0
            then return []
            else
-             (arb s).gen >>= fun c ->
+             (arb s).gen >>= fun (Pack_cmd c) ->
              let s' = try Spec.next_state c s with _ -> s in
              (gen_cmds arb s' (fuel-1)) >>= fun cs ->
-             return (c::cs))
+             return (Spec.Pack_cmd c :: cs))
     (** A fueled command list generator.
         Accepts a state parameter to enable state-dependent [cmd] generation. *)
 
     let rec cmds_ok s cs = match cs with
       | [] -> true
-      | c::cs ->
+      | Spec.Pack_cmd c :: cs ->
         Spec.precond c s &&
         let s' = try Spec.next_state c s with _ -> s in
         cmds_ok s' cs
@@ -157,7 +169,7 @@ struct
       | None -> () (* no elem. shrinker provided *)
       | Some shrink -> Shrink.list_elems shrink l yield
 
-    let arb_cmds s =
+    let arb_cmds (s : Spec.state) : Spec.packed_cmd list QCheck.arbitrary =
       let cmds_gen = Gen.sized (gen_cmds Spec.arb_cmd s) in
       let shrinker = shrink_list ?shrink:(Spec.arb_cmd s).shrink in (* pass opt. elem. shrinker *)
       let ac = QCheck.make ~shrink:(Shrink.filter (cmds_ok Spec.init_state) shrinker) cmds_gen in
@@ -170,44 +182,44 @@ struct
 
     let rec interp_agree s sut cs = match cs with
       | [] -> true
-      | c::cs ->
-        let res = Spec.run c sut in
-        let b   = Spec.postcond c s res in
-        let s'  = Spec.next_state c s in
+      | Spec.Pack_cmd  c :: cs ->
+        let _, res = Spec.run c sut in
+        let b = Spec.postcond c s res in
+        let s' = Spec.next_state c s in
         b && interp_agree s' sut cs
 
     let rec check_disagree s sut cs = match cs with
       | [] -> None
-      | c::cs ->
-        let res = Spec.run c sut in
-        let b   = Spec.postcond c s res in
+      | Spec.Pack_cmd c :: cs ->
+        let _, r as res = Spec.run c sut in
+        let b   = Spec.postcond c s r in
         if b
         then
           let s'  = Spec.next_state c s in
           match check_disagree s' sut cs with
           | None -> None
-          | Some rest -> Some ((c,res)::rest)
-        else Some [c,res]
+          | Some rest -> Some (Pack_cmd_res (c,res) :: rest)
+        else Some [ Pack_cmd_res (c,res) ]
 
     (* checks that all interleavings of a cmd triple satisfies all preconditions *)
     let rec all_interleavings_ok pref cs1 cs2 s =
       match pref with
-      | c::pref' ->
+      | Spec.Pack_cmd c :: pref' ->
         Spec.precond c s &&
         let s' = try Spec.next_state c s with _ -> s in
         all_interleavings_ok pref' cs1 cs2 s'
       | [] ->
         match cs1,cs2 with
         | [],[] -> true
-        | [],c2::cs2' ->
+        | [], Spec.Pack_cmd c2 :: cs2' ->
           Spec.precond c2 s &&
           let s' = try Spec.next_state c2 s with _ -> s in
           all_interleavings_ok pref cs1 cs2' s'
-        | c1::cs1',[] ->
+        | Spec.Pack_cmd c1 :: cs1', [] ->
           Spec.precond c1 s &&
           let s' = try Spec.next_state c1 s with _ -> s in
           all_interleavings_ok pref cs1' cs2 s'
-        | c1::cs1',c2::cs2' ->
+        | Spec.Pack_cmd c1 :: cs1', Spec.Pack_cmd c2 :: cs2' ->
           (Spec.precond c1 s &&
            let s' = try Spec.next_state c1 s with _ -> s in
            all_interleavings_ok pref cs1' cs2 s')
@@ -218,19 +230,19 @@ struct
 
     let rec check_obs pref cs1 cs2 s =
       match pref with
-      | (c,res)::pref' ->
+      | Pack_cmd_res (c, (_, res)) :: pref' ->
         let b = Spec.postcond c s res in
         b && check_obs pref' cs1 cs2 (Spec.next_state c s)
       | [] ->
         match cs1,cs2 with
         | [],[] -> true
-        | [],(c2,res2)::cs2' ->
+        | [], Pack_cmd_res (c2, (_, res2)) :: cs2' ->
           let b = Spec.postcond c2 s res2 in
           b && check_obs pref cs1 cs2' (Spec.next_state c2 s)
-        | (c1,res1)::cs1',[] ->
+        | Pack_cmd_res (c1, (_, res1)) :: cs1', [] ->
           let b = Spec.postcond c1 s res1 in
           b && check_obs pref cs1' cs2 (Spec.next_state c1 s)
-        | (c1,res1)::cs1',(c2,res2)::cs2' ->
+        | Pack_cmd_res (c1, (_, res1)) :: cs1', Pack_cmd_res (c2, (_, res2)) :: cs2' ->
           (let b1 = Spec.postcond c1 s res1 in
            b1 && check_obs pref cs1' cs2 (Spec.next_state c1 s))
           ||
@@ -240,19 +252,31 @@ struct
     let gen_cmds_size gen s size_gen = Gen.sized_size size_gen (gen_cmds gen s)
 
     (* Shrinks a single cmd, starting in the given state *)
-    let shrink_cmd arb cmd state =
+    let shrink_cmd
+      :  (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
+      -> Spec.packed_cmd
+      -> Spec.state
+      -> Spec.packed_cmd Iter.t =
+      fun arb cmd state ->
       Option.value (arb state).shrink ~default:Shrink.nil @@ cmd
 
     (* Shrinks cmd list elements, starting in the given state *)
-    let rec shrink_cmd_list_elems arb cs state = match cs with
+    let rec shrink_cmd_list_elems
+      :  (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
+      -> Spec.packed_cmd list
+      -> Spec.state
+      -> Spec.packed_cmd list Iter.t =
+      fun arb cs state -> match cs with
       | [] -> Iter.empty
-      | c::cs ->
+      | Pack_cmd c as packed_c :: cs ->
         if Spec.precond c state
         then
           Iter.(
-            map (fun c -> c::cs) (shrink_cmd arb c state)
+            map (fun c -> c :: cs) (shrink_cmd arb packed_c state)
             <+>
-            map (fun cs -> c::cs) (shrink_cmd_list_elems arb cs Spec.(next_state c state))
+            map
+              (fun cs -> Spec.Pack_cmd c :: cs)
+              (shrink_cmd_list_elems arb cs Spec.(next_state c state))
           )
         else Iter.empty
 
@@ -267,13 +291,13 @@ struct
           Iter.(map (fun p1 -> (seq,p1,p2)) (shrink_cmd_list_elems arb1 p1 state)
                 <+>
                 map (fun p2 -> (seq,p1,p2)) (shrink_cmd_list_elems arb2 p2 state))
-        | c::cs ->
+        | Spec.Pack_cmd c :: cs ->
           (* walk seq prefix (again) to advance state *)
           if Spec.precond c state
           then shrink_par_suffix_elems cs Spec.(next_state c state)
           else Iter.empty
       in
-      match Spec.(arb_cmd init_state).shrink with
+      match (Spec.arb_cmd Spec.init_state).shrink with
       | None -> Iter.empty (* stop early if no cmd shrinker is available *)
       | Some _ ->
         Iter.(shrink_prefix_elems seq Spec.init_state
@@ -281,7 +305,12 @@ struct
               shrink_par_suffix_elems seq Spec.init_state)
 
     (* General shrinker of cmd triples *)
-    let shrink_triple arb0 arb1 arb2 =
+    let shrink_triple
+      :  (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
+      -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
+      -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
+      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) Shrink.t
+      = fun arb0 arb1 arb2 ->
       let open Iter in
       Shrink.filter
         (fun (seq,p1,p2) -> all_interleavings_ok seq p1 p2 Spec.init_state)
@@ -302,20 +331,34 @@ struct
            (* Secondly reduce the cmd data of individual list elements *)
            (shrink_triple_elems arb0 arb1 arb2 triple))
 
-    let arb_triple seq_len par_len arb0 arb1 arb2 =
+    let show_packed_cmd (Spec.Pack_cmd c) =
+      Spec.show_cmd c
+
+    let arb_triple
+      : int -> int
+        -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
+        -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
+        -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
+        -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) arbitrary =
+      fun seq_len par_len arb0 arb1 arb2 ->
       let seq_pref_gen = gen_cmds_size arb0 Spec.init_state (Gen.int_bound seq_len) in
       let shrink_triple = shrink_triple arb0 arb1 arb2 in
       let gen_triple =
         Gen.(seq_pref_gen >>= fun seq_pref ->
              int_range 2 (2*par_len) >>= fun dbl_plen ->
-             let spawn_state = List.fold_left (fun st c -> try Spec.next_state c st with _ -> st) Spec.init_state seq_pref in
+             let spawn_state =
+               List.fold_left
+                 (fun st (Spec.Pack_cmd c) -> try Spec.next_state c st with _ -> st)
+                 Spec.init_state seq_pref
+             in
              let par_len1 = dbl_plen/2 in
              let par_gen1 = gen_cmds_size arb1 spawn_state (return par_len1) in
              let par_gen2 = gen_cmds_size arb2 spawn_state (return (dbl_plen - par_len1)) in
              triple (return seq_pref) par_gen1 par_gen2) in
-      make ~print:(Util.print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple
+      make ~print:(Util.print_triple_vertical show_packed_cmd) ~shrink:shrink_triple gen_triple
 
-    let arb_cmds_triple seq_len par_len = arb_triple seq_len par_len Spec.arb_cmd Spec.arb_cmd Spec.arb_cmd
+    let arb_cmds_triple seq_len par_len =
+      arb_triple seq_len par_len Spec.arb_cmd Spec.arb_cmd Spec.arb_cmd
   end
 end
 
diff --git a/lib/STM.mli b/lib/STM.mli
index f90cfedea..b745e451f 100644
--- a/lib/STM.mli
+++ b/lib/STM.mli
@@ -69,34 +69,35 @@ val array : 'a ty_show -> 'a array ty_show
 val seq : 'a ty_show -> 'a Seq.t ty_show
 (** [seq t] builds a [t] {{!Stdlib.Seq.t}[Seq.t]} type representation *)
 
-type res =
-  Res : 'a ty_show * 'a -> res
+type 'a res = 'a ty_show * 'a
 
-val show_res : res -> string
+val show_res : 'a res -> string
 
 
 (** The specification of a state machine. *)
 module type Spec =
 sig
-  type cmd
+  type 'a cmd
   (** The type of commands *)
 
+  type packed_cmd = Pack_cmd : 'a cmd -> packed_cmd
+
   type state
   (** The type of the model's state *)
 
   type sut
   (** The type of the system under test *)
 
-  val arb_cmd : state -> cmd QCheck.arbitrary
+  val arb_cmd : 'a. state -> packed_cmd QCheck.arbitrary
   (** A command generator. Accepts a state parameter to enable state-dependent {!cmd} generation. *)
 
   val init_state : state
   (** The model's initial state. *)
 
-  val show_cmd : cmd -> string
+  val show_cmd : 'a. 'a cmd -> string
   (** [show_cmd c] returns a string representing the command [c]. *)
 
-  val next_state : cmd -> state -> state
+  val next_state : 'a. 'a cmd -> state -> state
   (** [next_state c s] expresses how interpreting the command [c] moves the
       model's internal state machine from the state [s] to the next state.
       Ideally a [next_state] function is pure, as it is run more than once.  *)
@@ -108,16 +109,16 @@ sig
   (** Utility function to clean up the {!sut} after each test instance,
       e.g., for closing sockets, files, or resetting global parameters*)
 
-  val precond : cmd -> state -> bool
+  val precond : 'a. 'a cmd -> state -> bool
   (** [precond c s] expresses preconditions for command [c] in terms of the model state [s].
       A [precond] function should be pure.
       [precond] is useful, e.g., to prevent the shrinker from breaking invariants when minimizing
       counterexamples. *)
 
-  val run : cmd -> sut -> res
+  val run : 'a. 'a cmd -> sut -> 'a res
   (** [run c i] should interpret the command [c] over the system under test (typically side-effecting). *)
 
-  val postcond : cmd -> state -> res -> bool
+  val postcond : 'a. 'a cmd -> state -> 'a -> bool
   (** [postcond c s res] checks whether [res] arising from interpreting the
       command [c] over the system under test with {!run} agrees with the
       model's result. A [postcond] function should be a pure.
@@ -137,12 +138,18 @@ module Make (Spec : Spec) :
 sig
   (** {3 The resulting test framework derived from a state machine specification} *)
 
-    val cmds_ok : Spec.state -> Spec.cmd list -> bool
+    type packed_res = Pack_res : 'a res -> packed_res [@@unboxed]
+
+    type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a res -> cmd_res
+
+    val show_packed_cmd : Spec.packed_cmd -> string
+
+    val cmds_ok : Spec.state -> Spec.packed_cmd list -> bool
     (** A precondition checker (stops early, thanks to short-circuit Boolean evaluation).
         Accepts the initial state and the command sequence as parameters.
         [cmds_ok] catches and ignores exceptions arising from {!next_state}.  *)
 
-    val arb_cmds : Spec.state -> Spec.cmd list arbitrary
+    val arb_cmds : Spec.state -> Spec.packed_cmd list arbitrary
     (** A generator of command sequences. Accepts the initial state as parameter. *)
 
     val consistency_test : count:int -> name:string -> QCheck.Test.t
@@ -151,45 +158,66 @@ sig
         Accepts two labeled parameters:
         [count] is the test count and [name] is the printed test name. *)
 
-    val interp_agree : Spec.state -> Spec.sut -> Spec.cmd list -> bool
+    val interp_agree : Spec.state -> Spec.sut -> Spec.packed_cmd list -> bool
     (** Checks agreement between the model and the system under test
         (stops early, thanks to short-circuit Boolean evaluation). *)
 
-    val check_disagree : Spec.state -> Spec.sut -> Spec.cmd list -> (Spec.cmd * res) list option
+    val check_disagree
+      : Spec.state -> Spec.sut -> Spec.packed_cmd list -> cmd_res list option
     (** [check_disagree state sut pg] checks that none of the commands present
         in [pg] violated the declared postconditions when [pg] is run in [state].
         Return [None] if none of the commands violate its postcondition, and
         [Some] list corresponding to the prefix of [pg] ending with the [cmd]
         violating its postcondition. *)
 
-    val check_obs : (Spec.cmd * res) list -> (Spec.cmd * res) list -> (Spec.cmd * res) list -> Spec.state -> bool
+    val check_obs : cmd_res list -> cmd_res list -> cmd_res list -> Spec.state -> bool
     (** [check_obs pref cs1 cs2 s] tests whether the observations from the sequential prefix [pref]
         and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *)
 
-    val gen_cmds_size : (Spec.state -> Spec.cmd arbitrary) -> Spec.state -> int Gen.t -> Spec.cmd list Gen.t
+    type arb_cmd_of_state = { arb_cmd_of_state : 'r. Spec.state -> 'r Spec.cmd arbitrary }
+    (** Boilerplate wrapping around a function of type [Spec.state -> 'r
+        Spec.cmd arbitrary] in order to have second-rank polymorphism. *)
+
+    val gen_cmds_size
+      :  Spec.(state -> packed_cmd arbitrary)
+      -> Spec.state
+      -> int Gen.t
+      -> Spec.packed_cmd list Gen.t
     (** [gen_cmds_size arb state gen_int] generates a program of size generated
         by [gen_int] using [arb] to generate [cmd]s according to the current
         state. [state] is the starting state.
         [gen_cmds_size] catches and ignores generation-time exceptions arising
         from {!next_state}. *)
 
-    val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) arbitrary
+    val arb_cmds_triple
+      : int -> int -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) arbitrary
     (** [arb_cmds_triple seq_len par_len] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         [arb_cmds_triple] catches and ignores generation-time exceptions arising
         from {!next_state}. *)
 
-    val all_interleavings_ok : Spec.cmd list -> Spec.cmd list -> Spec.cmd list -> Spec.state -> bool
+    val all_interleavings_ok
+      : Spec.(packed_cmd list -> packed_cmd list -> packed_cmd list -> Spec.state -> bool)
     (** [all_interleavings_ok seq spawn0 spawn1 state] checks that
         preconditions of all the {!cmd}s of [seq], [spawn0], and [spawn1] are satisfied in all the
         possible interleavings and starting with [state].
         [all_interleavings_ok] catches and ignores exceptions arising from
         {!next_state}. *)
 
-    val shrink_triple : (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) Shrink.t
+    val shrink_triple
+      :  Spec.(state -> packed_cmd arbitrary)
+      -> Spec.(state -> packed_cmd arbitrary)
+      -> Spec.(state -> packed_cmd arbitrary)
+      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) Shrink.t
     (** [shrink_triple arb0 arb1 arb2] is a {!QCheck.Shrink.t} for programs (triple of list of [cmd]s) that is specialized for each part of the program. *)
 
-    val arb_triple : int -> int -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) arbitrary
+    val arb_triple
+      :  int
+      -> int
+      -> Spec.(state -> packed_cmd arbitrary)
+      -> Spec.(state -> packed_cmd arbitrary)
+      -> Spec.(state -> packed_cmd arbitrary)
+      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) arbitrary
     (** [arb_triple seq_len par_len arb0 arb1 arb2] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         The three [cmd] components are generated with [arb0], [arb1], and [arb2], respectively.
diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml
index aa1408df0..2e1b6cb69 100644
--- a/lib/STM_domain.ml
+++ b/lib/STM_domain.ml
@@ -7,6 +7,18 @@ module Make (Spec: Spec) = struct
   open Internal.Make(Spec)
     [@alert "-internal"]
 
+  type packed_res = Internal.Make(Spec).packed_res
+                  = Pack_res : 'a STM.res -> packed_res [@@unboxed]
+    [@@alert "-internal"]
+
+  type cmd_res = Internal.Make(Spec).cmd_res
+               = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
+    [@@alert "-internal"]
+
+  type arb_cmd_of_state = Internal.Make(Spec).arb_cmd_of_state
+                        = { arb_cmd_of_state : 'r. Spec.state -> 'r Spec.cmd QCheck.arbitrary }
+    [@@alert "-internal"]
+
   let check_obs = check_obs
   let all_interleavings_ok (seq_pref,cmds1,cmds2) =
     all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state
@@ -14,15 +26,21 @@ module Make (Spec: Spec) = struct
   let arb_triple = arb_triple
   let arb_triple_asym seq_len par_len arb0 arb1 arb2 =
     let arb_triple = arb_triple seq_len par_len arb0 arb1 arb2 in
-    set_print (print_triple_vertical ~center_prefix:false Spec.show_cmd) arb_triple
+    set_print (print_triple_vertical ~center_prefix:false show_packed_cmd) arb_triple
 
   (* operate over arrays to avoid needless allocation underway *)
   let interp_sut_res sut cs =
     let cs_arr = Array.of_list cs in
-    let res_arr = Array.map (fun c -> Domain.cpu_relax(); Spec.run c sut) cs_arr in
-    List.combine cs (Array.to_list res_arr)
+    let res_arr =
+      Array.map
+        (fun (Spec.Pack_cmd c) ->
+          Domain.cpu_relax();
+          Pack_cmd_res (c, Spec.run c sut))
+        cs_arr
+    in
+    Array.to_list res_arr
 
-  let agree_prop_par (seq_pref,cmds1,cmds2) =
+  let run_par seq_pref cmds1 cmds2 =
     let sut = Spec.init_sut () in
     let pref_obs = interp_sut_res sut seq_pref in
     let wait = Atomic.make true in
@@ -31,14 +49,23 @@ module Make (Spec: Spec) = struct
     let obs1 = Domain.join dom1 in
     let obs2 = Domain.join dom2 in
     let ()   = Spec.cleanup sut in
+    pref_obs,obs1,obs2
+
+  let agree_prop_par (seq_pref,cmds1,cmds2) =
+    let pref_obs,obs1,obs2 = run_par seq_pref cmds1 cmds2 in
     let obs1 = match obs1 with Ok v -> v | Error exn -> raise exn in
     let obs2 = match obs2 with Ok v -> v | Error exn -> raise exn in
     check_obs pref_obs obs1 obs2 Spec.init_state
       || Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
          @@ print_triple_vertical ~fig_indent:5 ~res_width:35
-           (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
+           (fun (Pack_cmd_res (c,r)) ->
+             Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
            (pref_obs,obs1,obs2)
 
+  let stress_test_prop_par (seq_pref,cmds1,cmds2) =
+    let _ = run_par seq_pref cmds1 cmds2 in
+    true
+
   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
@@ -59,7 +86,8 @@ module Make (Spec: Spec) = struct
     check_obs pref_obs parent_obs child_obs Spec.init_state
       || Test.fail_reportf "  Results incompatible with linearized model:\n\n%s"
          @@ print_triple_vertical ~fig_indent:5 ~res_width:35 ~center_prefix:false
-           (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
+           (fun (Pack_cmd_res (c,r)) ->
+             Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
            (pref_obs,parent_obs,child_obs)
 
   let agree_test_par ~count ~name =
@@ -72,6 +100,16 @@ module Make (Spec: Spec) = struct
          assume (all_interleavings_ok triple);
          repeat rep_count agree_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
 
+  let stress_test_par ~count ~name =
+    let rep_count = 25 in
+    let seq_len,par_len = 20,12 in
+    let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
+    Test.make ~retries:10 ~max_gen ~count ~name
+      (arb_cmds_triple seq_len par_len)
+      (fun triple ->
+         assume (all_interleavings_ok triple);
+         repeat rep_count stress_test_prop_par triple) (* 25 times each, then 25 * 10 times when shrinking *)
+
   let neg_agree_test_par ~count ~name =
     let rep_count = 25 in
     let seq_len,par_len = 20,12 in
diff --git a/lib/STM_domain.mli b/lib/STM_domain.mli
index 7280b3546..da858bf10 100644
--- a/lib/STM_domain.mli
+++ b/lib/STM_domain.mli
@@ -2,25 +2,43 @@
 
 module Make : functor (Spec : STM.Spec) ->
   sig
-    val check_obs : (Spec.cmd * STM.res) list -> (Spec.cmd * STM.res) list -> (Spec.cmd * STM.res) list -> Spec.state -> bool
+    type packed_res = Pack_res : 'a STM.res -> packed_res [@@unboxed]
+
+    type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
+
+    val check_obs : cmd_res list -> cmd_res list -> cmd_res list -> Spec.state -> bool
     (** [check_obs pref cs1 cs2 s] tests whether the observations from the sequential prefix [pref]
         and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *)
 
-    val all_interleavings_ok : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
+    val all_interleavings_ok
+      : Spec.(packed_cmd list * packed_cmd list * packed_cmd list) -> bool
     (** [all_interleavings_ok (seq,spawn0,spawn1)] checks that
         preconditions of all the {!cmd}s of [seq], [spawn0], and [spawn1] are satisfied in all the
         possible interleavings and starting with {!Spec.init_state}.
         [all_interleavings_ok] catches and ignores exceptions arising from
         {!next_state}. *)
 
-    val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
+    val arb_cmds_triple
+      :  int -> int
+      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) QCheck.arbitrary
     (** [arb_cmds_triple seq_len par_len] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         All [cmds] are generated with {!Spec.arb_cmd}.
         [arb_cmds_triple] catches and ignores generation-time exceptions arising
         from {!Spec.next_state}. *)
 
-    val arb_triple : int -> int -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
+    type arb_cmd_of_state =
+      { arb_cmd_of_state : 'r. Spec.state -> 'r Spec.cmd QCheck.arbitrary }
+    (** Boilerplate wrapping around a function of type [Spec.state -> 'r
+        Spec.cmd arbitrary] in order to have second-rank polymorphism. *)
+
+    val arb_triple
+      :  int
+      -> int
+      -> Spec.(state -> packed_cmd QCheck.arbitrary)
+      -> Spec.(state -> packed_cmd QCheck.arbitrary)
+      -> Spec.(state -> packed_cmd QCheck.arbitrary)
+      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) QCheck.arbitrary
     (** [arb_triple seq_len par_len arb0 arb1 arb2] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         The three {!Spec.cmd} components are generated with [arb0], [arb1], and [arb2], respectively.
@@ -28,7 +46,13 @@ module Make : functor (Spec : STM.Spec) ->
         [arb_triple] catches and ignores generation-time exceptions arising
         from {!Spec.next_state}. *)
 
-    val arb_triple_asym : int -> int -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.state -> Spec.cmd QCheck.arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
+    val arb_triple_asym
+      :  int
+      -> int
+      -> Spec.(state -> packed_cmd QCheck.arbitrary)
+      -> Spec.(state -> packed_cmd QCheck.arbitrary)
+      -> Spec.(state -> packed_cmd QCheck.arbitrary)
+      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) QCheck.arbitrary
     (** [arb_triple_asym seq_len par_len arb0 arb1 arb2] creates a triple [cmd]
         generator like {!arb_triple}. It differs in that the resulting printer
         is asymmetric, printing [arb1]'s result below [arb0]'s result and
@@ -36,11 +60,12 @@ module Make : functor (Spec : STM.Spec) ->
         [arb_triple_asym] catches and ignores generation-time exceptions arising
         from {!Spec.next_state}. *)
 
-    val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM.res) list
+    val interp_sut_res : Spec.sut -> Spec.packed_cmd list -> cmd_res list
     (** [interp_sut_res sut cs] interprets the commands [cs] over the system {!Spec.sut}
         and returns the list of corresponding {!Spec.cmd} and result pairs. *)
 
-    val agree_prop_par : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
+    val agree_prop_par
+      : Spec.(packed_cmd list * packed_cmd list * packed_cmd list) -> bool
     (** Parallel agreement property based on {!Stdlib.Domain}.
         [agree_prop_par (seq_pref, tl1, tl2)] first interprets [seq_pref]
         and then spawns two parallel, symmetric domains interpreting [tl1] and
@@ -49,7 +74,8 @@ module Make : functor (Spec : STM.Spec) ->
         @return [true] if there exists a sequential interleaving of the results
         which agrees with a model interpretation. *)
 
-    val agree_prop_par_asym : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
+    val agree_prop_par_asym
+      : Spec.(packed_cmd list * packed_cmd list * packed_cmd list) -> bool
     (** Asymmetric parallel agreement property based on {!Stdlib.Domain}.
         [agree_prop_par_asym (seq_pref, tl1, tl2)] first interprets [seq_pref],
         and then interprets [tl1] while a spawned domain interprets [tl2]
@@ -63,6 +89,14 @@ module Make : functor (Spec : STM.Spec) ->
         Accepts two labeled parameters:
         [count] is the number of test iterations and [name] is the printed test name. *)
 
+    val stress_test_par : count:int -> name:string -> QCheck.Test.t
+    (** Parallel stress test based on {!Stdlib.Domain} which combines [repeat] and [~retries].
+        Accepts two labeled parameters:
+        [count] is the number of test iterations and [name] is the printed test name.
+        The test fails if an unexpected exception is raised underway. It is
+        intended as a stress test and does not perform an interleaving search
+        like {!agree_test_par} and {!neg_agree_test_par}. *)
+
     val neg_agree_test_par : count:int -> name:string -> QCheck.Test.t
     (** A negative parallel agreement test (for convenience). Accepts two labeled parameters:
         [count] is the number of test iterations and [name] is the printed test name. *)
diff --git a/lib/STM_sequential.ml b/lib/STM_sequential.ml
index c3d240a64..31c1d2d9e 100644
--- a/lib/STM_sequential.ml
+++ b/lib/STM_sequential.ml
@@ -6,13 +6,22 @@ module Make (Spec: Spec) = struct
   open Internal.Make(Spec)
     [@alert "-internal"]
 
+  type packed_res = Internal.Make(Spec).packed_res
+                  = Pack_res : 'a STM.res -> packed_res [@@unboxed]
+    [@@alert "-internal"]
+
+  type cmd_res = Internal.Make(Spec).cmd_res
+               = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
+    [@@alert "-internal"]
+
   (* re-export some functions *)
   let cmds_ok        = cmds_ok
   let arb_cmds       = arb_cmds
 
   let print_seq_trace trace =
     List.fold_left
-      (fun acc (c,r) -> Printf.sprintf "%s\n   %s : %s" acc (Spec.show_cmd c) (show_res r))
+      (fun acc (Pack_cmd_res (c,r)) ->
+        Printf.sprintf "%s\n   %s : %s" acc (Spec.show_cmd c) (show_res r))
       "" trace
 
   let agree_prop cs =
diff --git a/lib/STM_sequential.mli b/lib/STM_sequential.mli
index c08baacfb..6b57d3068 100644
--- a/lib/STM_sequential.mli
+++ b/lib/STM_sequential.mli
@@ -2,17 +2,21 @@
 
 module Make : functor (Spec : STM.Spec) ->
   sig
-    val cmds_ok : Spec.state -> Spec.cmd list -> bool
+    type packed_res = Pack_res : 'a STM.res -> packed_res [@@unboxed]
+
+    type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
+
+    val cmds_ok : Spec.state -> Spec.packed_cmd list -> bool
     (** A precondition checker (stops early, thanks to short-circuit Boolean evaluation).
         Accepts the initial state and the command sequence as parameters.
         [cmds_ok] catches and ignores exceptions arising from {!next_state}.  *)
 
-    val arb_cmds : Spec.state -> Spec.cmd list QCheck.arbitrary
+    val arb_cmds : Spec.state -> Spec.packed_cmd list QCheck.arbitrary
     (** A generator of {!Spec.cmd} sequences. Accepts the initial state as a parameter.
         [arb_cmds] catches and ignores generation-time exceptions arising from
         {!Spec.next_state}. *)
 
-    val agree_prop : Spec.cmd list -> bool
+    val agree_prop : Spec.packed_cmd list -> bool
     (** The agreement property: the command sequence [cs] yields the same observations
         when interpreted from the model's initial state and the [sut]'s initial state.
         Cleans up after itself by calling {!Spec.cleanup}. *)
diff --git a/lib/STM_thread.ml b/lib/STM_thread.ml
index 89447ff42..9ec87145c 100644
--- a/lib/STM_thread.ml
+++ b/lib/STM_thread.ml
@@ -7,6 +7,14 @@ module Make (Spec: Spec) = struct
   open Internal.Make(Spec)
     [@alert "-internal"]
 
+  type packed_res = Internal.Make(Spec).packed_res
+                  = Pack_res : 'a STM.res -> packed_res [@@unboxed]
+    [@@alert "-internal"]
+
+  type cmd_res = Internal.Make(Spec).cmd_res
+               = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
+    [@@alert "-internal"]
+
   exception ThreadNotFinished
 
   let arb_cmds_triple = arb_cmds_triple
@@ -14,10 +22,10 @@ module Make (Spec: Spec) = struct
   (* [interp_sut_res] specialized for [Threads] *)
   let rec interp_sut_res sut cs = match cs with
     | [] -> []
-    | c::cs ->
+    | Spec.Pack_cmd c :: cs ->
        Thread.yield ();
        let res = Spec.run c sut in
-       (c,res)::interp_sut_res sut cs
+       Pack_cmd_res (c,res) :: interp_sut_res sut cs
 
   (* Concurrent agreement property based on [Threads] *)
   let agree_prop_conc (seq_pref,cmds1,cmds2) =
@@ -35,7 +43,8 @@ module Make (Spec: Spec) = struct
     check_obs pref_obs obs1 obs2 Spec.init_state
       || Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
          @@ print_triple_vertical ~fig_indent:5 ~res_width:35
-           (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
+           (fun (Pack_cmd_res (c,r)) ->
+             Printf.sprintf "%s : %s" (Spec.show_cmd c) (show_res r))
            (pref_obs,obs1,obs2)
 
   let agree_test_conc ~count ~name =
diff --git a/lib/STM_thread.mli b/lib/STM_thread.mli
index 50d50629e..43a826140 100644
--- a/lib/STM_thread.mli
+++ b/lib/STM_thread.mli
@@ -2,20 +2,26 @@
 
 module Make : functor (Spec : STM.Spec) ->
   sig
+    type packed_res = Pack_res : 'a STM.res -> packed_res [@@unboxed]
+
+    type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
+
     exception ThreadNotFinished
 
-    val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
+    val arb_cmds_triple
+    : int -> int -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) QCheck.arbitrary
     (** [arb_cmds_triple seq_len conc_len] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [conc_len] concurrent commands each.
         All [cmds] are generated with {!Spec.arb_cmd}.
         [arb_cmds_triple] catches and ignores generation-time exceptions arising
         from {!Spec.next_state}. *)
 
-    val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * STM.res) list
+    val interp_sut_res : Spec.sut -> Spec.packed_cmd list -> cmd_res list
     (** [interp_sut_res sut cs] interprets the commands [cs] over the system [sut]
         and returns the list of corresponding {!Spec.cmd} and result pairs. *)
 
-    val agree_prop_conc : Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool
+    val agree_prop_conc
+      : Spec.(packed_cmd list * packed_cmd list * packed_cmd list) -> bool
     (** Concurrent agreement property based on {!Thread} *)
 
     val agree_test_conc : count:int -> name:string -> QCheck.Test.t
diff --git a/src/atomic/stm_tests.ml b/src/atomic/stm_tests.ml
index 5a1c9c572..63b5e4ed7 100644
--- a/src/atomic/stm_tests.ml
+++ b/src/atomic/stm_tests.ml
@@ -5,16 +5,16 @@ open STM
 
 module CConf =
 struct
-  type cmd =
-    | Get
-    | Set of int
-    | Exchange of int
-    | Compare_and_set of int * int
-    | Fetch_and_add of int
-    | Incr
-    | Decr
+  type _ cmd =
+    | Get : int cmd
+    | Set : int -> unit cmd
+    | Exchange : int -> int cmd
+    | Compare_and_set : int * int -> bool cmd
+    | Fetch_and_add : int -> int cmd
+    | Incr : unit cmd
+    | Decr : unit cmd
 
-  let pp_cmd par fmt x =
+  let pp_cmd : type r. bool -> Format.formatter -> r cmd -> unit = fun par fmt x ->
     let open Util.Pp in
     match x with
     | Get -> cst0 "Get" fmt
@@ -25,29 +25,35 @@ struct
     | Incr -> cst0 "Incr" fmt
     | Decr -> cst0 "Decr" fmt
 
-  let show_cmd = Util.Pp.to_show pp_cmd
+  let show_cmd : type r. r cmd -> string = fun cmd ->
+    Util.Pp.to_show pp_cmd cmd
 
   type state = int
   type sut = int Atomic.t
 
+  type packed_cmd = Pack_cmd : 'r cmd -> packed_cmd
+
+  let show_packed_cmd (Pack_cmd c) = show_cmd c
+
   let arb_cmd s =
     let int_gen = Gen.nat in
-    QCheck.make ~print:show_cmd
+    QCheck.make ~print:show_packed_cmd
       (Gen.oneof
-         [Gen.return Get;
-	  Gen.map (fun i -> Set i) int_gen;
-	  Gen.map (fun i -> Exchange i) int_gen;
-	  Gen.map (fun i -> Fetch_and_add i) int_gen;
-	  Gen.map2 (fun seen v -> Compare_and_set (seen,v)) (Gen.oneof [Gen.return s; int_gen]) int_gen;
-          Gen.return Incr;
-	  Gen.return Decr;
+         [Gen.return (Pack_cmd Get);
+	  Gen.map (fun i -> Pack_cmd (Set i)) int_gen;
+	  Gen.map (fun i -> Pack_cmd (Exchange i)) int_gen;
+	  Gen.map (fun i -> Pack_cmd (Fetch_and_add i)) int_gen;
+	  Gen.map2 (fun seen v -> Pack_cmd (Compare_and_set (seen,v))) (Gen.oneof [Gen.return s; int_gen]) int_gen;
+          Gen.return (Pack_cmd Incr);
+	  Gen.return (Pack_cmd Decr);
          ])
 
   let init_state  = 0
   let init_sut () = Atomic.make 0
   let cleanup _   = ()
 
-  let next_state c s = match c with
+  let next_state : type r. r cmd -> state -> state = fun c s ->
+    match c with
     | Get                      -> s
     | Set i                    -> i (*if i<>1213 then i else s*) (* an artificial fault *)
     | Exchange i               -> i
@@ -58,26 +64,25 @@ struct
 
   let precond _ _ = true
 
-  let run c r =
+  let run : type r. r cmd -> sut -> r res  = fun c r ->
     match c with
-    | Get                      -> Res (int,  Atomic.get r)
-    | Set i                    -> Res (unit, Atomic.set r i)
-    | Exchange i               -> Res (int,  Atomic.exchange r i)
-    | Fetch_and_add i          -> Res (int,  Atomic.fetch_and_add r i)
-    | Compare_and_set (seen,v) -> Res (bool, Atomic.compare_and_set r seen v)
-    | Incr                     -> Res (unit, Atomic.incr r)
-    | Decr                     -> Res (unit, Atomic.decr r)
+    | Get                      -> int,  Atomic.get r
+    | Set i                    -> unit, Atomic.set r i
+    | Exchange i               -> int,  Atomic.exchange r i
+    | Fetch_and_add i          -> int,  Atomic.fetch_and_add r i
+    | Compare_and_set (seen,v) -> bool, Atomic.compare_and_set r seen v
+    | Incr                     -> unit, Atomic.incr r
+    | Decr                     -> unit, Atomic.decr r
 
-  let postcond c (s : state) res =
+  let postcond : type r. r cmd -> state -> r -> bool = fun c s res ->
     match c,res with
-    | Get,             Res ((Int,_),v)  -> v = s (*&& v<>42*) (*an injected bug*)
-    | Set _,           Res ((Unit,_),_) -> true
-    | Exchange _,      Res ((Int,_),v)  -> v = s
-    | Fetch_and_add _, Res ((Int,_),v)  -> v = s
-    | Compare_and_set (seen,_), Res ((Bool,_),b) -> b = (s=seen)
-    | Incr,            Res ((Unit,_),_) -> true
-    | Decr,            Res ((Unit,_),_) -> true
-    | _,_ -> false
+    | Get,             v  -> v = s (*&& v<>42*) (*an injected bug*)
+    | Set _,           _  -> true
+    | Exchange _,      v  -> v = s
+    | Fetch_and_add _, v  -> v = s
+    | Compare_and_set (seen,_), b -> b = (s=seen)
+    | Incr,            () -> true
+    | Decr,            () -> true
 end
 
 module AT_seq = STM_sequential.Make(CConf)

From 66a5d5e21b122eecec9fb3ab66b4eb442adcfff8 Mon Sep 17 00:00:00 2001
From: Olivier Nicole <olivier@chnik.fr>
Date: Fri, 26 Apr 2024 17:14:46 +0200
Subject: [PATCH 2/2] Hide existential type behind nicer functions

---
 lib/STM.ml              | 111 ++++++++++++++++++++++++++--------------
 lib/STM.mli             |  75 +++++++++++++++++----------
 lib/STM_domain.ml       |   6 +--
 lib/STM_domain.mli      |  28 +++++-----
 lib/STM_sequential.ml   |   4 --
 lib/STM_sequential.mli  |   8 ++-
 lib/STM_thread.ml       |   6 +--
 lib/STM_thread.mli      |   8 ++-
 src/atomic/stm_tests.ml |  26 ++++++----
 9 files changed, 157 insertions(+), 115 deletions(-)

diff --git a/lib/STM.ml b/lib/STM.ml
index 8cfdbab06..bc6b0b9f4 100644
--- a/lib/STM.ml
+++ b/lib/STM.ml
@@ -61,13 +61,49 @@ type 'a res = 'a ty_show * 'a
 
 let show_res ((_,show), v) = show v
 
+module Cmd (C : sig
+  type 'r t
+  val show : 'r t -> string
+end) : sig
+  type any = Pack_cmd : 'r C.t -> any
+
+  val print : any -> string
+
+  module Gen : sig
+    val map : 'r C.t QCheck.Gen.t -> any QCheck.Gen.t
+  end
+
+  module Arbitrary : sig
+    val map : 'r C.t QCheck.arbitrary -> any QCheck.arbitrary
+  end
+end = struct
+  type any = Pack_cmd : 'r C.t -> any
+
+  let print (Pack_cmd c) = C.show c
+
+  module Gen = struct
+    let map cmd = QCheck.Gen.map (fun c -> Pack_cmd c) cmd
+  end
+
+  module Arbitrary = struct
+    let map cmd = QCheck.map (fun c -> Pack_cmd c) cmd
+  end
+end
+
 (** The specification of a state machine. *)
 module type Spec =
 sig
   type 'a cmd
   (** The type of commands *)
 
-  type packed_cmd = Pack_cmd : 'a cmd -> packed_cmd
+  val show_cmd : 'a cmd -> string
+  (** [show_cmd c] returns a string representing the command [c]. *)
+
+  module Cmd
+    : module type of Cmd (struct
+        type 'r t = 'r cmd
+        let show = show_cmd
+      end)
 
   type state
   (** The type of the model's state *)
@@ -75,16 +111,13 @@ sig
   type sut
   (** The type of the system under test *)
 
-  val arb_cmd : 'a. state -> packed_cmd arbitrary
+  val arb_cmd : state -> Cmd.any arbitrary
   (** A command generator. Accepts a state parameter to enable state-dependent [cmd] generation. *)
 
   val init_state : state
   (** The model's initial state. *)
 
-  val show_cmd : 'a. 'a cmd -> string
-  (** [show_cmd c] returns a string representing the command [c]. *)
-
-  val next_state : 'a. 'a cmd -> state -> state
+  val next_state : 'a cmd -> state -> state
   (** Move the internal state machine to the next state. *)
 
   val init_sut : unit -> sut
@@ -94,15 +127,15 @@ sig
   (** Utility function to clean up the [sut] after each test instance,
       e.g., for closing sockets, files, or resetting global parameters*)
 
-  val precond : 'a. 'a cmd -> state -> bool
+  val precond : 'a cmd -> state -> bool
   (** [precond c s] expresses preconditions for command [c].
       This is useful, e.g., to prevent the shrinker from breaking invariants when minimizing
       counterexamples. *)
 
-  val run : 'a. 'a cmd -> sut -> 'a res
+  val run : 'a cmd -> sut -> 'a res
   (** [run c i] should interpret the command [c] over the system under test (typically side-effecting). *)
 
-  val postcond : 'a. 'a cmd -> state -> 'a -> bool
+  val postcond : 'a cmd -> state -> 'a -> bool
   (** [postcond c s res] checks whether [res] arising from interpreting the
       command [c] over the system under test with [run] agrees with the
       model's result.
@@ -114,17 +147,17 @@ module Internal =
 struct
   module Make(Spec : Spec) = struct
 
-    type packed_res = Pack_res : 'a res -> packed_res [@@unboxed]
+    module Cmd = Spec.Cmd
 
     type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a res -> cmd_res
 
     type arb_cmd_of_state = { arb_cmd_of_state : 'r. Spec.state -> 'r Spec.cmd arbitrary }
 
     let rec gen_cmds
-      :  (Spec.state -> Spec.packed_cmd arbitrary)
+      :  (Spec.state -> Cmd.any arbitrary)
       -> Spec.state
       -> int
-      -> Spec.packed_cmd list QCheck.Gen.t =
+      -> Cmd.any list QCheck.Gen.t =
       fun arb s fuel ->
       Gen.(if fuel = 0
            then return []
@@ -132,13 +165,13 @@ struct
              (arb s).gen >>= fun (Pack_cmd c) ->
              let s' = try Spec.next_state c s with _ -> s in
              (gen_cmds arb s' (fuel-1)) >>= fun cs ->
-             return (Spec.Pack_cmd c :: cs))
+             return (Cmd.Pack_cmd c :: cs))
     (** A fueled command list generator.
         Accepts a state parameter to enable state-dependent [cmd] generation. *)
 
     let rec cmds_ok s cs = match cs with
       | [] -> true
-      | Spec.Pack_cmd c :: cs ->
+      | Cmd.Pack_cmd c :: cs ->
         Spec.precond c s &&
         let s' = try Spec.next_state c s with _ -> s in
         cmds_ok s' cs
@@ -169,7 +202,7 @@ struct
       | None -> () (* no elem. shrinker provided *)
       | Some shrink -> Shrink.list_elems shrink l yield
 
-    let arb_cmds (s : Spec.state) : Spec.packed_cmd list QCheck.arbitrary =
+    let arb_cmds (s : Spec.state) : Cmd.any list QCheck.arbitrary =
       let cmds_gen = Gen.sized (gen_cmds Spec.arb_cmd s) in
       let shrinker = shrink_list ?shrink:(Spec.arb_cmd s).shrink in (* pass opt. elem. shrinker *)
       let ac = QCheck.make ~shrink:(Shrink.filter (cmds_ok Spec.init_state) shrinker) cmds_gen in
@@ -182,7 +215,7 @@ struct
 
     let rec interp_agree s sut cs = match cs with
       | [] -> true
-      | Spec.Pack_cmd  c :: cs ->
+      | Cmd.Pack_cmd  c :: cs ->
         let _, res = Spec.run c sut in
         let b = Spec.postcond c s res in
         let s' = Spec.next_state c s in
@@ -190,7 +223,7 @@ struct
 
     let rec check_disagree s sut cs = match cs with
       | [] -> None
-      | Spec.Pack_cmd c :: cs ->
+      | Cmd.Pack_cmd c :: cs ->
         let _, r as res = Spec.run c sut in
         let b   = Spec.postcond c s r in
         if b
@@ -204,22 +237,22 @@ struct
     (* checks that all interleavings of a cmd triple satisfies all preconditions *)
     let rec all_interleavings_ok pref cs1 cs2 s =
       match pref with
-      | Spec.Pack_cmd c :: pref' ->
+      | Cmd.Pack_cmd c :: pref' ->
         Spec.precond c s &&
         let s' = try Spec.next_state c s with _ -> s in
         all_interleavings_ok pref' cs1 cs2 s'
       | [] ->
         match cs1,cs2 with
         | [],[] -> true
-        | [], Spec.Pack_cmd c2 :: cs2' ->
+        | [], Cmd.Pack_cmd c2 :: cs2' ->
           Spec.precond c2 s &&
           let s' = try Spec.next_state c2 s with _ -> s in
           all_interleavings_ok pref cs1 cs2' s'
-        | Spec.Pack_cmd c1 :: cs1', [] ->
+        | Cmd.Pack_cmd c1 :: cs1', [] ->
           Spec.precond c1 s &&
           let s' = try Spec.next_state c1 s with _ -> s in
           all_interleavings_ok pref cs1' cs2 s'
-        | Spec.Pack_cmd c1 :: cs1', Spec.Pack_cmd c2 :: cs2' ->
+        | Cmd.Pack_cmd c1 :: cs1', Cmd.Pack_cmd c2 :: cs2' ->
           (Spec.precond c1 s &&
            let s' = try Spec.next_state c1 s with _ -> s in
            all_interleavings_ok pref cs1' cs2 s')
@@ -253,19 +286,19 @@ struct
 
     (* Shrinks a single cmd, starting in the given state *)
     let shrink_cmd
-      :  (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
-      -> Spec.packed_cmd
+      :  (Spec.state -> Cmd.any QCheck.arbitrary)
+      -> Cmd.any
       -> Spec.state
-      -> Spec.packed_cmd Iter.t =
+      -> Cmd.any Iter.t =
       fun arb cmd state ->
       Option.value (arb state).shrink ~default:Shrink.nil @@ cmd
 
     (* Shrinks cmd list elements, starting in the given state *)
     let rec shrink_cmd_list_elems
-      :  (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
-      -> Spec.packed_cmd list
+      :  (Spec.state -> Cmd.any QCheck.arbitrary)
+      -> Cmd.any list
       -> Spec.state
-      -> Spec.packed_cmd list Iter.t =
+      -> Cmd.any list Iter.t =
       fun arb cs state -> match cs with
       | [] -> Iter.empty
       | Pack_cmd c as packed_c :: cs ->
@@ -275,7 +308,7 @@ struct
             map (fun c -> c :: cs) (shrink_cmd arb packed_c state)
             <+>
             map
-              (fun cs -> Spec.Pack_cmd c :: cs)
+              (fun cs -> Cmd.Pack_cmd c :: cs)
               (shrink_cmd_list_elems arb cs Spec.(next_state c state))
           )
         else Iter.empty
@@ -291,7 +324,7 @@ struct
           Iter.(map (fun p1 -> (seq,p1,p2)) (shrink_cmd_list_elems arb1 p1 state)
                 <+>
                 map (fun p2 -> (seq,p1,p2)) (shrink_cmd_list_elems arb2 p2 state))
-        | Spec.Pack_cmd c :: cs ->
+        | Cmd.Pack_cmd c :: cs ->
           (* walk seq prefix (again) to advance state *)
           if Spec.precond c state
           then shrink_par_suffix_elems cs Spec.(next_state c state)
@@ -306,10 +339,10 @@ struct
 
     (* General shrinker of cmd triples *)
     let shrink_triple
-      :  (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
-      -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
-      -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
-      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) Shrink.t
+      :  (Spec.state -> Cmd.any QCheck.arbitrary)
+      -> (Spec.state -> Cmd.any QCheck.arbitrary)
+      -> (Spec.state -> Cmd.any QCheck.arbitrary)
+      -> (Cmd.any list * Cmd.any list * Cmd.any list) Shrink.t
       = fun arb0 arb1 arb2 ->
       let open Iter in
       Shrink.filter
@@ -331,15 +364,15 @@ struct
            (* Secondly reduce the cmd data of individual list elements *)
            (shrink_triple_elems arb0 arb1 arb2 triple))
 
-    let show_packed_cmd (Spec.Pack_cmd c) =
+    let show_packed_cmd (Cmd.Pack_cmd c) =
       Spec.show_cmd c
 
     let arb_triple
       : int -> int
-        -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
-        -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
-        -> (Spec.state -> Spec.packed_cmd QCheck.arbitrary)
-        -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) arbitrary =
+        -> (Spec.state -> Cmd.any QCheck.arbitrary)
+        -> (Spec.state -> Cmd.any QCheck.arbitrary)
+        -> (Spec.state -> Cmd.any QCheck.arbitrary)
+        -> (Cmd.any list * Cmd.any list * Cmd.any list) arbitrary =
       fun seq_len par_len arb0 arb1 arb2 ->
       let seq_pref_gen = gen_cmds_size arb0 Spec.init_state (Gen.int_bound seq_len) in
       let shrink_triple = shrink_triple arb0 arb1 arb2 in
@@ -348,7 +381,7 @@ struct
              int_range 2 (2*par_len) >>= fun dbl_plen ->
              let spawn_state =
                List.fold_left
-                 (fun st (Spec.Pack_cmd c) -> try Spec.next_state c st with _ -> st)
+                 (fun st (Cmd.Pack_cmd c) -> try Spec.next_state c st with _ -> st)
                  Spec.init_state seq_pref
              in
              let par_len1 = dbl_plen/2 in
diff --git a/lib/STM.mli b/lib/STM.mli
index b745e451f..0ad297edf 100644
--- a/lib/STM.mli
+++ b/lib/STM.mli
@@ -74,13 +74,37 @@ type 'a res = 'a ty_show * 'a
 val show_res : 'a res -> string
 
 
+module Cmd (C : sig
+  type 'r t
+  val show : 'r t -> string
+end) : sig
+  type any = Pack_cmd : 'r C.t -> any
+
+  val print : any -> string
+
+  module Gen : sig
+    val map : 'r C.t QCheck.Gen.t -> any QCheck.Gen.t
+  end
+
+  module Arbitrary : sig
+    val map : 'r C.t QCheck.arbitrary -> any QCheck.arbitrary
+  end
+end
+
 (** The specification of a state machine. *)
 module type Spec =
 sig
   type 'a cmd
   (** The type of commands *)
 
-  type packed_cmd = Pack_cmd : 'a cmd -> packed_cmd
+  val show_cmd : 'a cmd -> string
+  (** [show_cmd c] returns a string representing the command [c]. *)
+
+  module Cmd
+    : module type of Cmd (struct
+        type 'r t = 'r cmd
+        let show = show_cmd
+      end)
 
   type state
   (** The type of the model's state *)
@@ -88,16 +112,13 @@ sig
   type sut
   (** The type of the system under test *)
 
-  val arb_cmd : 'a. state -> packed_cmd QCheck.arbitrary
+  val arb_cmd : state -> Cmd.any QCheck.arbitrary
   (** A command generator. Accepts a state parameter to enable state-dependent {!cmd} generation. *)
 
   val init_state : state
   (** The model's initial state. *)
 
-  val show_cmd : 'a. 'a cmd -> string
-  (** [show_cmd c] returns a string representing the command [c]. *)
-
-  val next_state : 'a. 'a cmd -> state -> state
+  val next_state : 'a cmd -> state -> state
   (** [next_state c s] expresses how interpreting the command [c] moves the
       model's internal state machine from the state [s] to the next state.
       Ideally a [next_state] function is pure, as it is run more than once.  *)
@@ -109,16 +130,16 @@ sig
   (** Utility function to clean up the {!sut} after each test instance,
       e.g., for closing sockets, files, or resetting global parameters*)
 
-  val precond : 'a. 'a cmd -> state -> bool
+  val precond : 'a cmd -> state -> bool
   (** [precond c s] expresses preconditions for command [c] in terms of the model state [s].
       A [precond] function should be pure.
       [precond] is useful, e.g., to prevent the shrinker from breaking invariants when minimizing
       counterexamples. *)
 
-  val run : 'a. 'a cmd -> sut -> 'a res
+  val run : 'a cmd -> sut -> 'a res
   (** [run c i] should interpret the command [c] over the system under test (typically side-effecting). *)
 
-  val postcond : 'a. 'a cmd -> state -> 'a -> bool
+  val postcond : 'a cmd -> state -> 'a -> bool
   (** [postcond c s res] checks whether [res] arising from interpreting the
       command [c] over the system under test with {!run} agrees with the
       model's result. A [postcond] function should be a pure.
@@ -138,18 +159,16 @@ module Make (Spec : Spec) :
 sig
   (** {3 The resulting test framework derived from a state machine specification} *)
 
-    type packed_res = Pack_res : 'a res -> packed_res [@@unboxed]
-
     type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a res -> cmd_res
 
-    val show_packed_cmd : Spec.packed_cmd -> string
+    val show_packed_cmd : Spec.Cmd.any -> string
 
-    val cmds_ok : Spec.state -> Spec.packed_cmd list -> bool
+    val cmds_ok : Spec.state -> Spec.Cmd.any list -> bool
     (** A precondition checker (stops early, thanks to short-circuit Boolean evaluation).
         Accepts the initial state and the command sequence as parameters.
         [cmds_ok] catches and ignores exceptions arising from {!next_state}.  *)
 
-    val arb_cmds : Spec.state -> Spec.packed_cmd list arbitrary
+    val arb_cmds : Spec.state -> Spec.Cmd.any list arbitrary
     (** A generator of command sequences. Accepts the initial state as parameter. *)
 
     val consistency_test : count:int -> name:string -> QCheck.Test.t
@@ -158,12 +177,12 @@ sig
         Accepts two labeled parameters:
         [count] is the test count and [name] is the printed test name. *)
 
-    val interp_agree : Spec.state -> Spec.sut -> Spec.packed_cmd list -> bool
+    val interp_agree : Spec.state -> Spec.sut -> Spec.Cmd.any list -> bool
     (** Checks agreement between the model and the system under test
         (stops early, thanks to short-circuit Boolean evaluation). *)
 
     val check_disagree
-      : Spec.state -> Spec.sut -> Spec.packed_cmd list -> cmd_res list option
+      : Spec.state -> Spec.sut -> Spec.Cmd.any list -> cmd_res list option
     (** [check_disagree state sut pg] checks that none of the commands present
         in [pg] violated the declared postconditions when [pg] is run in [state].
         Return [None] if none of the commands violate its postcondition, and
@@ -179,10 +198,10 @@ sig
         Spec.cmd arbitrary] in order to have second-rank polymorphism. *)
 
     val gen_cmds_size
-      :  Spec.(state -> packed_cmd arbitrary)
+      :  (Spec.state -> Spec.Cmd.any arbitrary)
       -> Spec.state
       -> int Gen.t
-      -> Spec.packed_cmd list Gen.t
+      -> Spec.Cmd.any list Gen.t
     (** [gen_cmds_size arb state gen_int] generates a program of size generated
         by [gen_int] using [arb] to generate [cmd]s according to the current
         state. [state] is the starting state.
@@ -190,14 +209,14 @@ sig
         from {!next_state}. *)
 
     val arb_cmds_triple
-      : int -> int -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) arbitrary
+      : int -> int -> (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) arbitrary
     (** [arb_cmds_triple seq_len par_len] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         [arb_cmds_triple] catches and ignores generation-time exceptions arising
         from {!next_state}. *)
 
     val all_interleavings_ok
-      : Spec.(packed_cmd list -> packed_cmd list -> packed_cmd list -> Spec.state -> bool)
+      : Spec.Cmd.any list -> Spec.Cmd.any list -> Spec.Cmd.any list -> Spec.state -> bool
     (** [all_interleavings_ok seq spawn0 spawn1 state] checks that
         preconditions of all the {!cmd}s of [seq], [spawn0], and [spawn1] are satisfied in all the
         possible interleavings and starting with [state].
@@ -205,19 +224,19 @@ sig
         {!next_state}. *)
 
     val shrink_triple
-      :  Spec.(state -> packed_cmd arbitrary)
-      -> Spec.(state -> packed_cmd arbitrary)
-      -> Spec.(state -> packed_cmd arbitrary)
-      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) Shrink.t
+      :  (Spec.state -> Spec.Cmd.any arbitrary)
+      -> (Spec.state -> Spec.Cmd.any arbitrary)
+      -> (Spec.state -> Spec.Cmd.any arbitrary)
+      -> (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) Shrink.t
     (** [shrink_triple arb0 arb1 arb2] is a {!QCheck.Shrink.t} for programs (triple of list of [cmd]s) that is specialized for each part of the program. *)
 
     val arb_triple
       :  int
       -> int
-      -> Spec.(state -> packed_cmd arbitrary)
-      -> Spec.(state -> packed_cmd arbitrary)
-      -> Spec.(state -> packed_cmd arbitrary)
-      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) arbitrary
+      -> (Spec.state -> Spec.Cmd.any arbitrary)
+      -> (Spec.state -> Spec.Cmd.any arbitrary)
+      -> (Spec.state -> Spec.Cmd.any arbitrary)
+      -> (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) arbitrary
     (** [arb_triple seq_len par_len arb0 arb1 arb2] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         The three [cmd] components are generated with [arb0], [arb1], and [arb2], respectively.
diff --git a/lib/STM_domain.ml b/lib/STM_domain.ml
index 2e1b6cb69..135080841 100644
--- a/lib/STM_domain.ml
+++ b/lib/STM_domain.ml
@@ -7,9 +7,7 @@ module Make (Spec: Spec) = struct
   open Internal.Make(Spec)
     [@alert "-internal"]
 
-  type packed_res = Internal.Make(Spec).packed_res
-                  = Pack_res : 'a STM.res -> packed_res [@@unboxed]
-    [@@alert "-internal"]
+  module Cmd = Spec.Cmd
 
   type cmd_res = Internal.Make(Spec).cmd_res
                = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
@@ -33,7 +31,7 @@ module Make (Spec: Spec) = struct
     let cs_arr = Array.of_list cs in
     let res_arr =
       Array.map
-        (fun (Spec.Pack_cmd c) ->
+        (fun (Cmd.Pack_cmd c) ->
           Domain.cpu_relax();
           Pack_cmd_res (c, Spec.run c sut))
         cs_arr
diff --git a/lib/STM_domain.mli b/lib/STM_domain.mli
index da858bf10..ca5ebb011 100644
--- a/lib/STM_domain.mli
+++ b/lib/STM_domain.mli
@@ -2,8 +2,6 @@
 
 module Make : functor (Spec : STM.Spec) ->
   sig
-    type packed_res = Pack_res : 'a STM.res -> packed_res [@@unboxed]
-
     type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
 
     val check_obs : cmd_res list -> cmd_res list -> cmd_res list -> Spec.state -> bool
@@ -11,7 +9,7 @@ module Make : functor (Spec : STM.Spec) ->
         and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *)
 
     val all_interleavings_ok
-      : Spec.(packed_cmd list * packed_cmd list * packed_cmd list) -> bool
+      : (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) -> bool
     (** [all_interleavings_ok (seq,spawn0,spawn1)] checks that
         preconditions of all the {!cmd}s of [seq], [spawn0], and [spawn1] are satisfied in all the
         possible interleavings and starting with {!Spec.init_state}.
@@ -20,7 +18,7 @@ module Make : functor (Spec : STM.Spec) ->
 
     val arb_cmds_triple
       :  int -> int
-      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) QCheck.arbitrary
+      -> (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) QCheck.arbitrary
     (** [arb_cmds_triple seq_len par_len] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         All [cmds] are generated with {!Spec.arb_cmd}.
@@ -35,10 +33,10 @@ module Make : functor (Spec : STM.Spec) ->
     val arb_triple
       :  int
       -> int
-      -> Spec.(state -> packed_cmd QCheck.arbitrary)
-      -> Spec.(state -> packed_cmd QCheck.arbitrary)
-      -> Spec.(state -> packed_cmd QCheck.arbitrary)
-      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) QCheck.arbitrary
+      -> (Spec.state -> Spec.Cmd.any QCheck.arbitrary)
+      -> (Spec.state -> Spec.Cmd.any QCheck.arbitrary)
+      -> (Spec.state -> Spec.Cmd.any QCheck.arbitrary)
+      -> (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) QCheck.arbitrary
     (** [arb_triple seq_len par_len arb0 arb1 arb2] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [par_len] parallel commands each.
         The three {!Spec.cmd} components are generated with [arb0], [arb1], and [arb2], respectively.
@@ -49,10 +47,10 @@ module Make : functor (Spec : STM.Spec) ->
     val arb_triple_asym
       :  int
       -> int
-      -> Spec.(state -> packed_cmd QCheck.arbitrary)
-      -> Spec.(state -> packed_cmd QCheck.arbitrary)
-      -> Spec.(state -> packed_cmd QCheck.arbitrary)
-      -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) QCheck.arbitrary
+      -> (Spec.state -> Spec.Cmd.any QCheck.arbitrary)
+      -> (Spec.state -> Spec.Cmd.any QCheck.arbitrary)
+      -> (Spec.state -> Spec.Cmd.any QCheck.arbitrary)
+      -> (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) QCheck.arbitrary
     (** [arb_triple_asym seq_len par_len arb0 arb1 arb2] creates a triple [cmd]
         generator like {!arb_triple}. It differs in that the resulting printer
         is asymmetric, printing [arb1]'s result below [arb0]'s result and
@@ -60,12 +58,12 @@ module Make : functor (Spec : STM.Spec) ->
         [arb_triple_asym] catches and ignores generation-time exceptions arising
         from {!Spec.next_state}. *)
 
-    val interp_sut_res : Spec.sut -> Spec.packed_cmd list -> cmd_res list
+    val interp_sut_res : Spec.sut -> Spec.Cmd.any list -> cmd_res list
     (** [interp_sut_res sut cs] interprets the commands [cs] over the system {!Spec.sut}
         and returns the list of corresponding {!Spec.cmd} and result pairs. *)
 
     val agree_prop_par
-      : Spec.(packed_cmd list * packed_cmd list * packed_cmd list) -> bool
+      : (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) -> bool
     (** Parallel agreement property based on {!Stdlib.Domain}.
         [agree_prop_par (seq_pref, tl1, tl2)] first interprets [seq_pref]
         and then spawns two parallel, symmetric domains interpreting [tl1] and
@@ -75,7 +73,7 @@ module Make : functor (Spec : STM.Spec) ->
         which agrees with a model interpretation. *)
 
     val agree_prop_par_asym
-      : Spec.(packed_cmd list * packed_cmd list * packed_cmd list) -> bool
+      : (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) -> bool
     (** Asymmetric parallel agreement property based on {!Stdlib.Domain}.
         [agree_prop_par_asym (seq_pref, tl1, tl2)] first interprets [seq_pref],
         and then interprets [tl1] while a spawned domain interprets [tl2]
diff --git a/lib/STM_sequential.ml b/lib/STM_sequential.ml
index 31c1d2d9e..273b1c6ee 100644
--- a/lib/STM_sequential.ml
+++ b/lib/STM_sequential.ml
@@ -6,10 +6,6 @@ module Make (Spec: Spec) = struct
   open Internal.Make(Spec)
     [@alert "-internal"]
 
-  type packed_res = Internal.Make(Spec).packed_res
-                  = Pack_res : 'a STM.res -> packed_res [@@unboxed]
-    [@@alert "-internal"]
-
   type cmd_res = Internal.Make(Spec).cmd_res
                = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
     [@@alert "-internal"]
diff --git a/lib/STM_sequential.mli b/lib/STM_sequential.mli
index 6b57d3068..8f8ad46e1 100644
--- a/lib/STM_sequential.mli
+++ b/lib/STM_sequential.mli
@@ -2,21 +2,19 @@
 
 module Make : functor (Spec : STM.Spec) ->
   sig
-    type packed_res = Pack_res : 'a STM.res -> packed_res [@@unboxed]
-
     type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
 
-    val cmds_ok : Spec.state -> Spec.packed_cmd list -> bool
+    val cmds_ok : Spec.state -> Spec.Cmd.any list -> bool
     (** A precondition checker (stops early, thanks to short-circuit Boolean evaluation).
         Accepts the initial state and the command sequence as parameters.
         [cmds_ok] catches and ignores exceptions arising from {!next_state}.  *)
 
-    val arb_cmds : Spec.state -> Spec.packed_cmd list QCheck.arbitrary
+    val arb_cmds : Spec.state -> Spec.Cmd.any list QCheck.arbitrary
     (** A generator of {!Spec.cmd} sequences. Accepts the initial state as a parameter.
         [arb_cmds] catches and ignores generation-time exceptions arising from
         {!Spec.next_state}. *)
 
-    val agree_prop : Spec.packed_cmd list -> bool
+    val agree_prop : Spec.Cmd.any list -> bool
     (** The agreement property: the command sequence [cs] yields the same observations
         when interpreted from the model's initial state and the [sut]'s initial state.
         Cleans up after itself by calling {!Spec.cleanup}. *)
diff --git a/lib/STM_thread.ml b/lib/STM_thread.ml
index 9ec87145c..67acaadbf 100644
--- a/lib/STM_thread.ml
+++ b/lib/STM_thread.ml
@@ -7,9 +7,7 @@ module Make (Spec: Spec) = struct
   open Internal.Make(Spec)
     [@alert "-internal"]
 
-  type packed_res = Internal.Make(Spec).packed_res
-                  = Pack_res : 'a STM.res -> packed_res [@@unboxed]
-    [@@alert "-internal"]
+  module Cmd = Spec.Cmd
 
   type cmd_res = Internal.Make(Spec).cmd_res
                = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
@@ -22,7 +20,7 @@ module Make (Spec: Spec) = struct
   (* [interp_sut_res] specialized for [Threads] *)
   let rec interp_sut_res sut cs = match cs with
     | [] -> []
-    | Spec.Pack_cmd c :: cs ->
+    | Cmd.Pack_cmd c :: cs ->
        Thread.yield ();
        let res = Spec.run c sut in
        Pack_cmd_res (c,res) :: interp_sut_res sut cs
diff --git a/lib/STM_thread.mli b/lib/STM_thread.mli
index 43a826140..fa164dbac 100644
--- a/lib/STM_thread.mli
+++ b/lib/STM_thread.mli
@@ -2,26 +2,24 @@
 
 module Make : functor (Spec : STM.Spec) ->
   sig
-    type packed_res = Pack_res : 'a STM.res -> packed_res [@@unboxed]
-
     type cmd_res = Pack_cmd_res : 'a Spec.cmd * 'a STM.res -> cmd_res
 
     exception ThreadNotFinished
 
     val arb_cmds_triple
-    : int -> int -> Spec.(packed_cmd list * packed_cmd list * packed_cmd list) QCheck.arbitrary
+    : int -> int -> (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) QCheck.arbitrary
     (** [arb_cmds_triple seq_len conc_len] generates a [cmd] triple with at most [seq_len]
         sequential commands and at most [conc_len] concurrent commands each.
         All [cmds] are generated with {!Spec.arb_cmd}.
         [arb_cmds_triple] catches and ignores generation-time exceptions arising
         from {!Spec.next_state}. *)
 
-    val interp_sut_res : Spec.sut -> Spec.packed_cmd list -> cmd_res list
+    val interp_sut_res : Spec.sut -> Spec.Cmd.any list -> cmd_res list
     (** [interp_sut_res sut cs] interprets the commands [cs] over the system [sut]
         and returns the list of corresponding {!Spec.cmd} and result pairs. *)
 
     val agree_prop_conc
-      : Spec.(packed_cmd list * packed_cmd list * packed_cmd list) -> bool
+      : (Spec.Cmd.any list * Spec.Cmd.any list * Spec.Cmd.any list) -> bool
     (** Concurrent agreement property based on {!Thread} *)
 
     val agree_test_conc : count:int -> name:string -> QCheck.Test.t
diff --git a/src/atomic/stm_tests.ml b/src/atomic/stm_tests.ml
index 63b5e4ed7..6473e775b 100644
--- a/src/atomic/stm_tests.ml
+++ b/src/atomic/stm_tests.ml
@@ -31,21 +31,25 @@ struct
   type state = int
   type sut = int Atomic.t
 
-  type packed_cmd = Pack_cmd : 'r cmd -> packed_cmd
-
-  let show_packed_cmd (Pack_cmd c) = show_cmd c
+  module Cmd =
+    STM.Cmd
+      (struct
+        type 'r t = 'r cmd
+        let show = show_cmd
+      end)
 
   let arb_cmd s =
     let int_gen = Gen.nat in
-    QCheck.make ~print:show_packed_cmd
+    let mkgen = Cmd.Gen.map in
+    QCheck.make ~print:Cmd.print
       (Gen.oneof
-         [Gen.return (Pack_cmd Get);
-	  Gen.map (fun i -> Pack_cmd (Set i)) int_gen;
-	  Gen.map (fun i -> Pack_cmd (Exchange i)) int_gen;
-	  Gen.map (fun i -> Pack_cmd (Fetch_and_add i)) int_gen;
-	  Gen.map2 (fun seen v -> Pack_cmd (Compare_and_set (seen,v))) (Gen.oneof [Gen.return s; int_gen]) int_gen;
-          Gen.return (Pack_cmd Incr);
-	  Gen.return (Pack_cmd Decr);
+         [ mkgen @@ Gen.return Get;
+	   mkgen @@ Gen.map (fun i -> Set i) int_gen;
+	   mkgen @@ Gen.map (fun i -> Exchange i) int_gen;
+	   mkgen @@ Gen.map (fun i -> Fetch_and_add i) int_gen;
+	   mkgen @@ Gen.map2 (fun seen v -> Compare_and_set (seen,v)) (Gen.oneof [Gen.return s; int_gen]) int_gen;
+           mkgen @@ Gen.return Incr;
+	   mkgen @@ Gen.return Decr;
          ])
 
   let init_state  = 0