Initial STM precond fix, add Domainslib.Chan tests

lib/STM.ml

@@ -167,7 +167,35 @@ struct
     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 rec check_obs pref cs1 cs2 s = match pref with
+  (* 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.precond c s &&
+        let s' = Spec.next_state c s in
+        all_interleavings_ok pref' cs1 cs2 s'
+    | [] ->
+        match cs1,cs2 with
+        | [],[] -> true
+        | [],c2::cs2' ->
+            Spec.precond c2 s &&
+            let s' = Spec.next_state c2 s in
+            all_interleavings_ok pref cs1 cs2' s'
+        | c1::cs1',[] ->
+            Spec.precond c1 s &&
+            let s' = Spec.next_state c1 s in
+            all_interleavings_ok pref cs1' cs2 s'
+        | c1::cs1',c2::cs2' ->
+            (Spec.precond c1 s &&
+             let s' = Spec.next_state c1 s in
+             all_interleavings_ok pref cs1' cs2 s')
+            &&
+            (Spec.precond c2 s &&
+             let s' = Spec.next_state c2 s in
+             all_interleavings_ok pref cs1 cs2' s')
+
+  let rec check_obs pref cs1 cs2 s =
+    match pref with
     | p::pref' ->
        let b,s' = check_and_next p s in
        b && check_obs pref' cs1 cs2 s'
@@ -193,7 +221,7 @@ struct
     let open Iter in
     let shrink_cmd = Option.value Spec.(arb_cmd init_state).shrink ~default:Shrink.nil in
     Shrink.filter
-      (fun (seq,p1,p2) -> cmds_ok Spec.init_state (seq@p1) && cmds_ok Spec.init_state (seq@p2))
+      (fun (seq,p1,p2) -> all_interleavings_ok seq p1 p2 Spec.init_state)
       (fun (seq,p1,p2) ->
         (map (fun seq' -> (seq',p1,p2)) (Shrink.list ~shrink:shrink_cmd seq))
         <+>
@@ -209,16 +237,18 @@ struct
     let seq_pref_gen = gen_cmds_size Spec.init_state (Gen.int_bound seq_len) 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 -> Spec.next_state c st) Spec.init_state seq_pref in
