TD Parallel Base

src/common/util/messages.ml

@@ -8,6 +8,8 @@ module Category = MessageCategory
 
 open GobResult.Syntax
 
+module Format = BatFormat
+
 
 module Severity =
 struct
@@ -195,10 +197,14 @@ let print ?(ppf= !formatter) (m: Message.t) =
     | Debug -> "white" (* non-bright white is actually some gray *)
     | Success -> "green"
   in
-  let pp_prefix = Format.dprintf "@{<%s>[%a]%a@}" severity_stag Severity.pp m.severity Tags.pp m.tags in
+  let pp_print_option ?(none = fun _ () -> ()) pp_v ppf = function
+    | None -> none ppf ()
+    | Some v -> pp_v ppf v
+  in
+  let pp_prefix = (fun ppf -> Format.fprintf ppf "@{<%s>[%a]%a@}" severity_stag Severity.pp m.severity Tags.pp m.tags) in
   let pp_loc ppf = Format.fprintf ppf " @{<violet>(%a)@}" CilType.Location.pp in
   let pp_loc ppf loc =
-    Format.fprintf ppf "%a" (Format.pp_print_option pp_loc) (Option.map Location.to_cil loc)
+    Format.fprintf ppf "%a" (pp_print_option pp_loc) (Option.map Location.to_cil loc)
   in
   let pp_piece ppf piece =
     Format.fprintf ppf "@{<%s>%s@}%a" severity_stag (Piece.text_with_context piece) pp_loc piece.loc
@@ -229,7 +235,7 @@ let print ?(ppf= !formatter) (m: Message.t) =
   let pp_quote ppf loc =
     if get_bool "warn.quote-code" then (
       let pp_cut_quote ppf = Format.fprintf ppf "@,@[<v 0>%a@,@]" pp_quote in
-      (Format.pp_print_option pp_cut_quote) ppf (Option.map Location.to_cil loc)
+      (pp_print_option pp_cut_quote) ppf (Option.map Location.to_cil loc)
     )
   in
   let pp_piece ppf piece = Format.fprintf ppf "%a%a" pp_piece piece pp_quote piece.loc in

src/solver/dune

