tests

Author: bartoszmodelski

dscheck.opam

@@ -3,13 +3,14 @@ opam-version: "2.0"
 synopsis: "Traced Atomics"
 maintainer: ["Sadiq Jaffer"]
 authors: ["Sadiq Jaffer"]
-homepage: "https://github.com/ocaml-multicore/dscheck"
-bug-reports: "https://github.com/ocaml-multicore/dscheck/issues"
+homepage: "https://github.com/sadiqj/dscheck"
+bug-reports: "https://github.com/sadiqj/dscheck/issues"
 depends: [
   "ocaml" {>= "5.0.0"}
   "dune" {>= "2.9"}
   "containers"
   "oseq"
+  "alcotest" {>= "1.6.0"}
   "odoc" {with-doc}
 ]
 build: [
@@ -28,4 +29,4 @@ build: [
   ]
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
-dev-repo: "git+https://github.com/ocaml-multicore/dscheck.git"
+dev-repo: "git+https://github.com/sadiqj/dscheck.git"

dune-project

@@ -10,5 +10,6 @@
 (package
  (name dscheck)
  (synopsis "Traced Atomics")
- (depends (ocaml (>= 5.0.0)) dune containers oseq))
+ (depends (ocaml (>= 5.0.0)) dune containers oseq (alcotest (>= 1.6.0))))
+
 

src/tracedAtomic.ml

@@ -267,8 +267,17 @@ let check f =
   end;
   tracing := tracing_at_start
 
+let reset_state () = 
+  finished_processes := 0; 
+  atomics_counter := 1;
+  num_runs := 0;
+  schedule_for_checks := [];
+  CCVector.clear processes;
+;;
+
 
 let trace func =
+  reset_state ();
   let empty_state = do_run func [(0, Start, None)] :: [] in
   let empty_clock = IntMap.empty in
   let empty_last_access = IntMap.empty in

tests/dune

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

tests/test_list.ml

@@ -2,46 +2,66 @@ module Atomic = Dscheck.TracedAtomic
 
 (* a simple concurrent list *)
 
-type conc_list = { value: int; next: conc_list option }
+type conc_list = { value : int; next : conc_list option }
 
-let rec add_node list_head n =
+let rec add_node_naive list_head n =
   (* try to add a new node to head *)
   let old_head = Atomic.get list_head in
-  let new_node = { value = n ; next = (Some old_head) } in
-    (* introduce bug *)
-    if Atomic.get list_head = old_head then begin
-      Atomic.set list_head new_node;
-      true
-    end
-    else
-      add_node list_head n
+  let new_node = { value = n; next = Some old_head } in
+  (* introduce bug *)
+  if Atomic.get list_head = old_head then (
+    Atomic.set list_head new_node;
+    true)
+  else add_node_naive list_head n
+
+let rec add_node_safe list_head n =
+  let old_head = Atomic.get list_head in
+  let new_node = { value = n; next = Some old_head } in
+  if Atomic.compare_and_set list_head old_head new_node then true
+  else add_node_safe list_head n
 
 let check_node list_head n =
   let rec check_from_node node =
     match (node.value, node.next) with
-    | (v, _) when v = n -> true
-    | (_, None) -> false
-    | (_ , Some(next_node)) -> begin
-      check_from_node next_node
-    end
+    | v, _ when v = n -> true
+    | _, None -> false
+    | _, Some next_node -> check_from_node next_node
   in
   (* try to find the node *)
-    check_from_node (Atomic.get list_head)
-
-let add_and_check list_head n () =
-  assert(add_node list_head n);
-  assert(check_node list_head n)
+  check_from_node (Atomic.get list_head)
 
-let create_test upto () =
-  let list_head = Atomic.make { value = 0 ; next = None } in
+let create_test add_node_f upto () =
+  let list_head = Atomic.make { value = 0; next = None } in
   for x = 1 to upto do
-    Atomic.spawn (add_and_check list_head x);
+    Atomic.spawn (fun () ->
+        assert (add_node_f list_head x);
+        assert (check_node list_head x))
   done;
   Atomic.final (fun () ->
-    for x = 1 to upto do
-      Atomic.check(fun () -> check_node list_head x)
-    done
-  )
+      for x = 1 to upto do
+        Atomic.check (fun () -> check_node list_head x)
+      done)
+
+let test_list_naive_single_domain () =
+  Atomic.trace (create_test add_node_naive 1)
+
+let test_list_naive domains () =
+  match Atomic.trace (create_test add_node_naive domains) with
+  | exception _ -> ()
+  | _ -> failwith "expected failure"
+
+let test_list_safe () = Atomic.trace (create_test add_node_safe 3)
+(* 4 takes over 10 Gb of RAM *)
 
 let () =
-  Atomic.trace (create_test 8)
+  let open Alcotest in
+  run "dscheck"
+    [
+      ( "list",
+        [
+          test_case "naive-1-domain" `Quick (test_list_naive_single_domain);
+          test_case "naive-2-domains" `Quick (test_list_naive 8);
+          test_case "naive-8-domains" `Quick (test_list_naive 8);
+          test_case "safe" `Quick test_list_safe;
+        ] );
+    ]

tests/test_naive_counter.ml

@@ -1,10 +1,26 @@
 module Atomic = Dscheck.TracedAtomic
 
-let test_counter () =
+let counter incr () =
   let counter = Atomic.make 0 in
-  let incr () = Atomic.set counter (Atomic.get counter + 1) in 
-  Atomic.spawn incr;
-  Atomic.spawn incr;
+  Atomic.spawn (fun () -> incr counter);
+  Atomic.spawn (fun () -> incr counter);
   Atomic.final (fun () -> Atomic.check (fun () -> Atomic.get counter == 2))
 
-let () = Atomic.trace test_counter
+let test_naive_counter () =
+  let naive_incr counter = Atomic.set counter (Atomic.get counter + 1) in
+  match Atomic.trace (counter naive_incr) with
+  | exception _ -> ()
+  | _ -> failwith "expected failure"
+
+let test_safe_counter () = Atomic.trace (counter Atomic.incr)
+
+let () =
+  let open Alcotest in
+  run "dscheck"
+    [
+      ( "counter",
+        [
+          test_case "naive" `Quick test_naive_counter;
+          test_case "safe" `Quick test_safe_counter;
+        ] );
+    ]