trace tracker

create trace tracker, add two tests with conditionals and dump traces
for all tests

dscheck.opam

@@ -10,6 +10,7 @@ depends: [
   "ocaml" {>= "5.0.0"}
   "dune" {>= "2.9"}
   "containers"
+  "tsort"
   "oseq"
   "alcotest" {>= "1.6.0" & with-test}
   "odoc" {with-doc}

dune-project

@@ -11,6 +11,6 @@
 (package
  (name dscheck)
  (synopsis "Traced Atomics")
- (depends (ocaml (>= 5.0.0)) dune containers oseq (alcotest (and (>= 1.6.0) :with-test))))
+ (depends (ocaml (>= 5.0.0)) dune containers tsort oseq (alcotest (and (>= 1.6.0) :with-test))))
 
 

gen_traces.sh

@@ -0,0 +1,7 @@
+set -eux pipefail
+
+dscheck_trace_file="tests/traces/ms_queue" dune exec tests/test_michael_scott_queue.exe
+dscheck_trace_file="tests/traces/naive_counter" dune exec tests/test_naive_counter.exe
+dscheck_trace_file="tests/traces/list" dune exec tests/test_list.exe
+dscheck_trace_file="tests/traces/conditional1" dune exec tests/test_conditional1.exe
+dscheck_trace_file="tests/traces/conditional2" dune exec tests/test_conditional2.exe

src/trace_tracker.ml

@@ -0,0 +1,106 @@
+module Op = struct
+  type t = { proc : int; variable : int; step : int }
+
+  let is_dependent t1 t2 = t1.variable == t2.variable
+
+  let compare_proc_step t1 t2 =
+    let c1 = Int.compare t1.proc t2.proc in
+    if c1 <> 0 then c1 else Int.compare t1.step t2.step
+
+  let to_str t = Printf.sprintf "(%d,%c)" t.proc (Char.chr (t.variable + 96))
+end
+
+module Trace = struct
+  module Key = struct
+    type t = (Op.t * Op.t option) list
+
+    let compare t1 t2 =
+      List.compare
+        (fun (op1, dep1) (op2, dep2) ->
+          let c1 = Op.compare_proc_step op1 op2 in
+          if c1 <> 0 then c1 else Option.compare Op.compare_proc_step dep1 dep2)
+        t1 t2
+  end
+
+  type t = Op.t List.t
+
+  let of_schedule_for_checks schedule_for_checks : t =
+    let steps = Hashtbl.create 10 in
+    List.map
+      (fun (proc, _, variable) ->
+        Option.map
+          (fun variable : Op.t ->
+            (match Hashtbl.find_opt steps proc with
+            | None -> Hashtbl.add steps proc 1
+            | Some v ->
+                Hashtbl.remove steps proc;
+                Hashtbl.add steps proc (v + 1));
+
+            let step = Hashtbl.find steps proc in
+
+            { proc; variable; step })
+          variable)
+      schedule_for_checks
+    |> List.filter_map Fun.id
+
+  let to_string t = List.map Op.to_str t |> String.concat ","
+
+  let tag_with_deps (t : t) : Key.t =
+    let next_dep op t = List.find_opt (Op.is_dependent op) t in
+    let rec f t =
+      match t with
+      | [] -> []
+      | hd :: [] -> [ (hd, None) ]
+      | hd :: tl -> (hd, next_dep hd tl) :: f tl
+    in
+    let tagged = f t in
+    List.sort (fun (op1, _) (op2, _) -> Op.compare_proc_step op1 op2) tagged
+
+  let deps_to_str (key : Key.t) : string =
+    List.map
+      (fun (op, dep) ->
+        Op.to_str op ^ "-"
+        ^ (Option.map Op.to_str dep |> Option.value ~default:"none"))
+      key
+    |> String.concat ","
+end
+
+module TraceMap = Map.Make (Trace.Key)
+
+type t = Trace.t TraceMap.t
+
+let traces = ref TraceMap.empty
+
+let add_trace trace =
+  let trace = Trace.of_schedule_for_checks trace in
+  let key = Trace.tag_with_deps trace in
+  traces :=
+    TraceMap.update key
+      (function Some v -> Some v | None -> Some trace)
+      !traces
+
+let print traces channel =
+  Printf.fprintf channel "----\n";
+  TraceMap.iter
+    (fun _ trace -> Printf.fprintf channel "%s\n" (Trace.to_string trace))
+    traces;
+  Printf.fprintf channel "----\n";
+  flush channel
+
+let print_traces chan = print !traces chan
+let clear_traces () = traces := TraceMap.empty
+let get_traces () = !traces
+
+let get_deps_str traces =
+  TraceMap.to_seq traces |> List.of_seq
+  |> List.map (fun (_, value) -> value)
+  |> List.map Trace.tag_with_deps
+  |> List.map Trace.deps_to_str |> String.concat "\n"
+
+let equal t1 t2 =
+  TraceMap.compare
+    (fun _ _ ->
+      0
+      (* any values under the same key are known to be equivalent, even if the exact sequence is not identical *))
+    t1 t2
+  == 0

