Merge pull request #34 from bartoszmodelski/dscheck-tests

dscheck tests for current data structures.

Author: lyrm

atomic/README.md

@@ -0,0 +1,12 @@
+# Virtual atomic 
+
+Virtual atomic lets us vary the implementation of `Atomic` module. The are two options: 
+
+* `Stdlib.Atomic` - the standard library implementation. 
+* `Dscheck.TracedAtomic` - wrapper provided by a model checker ([DSCheck](https://github.com/ocaml-multicore/dscheck)) for exhaustively testing all interleavings.  
+
+## User perspective 
+
+`Lockfree` defaults to standard library implementation, thus user does not need to do select anything explicitely to use our data structures. 
+
+However, it can be useful to write your own DSCheck tests (e.g. when composing two lock-free structures). In such a case, import `lockfree.atomic_traced` to override the default choice. See [../test/dscheck/dune](../test/dscheck/dune) for example.

atomic/dune

@@ -0,0 +1,5 @@
+(library
+ (name virtual_atomic)
+ (public_name lockfree.virtual_atomic)
+ (virtual_modules virtual_atomic)
+ (default_implementation atomic_stdlib))

atomic/stdlib/dune

@@ -0,0 +1,4 @@
+(library
+ (name atomic_stdlib)
+ (public_name lockfree.atomic_stdlib)
+ (implements virtual_atomic))

atomic/stdlib/virtual_atomic.ml

@@ -0,0 +1,3 @@
+module Atomic = struct
+  include Stdlib.Atomic
+end

atomic/traced/dune

@@ -0,0 +1,5 @@
+(library
+ (name atomic_traced)
+ (public_name lockfree.atomic_traced)
+ (libraries dscheck)
+ (implements virtual_atomic))

atomic/traced/virtual_atomic.ml

@@ -0,0 +1,3 @@
+module Atomic = struct
+  include Dscheck.TracedAtomic
+end

atomic/virtual_atomic.mli

@@ -0,0 +1,35 @@
+(** Copied from standard library. *)
+
+module Atomic : sig
+  type !'a t
+  (** An atomic (mutable) reference to a value of type ['a]. *)
+
+  val make : 'a -> 'a t
+  (** Create an atomic reference. *)
+
+  val get : 'a t -> 'a
+  (** Get the current value of the atomic reference. *)
+
+  val set : 'a t -> 'a -> unit
+  (** Set a new value for the atomic reference. *)
+
+  val exchange : 'a t -> 'a -> 'a
+  (** Set a new value for the atomic reference, and return the current value. *)
+
+  val compare_and_set : 'a t -> 'a -> 'a -> bool
+  (** [compare_and_set r seen v] sets the new value of [r] to [v] only
+      if its current value is physically equal to [seen] -- the
+      comparison and the set occur atomically. Returns [true] if the
+      comparison succeeded (so the set happened) and [false]
+      otherwise. *)
+
+  val fetch_and_add : int t -> int -> int
+  (** [fetch_and_add r n] atomically increments the value of [r] by [n],
+      and returns the current value (before the increment). *)
+
+  val incr : int t -> unit
+  (** [incr r] atomically increments the value of [r] by [1]. *)
+
+  val decr : int t -> unit
+  (** [decr r] atomically decrements the value of [r] by [1]. *)
+end

lockfree.opam

@@ -13,7 +13,9 @@ depends: [
   "dune" {>= "3.0"}
   "qcheck" {with-test & >= "0.18.1"}
   "qcheck-alcotest" {with-test & >= "0.18.1"}
+  "alcotest" {>= "1.6.0"}
   "yojson" {>= "2.0.2"}
+  "dscheck" {>= "0.0.1"}
 ]
 depopts: []
 build: ["dune" "build" "-p" name "-j" jobs]

src/dune

@@ -1,3 +1,4 @@
 (library
  (name lockfree)
- (public_name lockfree))
+ (public_name lockfree)
+ (libraries dscheck virtual_atomic))

src/mpsc_queue.ml

@@ -7,6 +7,8 @@
    It is simplified slightly because we don't need multiple consumers.
    Therefore [head] is not atomic. *)
 
+open Virtual_atomic
+
 exception Closed
 
 module Node : sig

src/spsc_queue.ml

@@ -21,6 +21,8 @@
  * https://dl.acm.org/doi/pdf/10.1145/3437801.3441583
  *)
 
+open Virtual_atomic
+
 type 'a t = {
   array : 'a Option.t Array.t;
   tail : int Atomic.t;

src/ws_deque.ml

@@ -27,6 +27,8 @@
  *   https://dl.acm.org/doi/abs/10.1145/2442516.2442524
  *)
 
