package dscheck
Traced Atomics
Install
Dune Dependency
Authors
Maintainers
Sources
dscheck-0.1.0.tbz
sha256=ce8a2e15925c529ef5c9e96e55bd712d420c705bfdf4ea647104021e43d329c2
sha512=a8c5bf477190b88d4c063efd84392af88fdbd484c4da9affbceae79d96c75ebf15d0623fb8b79b3316d4d822e262ea22f2b949c619c17b6e500442500e7c9911
Description
Published: 17 Nov 2022
README
dscheck
— tool for testing concurrent OCaml programs
Experimental model checker for testing concurrent algorithms based on Dynamic Partial-Order Reduction for Model Checking Software. At the core, dscheck
runs each test numerous times, exhaustively trying every single interleaving of atomic operations. User-provided assertions are run at the end of every execution.
Usage
Dscheck can be installed from opam
: opam install dscheck
. Sample usage on a naive counter is shown below.
module Atomic = Dscheck.TracedAtomic
(* tested implementation needs to use dscheck's atomic module *)
let test_counter () =
let counter = Atomic.make 0 in
let incr () = Atomic.set counter (Atomic.get counter + 1) in
Atomic.spawn incr;
Atomic.spawn incr;
Atomic.final (fun () -> Atomic.check (fun () -> Atomic.get counter == 2))
This is a classic example of a race condition with two threads trying to increment a counter without synchronisation. When the race occurs, one of the updates is lost. dscheck
finds the interleaving that leads to that:
Found assertion violation at run 12:
Process 0: start
Process 0: get 1
Process 1: start
Process 1: get 1
Process 0: set 1
Process 1: set 1
Fatal error: exception File "src/tracedAtomic.ml", line 266, characters 6-12: Assertion failed
Contributions
Contributions are appreciated! Please create issues/PRs to this repo.
Dependencies (4)
- oseq
- containers
-
dune
>= "2.9"
-
ocaml
>= "5.0.0"
Dev Dependencies (1)
-
odoc
with-doc
Used by (4)
-
eio
>= "0.8.1"
-
lockfree
>= "0.3.0"
-
saturn
< "0.5.0"
-
saturn_lockfree
< "0.5.0"
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page