Merge pull request #472 from ocaml-multicore/stm-cmd-list-dist

Reduce `STM.cmds_gen` list size

Author: jmid

CHANGES.md

@@ -8,6 +8,9 @@
   requiring an interleaving search.
 - #462: Add `STM_domain.stress_test_par`, similar to `Lin_domain.stress_test`
   for STM models.
+- #472: Switch `arb_cmds` to use an exponential distribution with a
+  mean of 10, avoiding lists of up to 10000 cmds in `STM_sequential`
+  (reported by @nikolaushuber).
 
 ## 0.3
 

lib/STM.ml

@@ -157,8 +157,19 @@ struct
       | None -> () (* no elem. shrinker provided *)
       | Some shrink -> Shrink.list_elems shrink l yield
 
+    let gen_cmds_size gen s size_gen = Gen.sized_size size_gen (gen_cmds gen s)
+
+    let exp_dist_gen mean =
+      let unit_gen = Gen.float_bound_inclusive 1.0 in
+      Gen.map (fun p -> -. mean *. (log p)) unit_gen
+
+    let cmd_list_size_dist mean =
+      let skew = 0.75 in (* to avoid too many empty cmd lists *)
+      Gen.map (fun p -> int_of_float (p +. skew)) (exp_dist_gen mean)
+
     let arb_cmds s =
-      let cmds_gen = Gen.sized (gen_cmds Spec.arb_cmd s) in
+      let mean = 10. in (* generate on average ~10 cmds, ignoring skew *)
+      let cmds_gen = gen_cmds_size Spec.arb_cmd s (cmd_list_size_dist mean) 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
       (match (Spec.arb_cmd s).print with
@@ -237,8 +248,6 @@ struct
           (let b2 = Spec.postcond c2 s res2 in
            b2 && check_obs pref cs1 cs2' (Spec.next_state c2 s))
 
-    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 =
       Option.value (arb state).shrink ~default:Shrink.nil @@ cmd

test/mutable_set_v4.expected.32

@@ -2,10 +2,10 @@
 
 --- Failure --------------------------------------------------------------------
 
-Test STM sequential tests failed (13 shrink steps):
+Test STM sequential tests failed (9 shrink steps):
 
-   Add (-605797133)
-   Remove (-605797133)
+   Add (-923247292)
+   Remove (-923247292)
    Cardinal
 
 
@@ -15,8 +15,8 @@ Messages for test STM sequential tests:
 
   Results incompatible with model
 
-   Add (-605797133) : ()
-   Remove (-605797133) : Some (-605797133)
+   Add (-923247292) : ()
+   Remove (-923247292) : Some (-923247292)
    Cardinal : 1
 ================================================================================
 failure (1 tests failed, 0 tests errored, ran 1 tests)

test/mutable_set_v4.expected.64

@@ -2,7 +2,7 @@
 
 --- Failure --------------------------------------------------------------------
 
-Test STM sequential tests failed (13 shrink steps):
+Test STM sequential tests failed (11 shrink steps):
 
    Add (-3576245632788335623)
    Remove (-3576245632788335623)

test/mutable_set_v5.expected.32

@@ -4,8 +4,8 @@
 
 Test STM sequential tests failed (2 shrink steps):
 
-   Add (-942638288)
-   Remove (-942638288)
+   Add (-286715106)
+   Remove (-286715106)
    Cardinal
 
 
@@ -15,8 +15,8 @@ Messages for test STM sequential tests:
 
   Results incompatible with model
 
-   Add (-942638288) : ()
-   Remove (-942638288) : Some (-942638288)
+   Add (-286715106) : ()
+   Remove (-286715106) : Some (-286715106)
    Cardinal : 1
 ================================================================================
 failure (1 tests failed, 0 tests errored, ran 1 tests)

test/mutable_set_v5.expected.64

@@ -2,10 +2,10 @@
 
 --- Failure --------------------------------------------------------------------
 
-Test STM sequential tests failed (15 shrink steps):
+Test STM sequential tests failed (6 shrink steps):
 
-   Add (-3922091896265746428)
-   Remove (-3922091896265746428)
+   Add 3036269937054427589
+   Remove 3036269937054427589
    Cardinal
 
 
@@ -15,8 +15,8 @@ Messages for test STM sequential tests:
 
   Results incompatible with model
 
-   Add (-3922091896265746428) : ()
-   Remove (-3922091896265746428) : Some (-3922091896265746428)
+   Add 3036269937054427589 : ()
+   Remove 3036269937054427589 : Some (3036269937054427589)
    Cardinal : 1
 ================================================================================
 failure (1 tests failed, 0 tests errored, ran 1 tests)