Improve context switching chance in Lin_thread and STM_thread modes

CHANGES.md

@@ -2,7 +2,9 @@
 
 ## NEXT RELEASE
 
-- ...
+- #540: Significantly increase the probability of context switching in `Lin_thread`
+        and `STM_thread` by utilizing `Gc.Memprof` callbacks. Avoid on 5.0-5.2
+        without `Gc.Memprof` support.
 
 ## 0.7
 

lib/STM_thread.ml

@@ -11,6 +11,14 @@ module MakeExt (Spec: SpecExt) = struct
 
   let arb_cmds_triple = arb_cmds_triple
 
+  let alloc_callback _src =
+    Thread.yield ();
+    None
+
+  let yield_tracker =
+    Gc.Memprof.{ null_tracker with alloc_minor = alloc_callback;
+                                   alloc_major = alloc_callback; }
+
   (* [interp_sut_res] specialized for [Threads] *)
   let rec interp_sut_res sut cs = match cs with
     | [] -> []
@@ -23,13 +31,16 @@ module MakeExt (Spec: SpecExt) = struct
   let agree_prop_conc (seq_pref,cmds1,cmds2) =
     let sut = Spec.init_sut () in
     let obs1,obs2 = ref (Error ThreadNotFinished), ref (Error ThreadNotFinished) in
+    (* Gc.Memprof.{start,stop} raises Failure on OCaml 5.0 and 5.1 *)
+    (try ignore (Gc.Memprof.start ~sampling_rate:1e-1 ~callstack_size:0 yield_tracker) with Failure _ -> ());
     let pref_obs = Spec.wrap_cmd_seq @@ fun () -> interp_sut_res sut seq_pref in
     let wait = ref true in
     let th1 = Thread.create (fun () -> Spec.wrap_cmd_seq @@ fun () -> while !wait do Thread.yield () done; obs1 := try Ok (interp_sut_res sut cmds1) with exn -> Error exn) () in
     let th2 = Thread.create (fun () -> Spec.wrap_cmd_seq @@ fun () -> wait := false; obs2 := try Ok (interp_sut_res sut cmds2) with exn -> Error exn) () in
-    let ()   = Thread.join th1 in
-    let ()   = Thread.join th2 in
-    let ()   = Spec.cleanup sut in
+    Thread.join th1;
+    Thread.join th2;
+    (try Gc.Memprof.stop () with Failure _ -> ());
+    Spec.cleanup sut;
     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
@@ -40,25 +51,25 @@ module MakeExt (Spec: SpecExt) = struct
 
   let agree_test_conc ~count ~name =
     (* a bigger [rep_count] for [Threads] as it is more difficult to trigger a problem *)
-    let rep_count = 100 in
+    let rep_count = 3 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:15 ~max_gen ~count ~name
+    Test.make ~retries:25 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun ((seq_pref,cmds1,cmds2) as triple) ->
          assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
          repeat rep_count agree_prop_conc triple) (* 100 times each, then 100 * 15 times when shrinking *)
 
   let neg_agree_test_conc ~count ~name =
-    let rep_count = 100 in
+    let rep_count = 3 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_neg ~retries:15 ~max_gen ~count ~name
+    Test.make_neg ~retries:25 ~max_gen ~count ~name
       (arb_cmds_triple seq_len par_len)
       (fun ((seq_pref,cmds1,cmds2) as triple) ->
          assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
          repeat rep_count agree_prop_conc triple) (* 100 times each, then 100 * 15 times when shrinking *)