src/trace_tracker.mli

@@ -0,0 +1,9 @@
+type t
+
+val add_trace : (int * 'a * int option) list -> unit
+val clear_traces : unit -> unit
+val get_traces : unit -> t
+val print_traces : out_channel -> unit
+val print : t -> out_channel -> unit
+val equal : t -> t -> bool
+val get_deps_str : t -> string

src/tracedAtomic.ml

@@ -205,7 +205,7 @@ let var_name i =
       let c = Char.chr (i + 96) in
       Printf.sprintf "%c" c
 
-let print_execution_sequence () =
+let print_execution_sequence chan =
   let highest_proc =
     List.fold_left
       (fun highest (curr_proc, _, _) ->
@@ -216,11 +216,12 @@ let print_execution_sequence () =
   let bar =
     List.init ((highest_proc * 20) + 20) (fun _ -> "-") |> String.concat ""
   in
-  Printf.printf "\nsequence %d\n" !num_interleavings;
-  Printf.printf "%s\n" bar;
-  List.init (highest_proc + 1) (fun proc -> Printf.printf "P%d\t\t\t" proc)
+  Printf.fprintf chan "\nsequence %d\n" !num_interleavings;
+  Printf.fprintf chan "%s\n" bar;
+  List.init (highest_proc + 1) (fun proc ->
+      Printf.fprintf chan "P%d\t\t\t" proc)
   |> ignore;
-  Printf.printf "\n%s\n" bar;
+  Printf.fprintf chan "\n%s\n" bar;
 
   List.iter
     (fun s ->
@@ -230,13 +231,14 @@ let print_execution_sequence () =
           let tabs =
             List.init last_run_proc (fun _ -> "\t\t\t") |> String.concat ""
           in
-          Printf.printf "%s%s %s\n" tabs
+          Printf.fprintf chan "%s%s %s\n" tabs
             (atomic_op_str last_run_op)
             last_run_ptr)
     !schedule_for_checks;
-  Printf.printf "%s\n%!" bar
+  Printf.fprintf chan "%s\n%!" bar
 
-let print_max_exec_seq = ref false
+let interleavings_chan = (ref None : out_channel option ref)
+let record_traces_flag = ref false
 
 let do_run init_func init_schedule =
   init_func ();
@@ -254,8 +256,15 @@ let do_run init_func init_schedule =
     | [] ->
         if !finished_processes == num_processes then (
           tracing := false;
+
           num_interleavings := !num_interleavings + 1;
-          if !print_max_exec_seq then print_execution_sequence ();
+          if !record_traces_flag then
+            Trace_tracker.add_trace !schedule_for_checks;
+
+          (match !interleavings_chan with
+          | None -> ()
+          | Some chan -> print_execution_sequence chan);
+
           !final_func ();
           tracing := true)
     | (process_id_to_run, next_op, next_ptr) :: schedule ->
@@ -274,7 +283,7 @@ let do_run init_func init_schedule =
   finished_processes := 0;
   tracing := false;
   num_states := !num_states + 1;
-  if !num_states mod 1000 == 0 then Printf.printf "run: %d\n%!" !num_states;
+  (* if !num_states mod 1000 == 0 then Printf.printf "run: %d\n%!" !num_states; *)
   let procs =
     CCVector.mapi
       (fun i p -> { proc_id = i; op = p.next_op; obj_ptr = p.next_repr })
@@ -347,7 +356,7 @@ let check f =
   tracing := false;
   if not (f ()) then (
     Printf.printf "Found assertion violation at run %d:\n" !num_interleavings;
-    print_execution_sequence ();
+    print_execution_sequence stdout;
     assert false);
   tracing := tracing_at_start
 
@@ -357,15 +366,34 @@ let reset_state () =
   num_states := 0;
   num_interleavings := 0;
   schedule_for_checks := [];
+  Trace_tracker.clear_traces ();
   CCVector.clear processes
 
-let trace ?(print_interleavings = false) func =
-  print_max_exec_seq := print_interleavings;
+let dscheck_trace_file_env = Sys.getenv_opt "dscheck_trace_file"
+
+let dpor 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;
-  if print_interleavings then
-    Printf.printf "\nexplored %d maximal interleavings and %d states\n"
-      !num_interleavings !num_states
+  explore func empty_state empty_clock empty_last_access
+
+let trace ?interleavings ?(record_traces = false) func =
+  record_traces_flag := record_traces || Option.is_some dscheck_trace_file_env;
+  interleavings_chan := interleavings;
+
+  dpor func;
+
+  (* print reports *)
+  (match !interleavings_chan with
+  | None -> ()
+  | Some chan ->
+      Printf.fprintf chan "\nexplored %d maximal interleavings and %d states\n"
+        !num_interleavings !num_states);
+
+  match dscheck_trace_file_env with
+  | None -> ()
+  | Some path ->
+      let chan = open_out path in
+      Trace_tracker.print_traces chan;
+      close_out chan

src/tracedAtomic.mli

@@ -46,11 +46,9 @@ val incr : int t -> unit
 val decr : int t -> unit
 (** [decr r] atomically decrements the value of [r] by [1]. *)
 
-val trace : ?print_interleavings:bool -> (unit -> unit) -> unit
-(** start the simulation trace 
-
-    print_interleavings - print out explored interleavings
-*)
+val trace :
+  ?interleavings:out_channel -> ?record_traces:bool -> (unit -> unit) -> unit
+(** start the simulation trace *)
 
 val spawn : (unit -> unit) -> unit
 (** spawn [f] as a new 'thread' *)

tests/dune

@@ -13,8 +13,27 @@
  (libraries dscheck alcotest)
  (modules test_michael_scott_queue michael_scott_queue))
 
-
 (test
  (name test_trace)
  (libraries dscheck alcotest)
- (modules test_trace))
+ (modules test_trace))
+
+(rule
+ (with-stdout-to
+  report_trace.output
+  (run ./test_trace.exe)))
+
+(rule
+ (alias runtest)
+ (action
+  (diff report_trace.expected report_trace.output)))
+
+(test
+ (name test_conditional1)
+ (libraries dscheck alcotest)
+ (modules test_conditional1))
+
+(test
+ (name test_conditional2)
+ (libraries dscheck alcotest)
+ (modules test_conditional2))

