.

Author: bartoszmodelski

src/tracedAtomic.ml

@@ -239,7 +239,7 @@ let do_run init_func init_schedule =
     | [] ->
         if !finished_processes == num_processes then (
           tracing := false;
-          print_trace ();
+          (* print_trace (); *)
           num_traces := !num_traces + 1;
           !final_func ();
           tracing := true)
@@ -296,18 +296,19 @@ let rec explore_source depth func state sleep_sets =
      (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
+  | 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);
+        (* 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, %s\n%!" depth p
-          (atomic_op_str proc.op) (var_name proc.obj_ptr);
+        (* Printf.printf "[depth=%d]  p=%d, %s, %s\n%!" depth p
+          (atomic_op_str proc.op) (var_name proc.obj_ptr); *)
         (* run *)
         let state_top =
           let schedule =
@@ -340,9 +341,9 @@ let rec explore_source depth func state sleep_sets =
            (List.length reversible_races); *)
         for i = 0 to List.length reversible_races - 1 do
           let e = List.nth reversible_races i in
-          Printf.printf
+          (* Printf.printf
             "[depth=%d]   inner loop, racing op: e=(p'=%d, %s, %s)\n%!" depth
-            e.run_proc (atomic_op_str e.run_op) (var_name e.run_ptr);
+            e.run_proc (atomic_op_str e.run_op) (var_name e.run_ptr); *)
           let found_e, prefix_rev, suffix_rev =
             List.fold_left
               (fun (seen_e, prefix, suffix) proc' ->
@@ -358,28 +359,28 @@ let rec explore_source depth func state sleep_sets =
 
           if List.length prefix_rev > 0 then (
             let prefix (* E' *) = List.rev prefix_rev in
-            List.iter
+            (* List.iter
               (fun proc ->
                 Printf.printf "[depth=%d]     ::prefix:: (p=%d, %s, %s)\n%!"
                   depth proc.run_proc
                   (atomic_op_str proc.run_op)
                   (var_name proc.run_ptr))
-              prefix;
+              prefix; *)
             let suffix = List.rev suffix_rev in
 
-            List.iter
+            (* List.iter
               (fun proc ->
                 Printf.printf "[depth=%d]     ::suffix:: (p=%d, %s, %s)\n%!"
                   depth proc.run_proc
                   (atomic_op_str proc.run_op)
                   (var_name proc.run_ptr))
-              suffix;
+              suffix; *)
             let prefix_top = last_element prefix in
 
-            Printf.printf
+            (* Printf.printf
               "[depth=%d]     nonempty prefix, prefix_top: (p=%d, %s)\n%!" depth
               prefix_top.run_proc
-              (atomic_op_str prefix_top.run_op);
+              (atomic_op_str prefix_top.run_op); *)
             let v_E (* occurs after e but independent of e *) =
               List.filter
                 (fun proc' ->
@@ -398,12 +399,12 @@ let rec explore_source depth func state sleep_sets =
                v_E; *)
             let v = v_E @ [ state_top ] in
 
-            List.iter
+            (* List.iter
               (fun proc ->
                 Printf.printf "[depth=%d]     ::v:: (p=%d, %s)\n%!" depth
                   proc.run_proc
                   (atomic_op_str proc.run_op))
-              v;
+              v; *)
             let initials =
               let initials_map, initials_spawns =
                 List.fold_left
@@ -431,7 +432,7 @@ let rec explore_source depth func state sleep_sets =
                   IntSet.add run_proc initials_set)
                 initials_map initials_spawns
             in
-
+(* 
             Printf.printf
               "[depth=%d]     initials=[%s], backtrack=[%s] at depth=%d, p=%d, \
                op=%s \n\
@@ -440,7 +441,7 @@ let rec explore_source depth func state sleep_sets =
               (_set_to_str prefix_top.backtrack)
               (List.length prefix - 1)
               prefix_top.run_proc
-              (atomic_op_str prefix_top.run_op);
+              (atomic_op_str prefix_top.run_op); *)
             let prefix_top_sleep =
               !(List.nth sleep_sets (List.length prefix - 1))
             in
@@ -455,9 +456,9 @@ let rec explore_source depth func state sleep_sets =
                 | Some initial -> initial
                 | None -> IntSet.min_elt initials
               in
-
+(* 
               Printf.printf "[depth=%d]     adding initial to backtrack\n%!"
-                depth;
+                depth; *)
               prefix_top.backtrack <- IntSet.add _initial prefix_top.backtrack))
         done;
 
@@ -475,9 +476,9 @@ let rec explore_source depth func state sleep_sets =
         in
         explore_source (depth + 1) func new_state (sleep_sets @ [ ref sleep' ]);
         sleep := IntSet.add p !sleep
-      done;
-      Printf.printf "[depth=%d] exit (backtrack=[%s], sleep=[%s])\n%!" depth
-        (_set_to_str s.backtrack) (_set_to_str !sleep)
+      done;;
+      (* Printf.printf "[depth=%d] exit (backtrack=[%s], sleep=[%s])\n%!" depth
+        (_set_to_str s.backtrack) (_set_to_str !sleep) *)
 
 let rec explore func state clock last_access =
   let s = last_element state in