-           let par = gen_cmds_size spawn_state (Gen.int_bound par_len) in
-           map2 (fun par1 par2 -> (seq_pref,par1,par2)) par par) in
+           let par_len1 = dbl_plen/2 in
+           let par_gen1 = gen_cmds_size spawn_state (return par_len1) in
+           let par_gen2 = gen_cmds_size spawn_state (return (dbl_plen - par_len1)) in
+           triple (return seq_pref) par_gen1 par_gen2) in
     make ~print:(print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple
 
   (* Parallel agreement property based on [Domain] *)
   let agree_prop_par =
     (fun (seq_pref,cmds1,cmds2) ->
-      assume (cmds_ok Spec.init_state (seq_pref@cmds1));
-      assume (cmds_ok Spec.init_state (seq_pref@cmds2));
+      assume (all_interleavings_ok seq_pref cmds1 cmds2 Spec.init_state);
       let sut = Spec.init_sut () in
       let pref_obs = interp_sut_res sut seq_pref in
       let wait = Atomic.make true in
@@ -237,7 +267,8 @@ struct
   let agree_test_par ~count ~name =
     let rep_count = 25 in
     let seq_len,par_len = 20,12 in
-    Test.make ~retries:15 ~count ~name:("parallel " ^ name)
+    let max_gen = 3*count in (* precond filtering may require extra generation: max. 3*count though *)
+    Test.make ~retries:15 ~max_gen ~count ~name:("parallel " ^ name)
       (arb_cmds_par seq_len par_len)
       (repeat rep_count agree_prop_par) (* 25 times each, then 25 * 15 times when shrinking *)
 end

src/domainslib/chan_tests.ml

@@ -0,0 +1,81 @@
+open QCheck
+open Domainslib
+
+(** This is a parallel test of Domainslib.Chan *)
+
+module ChConf =
+struct
+  type state = int list
+  type sut = int Domainslib.Chan.t
+  type cmd =
+    | Send of int
+    | Send_poll of int
+    | Recv
+    | Recv_poll [@@deriving show { with_path = false }]
+
+  let capacity = 8
+
+  let arb_cmd s =
+    let int_gen = Gen.nat in
+    QCheck.make ~print:show_cmd
+      (if s=[]
+       then
+         Gen.oneof
+           [Gen.map (fun i -> Send i) int_gen;
+	    Gen.map (fun i -> Send_poll i) int_gen;
+	    Gen.return Recv_poll] (* don't generate blocking Recv cmds on an empty channel *)
+       else
+       if List.length s >= capacity
+       then
+         Gen.oneof
+           [Gen.map (fun i -> Send_poll i) int_gen;
+            Gen.return Recv;
+	    Gen.return Recv_poll] (* don't generate blocking Send cmds on a full channel *)
+       else
+         Gen.oneof
+           [Gen.map (fun i -> Send i) int_gen;
+	    Gen.map (fun i -> Send_poll i) int_gen;
+            Gen.return Recv;
+	    Gen.return Recv_poll])
+  let init_state  = []
+  let init_sut () = Chan.make_bounded capacity
+  let cleanup _   = ()
+
+  let next_state c s = match c with
+    | Send i      -> if List.length s < capacity then s@[i] else s
+    | Send_poll i -> if List.length s < capacity then s@[i] else s
+    | Recv        -> begin match s with [] -> [] | _::s' -> s' end
+    | Recv_poll   -> begin match s with [] -> [] | _::s' -> s' end
+
+  let precond c s = match c,s with
+    | Recv,   [] -> false
+    | Send _, _  -> List.length s < capacity
+    | _,      _  -> true
+
+  type res = RSend | RSend_poll of bool | RRecv of int | RRecv_poll of int option [@@deriving show { with_path = false }]
+
+  let run c chan =
+    match c with
+    | Send i       -> (Chan.send chan i; RSend)
+    | Send_poll i  -> RSend_poll (Chan.send_poll chan i)
+    | Recv         -> RRecv (Chan.recv chan)
+    | Recv_poll    -> RRecv_poll (Chan.recv_poll chan)
+
+  let postcond c s res = match c,res with
+    | Send _,      RSend          -> (List.length s < capacity)
+    | Send_poll _, RSend_poll res -> res = (List.length s < capacity)
+    | Recv,        RRecv res      -> (match s with [] -> false | res'::_ -> res=res')
+    | Recv_poll,   RRecv_poll opt -> (match s with [] -> None | res'::_ -> Some res') = opt
+    | _,_ -> false
+end
+
+
+module ChT = STM.Make(ChConf)
+;;
+Util.set_ci_printing ()
+;;
+QCheck_runner.run_tests_main
+  (let count,name = 1000,"global Domainslib.Chan test" in [
+      ChT.agree_test     ~count ~name;
+      ChT.agree_test_par ~count ~name;
+    ])

src/domainslib/dune

@@ -45,3 +45,18 @@
  (package multicoretests)
  (deps task_parallel.exe)
  (action (run ./%{deps} --no-colors --verbose)))
+
+
+;; STM test of Domainslib.Chan
+
+(executable
+ (name chan_tests)
+ (modes native byte)
+ (modules chan_tests)
+ (libraries util qcheck STM domainslib)
+ (preprocess (pps ppx_deriving.show)))
+
+(rule
+ (alias runtest)
+ (deps chan_tests.exe)
+ (action (run ./%{deps} --no-colors --verbose)))

src/lazy/lazy_stm_test.ml

@@ -107,7 +107,7 @@ module LTfromfun = STM.Make(struct
 Util.set_ci_printing ()
 ;;
 QCheck_runner.run_tests_main
-  (let count = 100 in
+  (let count = 200 in
    [LTlazy.agree_test        ~count ~name:"lazy test";
     LTfromval.agree_test     ~count ~name:"lazy test from_val";
     LTfromfun.agree_test     ~count ~name:"lazy test from_fun";