tests/report_trace.expected

@@ -0,0 +1,39 @@
+
+sequence 1
+----------------------------------------
+P0			P1			
+----------------------------------------
+start 
+fetch_and_add a
+			start 
+			fetch_and_add a
+			fetch_and_add b
+----------------------------------------
+
+sequence 2
+----------------------------------------
+P0			P1			
+----------------------------------------
+start 
+			start 
+fetch_and_add a
+			fetch_and_add a
+			fetch_and_add b
+----------------------------------------
+
+sequence 3
+----------------------------------------
+P0			P1			
+----------------------------------------
+start 
+			start 
+			fetch_and_add a
+fetch_and_add a
+			fetch_and_add b
+----------------------------------------
+
+explored 3 maximal interleavings and 12 states
+----
+(1,a),(0,a),(1,b)
+(0,a),(1,a),(1,b)
+----

tests/test_conditional1.ml

@@ -0,0 +1,22 @@
+module Atomic = Dscheck.TracedAtomic
+
+let test () =
+  let b = Atomic.make 0 in
+  let c = Atomic.make 0 in
+  let ok = Atomic.make false in
+  let seen_b = ref (-1) 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 (
+        seen_b := Atomic.get b;
+        if !seen_b = 0 then Atomic.set ok true))
+
+(* Atomic.final (fun () ->
+    Format.printf "seen_b=%i b=%i c=%i ok=%b@." (!seen_b) (Atomic.get b) (Atomic.get c)
+      (Atomic.get ok)) *)
+
+let () = Atomic.trace test

tests/test_conditional2.ml

@@ -0,0 +1,26 @@
+module Atomic = Dscheck.TracedAtomic
+
+let test () =
+  let x = Atomic.make 0 in
+  let y = Atomic.make 0 in
+  let z = Atomic.make 0 in
+
+  let tmp = ref (-1) in
+  Atomic.spawn (fun () -> tmp := Atomic.get x);
+  Atomic.spawn (fun () -> Atomic.set y 1);
+
+  Atomic.spawn (fun () ->
+      let m = Atomic.get y in
+      if m = 0 then Atomic.set z 1);
+
+  Atomic.spawn (fun () ->
+      let n = Atomic.get z in
+      let l = Atomic.get y in
+      if n = 1 then if l = 0 then Atomic.set x 1)
+
+(*
+   Atomic.final (fun () ->
+       Format.printf "tmp=%d x=%d y=%d z=%d\n%!" !tmp (Atomic.get x)
+         (Atomic.get y) (Atomic.get z)) *)
+
+let () = Atomic.trace test