@@ -5,6 +5,7 @@
  (public_name goblint.solver)
  (libraries
    batteries.unthreaded
+   saturn
    goblint_std
    goblint_parallel
    goblint_logs

src/solver/parallelStats.bak.ml

@@ -0,0 +1,228 @@
+open Batteries
+open GobConfig
+open Goblint_constraint.ConstrSys
+
+module ParallelSolverStats (S:EqConstrSys) (HM:Hashtbl.S with type key = S.v) =
+struct
+  open S
+  open Messages
+
+  let cas_success = Atomic.make 0
+  let cas_fail = Atomic.make 0
+
+  let cas_succsess_event () = Atomic.incr cas_success
+  let cas_fail_event () = Atomic.incr cas_fail
+
+  (* (* This allows us to use a simple array to store thread specifics statistics *) *)
+  (* let maximal_number_of_threads = 10000 *)
+  (**)
+  (**)
+  (* let stack_d = Atomic.make 0 *)
+  (* let vars = Atomic.make 0 *)
+  (* let vars_by_thread = Array.init maximal_number_of_threads (fun _ -> Atomic.make 0)  *)
+  (* let queries = Atomic.make 0 *)
+  (* let queries_by_thread = Array.init maximal_number_of_threads (fun _ -> Atomic.make 0) *)
+  (* let evals = Atomic.make 0 *)
+  (* let evals_by_thread = Array.init maximal_number_of_threads (fun _ -> Atomic.make 0) *)
+  (* let instant_returns = Atomic.make 0 *)
+  (* let thread_starts = Atomic.make 0 *)
+  (* let thread_creates = Atomic.make 0 *)
+  (* let thread_start_times = Array.init maximal_number_of_threads (fun _ -> 0.0) *)
+  (* let thread_end_times = Array.init maximal_number_of_threads (fun _ -> 0.0) *)
+  (**)
+  (* let active_threads = Atomic.make 0 *)
+  (* let first_thread_activation_time = Atomic.make 0.0 *)
+  (* let last_thread_activation_update_time = Atomic.make 0.0 *)
+  (* let total_thread_activation_time = Atomic.make 0.0 *)
+  (**)
+  (* let iterations = Atomic.make 0 *)
+  (**)
+  (* let updates = Atomic.make 0 *)
+  (* let updates_by_thread = Array.init maximal_number_of_threads (fun _ -> Atomic.make 0) *)
+  (**)
+  (* let full_trace = false *)
+  (* let start_c = 0 *)
+  (* let max_c   : int ref = ref (-1) *)
+  (* let max_var : Var.t option ref = ref None *)
+  (**)
+  (* let histo = HM.create 1024 *)
+  (* let increase (v:Var.t) = *)
+  (*   let set v c = *)
+  (*     if not full_trace && (c > start_c && c > !max_c && not (GobOption.exists (Var.equal v) !max_var)) then begin *)
+  (*       if tracing then trace "sol" "Switched tracing to %a" Var.pretty_trace v; *)
+  (*       max_c := c; *)
+  (*       max_var := Some v *)
+  (*     end *)
+  (*   in *)
+  (*   try let c = HM.find histo v in *)
+  (*     set v (c+1); *)
+  (*     HM.replace histo v (c+1) *)
+  (*   with Not_found -> begin *)
+  (*       set v 1; *)
+  (*       HM.add histo v 1 *)
+  (*     end *)
+  (**)
+  (* let start_event () = () *)
+  (* let stop_event () = () *)
+  (**)
+  (* let new_var_event thread_id x = *)
+  (*   Atomic.incr vars; *)
+  (*   Atomic.incr vars_by_thread.(thread_id); *)
+  (*   if tracing then trace "sol" "New %a" Var.pretty_trace x *)
+  (**)
+  (* let get_var_event x = *)
+  (*   Atomic.incr queries; *)
+  (*   if tracing && full_trace then trace "sol" "Querying %a" Var.pretty_trace x *)
+  (**)
+  (* let eval_rhs_event thread_id x = *)
+  (*   if tracing && full_trace then trace "sol" "(Re-)evaluating %a" Var.pretty_trace x; *)
+  (*   Atomic.incr evals; *)
+  (*   Atomic.incr evals_by_thread.(thread_id); *)
+  (*   if (get_bool "dbg.solver-progress") then (Atomic.incr stack_d; Logs.debug "%d" @@ Atomic.get stack_d) *)
+  (**)
+  (* let update_var_event thread_id x o n = *)
+  (*   Atomic.incr updates; *)
+  (*   Atomic.incr updates_by_thread.(thread_id); *)
+  (*   if tracing then increase x; *)
+  (*   if full_trace || (not (Dom.is_bot o) && GobOption.exists (Var.equal x) !max_var) then begin *)
+  (*     if tracing then tracei "sol_max" "(%d) Update to %a" !max_c Var.pretty_trace x; *)
+  (*     if tracing then traceu "sol_max" "%a" Dom.pretty_diff (n, o) *)
+  (*   end *)
+  (**)
+  (* let instant_return_event () = *)
+  (*   Atomic.incr instant_returns *)
+  (**)
+  (* let create_task_event thread_id = *)
+  (*   Atomic.incr thread_creates *)
+  (**)
+  (* let rec thread_starts_solve_event thread_id = *)
+  (*   Atomic.incr thread_starts; *)
+  (*   let t = Unix.gettimeofday () in *)
+  (*   thread_start_times.(thread_id) <- t *)
+  (**)
+  (* let rec thread_ends_solve_event thread_id = *)
+  (*   let t = Unix.gettimeofday () in *)
+  (*   thread_end_times.(thread_id) <- t *)
+  (**)
+  (* (* solvers can assign this to print solver specific statistics using their data structures *) *)
+  (* let print_solver_stats = ref (fun () -> ()) *)
+  (**)
+  (* (* this can be used in print_solver_stats *) *)
+  (* let ncontexts = ref 0 *)
+  (* let print_context_stats rho = *)
+  (*   let histo = Hashtbl.create 13 in (* histogram: node id -> number of contexts *) *)
+  (*   let str k = GobPretty.sprint S.Var.pretty_trace k in (* use string as key since k may have cycles which lead to exception *) *)
+  (*   let is_fun k = match S.Var.node k with FunctionEntry _ -> true | _ -> false in (* only count function entries since other nodes in function will have leq number of contexts *) *)
+  (*   HM.iter (fun k _ -> if is_fun k then Hashtbl.modify_def 0 (str k) ((+)1) histo) rho; *)
+  (*   (* let max_k, n = Hashtbl.fold (fun k v (k',v') -> if v > v' then k,v else k',v') histo (Obj.magic (), 0) in *) *)
+  (*   (* Logs.debug "max #contexts: %d for %s" n max_k; *) *)
+  (*   ncontexts := Hashtbl.fold (fun _ -> (+)) histo 0; *)
+  (*   let topn = 5 in *)
+  (*   Logs.debug "Found %d contexts for %d functions. Top %d functions:" !ncontexts (Hashtbl.length histo) topn; *)
+  (*   Hashtbl.to_list histo *)
+  (*   |> List.sort (fun (_,n1) (_,n2) -> compare n2 n1) *)
+  (*   |> List.take topn *)
+  (*   |> List.iter @@ fun (k,n) -> Logs.debug "%d\tcontexts for %s" n k *)
+  (**)
+  (* let stats_csv = *)
+  (*   let save_run_str = GobConfig.get_string "save_run" in *)
+  (*   if save_run_str <> "" then ( *)
+  (*     let save_run = Fpath.v save_run_str in *)
+  (*     GobSys.mkdir_or_exists save_run; *)
+  (*     Fpath.(to_string (save_run / "solver_stats.csv")) |> open_out |> Option.some *)
+  (*   ) else None *)
+  (* let write_csv xs oc = output_string oc @@ String.concat ",\t" xs ^ "\n" *)
+  (**)
+  (* (* print generic and specific stats *) *)
+  (* let print_stats _ =  *)
+  (*   Logs.newline (); *)
+  (*   (* print_endline "# Generic solver stats"; *) *)
+  (*   Logs.info "runtime: %s" (GobSys.string_of_time ()); *)
+  (*   Logs.info "vars: %d, evals: %d" (Atomic.get vars) (Atomic.get evals); *)
+  (*   Logs.info "vars: %d" (Atomic.get vars); *)
+  (*   Logs.info "queries: %d" (Atomic.get queries); *)
+  (**)
+  (*   (* let threads_data = Seq.zip (Array.to_seq vars_by_thread) (Array.to_seq evals_by_thread) in *) *)
+  (*   (* let threads_data = Seq.zip threads_data (Array.to_seq updates_by_thread) in *) *)
+  (*   let threads_with_update = ref 0 in *)
+  (*   let threads_with_anything = ref 0 in *)
+  (*   (* The following is an important statistics, here left out for simplicity *) *)
+  (*   (* Seq.iteri (fun i ((vars, evals), updates) ->  *) *)
+  (*   (*     if (Atomic.get vars) <> 0 || (Atomic.get evals) > 0 || (Atomic.get updates) <> 0 then *) *)
+  (*   (*       begin *) *)
+  (*   (*         Logs.info "Thread %d: vars: %d, evals: %d, updates: %d" i (Atomic.get vars) (Atomic.get evals) (Atomic.get updates); *) *)
+  (*   (*         threads_with_anything := !threads_with_anything + 1; *) *)
+  (*   (*       end; *) *)
+  (*   (*     if (Atomic.get updates) <> 0 then threads_with_update := !threads_with_update + 1 *) *)
+  (*   (*   ) threads_data; *) *)
+  (*   Logs.info "Threads with updates: %d" !threads_with_update; *)
+  (*   Logs.info "Threads with anything: %d" !threads_with_anything; *)
+  (*   Logs.info "Threads returned instantly: %d" (Atomic.get instant_returns); *)
+  (*   Logs.info "Threads started: %d" (Atomic.get thread_starts); *)
+  (*   Logs.info "Threads created: %d" (Atomic.get thread_creates); *)
+  (*   Logs.info "Threads active: %d" (Atomic.get active_threads); *)
+  (**)
+  (*   let non_zero_start_times = Array.filter (fun t -> t <> 0.0) thread_start_times in *)
+  (*   let first_thread_start = Array.fold_left min infinity non_zero_start_times in *)
+  (*   let current_time = Unix.gettimeofday () in *)
+  (*   let total_runtime = Seq.zip (Array.to_seq thread_start_times) (Array.to_seq thread_end_times)  *)
+  (*                       |> Seq.filter (fun (start, end_) -> start <> 0.0)  *)
+  (*                       |> Seq.map (fun (start, end_) -> if end_ = 0.0 then (start, current_time) else (start, end_)) *)
+  (*                       |> Seq.fold_left (fun acc (start, end_) -> acc +. (end_ -. start)) 0.0 in *)
+  (*   let walltime = current_time -. first_thread_start in *)
+  (*   Logs.info "Total runtime: %f" total_runtime; *)
+  (*   Logs.info "Walltime: %f" walltime; *)
+  (*   let average_active_threads = total_runtime /. walltime in *)
+  (*   Logs.info "Average active threads: %f" average_active_threads; *)
+  (**)
+  (**)
+  (**)
+  (**)
+  (*   (* Logs.info "vars: %d" (Atomic.get vars); *) *)
+  (**)
+  (*   (* Array.iteri (fun i v -> if Atomic.get v <> 0 then Logs.info "vars (%d): %d" i (Atomic.get v)) vars_by_thread; *) *)
+  (*   (**) *)
+  (*   (* Logs.info "evals: %d" (Atomic.get evals); *) *)
+  (*   (* Array.iteri (fun i v -> if Atomic.get v <> 0 then Logs.info "    evals (%d): %d" i (Atomic.get v)) evals_by_thread; *) *)
+  (*   (**) *)
+  (*   (* Logs.info "updates: %d" (Atomic.get updates); *) *)
+  (*   (* jrray.iteri (fun i v -> Logs.info "    updates (%d): %d" i (Atomic.get v)) updates_by_thread; *) *)
+  (**)
+  (*   (* let first_thread_start = Atomic.get first_thread_activation_time in *) *)
+  (*   (* let last_registered = Atomic.get last_thread_activation_update_time in *) *)
+  (*   (* let average_thread_activation_time = Atomic.get total_thread_activation_time /. (last_registered -. first_thread_start) in *) *)
+  (*   (* let total_time = last_registered -. first_thread_start in *) *)
+  (*   (* Logs.info "average nr_threads: %f" (average_thread_activation_time); *) *)
+  (*   (* Logs.info "Evaluations per CPU-second: %f" ((float_of_int @@ Atomic.get evals) /. average_thread_activation_time /. total_time); *) *)
+  (*   (* Logs.info "Updates per CPU-second: %f" ((float_of_int @@ Atomic.get updates) /. average_thread_activation_time /. total_time); *) *)
+  (*   (**) *)
+  (*   (* Option.may (fun v -> ignore @@ Logs.info "max updates: %d for var %a" !max_c Var.pretty_trace v) !max_var; *) *)
+  (*   (* Logs.newline (); *) *)
+  (*   (* (* print_endline "# Solver specific stats"; *) *) *)
+  (*   (* !print_solver_stats (); *) *)
+  (*   (* Logs.newline (); *) *)
+  (*   (* (* Timing.print (M.get_out "timing" Legacy.stdout) "Timings:\n"; *) *) *)
+  (*   (* (* Gc.print_stat stdout; (* too verbose, slow and words instead of MB *) *) *) *)
+  (*   (* let gc = GobGc.print_quick_stat Legacy.stderr in *) *)
+  (*   (* Logs.newline (); *) *)
+  (*   (* Option.may (write_csv [GobSys.string_of_time (); string_of_int !SolverStats.vars; string_of_int !SolverStats.evals; string_of_int !ncontexts; string_of_int gc.Gc.top_heap_words]) stats_csv *) *)
+  (**)
+  (*   () *)
+  (* (* print_string "Do you want to continue? [Y/n]"; *) *)
+  (* (* flush stdout *) *)
+  (* (* if read_line () = "n" then raise Break *) *)
+  (**)
+  (* let () = *)
+  (*   let write_header = write_csv ["runtime"; "vars"; "evals"; "contexts"; "max_heap"] (* TODO @ !solver_stats_headers *) in *)
+  (*   Option.may write_header stats_csv; *)
+  (*   (* call print_stats on dbg.solver-signal *) *)
+  (*   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) (Signal_handle print_stats); *)
+  (*   (* call print_stats every dbg.solver-stats-interval *) *)
+  (*   Sys.set_signal Sys.sigvtalrm (Signal_handle print_stats); *)
+  (*   (* https://ocaml.org/api/Unix.html#TYPEinterval_timer ITIMER_VIRTUAL is user time; sends sigvtalarm; ITIMER_PROF/sigprof is already used in Timeout.Unix.timeout *) *)
+  (*   let ssi = get_int "dbg.solver-stats-interval" in *)
+  (*   if ssi > 0 then *)
+  (*     let it = float_of_int ssi in *)
+  (*     ignore Unix.(setitimer ITIMER_VIRTUAL { it_interval = it; it_value = it }); *)
+end
+

src/solver/parallelStats.ml

@@ -0,0 +1,40 @@
+open Batteries
+open GobConfig
+open Goblint_constraint.ConstrSys
+
+module ParallelSolverStats = 
+struct
+  open Messages
+
+  let cas_success = Atomic.make 0
+  let cas_fail = Atomic.make 0
+  let nr_iterations = Atomic.make 0
+
+  let start_time = ref 0.
+  let end_time = ref 0.
+
+  let solver_start_event () =
+    start_time := Unix.gettimeofday ();
+    Atomic.set cas_success 0;
+    Atomic.set cas_fail 0
+
+  let solver_end_event () =
+    end_time := Unix.gettimeofday ()
+
+  let start_iterate_event job_id =
+    Atomic.incr nr_iterations
+
+  let cas_success_event () = Atomic.incr cas_success
+  let cas_fail_event () = Atomic.incr cas_fail
+
+  let print_stats () =
+    Logs.info "Cas success: %d" (Atomic.get cas_success);
+    Logs.info "Cas fail: %d" (Atomic.get cas_fail);
+
+    let duration = !end_time -. !start_time in
+    Logs.info "Solver duration: %.2f" duration;
+
+    Logs.info "Iterations: %d" (Atomic.get nr_iterations);
+
+end
+

src/solver/postSolver.ml

@@ -349,3 +349,21 @@ module DemandEqIncrSolverFromEqSolver (Sol: GenericEqSolver): DemandEqIncrSolver
       Post.post xs vs vh;
       (vh, ())
   end
+
+
+module DemandEqIncrSolverFromDemandEqSolver (Sol: DemandEqSolver): DemandEqIncrSolver =
+  functor (Arg: IncrSolverArg) (S: DemandEqConstrSys) (VH: Hashtbl.S with type key = S.v) ->
+  struct
+    module EqSys = EqConstrSysFromDemandConstrSys (S)
+    module Sol = Sol (S) (VH)
+    module Post = MakeList (ListArgFromStdArg (EqSys) (VH) (Arg))
+
+    type marshal = unit
+    let copy_marshal () = ()
+    let relift_marshal () = ()
+
+    let solve xs vs _ =
+      let vh = Sol.solve xs vs in
+      Post.post xs vs vh;
+      (vh, ())
+  end