Faster Lin check for pure operations

lib/lin.ml

@@ -20,6 +20,9 @@ struct
     (** A command shrinker.
         To a first approximation you can use [Shrink.nil]. *)
 
+    val is_pure : cmd -> bool
+    (** [is_pure c] returns [true] if the command [c] is free of side-effects. *)
+
     type res
     (** The command result type *)
 
@@ -90,33 +93,49 @@ struct
              triple seq_pref_gen par_gen1 par_gen2) in
       make ~print:(print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple
 
-    let rec check_seq_cons pref cs1 cs2 seq_sut seq_trace = match pref with
-      | (c,res)::pref' ->
-        if Spec.equal_res res (Spec.run c seq_sut)
-        then check_seq_cons pref' cs1 cs2 seq_sut (c::seq_trace)
-        else (Spec.cleanup seq_sut; false)
+
+    let check c res seq_sut = Spec.equal_res res (Spec.run c seq_sut)
+
+    let rec check_seq pref seq_sut seq_trace = match pref with
+      | [] -> Some seq_trace
+      | (c, res) :: pref' ->
+          if check c res seq_sut
+          then let seq_trace = if Spec.is_pure c then seq_trace else c::seq_trace in
+               check_seq pref' seq_sut seq_trace
+          else (Spec.cleanup seq_sut; None)
+
+    let rec check_seq_step c res cs1 cs2 seq_sut seq_trace =
+      if check c res seq_sut
+      then check_seq_cons cs1 cs2 seq_sut (c::seq_trace)
+      else (Spec.cleanup seq_sut; false)
       (* Invariant: call Spec.cleanup immediately after mismatch  *)
-      | [] -> match cs1,cs2 with
-        | [],[] -> Spec.cleanup seq_sut; true
-        | [],(c2,res2)::cs2' ->
-          if Spec.equal_res res2 (Spec.run c2 seq_sut)
-          then check_seq_cons pref cs1 cs2' seq_sut (c2::seq_trace)
-          else (Spec.cleanup seq_sut; false)
-        | (c1,res1)::cs1',[] ->
-          if Spec.equal_res res1 (Spec.run c1 seq_sut)
-          then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace)
-          else (Spec.cleanup seq_sut; false)
-        | (c1,res1)::cs1',(c2,res2)::cs2' ->
-          (if Spec.equal_res res1 (Spec.run c1 seq_sut)
-           then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace)
-           else (Spec.cleanup seq_sut; false))
-          ||
-          (* rerun to get seq_sut to same cmd branching point *)
-          (let seq_sut' = Spec.init () in
-           let _ = interp_plain seq_sut' (List.rev seq_trace) in
-           if Spec.equal_res res2 (Spec.run c2 seq_sut')
-           then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace)
-           else (Spec.cleanup seq_sut'; false))
+
+    and check_seq_cons cs1 cs2 seq_sut seq_trace = match cs1, cs2 with
+      | [], [] -> Spec.cleanup seq_sut; true
+      | [], cs2' -> Option.is_some (check_seq cs2' seq_sut seq_trace)
+      | cs1', [] -> Option.is_some (check_seq cs1' seq_sut seq_trace)
+      | (c1,res1)::cs1', (c2,res2)::cs2' ->
+          begin match Spec.is_pure c1, Spec.is_pure c2 with
+          | true, _ when check c1 res1 seq_sut ->
+            check_seq_cons cs1' cs2 seq_sut seq_trace
+          | _, true when check c2 res2 seq_sut ->
+            check_seq_cons cs1 cs2' seq_sut seq_trace
+          | true, true -> Spec.cleanup seq_sut; false
+          | true, false -> check_seq_step c2 res2 cs1 cs2' seq_sut seq_trace
+          | false, true -> check_seq_step c1 res1 cs1' cs2 seq_sut seq_trace
+          | false, false ->
+            check_seq_step c1 res1 cs1' cs2 seq_sut seq_trace
+            || (* rerun to get seq_sut to same cmd branching point *)
+              (let seq_sut' = Spec.init () in
+              let _ = interp_plain seq_sut' (List.rev seq_trace) in
+              check_seq_step c2 res2 cs1 cs2' seq_sut' seq_trace)
+          end
+
+    let check_seq_cons pref cs1 cs2 =
+      let seq_sut = Spec.init () in
+      match check_seq pref seq_sut [] with
+      | None -> false
+      | Some seq_trace -> check_seq_cons cs1 cs2 seq_sut seq_trace
 
     (* Linearization test *)
     let lin_test ~rep_count ~retries ~count ~name ~lin_prop =
