checkpoint

.ocamlformat

@@ -1,2 +1,2 @@
 profile = default
-version = 0.24.1
+version = 0.25.1

src/tracedAtomic.ml

@@ -12,7 +12,6 @@ type _ Effect.t +=
   | FetchAndAdd : (int t * int) -> int Effect.t
 
 module IntSet = Set.Make (Int)
-
 module IntMap = Map.Make (Int)
 
 let _string_of_set s = IntSet.fold (fun y x -> string_of_int y ^ "," ^ x) s ""
@@ -194,10 +193,36 @@ type state_cell = {
 }
 
 let num_runs = ref 0
+let num_traces = ref 0
 
 (* we stash the current state in case a check fails and we need to log it *)
 let schedule_for_checks = ref []
 
+let print_trace () =
+  Printf.printf "-----------------------\n";
+  List.iter
+    (fun s ->
+      match s with
+      | last_run_proc, last_run_op, last_run_ptr ->
+          let var_name i =
+            let c = Char.chr (i + 97) in
+            let seq = Seq.cons c Seq.empty in
+            String.of_seq seq
+          in
+
+          let last_run_ptr =
+            Option.map (* string_of_int *) var_name last_run_ptr
+            |> Option.value ~default:""
+          in
+          let tabs =
+            List.init last_run_proc (fun _ -> "\t\t") |> String.concat ""
+          in
+          Printf.printf "%sP%d: %s %s\n" tabs last_run_proc
+            (atomic_op_str last_run_op)
+            last_run_ptr)
+    !schedule_for_checks;
+  Printf.printf "-----------------------\n%!"
+
 let do_run init_func init_schedule =
   init_func ();
   (*set up run *)
@@ -214,6 +239,8 @@ let do_run init_func init_schedule =
     | [] ->
         if !finished_processes == num_processes then (
           tracing := false;
+          print_trace ();
+          num_traces := !num_traces + 1;
           !final_func ();
           tracing := true)
     | (process_id_to_run, next_op, next_ptr) :: schedule ->
@@ -259,6 +286,172 @@ let do_run init_func init_schedule =
         backtrack = IntSet.empty;
       }
 
