Merge pull request #5 from bartoszmodelski/readme

Add a simple readme

Author: sadiqj

CHANGES.md

@@ -0,0 +1,4 @@
+v0.1.0
+--------------------------
+
+* Initial experimental release.

LICENSE.md

@@ -0,0 +1,13 @@
+Copyright (c) 2022
+
+Permission to use, copy, modify, and/or distribute this software for any
+purpose with or without fee is hereby granted, provided that the above
+copyright notice and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

README.md

@@ -0,0 +1,39 @@
+# `dscheck` — tool for testing concurrent OCaml programs 
+
+Experimental model checker for testing concurrent algorithms based on [Dynamic Partial-Order Reduction for Model Checking Software](https://users.soe.ucsc.edu/~cormac/papers/popl05.pdf). 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
+
+Lockfree can be installed from `opam`: `opam install dscheck`. Sample usage on a [naive counter](tests/test_naive_counter.ml) is shown below. 
+
+```ocaml
+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.
+

tests/dune

@@ -1,4 +1,4 @@
-(executable
- (name test_list)
- (modules test_list)
+(executables
+ (names test_list test_naive_counter)
+ (modules test_list test_naive_counter)
  (libraries dscheck))

tests/test_naive_counter.ml

@@ -0,0 +1,10 @@
+module Atomic = Dscheck.TracedAtomic
+
+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))
+
+let () = Atomic.trace test_counter