@@ -257,15 +276,21 @@ let returning_or_exc_ a = Fun.Ret_ignore_or_exc a
 let (@->) a b = Fun.Fn (a,b)
 
 type _ elem =
-  | Elem : string * ('ftyp, 'r, 's) Fun.fn * 'ftyp -> 's elem
+  | Elem :
+      { name : string
+      ; pure : bool
+      ; fntyp : ('ftyp, 'r, 's) Fun.fn
+      ; value : 'ftyp
+      }
+      -> 's elem
 
 type 's api = (int * 's elem) list
 
-let val_ name value fntyp =
-  (1, Elem (name, fntyp, value))
+let val_ ?(pure = false) name value fntyp =
+  (1, Elem { name ; pure ; fntyp ; value })
 
-let val_freq freq name value fntyp =
-  (freq, Elem (name, fntyp, value))
+let val_freq ?(pure = false) freq name value fntyp =
+  (freq, Elem { name ; pure ; fntyp ; value })
 
 module type Spec = sig
   type t
@@ -292,15 +317,17 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
       | FnState : ('b,'r) args -> (t -> 'b, 'r) args
   end
 
-  (* Operation name, typed argument list, return type descriptor, printer, shrinker, function *)
+  (* Operation name, purity, typed argument list, return type descriptor, printer, shrinker, function *)
   type cmd =
       Cmd :
-        string *
-        ('ftyp, 'r) Args.args *
-        ('r, deconstructible, t, _) ty *
-        (('ftyp, 'r) Args.args -> string) *
-        (('ftyp, 'r) Args.args QCheck.Shrink.t) *
-        'ftyp
+        { name : string
+        ; is_pure : bool
+        ; args : ('ftyp, 'r) Args.args
+        ; rty : ('r, deconstructible, t, _) ty
+        ; print : (('ftyp, 'r) Args.args -> string)
+        ; shrink : (('ftyp, 'r) Args.args QCheck.Shrink.t)
+        ; f : 'ftyp
+        }
         -> cmd
 
   type res =
@@ -379,20 +406,20 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
                       | _ -> failwith "Fn/Some: should not happen"))
 
   let api =
-    List.map (fun (wgt, Elem (name, fdesc, f)) ->
+    List.map (fun (wgt, Elem { name ; pure = is_pure ; fntyp = fdesc ; value = f }) ->
         let rty = ret_type fdesc in
         let open QCheck.Gen in
         (wgt, gen_args_of_desc fdesc >>= fun args ->
          let print = gen_printer name fdesc in
          let shrink = gen_shrinker_of_desc fdesc in
-         return (Cmd (name, args, rty, print, shrink, f)))) ApiSpec.api
+         return (Cmd { name ; is_pure ; args ; rty ; print ; shrink ; f }))) ApiSpec.api
 
   let gen_cmd : cmd QCheck.Gen.t = QCheck.Gen.frequency api
 
-  let show_cmd (Cmd (_,args,_,print,_,_)) = print args
+  let show_cmd (Cmd { args ; print ; _ }) = print args
 
-  let shrink_cmd (Cmd (name,args,rty,print,shrink,f)) =
-    QCheck.Iter.map (fun args -> Cmd (name,args,rty,print,shrink,f)) (shrink args)
+  let shrink_cmd (Cmd cmd) =
+    QCheck.Iter.map (fun args -> Cmd { cmd with args }) (cmd.shrink cmd.args)
 
   (* Unsafe if called on two [res] whose internal values are of different
      types. *)
@@ -457,6 +484,8 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
       apply_f (f arg) rem state
 
   let run cmd state =
-    let Cmd (_, args, rty, _, _, f) = cmd in
+    let Cmd { args ; rty ; f ; _ } = cmd in
     Res (rty, apply_f f args state)
+
+  let is_pure (Cmd { is_pure ; _ }) = is_pure
 end

lib/lin.mli

@@ -24,6 +24,9 @@ module Internal : sig
     (** A command shrinker.
         To a first approximation you can use {!QCheck.Shrink.nil}. *)
 
+    val is_pure : cmd -> bool
+    (** [is_pure c] returns [true] if the command [c] is free of side-effects. *)
+
     type res
     (** The command result type *)
 