+let _set_to_str s =
+  IntSet.to_seq s |> List.of_seq |> List.map Int.to_string |> String.concat ", "
+
+let rec explore_source depth func state sleep =
+  (* sleep := IntSet.empty; *)
+  let s = last_element state in
+  (* Printf.printf "[depth=%d] explore (backtrack=[%s], sleep=[%s], enabled=[%s])\n%!" depth
+     (set_to_str s.backtrack) (set_to_str !sleep) (set_to_str s.enabled); *)
+  let p_maybe = IntSet.min_elt_opt (IntSet.diff s.enabled !sleep) in
+  match p_maybe with
+  | None -> () (* Printf.printf "[depth=%d] rtn\n%!" depth *)
+  | Some p ->
+      s.backtrack <- IntSet.singleton p;
+
+      while IntSet.(cardinal (diff s.backtrack !sleep)) > 0 do
+        (* Printf.printf "[depth=%d] loop (backtrack=[%s], sleep=[%s])\n%!" depth
+           (set_to_str s.backtrack) (set_to_str !sleep); *)
+        let p = IntSet.min_elt (IntSet.diff s.backtrack !sleep) in
+        let proc = List.nth s.procs p in
+
+        (* Printf.printf "[depth=%d]  p=%d, %s\n%!" depth p (atomic_op_str proc.op); *)
+        (* run *)
+        let state_top =
+          let schedule =
+            List.map (fun s -> (s.run_proc, s.run_op, s.run_ptr)) state
+            @ [ (p, proc.op, proc.obj_ptr) ]
+          in
+          do_run func schedule
+        in
+        assert (state_top.run_proc = p);
+        let new_state = state @ [ state_top ] in
+
+        let obj_ptr = Option.value proc.obj_ptr ~default:(-1) in
+        (* find reversible races *)
+        let reversible_races =
+          List.filter
+            (fun proc' ->
+              let run_ptr = Option.value proc'.run_ptr ~default:(-2) in
+              obj_ptr = run_ptr && proc'.run_proc <> p)
+            new_state
+        in
+        let reversible_races =
+          match reversible_races with
+          | [] -> []
+          | _ -> [ last_element reversible_races ]
+        in
+
+        (* Printf.printf "[depth=%d]   reversible races sz: %d\n%!" depth
+           (List.length reversible_races); *)
+        for i = 0 to List.length reversible_races - 1 do
+          let e = List.nth reversible_races i in
+          (* Printf.printf "[depth=%d]   inner loop, racing op: e=(q=%d, %s)\n%!"
+             depth e.run_proc (atomic_op_str e.run_op); *)
+          let found_e, prefix_rev, suffix_rev =
+            List.fold_left
+              (fun (seen_e, prefix, suffix) proc' ->
+                if seen_e then (seen_e, prefix, proc' :: suffix)
+                else if proc' == e then (true, prefix, suffix)
+                else (false, proc' :: prefix, suffix))
+              (false, [], []) state
+          in
+          assert (
+            List.length prefix_rev + List.length suffix_rev
+            = List.length state - 1);
+          assert found_e;
+          let prefix (* E' *) = List.rev prefix_rev in
+
+          if List.length prefix > 0 then
+            (* List.iter
+               (fun proc ->
+                 Printf.printf "[depth=%d]     ::prefix:: (p=%d, %s)\n%!" depth
+                   proc.run_proc
+                   (atomic_op_str proc.run_op))
+               prefix; *)
+            let suffix = List.rev suffix_rev in
+
+            (* List.iter
+               (fun proc ->
+                 Printf.printf "[depth=%d]     ::suffix:: (p=%d, %s)\n%!" depth
+                   proc.run_proc
+                   (atomic_op_str proc.run_op))
+               suffix; *)
+            let prefix_top = last_element prefix in
+
+            (* Printf.printf
+               "[depth=%d]     nonempty prefix, prefix_top: (p=%d, %s)\n%!" depth
+               prefix_top.run_proc
+               (atomic_op_str prefix_top.run_op); *)
+            let v_E (* occurs after e but independent of e *) =
+              List.filter
+                (fun proc' ->
+                  proc'.run_proc <> e.run_proc
+                  && Option.value proc'.run_ptr ~default:(-1)
+                     <> Option.value e.run_ptr ~default:(-2))
+                suffix
+            in
+
+            (* List.iter
+               (fun proc ->
+                 Printf.printf
+                   "[depth=%d]     ::occurs_after_e_but_indep:: (p=%d, %s)\n%!"
+                   depth proc.run_proc
+                   (atomic_op_str proc.run_op))
+               v_E; *)
+            let v = v_E @ [ state_top ] in
+
+            (* List.iter
+               (fun proc ->
+                 Printf.printf "[depth=%d]     ::v:: (p=%d, %s)\n%!" depth
+                   proc.run_proc
+                   (atomic_op_str proc.run_op))
+               v; *)
+            let initials =
+              let initials_map, initials_spawns =
+                List.fold_left
+                  (fun (first_accesses, spawns) (state_cell : state_cell) ->
+                    match state_cell.run_ptr with
+                    | None ->
+                        let new_spawns =
+                          IntSet.add state_cell.run_proc spawns
+                        in
+                        (first_accesses, new_spawns)
+                    | Some obj_ptr ->
+                        let new_first_accesses =
+                          IntMap.update obj_ptr
+                            (function
+                              | Some v -> Some v
+                              | None -> Some state_cell.run_proc)
+                            first_accesses
+                        in
+                        (new_first_accesses, spawns))
+                  (IntMap.empty, IntSet.empty)
+                  v
+              in
+              IntMap.fold
+                (fun _ run_proc initials_set ->
+                  IntSet.add run_proc initials_set)
+                initials_map initials_spawns
+            in
+
+            (* Printf.printf "[depth=%d]     initials=[%s], backtrack=[%s]\n%!"
+               depth (set_to_str initials)
+               (set_to_str prefix_top.backtrack); *)
+            if IntSet.(cardinal (inter prefix_top.backtrack initials)) = 0 then
+              let _initial = IntSet.min_elt initials in
+              (* Printf.printf "[depth=%d]     adding initial to backtrack\n%!"
+                 depth; *)
+              prefix_top.backtrack <- IntSet.add _initial prefix_top.backtrack
+        done;
+
+        let sleep' =
+          IntSet.filter
+            (fun q ->
+              (* only keep q that are independent with p: must be other thread of execution and act on a different object (or none) *)
+              if q == p then false
+              else
+                let proc' = List.nth s.procs q in
+                match proc'.obj_ptr with
+                | None -> true
+                | Some obj_ptr' -> obj_ptr' <> obj_ptr)
+            !sleep
+        in
+        explore_source (depth + 1) func new_state (ref sleep');
+        sleep := IntSet.add p !sleep
+      done
+
 let rec explore func state clock last_access =
   let s = last_element state in
   List.iter
@@ -305,17 +498,7 @@ let check f =
   tracing := false;
   if not (f ()) then (
     Printf.printf "Found assertion violation at run %d:\n" !num_runs;
-    List.iter
-      (fun s ->
-        match s with
-        | last_run_proc, last_run_op, last_run_ptr ->
-            let last_run_ptr =
-              Option.map string_of_int last_run_ptr |> Option.value ~default:""
-            in
-            Printf.printf "Process %d: %s %s\n" last_run_proc
-              (atomic_op_str last_run_op)
-              last_run_ptr)
-      !schedule_for_checks;
+    print_trace ();
     assert false);
   tracing := tracing_at_start
 
@@ -326,9 +509,18 @@ let reset_state () =
   schedule_for_checks := [];
   CCVector.clear processes
 
-let trace func =
+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
   explore func empty_state empty_clock empty_last_access
+
+let _trace_source func =
+  reset_state ();
+  let empty_state = do_run func [ (0, Start, None) ] in
+  explore_source 0 func [ empty_state ] (ref IntSet.empty)
+
+let trace func =
+  _trace_source func;
+  Printf.printf "\nnum_traces: %d\n%!" !num_traces

tests/dune

@@ -12,3 +12,13 @@
  (name test_michael_scott_queue)
  (libraries dscheck alcotest)
  (modules test_michael_scott_queue michael_scott_queue))
+
+(test
+ (name test_simple)
+ (libraries dscheck alcotest)
+ (modules test_simple))
+
+(test
+ (name test_simple2)
+ (libraries dscheck)
+ (modules test_simple2))

tests/test_michael_scott_queue.ml

@@ -8,29 +8,39 @@ let drain queue =
   done;
   !remaining
 
+let list_to_str s =
+  List.map (function Some i -> Int.to_string i | None -> "_") s
+  |> String.concat ", "
+
 let producer_consumer () =
   Atomic.trace (fun () ->
       let queue = Michael_scott_queue.create () in
       let items_total = 4 in
 
       Atomic.spawn (fun () ->
-          for _ = 1 to items_total do
-            Michael_scott_queue.push queue 0
+          for i = 1 to items_total do
+            Michael_scott_queue.push queue i
           done);
 
+      let result = ref [] in
+
       (* consumer *)
       let popped = ref 0 in
       Atomic.spawn (fun () ->
           for _ = 1 to items_total do
             match Michael_scott_queue.pop queue with
-            | None -> ()
-            | Some _ -> popped := !popped + 1
+            | None -> result := None :: !result
+            | Some v ->
+                (result := Some v :: !result;
+                popped := !popped + 1)
           done);
 
       (* checks*)
       Atomic.final (fun () ->
+          Printf.printf "pop sequence: %s\n" (list_to_str !result);
           Atomic.check (fun () ->
               let remaining = drain queue in
+              Printf.printf "popped=%d, remaining=%d\n%!" !popped remaining;
               !popped + remaining = items_total)))
 
 let () =

tests/test_simple.ml

@@ -0,0 +1,16 @@
+module Atomic = Dscheck.TracedAtomic
+
+let counter () =
+  let a = Atomic.make 0 in
+  let b = Atomic.make 0 in
+  Atomic.spawn (fun () ->
+      Atomic.set a 1;
+      Atomic.set b 2);
+  Atomic.spawn (fun () ->
+      Atomic.set a 3;
+      Atomic.set b 4);
+  Atomic.final (fun () ->
+      Printf.printf "a=%d, b=%d\n%!" (Atomic.get a) (Atomic.get b))
+
+let test_safe_counter () = Atomic.trace counter
+let _ = test_safe_counter ()

tests/test_simple2.ml

@@ -0,0 +1,19 @@
+module Atomic = Dscheck.TracedAtomic
+
+let test () =
+  let c = Atomic.make 0 in
+  let b = Atomic.make 0 in
+  let ok = Atomic.make false in
+
+  Atomic.spawn (fun () -> Atomic.set b 1);
+  Atomic.spawn (fun () ->
+      Atomic.set c 1;
+      Atomic.set b 2);
+  Atomic.spawn (fun () ->
+      if Atomic.get c = 0 then if Atomic.get b = 0 then Atomic.set ok true);
+
+  Atomic.final (fun () ->
+      Format.printf "b=%i c=%i ok=%b@." (Atomic.get b) (Atomic.get c)
+        (Atomic.get ok))
+
+let () = Atomic.trace test