I’m happy to share release 0.2 of qcheck-lin and qcheck-stm for black-box property-based testing.
qcheck-lin requires little more than an interface description. It allows to test a library for sequential consistency, that is, whether results obtained from using it in parallel agree with some linear, single domain execution.
qcheck-stm is a model-based, state-machine framework for both sequential and parallel testing. It allows to test an imperative interface against a pure model description, and thereby allows to express and test intended behaviour beyond a signature description.
For example, here’s a minimal qcheck-lin test of a selection of the StdlibHashtbl interface:
module HashtblSig =
struct
type t = (char, int) Hashtbl.t
let init () = Hashtbl.create ~random:false 42
let cleanup _ = ()
open Lin
let a,b = char_printable,nat_small
let api =
[ val_ "Hashtbl.add" Hashtbl.add (t @-> a @-> b @-> returning unit);
val_ "Hashtbl.remove" Hashtbl.remove (t @-> a @-> returning unit);
val_ "Hashtbl.find" Hashtbl.find (t @-> a @-> returning_or_exc b);
val_ "Hashtbl.mem" Hashtbl.mem (t @-> a @-> returning bool);
val_ "Hashtbl.length" Hashtbl.length (t @-> returning int); ]
end
module HT = Lin_domain.Make(HashtblSig)
;;
QCheck_base_runner.run_tests_main [
HT.lin_test ~count:1000 ~name:"Hashtbl DSL test";
]
Running this test quickly finds a minimal counterexample to illustrate that Hashtbl is not safe to use in parallel:
Messages for test Hashtbl DSL test:
Results incompatible with sequential execution
|
Hashtbl.add t '<' 0 : ()
|
.------------------------------------.
| |
Hashtbl.add t 'a' 0 : () Hashtbl.remove t '<' : ()
Hashtbl.length t : 0
We presented preliminary work on both these libraries at the OCaml Workshop 2022. The libraries furthermore underlie our continuing effort to test the multicore runtime of OCaml 5.x, and have helped identify several issues.
The 0.2 release adds a range of features and bugfixes, including support for OCaml 4.12.x, 4.13.x and 4.14.x without the Domain and Effect modes.
FYI, we just rolled out a 0.3 release of qcheck-lin, qcheck-stm, and qcheck-multicoretests-util: Release 0.3 · ocaml-multicore/multicoretests · GitHub
The release should be available in an opam repo near you shortly…
The 0.3 release brings 3 “usability improvements” to STM and Util and a Lin search improvement that should reduce memory allocation.
#400: Catch and delay exceptions in STM’s next_state for a nicer UX
#387: Reduce needless allocations in Lin’s sequential consistency search, as part of an Out_channel test cleanup
#379: Extend the set of Util.Pp pretty-printers and teach them to add break hints similar to ppx_deriving.show; teach to_show to generate truncated strings when $MCTUTILS_TRUNCATE environment variable is set
#368: Switch STM_domain.agree_prop_par_asym from using Semaphore.Binary to using an int Atomic.t which improves the error rate across platforms and backends
The testing libraries are useful for testing your OCaml code for parallelism safety:
qcheck-lin offer a low effort approach, requiring little more than type signatures of the target interface (example above)
qcheck-stm offers stronger correctness guarantees by comparing the observed behaviour to a functional model description - under both sequential and parallel usage.
The 0.4 release brings two new “stress test” functions and also adjusts the cmd list distribution of STM_sequential:
#415: Remove --verbose in internal mutable_set_v5 expect test to avoid a test failure on a slow machine
#443: Add Lin_domain.stress_test as a lighter stress test, not 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).
The biggest news in the 0.5 release is the addition of Util.Pp.pp_fun_ for printing function values generated with QCheck.To ensure quoted and escaped output for chars and strings, this required bumping the qcheck-core lower bound to the freshly released qcheck-core.0.23. This in turn, enabled a couple of other clean-ups:
#492: Also use the new, upstreamed Gen.exponential combinator in STM
#491: Require qcheck.0.23, simplify show functions by utilizing it, and update expect outputs accordingly
#486: Add Util.Pp.pp_fun_ printer for generated QCheck.fun_ functions