@@ -46,7 +49,7 @@ module Internal : sig
 
   module Make(Spec : CmdSpec) : sig
     val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
-    val check_seq_cons : (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> Spec.t -> Spec.cmd list -> bool
+    val check_seq_cons : (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> bool
     val interp_plain : Spec.t -> Spec.cmd list -> (Spec.cmd * Spec.res) list
     val lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t
     val neg_lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t
@@ -265,17 +268,19 @@ val ( @-> ) :
 (** {1 API description} *)
 
 (** Type and constructor to capture a single function signature *)
-type _ elem = private
-  | Elem : string * ('ftyp, 'r, 's) Fun.fn * 'ftyp -> 's elem
+type !_ elem
 
 type 's api = (int * 's elem) list
 (** The type of module signatures *)
 
-val val_ : string -> 'f -> ('f, 'r, 's) Fun.fn -> int * 's elem
+val val_ : ?pure:bool -> string -> 'f -> ('f, 'r, 's) Fun.fn -> int * 's elem
 (** [val_ str f sig] describes a function signature from a string [str],
-    a function value [f], and a signature description [sig]. *)
+    a function value [f], and a signature description [sig].
+
+    - The optional argument [?pure] is [false] by default. If [true] then the
+      function must be free of side-effects. *)
 
-val val_freq : int -> string -> 'f -> ('f, 'r, 's) Fun.fn -> int * 's elem
+val val_freq : ?pure:bool -> int -> string -> 'f -> ('f, 'r, 's) Fun.fn -> int * 's elem
 (** [val_freq w str f sig] describes a function signature like
     {!val_} [str f sig] but with relative weight [w] rather than 1.
     A function of weight 2 will have twice the probability of being

lib/lin_domain.ml

@@ -21,8 +21,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
     let obs2 = Domain.join dom2 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
-    let seq_sut = Spec.init () in
-    check_seq_cons pref_obs obs1 obs2 seq_sut []
+    check_seq_cons pref_obs obs1 obs2
       || QCheck.Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
          @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
               (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))

lib/lin_effect.ml

@@ -60,6 +60,10 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
       | SchedYield -> Iter.empty
       | UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd c)
 
+    let is_pure = function
+      | UserCmd c -> Spec.is_pure c
+      | SchedYield -> false
+
     type res = SchedYieldRes | UserRes of Spec.res
 
     let show_res r = match r with
@@ -103,9 +107,8 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
          fork (fun () -> let tmp2 = interp sut cmds2 in obs2 := tmp2); in
        let () = start_sched main in
        let () = Spec.cleanup sut in
-       let seq_sut = Spec.init () in
        (* exclude [Yield]s from sequential executions when searching for an interleaving *)
-       EffTest.check_seq_cons (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut []
+       EffTest.check_seq_cons (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2)
        || QCheck.Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
        @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
          (fun (c,r) -> Printf.sprintf "%s : %s" (EffSpec.show_cmd c) (EffSpec.show_res r))

lib/lin_thread.ml

@@ -29,9 +29,8 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
       Thread.join th1;
       Thread.join th2;
       Spec.cleanup sut;
-      let seq_sut = Spec.init () in
       (* we reuse [check_seq_cons] to linearize and interpret sequentially *)
-      check_seq_cons pref_obs !obs1 !obs2 seq_sut []
+      check_seq_cons pref_obs !obs1 !obs2
       || QCheck.Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
          @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
               (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))

src/array/lin_tests.ml

@@ -23,6 +23,10 @@ struct
 
   let shrink_cmd c = Iter.empty
 
+  let is_pure = function
+    | Length | Get _ | Sub _ | Copy | To_list | Mem _ | To_seq -> true
+    | Set _ | Fill _ | Sort -> false
+
   open Util
   (*let pp_exn = Util.pp_exn*)
   type res =

src/array/lin_tests_dsl.ml

@@ -13,16 +13,16 @@ struct
   let int,char = nat_small,char_printable
   let array_to_seq a = List.to_seq (List.of_seq (Array.to_seq a)) (* workaround: Array.to_seq is lazy and will otherwise see and report later Array.set state changes... *)
   let api =
