Skip to content

Commit abb1663

Browse files
arkocalarkocal
committed
parallelism: Introduce base solver and stats
1 parent 670cc27 commit abb1663

File tree

6 files changed

+711
-2
lines changed

6 files changed

+711
-2
lines changed

‎src/solver/dune‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
(public_name goblint.solver)
66
(libraries
77
batteries.unthreaded
8+
saturn
89
goblint_std
910
goblint_parallel
1011
goblint_logs

‎src/solver/parallelStats.bak.ml‎

Lines changed: 228 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,228 @@
1+
open Batteries
2+
open GobConfig
3+
open Goblint_constraint.ConstrSys
4+
5+
module ParallelSolverStats (S:EqConstrSys) (HM:Hashtbl.S with type key = S.v) =
6+
struct
7+
open S
8+
open Messages
9+
10+
let cas_success = Atomic.make 0
11+
let cas_fail = Atomic.make 0
12+
13+
let cas_succsess_event () = Atomic.incr cas_success
14+
let cas_fail_event () = Atomic.incr cas_fail
15+
16+
(* (* This allows us to use a simple array to store thread specifics statistics *) *)
17+
(* let maximal_number_of_threads = 10000 *)
18+
(**)
19+
(**)
20+
(* let stack_d = Atomic.make 0 *)
21+
(* let vars = Atomic.make 0 *)
22+
(* let vars_by_thread = Array.init maximal_number_of_threads (fun _ -> Atomic.make 0) *)
23+
(* let queries = Atomic.make 0 *)
24+
(* let queries_by_thread = Array.init maximal_number_of_threads (fun _ -> Atomic.make 0) *)
25+
(* let evals = Atomic.make 0 *)
26+
(* let evals_by_thread = Array.init maximal_number_of_threads (fun _ -> Atomic.make 0) *)
27+
(* let instant_returns = Atomic.make 0 *)
28+
(* let thread_starts = Atomic.make 0 *)
29+
(* let thread_creates = Atomic.make 0 *)
30+
(* let thread_start_times = Array.init maximal_number_of_threads (fun _ -> 0.0) *)
31+
(* let thread_end_times = Array.init maximal_number_of_threads (fun _ -> 0.0) *)
32+
(**)
33+
(* let active_threads = Atomic.make 0 *)
34+
(* let first_thread_activation_time = Atomic.make 0.0 *)
35+
(* let last_thread_activation_update_time = Atomic.make 0.0 *)
36+
(* let total_thread_activation_time = Atomic.make 0.0 *)
37+
(**)
38+
(* let iterations = Atomic.make 0 *)
39+
(**)
40+
(* let updates = Atomic.make 0 *)
41+
(* let updates_by_thread = Array.init maximal_number_of_threads (fun _ -> Atomic.make 0) *)
42+
(**)
43+
(* let full_trace = false *)
44+
(* let start_c = 0 *)
45+
(* let max_c : int ref = ref (-1) *)
46+
(* let max_var : Var.t option ref = ref None *)
47+
(**)
48+
(* let histo = HM.create 1024 *)
49+
(* let increase (v:Var.t) = *)
50+
(* let set v c = *)
51+
(* if not full_trace && (c > start_c && c > !max_c && not (GobOption.exists (Var.equal v) !max_var)) then begin *)
52+
(* if tracing then trace "sol" "Switched tracing to %a" Var.pretty_trace v; *)
53+
(* max_c := c; *)
54+
(* max_var := Some v *)
55+
(* end *)
56+
(* in *)
57+
(* try let c = HM.find histo v in *)
58+
(* set v (c+1); *)
59+
(* HM.replace histo v (c+1) *)
60+
(* with Not_found -> begin *)
61+
(* set v 1; *)
62+
(* HM.add histo v 1 *)
63+
(* end *)
64+
(**)
65+
(* let start_event () = () *)
66+
(* let stop_event () = () *)
67+
(**)
68+
(* let new_var_event thread_id x = *)
69+
(* Atomic.incr vars; *)
70+
(* Atomic.incr vars_by_thread.(thread_id); *)
71+
(* if tracing then trace "sol" "New %a" Var.pretty_trace x *)
72+
(**)
73+
(* let get_var_event x = *)
74+
(* Atomic.incr queries; *)
75+
(* if tracing && full_trace then trace "sol" "Querying %a" Var.pretty_trace x *)
76+
(**)
77+
(* let eval_rhs_event thread_id x = *)
78+
(* if tracing && full_trace then trace "sol" "(Re-)evaluating %a" Var.pretty_trace x; *)
79+
(* Atomic.incr evals; *)
80+
(* Atomic.incr evals_by_thread.(thread_id); *)
81+
(* if (get_bool "dbg.solver-progress") then (Atomic.incr stack_d; Logs.debug "%d" @@ Atomic.get stack_d) *)
82+
(**)
83+
(* let update_var_event thread_id x o n = *)
84+
(* Atomic.incr updates; *)
85+
(* Atomic.incr updates_by_thread.(thread_id); *)
86+
(* if tracing then increase x; *)
87+
(* if full_trace || (not (Dom.is_bot o) && GobOption.exists (Var.equal x) !max_var) then begin *)
88+
(* if tracing then tracei "sol_max" "(%d) Update to %a" !max_c Var.pretty_trace x; *)
89+
(* if tracing then traceu "sol_max" "%a" Dom.pretty_diff (n, o) *)
90+
(* end *)
91+
(**)
92+
(* let instant_return_event () = *)
93+
(* Atomic.incr instant_returns *)
94+
(**)
95+
(* let create_task_event thread_id = *)
96+
(* Atomic.incr thread_creates *)
97+
(**)
98+
(* let rec thread_starts_solve_event thread_id = *)
99+
(* Atomic.incr thread_starts; *)
100+
(* let t = Unix.gettimeofday () in *)
101+
(* thread_start_times.(thread_id) <- t *)
102+
(**)
103+
(* let rec thread_ends_solve_event thread_id = *)
104+
(* let t = Unix.gettimeofday () in *)
105+
(* thread_end_times.(thread_id) <- t *)
106+
(**)
107+
(* (* solvers can assign this to print solver specific statistics using their data structures *) *)
108+
(* let print_solver_stats = ref (fun () -> ()) *)
109+
(**)
110+
(* (* this can be used in print_solver_stats *) *)
111+
(* let ncontexts = ref 0 *)
112+
(* let print_context_stats rho = *)
113+
(* let histo = Hashtbl.create 13 in (* histogram: node id -> number of contexts *) *)
114+
(* let str k = GobPretty.sprint S.Var.pretty_trace k in (* use string as key since k may have cycles which lead to exception *) *)
115+
(* 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 *) *)
116+
(* HM.iter (fun k _ -> if is_fun k then Hashtbl.modify_def 0 (str k) ((+)1) histo) rho; *)
117+
(* (* 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 *) *)
118+
(* (* Logs.debug "max #contexts: %d for %s" n max_k; *) *)
119+
(* ncontexts := Hashtbl.fold (fun _ -> (+)) histo 0; *)
120+
(* let topn = 5 in *)
121+
(* Logs.debug "Found %d contexts for %d functions. Top %d functions:" !ncontexts (Hashtbl.length histo) topn; *)
122+
(* Hashtbl.to_list histo *)
123+
(* |> List.sort (fun (_,n1) (_,n2) -> compare n2 n1) *)
124+
(* |> List.take topn *)
125+
(* |> List.iter @@ fun (k,n) -> Logs.debug "%d\tcontexts for %s" n k *)
126+
(**)
127+
(* let stats_csv = *)
128+
(* let save_run_str = GobConfig.get_string "save_run" in *)
129+
(* if save_run_str <> "" then ( *)
130+
(* let save_run = Fpath.v save_run_str in *)
131+
(* GobSys.mkdir_or_exists save_run; *)
132+
(* Fpath.(to_string (save_run / "solver_stats.csv")) |> open_out |> Option.some *)
133+
(* ) else None *)
134+
(* let write_csv xs oc = output_string oc @@ String.concat ",\t" xs ^ "\n" *)
135+
(**)
136+
(* (* print generic and specific stats *) *)
137+
(* let print_stats _ = *)
138+
(* Logs.newline (); *)
139+
(* (* print_endline "# Generic solver stats"; *) *)
140+
(* Logs.info "runtime: %s" (GobSys.string_of_time ()); *)
141+
(* Logs.info "vars: %d, evals: %d" (Atomic.get vars) (Atomic.get evals); *)
142+
(* Logs.info "vars: %d" (Atomic.get vars); *)
143+
(* Logs.info "queries: %d" (Atomic.get queries); *)
144+
(**)
145+
(* (* let threads_data = Seq.zip (Array.to_seq vars_by_thread) (Array.to_seq evals_by_thread) in *) *)
146+
(* (* let threads_data = Seq.zip threads_data (Array.to_seq updates_by_thread) in *) *)
147+
(* let threads_with_update = ref 0 in *)
148+
(* let threads_with_anything = ref 0 in *)
149+
(* (* The following is an important statistics, here left out for simplicity *) *)
150+
(* (* Seq.iteri (fun i ((vars, evals), updates) -> *) *)
151+
(* (* if (Atomic.get vars) <> 0 || (Atomic.get evals) > 0 || (Atomic.get updates) <> 0 then *) *)
152+
(* (* begin *) *)
153+
(* (* Logs.info "Thread %d: vars: %d, evals: %d, updates: %d" i (Atomic.get vars) (Atomic.get evals) (Atomic.get updates); *) *)
154+
(* (* threads_with_anything := !threads_with_anything + 1; *) *)
155+
(* (* end; *) *)
156+
(* (* if (Atomic.get updates) <> 0 then threads_with_update := !threads_with_update + 1 *) *)
157+
(* (* ) threads_data; *) *)
158+
(* Logs.info "Threads with updates: %d" !threads_with_update; *)
159+
(* Logs.info "Threads with anything: %d" !threads_with_anything; *)
160+
(* Logs.info "Threads returned instantly: %d" (Atomic.get instant_returns); *)
161+
(* Logs.info "Threads started: %d" (Atomic.get thread_starts); *)
162+
(* Logs.info "Threads created: %d" (Atomic.get thread_creates); *)
163+
(* Logs.info "Threads active: %d" (Atomic.get active_threads); *)
164+
(**)
165+
(* let non_zero_start_times = Array.filter (fun t -> t <> 0.0) thread_start_times in *)
166+
(* let first_thread_start = Array.fold_left min infinity non_zero_start_times in *)
167+
(* let current_time = Unix.gettimeofday () in *)
168+
(* let total_runtime = Seq.zip (Array.to_seq thread_start_times) (Array.to_seq thread_end_times) *)
169+
(* |> Seq.filter (fun (start, end_) -> start <> 0.0) *)
170+
(* |> Seq.map (fun (start, end_) -> if end_ = 0.0 then (start, current_time) else (start, end_)) *)
171+
(* |> Seq.fold_left (fun acc (start, end_) -> acc +. (end_ -. start)) 0.0 in *)
172+
(* let walltime = current_time -. first_thread_start in *)
173+
(* Logs.info "Total runtime: %f" total_runtime; *)
174+
(* Logs.info "Walltime: %f" walltime; *)
175+
(* let average_active_threads = total_runtime /. walltime in *)
176+
(* Logs.info "Average active threads: %f" average_active_threads; *)
177+
(**)
178+
(**)
179+
(**)
180+
(**)
181+
(* (* Logs.info "vars: %d" (Atomic.get vars); *) *)
182+
(**)
183+
(* (* Array.iteri (fun i v -> if Atomic.get v <> 0 then Logs.info "vars (%d): %d" i (Atomic.get v)) vars_by_thread; *) *)
184+
(* (**) *)
185+
(* (* Logs.info "evals: %d" (Atomic.get evals); *) *)
186+
(* (* Array.iteri (fun i v -> if Atomic.get v <> 0 then Logs.info " evals (%d): %d" i (Atomic.get v)) evals_by_thread; *) *)
187+
(* (**) *)
188+
(* (* Logs.info "updates: %d" (Atomic.get updates); *) *)
189+
(* (* jrray.iteri (fun i v -> Logs.info " updates (%d): %d" i (Atomic.get v)) updates_by_thread; *) *)
190+
(**)
191+
(* (* let first_thread_start = Atomic.get first_thread_activation_time in *) *)
192+
(* (* let last_registered = Atomic.get last_thread_activation_update_time in *) *)
193+
(* (* let average_thread_activation_time = Atomic.get total_thread_activation_time /. (last_registered -. first_thread_start) in *) *)
194+
(* (* let total_time = last_registered -. first_thread_start in *) *)
195+
(* (* Logs.info "average nr_threads: %f" (average_thread_activation_time); *) *)
196+
(* (* Logs.info "Evaluations per CPU-second: %f" ((float_of_int @@ Atomic.get evals) /. average_thread_activation_time /. total_time); *) *)
197+
(* (* Logs.info "Updates per CPU-second: %f" ((float_of_int @@ Atomic.get updates) /. average_thread_activation_time /. total_time); *) *)
198+
(* (**) *)
199+
(* (* Option.may (fun v -> ignore @@ Logs.info "max updates: %d for var %a" !max_c Var.pretty_trace v) !max_var; *) *)
200+
(* (* Logs.newline (); *) *)
201+
(* (* (* print_endline "# Solver specific stats"; *) *) *)
202+
(* (* !print_solver_stats (); *) *)
203+
(* (* Logs.newline (); *) *)
204+
(* (* (* Timing.print (M.get_out "timing" Legacy.stdout) "Timings:\n"; *) *) *)
205+
(* (* (* Gc.print_stat stdout; (* too verbose, slow and words instead of MB *) *) *) *)
206+
(* (* let gc = GobGc.print_quick_stat Legacy.stderr in *) *)
207+
(* (* Logs.newline (); *) *)
208+
(* (* 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 *) *)
209+
(**)
210+
(* () *)
211+
(* (* print_string "Do you want to continue? [Y/n]"; *) *)
212+
(* (* flush stdout *) *)
213+
(* (* if read_line () = "n" then raise Break *) *)
214+
(**)
215+
(* let () = *)
216+
(* let write_header = write_csv ["runtime"; "vars"; "evals"; "contexts"; "max_heap"] (* TODO @ !solver_stats_headers *) in *)
217+
(* Option.may write_header stats_csv; *)
218+
(* (* call print_stats on dbg.solver-signal *) *)
219+
(* Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) (Signal_handle print_stats); *)
220+
(* (* call print_stats every dbg.solver-stats-interval *) *)
221+
(* Sys.set_signal Sys.sigvtalrm (Signal_handle print_stats); *)
222+
(* (* 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 *) *)
223+
(* let ssi = get_int "dbg.solver-stats-interval" in *)
224+
(* if ssi > 0 then *)
225+
(* let it = float_of_int ssi in *)
226+
(* ignore Unix.(setitimer ITIMER_VIRTUAL { it_interval = it; it_value = it }); *)
227+
end
228+

