REMOVE ME: add Lin.thread stats for {int,int64} x {ref,CList}

Author: jmid

lib/lin_thread.ml

@@ -54,6 +54,22 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
 
   let neg_lin_test ~count ~name =
     neg_lin_test ~rep_count:100 ~count ~retries:5 ~name ~lin_prop:lin_prop
+
+  let lin_stats ~count =
+    let rep_count = 25 in
+    let seq_len,par_len = 20,12 in
+    let exceptions = ref 0 in
+    let t =
+      QCheck.Test.make ~count
+        (arb_cmds_triple seq_len par_len)
+        (fun triple ->
+           try (* On purpose we include repetition, because triggering issue is very rare *)
+             Util.repeat rep_count lin_prop triple
+           with _ ->
+             incr exceptions;
+             true) in
+    QCheck.Test.check_exn t;
+    !exceptions
 end
 
 module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))

lib/lin_thread.mli

@@ -43,4 +43,10 @@ module Make (Spec : Spec) : sig
       is found, and succeeds if a counter example is indeed found, and prints it
       afterwards.
   *)
+
+  val lin_stats : count:int -> int
+  (** Repeatedly run a concurrent test based on {!Stdlib.Thread} and
+      return how many times sequential consistency failed.
+      Accepts a labeled parameter:
+      [count] is the number of test iterations. *)
 end

src/neg_tests/dune

@@ -118,6 +118,14 @@
  (action (progn))
 )
 
+(executable
+ (name lin_tests_thread_stats)
+ (modules lin_tests_thread_stats)
+ (flags (:standard -w -27))
+ (libraries lin_tests_common qcheck-lin.thread)
+ (modes native byte)
+)
+
 (test
  (name lin_tests_effect)
  (modules lin_tests_effect)

src/neg_tests/lin_tests_thread_stats.ml

@@ -0,0 +1,23 @@
+open Lin_tests_common
+
+(** This is a driver of the negative tests over the Thread module *)
+
+module CList_bis = struct include CList let add_node = add_node_thread end
+module RT_int_thread = Lin_thread.Make(Ref_int_spec)
+module RT_int64_thread = Lin_thread.Make(Ref_int64_spec)
+module CLT_int_thread = Lin_thread.Make(CList_spec_int(CList_bis))
+module CLT_int64_thread = Lin_thread.Make(CList_spec_int64(CList_bis))
+
+let count = 10000
+
+let failures = RT_int_thread.lin_stats ~count
+let () = Printf.printf "Lin int ref Thread %i / %i\n%!" failures count
+
+let failures = RT_int64_thread.lin_stats ~count
+let () = Printf.printf "Lin int64 ref Thread %i / %i\n%!" failures count
+
+let failures = CLT_int_thread.lin_stats ~count
+let () = Printf.printf "Lin int CList Thread %i / %i\n%!" failures count
+
+let failures = CLT_int64_thread.lin_stats ~count
+let () = Printf.printf "Lin int64 CList Thread %i / %i\n%!" failures count