-    [ val_ "Array.length"   Array.length   (t @-> returning int);
-      val_ "Array.get"      Array.get      (t @-> int @-> returning_or_exc char);
+    [ val_ "Array.length"   Array.length   (t @-> returning int) ~pure:true;
+      val_ "Array.get"      Array.get      (t @-> int @-> returning_or_exc char) ~pure:true;
       val_ "Array.set"      Array.set      (t @-> int @-> char @-> returning_or_exc unit);
-      val_ "Array.sub"      Array.sub      (t @-> int @-> int @-> returning_or_exc (array char));
-      val_ "Array.copy"     Array.copy     (t @-> returning (array char));
+      val_ "Array.sub"      Array.sub      (t @-> int @-> int @-> returning_or_exc (array char)) ~pure:true;
+      val_ "Array.copy"     Array.copy     (t @-> returning (array char)) ~pure:true;
       val_ "Array.fill"     Array.fill     (t @-> int @-> int @-> char @-> returning_or_exc unit);
-      val_ "Array.to_list"  Array.to_list  (t @-> returning (list char));
-      val_ "Array.mem"      Array.mem      (char @-> t @-> returning bool);
+      val_ "Array.to_list"  Array.to_list  (t @-> returning (list char)) ~pure:true;
+      val_ "Array.mem"      Array.mem      (char @-> t @-> returning bool) ~pure:true;
       val_ "Array.sort"     (Array.sort Char.compare) (t @-> returning unit);
-      val_ "Array.to_seq"   array_to_seq   (t @-> returning (seq char));
+      val_ "Array.to_seq"   array_to_seq   (t @-> returning (seq char)) ~pure:true;
     ]
 end
 

src/atomic/lin_tests.ml

@@ -19,6 +19,10 @@ struct
 
   let shrink_cmd = Shrink.nil
 
+  let is_pure = function
+    | Get -> true
+    | Set _ | Exchange _ | Compare_and_set _ | Fetch_and_add _ | Incr | Decr -> false
+
   type res =
     | RGet of int
     | RSet
@@ -62,6 +66,10 @@ struct
 
   let shrink_cmd = Shrink.nil
 
+  let is_pure = function
+    | Get _ -> true
+    | Set _ | Exchange _ | Compare_and_set _ | Fetch_and_add _ | Incr _ | Decr _ -> false
+
   type res =
     | RGet of int
     | RSet

src/atomic/lin_tests_dsl.ml

@@ -4,7 +4,7 @@ module Atomic_spec : Lin.Spec = struct
   let init () = Atomic.make 0
   let cleanup _ = ()
   let api =
-    [ val_ "Atomic.get"             Atomic.get             (t @-> returning int);
+    [ val_ "Atomic.get"             Atomic.get             (t @-> returning int) ~pure:true;
       val_ "Atomic.set"             Atomic.set             (t @-> int @-> returning unit);
       val_ "Atomic.exchange"        Atomic.exchange        (t @-> int @-> returning int);
       val_ "Atomic.fetch_and_add"   Atomic.fetch_and_add   (t @-> int @-> returning int);

src/bytes/lin_tests_dsl.ml

@@ -9,12 +9,12 @@ module BConf = struct
   open Lin
 
   let api = [
-    val_ "Bytes.get"         Bytes.get         (t @-> int @-> returning_or_exc char);
-    val_ "Bytes.sub_string"  Bytes.sub_string  (t @-> int @-> int @-> returning_or_exc string);
-    val_ "Bytes.length"      Bytes.length      (t @-> returning int);
+    val_ "Bytes.get"         Bytes.get         (t @-> int @-> returning_or_exc char) ~pure:true;
+    val_ "Bytes.sub_string"  Bytes.sub_string  (t @-> int @-> int @-> returning_or_exc string) ~pure:true;
+    val_ "Bytes.length"      Bytes.length      (t @-> returning int) ~pure:true;
     val_ "Bytes.fill"        Bytes.fill        (t @-> int @-> int @-> char @-> returning_or_exc unit);
     val_ "Bytes.blit_string" Bytes.blit_string (string @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
-    val_ "Bytes.index_from"  Bytes.index_from  (t @-> int @-> char @-> returning_or_exc int)]
+    val_ "Bytes.index_from"  Bytes.index_from  (t @-> int @-> char @-> returning_or_exc int) ~pure:true]
 end
 
 module BT_domain = Lin_domain.Make(BConf)

src/ephemeron/lin_tests_dsl.ml

@@ -28,12 +28,12 @@ module EConf =
       [ val_ "Ephemeron.clear"    E.clear    (t @-> returning unit);
         val_ "Ephemeron.add"      E.add      (t @-> int @-> string @-> returning unit);
         val_ "Ephemeron.remove"   E.remove   (t @-> int @-> returning unit);
-        val_ "Ephemeron.find"     E.find     (t @-> int @-> returning_or_exc string);
-        val_ "Ephemeron.find_opt" E.find_opt (t @-> int @-> returning (option string));
-        val_ "Ephemeron.find_all" E.find_all (t @-> int @-> returning (list string));
+        val_ "Ephemeron.find"     E.find     (t @-> int @-> returning_or_exc string) ~pure:true;
+        val_ "Ephemeron.find_opt" E.find_opt (t @-> int @-> returning (option string)) ~pure:true;
+        val_ "Ephemeron.find_all" E.find_all (t @-> int @-> returning (list string)) ~pure:true;
         val_ "Ephemeron.replace"  E.replace  (t @-> int @-> string @-> returning unit);
-        val_ "Ephemeron.mem"      E.mem      (t @-> int @-> returning bool);
-        val_ "Ephemeron.length"   E.length   (t @-> returning int);
+        val_ "Ephemeron.mem"      E.mem      (t @-> int @-> returning bool) ~pure:true;
+        val_ "Ephemeron.length"   E.length   (t @-> returning int) ~pure:true;
         val_ "Ephemeron.clean"    E.clean    (t @-> returning unit);
       ]
   end

src/floatarray/lin_tests_dsl.ml

@@ -18,18 +18,18 @@ struct
   let strict_to_seq a = List.to_seq (List.of_seq (Float.Array.to_seq a))
 
   let api =
-    [ val_ "Float.Array.length"      Float.Array.length                      (t@-> returning int);
-      val_ "Float.Array.get"         Float.Array.get                         (t@-> int @-> returning_or_exc float);
+    [ val_ "Float.Array.length"      Float.Array.length                      (t@-> returning int) ~pure:true;
+      val_ "Float.Array.get"         Float.Array.get                         (t@-> int @-> returning_or_exc float) ~pure:true;
       val_ "Float.Array.set"         Float.Array.set                         (t@-> int @-> float @-> returning_or_exc unit);
       val_ "Float.Array.fill"        Float.Array.fill                        (t@-> int @-> int @-> float @-> returning_or_exc unit);
-      val_ "Float.Array.to_list"     Float.Array.to_list                     (t@-> returning (list float));
-      val_ "Float.Array.mem"         Float.Array.mem                         (float @-> t @-> returning bool);
-      val_ "Float.Array.mem_ieee"    Float.Array.mem_ieee                    (float @-> t @-> returning bool);
+      val_ "Float.Array.to_list"     Float.Array.to_list                     (t@-> returning (list float)) ~pure:true;
+      val_ "Float.Array.mem"         Float.Array.mem                         (float @-> t @-> returning bool) ~pure:true;
+      val_ "Float.Array.mem_ieee"    Float.Array.mem_ieee                    (float @-> t @-> returning bool) ~pure:true;
       val_ "Float.Array.sort"        (Float.Array.sort compare)              (t@-> returning unit);
       val_ "Float.Array.stable_sort" (Float.Array.stable_sort compare)       (t@-> returning unit);
       val_ "Float.Array.fast_sort"   (Float.Array.fast_sort compare)         (t@-> returning unit);
-      val_ "Float.Array.to_seq"      strict_to_seq                           (t@-> returning (seq float));
-      val_ "Float.Array.to_array"    (Float.Array.map_to_array (fun x -> x)) (t@-> returning (array float));
+      val_ "Float.Array.to_seq"      strict_to_seq                           (t@-> returning (seq float)) ~pure:true;
+      val_ "Float.Array.to_array"    (Float.Array.map_to_array (fun x -> x)) (t@-> returning (array float)) ~pure:true;
     ]
 end
 

src/hashtbl/lin_tests.ml

@@ -38,6 +38,10 @@ struct
     | Mem c -> Iter.map (fun c -> Mem c) (Shrink.char c)
     | Length -> Iter.empty
 
+  let is_pure = function
+    | Find _ | Find_opt _ | Find_all _ | Mem _ | Length -> true
+    | Clear | Add _ | Remove _ | Replace _ -> false
+
   type res =
     | RClear
     | RAdd