‎src/solver/parallelStats.ml‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
open Batteries
2+
open GobConfig
3+
open Goblint_constraint.ConstrSys
4+
5+
module ParallelSolverStats =
6+
struct
7+
open Messages
8+
9+
let cas_success = Atomic.make 0
10+
let cas_fail = Atomic.make 0
11+
let nr_iterations = Atomic.make 0
12+
13+
let start_time = ref 0.
14+
let end_time = ref 0.
15+
16+
let solver_start_event () =
17+
start_time := Unix.gettimeofday ();
18+
Atomic.set cas_success 0;
19+
Atomic.set cas_fail 0
20+
21+
let solver_end_event () =
22+
end_time := Unix.gettimeofday ()
23+
24+
let start_iterate_event job_id =
25+
Atomic.incr nr_iterations
26+
27+
let cas_success_event () = Atomic.incr cas_success
28+
let cas_fail_event () = Atomic.incr cas_fail
29+
30+
let print_stats () =
31+
Logs.info "Cas success: %d" (Atomic.get cas_success);
32+
Logs.info "Cas fail: %d" (Atomic.get cas_fail);
33+
34+
let duration = !end_time -. !start_time in
35+
Logs.info "Solver duration: %.2f" duration;
36+
37+
Logs.info "Iterations: %d" (Atomic.get nr_iterations);
38+
39+
end
40+

0 commit comments

Comments
 (0)