Merge pull request #19 from ocaml-multicore/better-traces-output

Better traces

Author: bartoszmodelski

.ocamlformat

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

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/conditional_nested" dune exec tests/test_conditional_nested.exe
+dscheck_trace_file="tests/traces/conditional_ssb" dune exec tests/test_conditional_ssb.exe

src/trace_tracker.ml

@@ -0,0 +1,103 @@
+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 ->
+            let current =
+              Hashtbl.find_opt steps proc |> Option.value ~default:0
+            in
+            Hashtbl.replace steps proc (current + 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 attach_deps = function
+      | [] -> []
+      | hd :: [] -> [ (hd, None) ]
+      | hd :: tl -> (hd, next_dep hd tl) :: attach_deps tl
+    in
+    let tagged = attach_deps 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

@@ -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 ""
@@ -193,11 +192,54 @@ type state_cell = {
   mutable backtrack : IntSet.t;
 }
 
-let num_runs = ref 0
+let num_states = ref 0
+let num_interleavings = ref 0
 
 (* we stash the current state in case a check fails and we need to log it *)
 let schedule_for_checks = ref []
 
+let var_name i =
+  match i with
+  | None -> ""
+  | Some i ->
+      let c = Char.chr (i + 96) in
+      Printf.sprintf "%c" c
+
+let print_execution_sequence chan =
+  let highest_proc =
+    List.fold_left
+      (fun highest (curr_proc, _, _) ->
+        if curr_proc > highest then curr_proc else highest)
+      (-1) !schedule_for_checks
+  in
+
+  let bar =
+    List.init ((highest_proc * 20) + 20) (fun _ -> "-") |> String.concat ""
+  in
+  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.fprintf chan "\n%s\n" bar;
+
+  List.iter
+    (fun s ->
+      match s with
+      | last_run_proc, last_run_op, last_run_ptr ->
+          let last_run_ptr = var_name last_run_ptr in
+          let tabs =
+            List.init last_run_proc (fun _ -> "\t\t\t") |> String.concat ""
+          in
+          Printf.fprintf chan "%s%s %s\n" tabs
+            (atomic_op_str last_run_op)
+            last_run_ptr)
+    !schedule_for_checks;
+  Printf.fprintf chan "%s\n%!" bar
+
+let interleavings_chan = (ref None : out_channel option ref)
+let record_traces_flag = ref false
+
 let do_run init_func init_schedule =
   init_func ();
   (*set up run *)
@@ -214,6 +256,15 @@ let do_run init_func init_schedule =
     | [] ->
         if !finished_processes == num_processes then (
           tracing := false;
+
+          num_interleavings := !num_interleavings + 1;
+          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 ->
@@ -231,8 +282,8 @@ let do_run init_func init_schedule =
   run_trace init_schedule ();
   finished_processes := 0;
   tracing := false;
-  num_runs := !num_runs + 1;
-  if !num_runs mod 1000 == 0 then Printf.printf "run: %d\n%!" !num_runs;
+  num_states := !num_states + 1;
+  (* 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 })
@@ -304,31 +355,45 @@ let check f =
   let tracing_at_start = !tracing in
   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;
+    Printf.printf "Found assertion violation at run %d:\n" !num_interleavings;
+    print_execution_sequence stdout;
     assert false);
   tracing := tracing_at_start
 
 let reset_state () =
   finished_processes := 0;
   atomics_counter := 1;
-  num_runs := 0;
+  num_states := 0;
+  num_interleavings := 0;
   schedule_for_checks := [];
+  Trace_tracker.clear_traces ();
   CCVector.clear processes
 
-let trace func =
+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
+
+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 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,8 +46,16 @@ val incr : int t -> unit
 val decr : int t -> unit
 (** [decr r] atomically decrements the value of [r] by [1]. *)
 
-val trace : (unit -> unit) -> unit
-(** start the simulation trace *)
+val trace :
+  ?interleavings:out_channel -> ?record_traces:bool -> (unit -> unit) -> unit
+(** [trace ?interleavings ?record_traces f] starts the simulation trace.
+
+  If [interleavings] output channel is provided, DSCheck will continously
+  print the visited interleavings there.
+
+  [record_traces] enables [Trace_tracker], which is typically used for
+  testing DSCheck itself.
+*)
 
 val spawn : (unit -> unit) -> unit
 (** spawn [f] as a new 'thread' *)

tests/dune

@@ -12,3 +12,28 @@
  (name test_michael_scott_queue)
  (libraries dscheck alcotest)
  (modules test_michael_scott_queue michael_scott_queue))
+
+(test
+ (name test_trace)
+ (libraries dscheck alcotest)
+ (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_conditional_nested)
+ (libraries dscheck alcotest)
+ (modules test_conditional_nested))
+
+(test
+ (name test_conditional_ssb)
+ (libraries dscheck alcotest)
+ (modules test_conditional_ssb))

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 interleavings and 12 states
+----
+(1,a),(0,a),(1,b)
+(0,a),(1,a),(1,b)
+----