-  end
+end
 
 module Make (Spec: Spec) =
   MakeExt (struct

lib/STM_thread.mli

@@ -1,4 +1,21 @@
-(** Module for building concurrent STM tests over {!Thread}s *)
+(** Module for building concurrent [STM] tests over {!Thread}s
+
+    Context switches in {!Thread}s may happen
+    - at allocations and
+    - at safepoints {:https://github.com/ocaml/ocaml/pull/10039}.
+
+    This module relies on [Gc.Memprof] support to trigger more frequent context
+    switching between threads at allocation sites. This works well in OCaml
+    4.11.0-4.14.x and 5.3.0 onwards where [Gc.Memprof] is available.
+
+    In OCaml 5.0-5.2 without [Gc.Memprof] support the context switching at
+    allocation sites will be inferior. As a consequence the module may fail to
+    trigger concurrency issues.
+
+    Context switches at safepoints will trigger much less frequently. This
+    means the module may fail to trigger concurrency issues in connection with
+    these. Consider yourself warned.
+*)
 
 module Make : functor (Spec : STM.Spec) ->
   sig
@@ -26,8 +43,6 @@ module Make : functor (Spec : STM.Spec) ->
         [count] is the test count and [name] is the printed test name. *)
 
   end
-  [@@alert experimental "This module is experimental: It may fail to trigger concurrency issues that are present."]
 
 module MakeExt : functor (Spec : STM.SpecExt) ->
-  module type of Make (Spec) [@@alert "-experimental"]
-  [@@alert experimental "This module is experimental: It may fail to trigger concurrency issues that are present."]
+  module type of Make (Spec)

lib/lin_domain.mli

@@ -1,6 +1,6 @@
 open Lin
 
-(** functor to build an internal module representing parallel tests *)
+(** Functor to build an internal module representing parallel tests *)
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
   val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
   val lin_prop : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
@@ -11,7 +11,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
 end
   [@@alert internal "This module is exposed for internal uses only, its API may change at any time"]
 
-(** functor to build a module for parallel testing *)
+(** Functor to build a module for parallel testing *)
 module Make (Spec : Spec) : sig
   val lin_test : count:int -> name:string -> QCheck.Test.t
   (** [lin_test ~count:c ~name:n] builds a parallel test with the name [n] that

lib/lin_effect.mli

@@ -1,6 +1,6 @@
 open Lin
 
-(** functor to build an internal module representing {!Stdlib.Effect}-based tests *)
+(** Functor to build an internal module representing {!Stdlib.Effect}-based tests *)
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
   module EffSpec : sig
     type cmd
@@ -20,7 +20,7 @@ val yield : unit -> unit
 (** Helper function to yield control in the underlying {!Stdlib.Effect}-based scheduler
 *)
 
-(** functor to build a module for [Effect]-based testing *)
+(** Functor to build a module for [Effect]-based testing *)
 module Make (Spec : Spec) : sig
   val lin_test : count:int -> name:string -> QCheck.Test.t
   (** [lin_test ~count:c ~name:n] builds an {!Stdlib.Effect}-based test with the name

lib/lin_thread.ml

@@ -4,6 +4,14 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
   module M = Internal.Make(Spec) [@alert "-internal"]
   include M
 
+  let alloc_callback _src =
+    Thread.yield ();
+    None
+
+  let yield_tracker =
+    Gc.Memprof.{ null_tracker with alloc_minor = alloc_callback;
+                                   alloc_major = alloc_callback; }
+
   (* Note: On purpose we use
      - a non-tail-recursive function and
      - an (explicit) allocation in the loop body
@@ -21,12 +29,15 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
   let lin_prop (seq_pref, cmds1, cmds2) =
     let sut = Spec.init () in
     let obs1, obs2 = ref (Ok []), ref (Ok []) in
+    (* Gc.Memprof.{start,stop} raises Failure on OCaml 5.0 and 5.1 *)
+    (try ignore (Gc.Memprof.start ~sampling_rate:1e-1 ~callstack_size:0 yield_tracker) with Failure _ -> ());
     let pref_obs = interp_plain sut seq_pref in
     let wait = ref true in
     let th1 = Thread.create (fun () -> while !wait do Thread.yield () done; obs1 := try Ok (interp_thread sut cmds1) with exn -> Error exn) () in
     let th2 = Thread.create (fun () -> wait := false; obs2 := try Ok (interp_thread sut cmds2) with exn -> Error exn) () in
     Thread.join th1;
     Thread.join th2;
+    (try Gc.Memprof.stop () with Failure _ -> ());
     Spec.cleanup sut;
     let obs1 = match !obs1 with Ok v -> ref v | Error exn -> raise exn in
     let obs2 = match !obs2 with Ok v -> ref v | Error exn -> raise exn in
@@ -39,10 +50,10 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
             (pref_obs,!obs1,!obs2)
 
   let lin_test ~count ~name =
-    lin_test ~rep_count:100 ~count ~retries:5 ~name ~lin_prop:lin_prop
+    lin_test ~rep_count:3 ~count ~retries:25 ~name ~lin_prop:lin_prop
 
   let neg_lin_test ~count ~name =
-    neg_lin_test ~rep_count:100 ~count ~retries:5 ~name ~lin_prop:lin_prop
+    neg_lin_test ~rep_count:3 ~count ~retries:25 ~name ~lin_prop:lin_prop
 end
 
 module Make (Spec : Spec) = Make_internal(MakeCmd(Spec))

lib/lin_thread.mli

@@ -1,6 +1,25 @@
+(** Module for building concurrent [Lin] tests over {!Thread}s
+
+    Context switches in {!Thread}s may happen
+    - at allocations and
+    - at safepoints {:https://github.com/ocaml/ocaml/pull/10039}.
+
+    This module relies on [Gc.Memprof] support to trigger more frequent context
+    switching between threads at allocation sites. This works well in OCaml
+    4.11.0-4.14.x and 5.3.0 onwards where [Gc.Memprof] is available.
+
+    In OCaml 5.0-5.2 without [Gc.Memprof] support the context switching at
+    allocation sites will be inferior. As a consequence the module may fail to
+    trigger concurrency issues.
+
+    Context switches at safepoints will trigger much less frequently. This
+    means the module may fail to trigger concurrency issues in connection with
+    these. Consider yourself warned.
+*)
+
 open Lin
 
-(** functor to build an internal module representing concurrent tests *)
+(** Functor to build an internal module representing concurrent tests *)
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
   val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
   val lin_prop : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
@@ -9,7 +28,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
 end
   [@@alert internal "This module is exposed for internal uses only, its API may change at any time"]
 
-(** functor to build a module for concurrent testing *)
+(** Functor to build a module for concurrent testing *)
 module Make (Spec : Spec) : sig
   val lin_test : count:int -> name:string -> QCheck.Test.t
   (** [lin_test ~count:c ~name:n] builds a concurrent test with the name [n]
@@ -25,4 +44,3 @@ module Make (Spec : Spec) : sig
       afterwards.
   *)
 end
-[@@alert experimental "This module is experimental: It may fail to trigger concurrency issues that are present."]

src/bytes/lin_tests.ml

@@ -42,7 +42,7 @@ module BConf = struct
 end
 
 module BT_domain = Lin_domain.Make(BConf)
-module BT_thread = Lin_thread.Make(BConf) [@alert "-experimental"]
+module BT_thread = Lin_thread.Make(BConf)
 ;;
 QCheck_base_runner.run_tests_main [
   BT_domain.neg_lin_test ~count:5000 ~name:"Lin Bytes test with Domain";

src/io/lin_tests_thread.ml

@@ -2,7 +2,7 @@
 (*                      Tests of In_channels                              *)
 (* ********************************************************************** *)
 
-module IC_thread = Lin_thread.Make(Lin_tests_spec_io.ICConf) [@@alert "-experimental"]
+module IC_thread = Lin_thread.Make(Lin_tests_spec_io.ICConf)
 
 let _ =
   QCheck_base_runner.run_tests_main [

src/neg_tests/CList.ml

@@ -14,6 +14,18 @@ let rec add_node list_head n =
   else
     add_node list_head n
 
+let rec add_node_thread list_head n =
+  (* try to add a new node to head *)
+  let old_head = Atomic.get list_head in
+  if Atomic.get list_head = old_head then begin
+    (* introduce bug: as above but context switch can happen when allocating *)
+    let new_node = { value = n ; next = (Some old_head) } in
+    Atomic.set list_head new_node;
+    true
+  end
+  else
+    add_node_thread list_head n
+
 let list_init i = Atomic.make { value = i ; next = None }
 
 let member list_head n =

src/neg_tests/dune

@@ -46,10 +46,26 @@
 )
 
 (test
- (name stm_tests_conclist)
- (modules stm_tests_conclist)
+ (name stm_tests_clist_sequential)
+ (modules stm_tests_clist_spec stm_tests_clist_sequential)
  (package multicoretests)
- (libraries CList qcheck-stm.sequential qcheck-stm.domain)
+ (libraries CList qcheck-stm.sequential)
+ (action (run %{test} --verbose))
+)
+
+(test
+ (name stm_tests_clist_domain)
+ (modules stm_tests_clist_spec stm_tests_clist_domain)
+ (package multicoretests)
+ (libraries CList qcheck-stm.domain)
+ (action (run %{test} --verbose))
+)
+
+(test
+ (name stm_tests_clist_thread)
+ (modules stm_tests_clist_spec stm_tests_clist_thread)
+ (package multicoretests)
+ (libraries CList qcheck-stm.thread)
  (action (run %{test} --verbose))
 )
 
@@ -84,8 +100,7 @@
  (package multicoretests)
  (flags (:standard -w -27))
  (libraries lin_tests_common qcheck-lin.thread)
- ; (action (run %{test} --verbose))
- (action (progn))
+ (action (run %{test} --verbose))
 )
 
 (test
@@ -115,7 +130,8 @@
  (package multicoretests)
  (flags (:standard -w -27))
  (libraries lin_internal_tests_common qcheck-lin.thread)
- (action (run %{test} --verbose))
+ ; (action (run %{test} --verbose))
+ (action (progn))
 )
 
 (test

src/neg_tests/lin_internal_tests_common.ml

@@ -188,13 +188,20 @@ end
 (* ********************************************************************** *)
 (*                  Tests of the buggy concurrent list CList              *)
 (* ********************************************************************** *)
-module CLConf (T : sig
-                     type t
-                     val zero : t
-                     val of_int : int -> t
-                     val to_string : t -> string
-                     val shrink : t Shrink.t
-                   end) =
+module CLConf
+    (CList : sig
+       type 'a conc_list
+       val list_init : 'a -> 'a conc_list Atomic.t
+       val add_node: 'a conc_list Atomic.t -> 'a -> bool
+       val member : 'a conc_list Atomic.t -> 'a -> bool
+     end)
+    (T : sig
+       type t
+       val zero : t
+       val of_int : int -> t
+       val to_string : t -> string
+       val shrink : t Shrink.t
+     end) =
 struct
   module Lin = Lin.Internal [@alert "-internal"]
 

src/neg_tests/lin_internal_tests_domain.ml

@@ -2,8 +2,8 @@ open Lin_internal_tests_common
 
 module RT_int_domain = Lin_domain.Make_internal(RConf_int) [@alert "-internal"]
 module RT_int64_domain = Lin_domain.Make_internal(RConf_int64) [@alert "-internal"]
-module CLT_int_domain = Lin_domain.Make_internal(CLConf (Int)) [@alert "-internal"]
-module CLT_int64_domain = Lin_domain.Make_internal(CLConf (Int64)) [@alert "-internal"]
+module CLT_int_domain = Lin_domain.Make_internal(CLConf(CList)(Int)) [@alert "-internal"]
+module CLT_int64_domain = Lin_domain.Make_internal(CLConf(CList)(Int64)) [@alert "-internal"]
 
 (** This is a driver of the negative tests over the Domain module *)
 

src/neg_tests/lin_internal_tests_effect.ml

@@ -92,7 +92,7 @@ module RT_int64'_effect = Lin_effect.Make_internal(RConf_int64') [@alert "-inter
 
 module CLConf_int' =
 struct
-  include CLConf(Int)
+  include CLConf(CList)(Int)
   type res =
     | RAdd_node of (bool, exn) result
     | RMember of bool
@@ -116,12 +116,12 @@ struct
     | Add_node i -> RAdd_node (try Lin_effect.yield (); Ok (CList.add_node r i) with exn -> Error exn)
     | Member i   -> RMember (CList.member r i)
 end
-module CLT_int_effect = Lin_effect.Make_internal(CLConf (Int)) [@alert "-internal"]
+module CLT_int_effect = Lin_effect.Make_internal(CLConf(CList)(Int)) [@alert "-internal"]
 module CLT_int'_effect = Lin_effect.Make_internal(CLConf_int') [@alert "-internal"]
 
 module CLConf_int64' =
 struct
-  include CLConf(Int64)
+  include CLConf(CList)(Int64)
   type res =
     | RAdd_node of (bool, exn) result
     | RMember of bool
@@ -145,7 +145,7 @@ struct
     | Add_node i -> RAdd_node (try Lin_effect.yield (); Ok (CList.add_node r i) with exn -> Error exn)
     | Member i   -> RMember (CList.member r i)
 end
-module CLT_int64_effect = Lin_effect.Make_internal(CLConf(Int64)) [@alert "-internal"]
+module CLT_int64_effect = Lin_effect.Make_internal(CLConf(CList)(Int64)) [@alert "-internal"]
 module CLT_int64'_effect = Lin_effect.Make_internal(CLConf_int64') [@alert "-internal"]
 ;;
 QCheck_base_runner.run_tests_main