dscheck
dscheck copied to clipboard
ocaml-multicore
Experimental model checker for testing concurrent algorithms
Many lock-free implementations use some randomness as an easy way to load balance without coordination. This may be a source of nondeterminism and DSCheck does not like it. For example,...
An attempt at improving the test coverage: 1. Randomly generate a little program that do atomic operations 2. Run this program with a random scheduler to sample the possible values...
Lots of real-world programs don't have lock-free property and it's often optimal that way. For one, because we mostly have a somewhat fair OS scheduler, and it does not make...
The core of DSCheck is closely following the design introduced in the [DPOR paper](https://www.cs.columbia.edu/~junfeng/17sp-e6121/papers/dpor.pdf), except for clock vectors, which are missing. This PR adds them. ## Motivation We want to...
(Follow-up on https://github.com/sadiqj/dscheck/pull/2 ) Sorry for the big dirty PR! I was inspired to optimize the backtracking and it now terminates in a few seconds on the examples that I...
I think I'm a bit confused about how to use dscheck. Perhaps other people will be too. The README says: > At the core, dscheck runs each test numerous times,...
When reading a trace, it's not super easy to follow the Atomic operations in the original code... It would help if the `filename:line` of each operation was available (with [`Printexc.get_callstack`](https://v2.ocaml.org/api/Printexc.html#VALget_callstack)...
It's a bit of a pain to adapt existing code to `dscheck` because it doesn't have the standard `Domain.spawn` type (and `Domain.join` is missing). It would be super neat if...
When debugging a failing case produced by `qcheck-lin`, it would be nice if `dscheck` could explore only the interleavings that produce the same intermediate values as reported by `qcheck-lin` (and...
(Builds on https://github.com/sadiqj/dscheck/pull/3 ) I'm not quite convince yet about this tiny change! The scheduler was exhausting the first thread before moving on, so I though it could be interesting...
Metadata
Owner
Metadata
Experimental model checker for testing concurrent algorithms