+open Virtual_atomic
+
 module type S = sig
   type 'a t
 

test/dscheck/README.md

@@ -0,0 +1 @@
+This directory contains tests using [DSCheck](https://github.com/ocaml-multicore/dscheck). DSCheck lets us verify that relevant invariants indeed hold under all possible interleavings. 

test/dscheck/dune

@@ -0,0 +1,14 @@
+(test
+ (name spsc_queue)
+ (libraries lockfree lockfree.atomic_traced dscheck alcotest)
+ (modules spsc_queue))
+
+(test
+ (name ws_deque)
+ (libraries lockfree lockfree.atomic_traced dscheck alcotest)
+ (modules ws_deque))
+
+(test
+ (name mpsc_queue)
+ (libraries lockfree lockfree.atomic_traced dscheck alcotest)
+ (modules mpsc_queue))

test/dscheck/mpsc_queue.ml

@@ -0,0 +1,67 @@
+module Atomic = Dscheck.TracedAtomic
+open Lockfree
+
+let drain queue =
+  let remaining = ref 0 in
+  while not (Mpsc_queue.is_empty queue) do
+    remaining := !remaining + 1;
+    assert (Option.is_some (Mpsc_queue.pop queue))
+  done;
+  !remaining
+
+let producer_consumer () =
+  Atomic.trace (fun () ->
+      let queue = Mpsc_queue.create () in
+      let items_total = 4 in
+
+      (* producer *)
+      Atomic.spawn (fun () ->
+          for _ = 1 to items_total - 1 do
+            Mpsc_queue.push queue 0
+          done);
+
+      (* consumer *)
+      let popped = ref 0 in
+      Atomic.spawn (fun () ->
+          Mpsc_queue.push_head queue 1;
+          for _ = 1 to items_total do
+            match Mpsc_queue.pop queue with
+            | None -> ()
+            | Some _ -> popped := !popped + 1
+          done);
+
+      (* checks*)
+      Atomic.final (fun () ->
+          Atomic.check (fun () ->
+              let remaining = drain queue in
+              !popped + remaining = items_total)))
+
+let two_producers () =
+  Atomic.trace (fun () ->
+      let queue = Mpsc_queue.create () in
+      let items_total = 4 in
+
+      (* producers *)
+      for _ = 1 to 2 do
+        Atomic.spawn (fun () ->
+            for _ = 1 to items_total / 2 do
+              Mpsc_queue.push queue 0
+            done)
+      done;
+
+      (* checks*)
+      Atomic.final (fun () ->
+          Atomic.check (fun () ->
+              let remaining = drain queue in
+              remaining = items_total)))
+
+let () =
+  let open Alcotest in
+  run "mpsc_queue_dscheck"
+    [
+      ( "basic",
+        [
+          test_case "1-producer-1-consumer" `Slow producer_consumer;
+          test_case "2-producers" `Slow two_producers;
+        ] );
+    ]

test/dscheck/spsc_queue.ml

@@ -0,0 +1,71 @@
+open Lockfree
+module Atomic = Dscheck.TracedAtomic
+
+let create_test ~shift_by () =
+  let queue = Spsc_queue.create ~size_exponent:2 in
+  let items_count = 3 in
+
+  (* shift the queue, that helps testing overlap handling *)
+  for _ = 1 to shift_by do
+    Spsc_queue.push queue (-1);
+    assert (Option.is_some (Spsc_queue.pop queue))
+  done;
+
+  (* enqueuer *)
+  Atomic.spawn (fun () ->
+      for i = 1 to items_count do
+        Spsc_queue.push queue i
+      done);
+
+  (* dequeuer *)
+  let dequeued = ref 0 in
+  Atomic.spawn (fun () ->
+      for _ = 1 to items_count + 1 do
+        match Spsc_queue.pop queue with
+        | None -> ()
+        | Some v ->
+            assert (v = !dequeued + 1);
+            dequeued := v
+      done);
+
+  (* ending assertions *)
+  Atomic.final (fun () ->
+      Atomic.check (fun () -> Spsc_queue.size queue == items_count - !dequeued))
+
+let with_trace ?(shift_by = 0) f () = Atomic.trace (fun () -> f ~shift_by ())
+
+let size_linearizes_with_1_thr () =
+  Atomic.trace (fun () ->
+      let queue = Spsc_queue.create ~size_exponent:4 in
+      Spsc_queue.push queue (-1);
+      Spsc_queue.push queue (-1);
+
+      Atomic.spawn (fun () ->
+          for _ = 1 to 4 do
+            Spsc_queue.push queue (-1)
+          done);
+
+      let size = ref 0 in
+      Atomic.spawn (fun () ->
+          assert (Option.is_some (Spsc_queue.pop queue));
+          size := Spsc_queue.size queue);
+
+      Atomic.final (fun () -> Atomic.check (fun () -> 1 <= !size && !size <= 5)))
+
+let () =
+  let open Alcotest in
+  run "Spsc_queue_dscheck"
+    [
+      ("basic", [ test_case "simple-test" `Slow (with_trace create_test) ]);
+      ( "wrap-arounds",
+        let with_shift s =
+          test_case
+            (Printf.sprintf "shift-by-%d" s)
+            `Slow
+            (with_trace ~shift_by:s create_test)
+        in
+        [ with_shift 1; with_shift 6; with_shift 11 ] );
+      ( "size",
+        [ test_case "linearizes-with-1-thr" `Slow size_linearizes_with_1_thr ]
+      );
+    ]

test/dscheck/ws_deque.ml

@@ -0,0 +1,79 @@
+module Atomic = Dscheck.TracedAtomic
+open Lockfree
+
+let drain_remaining queue =
+  let remaining = ref 0 in
+  (try
+     while true do
+       Ws_deque.M.pop queue |> ignore;
+       remaining := !remaining + 1
+     done
+   with _ -> ());
+  !remaining
+
+let owner_stealer () =
+  Atomic.trace (fun () ->
+      let queue = Ws_deque.M.create () in
+      let total_items = 3 in
+
+      let popped = ref 0 in
+
+      (* owner thr *)
+      Atomic.spawn (fun () ->
+          for _ = 1 to total_items do
+            Ws_deque.M.push queue 0
+          done;
+          for _ = 1 to total_items / 2 do
+            match Ws_deque.M.pop queue with
+            | exception _ -> ()
+            | _ -> popped := !popped + 1
+          done);
+
+      (* stealer *)
+      Atomic.spawn (fun () ->
+          for _ = 1 to total_items / 2 do
+            match Ws_deque.M.steal queue with
+            | exception _ -> ()
+            | _ -> popped := !popped + 1
+          done);
+
+      Atomic.final (fun () ->
+          Atomic.check (fun () ->
+              let remaining = drain_remaining queue in
+              remaining + !popped == total_items)))
+
+let popper_stealer () =
+  Atomic.trace (fun () ->
+      let queue = Ws_deque.M.create () in
+      let total_items = 3 in
+      for _ = 1 to total_items do
+        Ws_deque.M.push queue 0
+      done;
+
+      (* stealers *)
+      let popped = ref 0 in
+      let stealer () =
+        match Ws_deque.M.steal queue with
+        | exception _ -> ()
+        | _ -> popped := !popped + 1
+      in
+      Atomic.spawn stealer |> ignore;
+      Atomic.spawn stealer |> ignore;
+
+      Atomic.final (fun () ->
+          Atomic.check (fun () ->
+              let remaining = drain_remaining queue in
+              remaining = 1 && !popped = 2)))
+
+let () =
+  let open Alcotest in
+  run "ws_deque_dscheck"
+    [
+      ( "basic",
+        [
+          test_case "1-owner-1-stealer" `Slow owner_stealer;
+          test_case "1-pusher-2-stealers" `Slow popper_stealer;
+          (* we'd really want to test cases with more threads here,
+             but dscheck is not optimized enough for that yet *)
+        ] );
+    ]