From fafb001934c7d7bdaac2fa150ff86e803c152a82 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 22 Dec 2020 16:27:45 -0500 Subject: [PATCH] feat: add profiling system based on TEF - a `Sidekick_util.Profile` module, deps-free - an optional sidekick.tef library that needs unix+mtime --- sidekick-bin.opam | 1 + src/arith/lra/sidekick_arith_lra.ml | 1 + src/main/dune | 2 +- src/main/main.ml | 2 + src/msat-solver/Sidekick_msat_solver.ml | 6 +- src/smtlib/Process.ml | 8 ++- src/smtlib/dune | 3 +- src/tef/Sidekick_tef.ml | 62 +++++++++++++++++++++ src/tef/Sidekick_tef.mli | 10 ++++ src/tef/dune | 8 +++ src/util/Profile.ml | 74 +++++++++++++++++++++++++ src/util/Profile.mli | 31 +++++++++++ src/util/Sidekick_util.ml | 1 + 13 files changed, 204 insertions(+), 5 deletions(-) create mode 100644 src/tef/Sidekick_tef.ml create mode 100644 src/tef/Sidekick_tef.mli create mode 100644 src/tef/dune create mode 100644 src/util/Profile.ml create mode 100644 src/util/Profile.mli diff --git a/sidekick-bin.opam b/sidekick-bin.opam index 865f7c3b..1f8b71b7 100644 --- a/sidekick-bin.opam +++ b/sidekick-bin.opam @@ -18,6 +18,7 @@ depends: [ "smtlib-utils" { >= "0.1" & < "0.3" } "sidekick" { = version } "menhir" + "mtime" "msat" { >= "0.8" < "0.9" } "ocaml" { >= "4.03" } ] diff --git a/src/arith/lra/sidekick_arith_lra.ml b/src/arith/lra/sidekick_arith_lra.ml index 09c0e85d..2cfc6a6e 100644 --- a/src/arith/lra/sidekick_arith_lra.ml +++ b/src/arith/lra/sidekick_arith_lra.ml @@ -316,6 +316,7 @@ module Make(A : ARG) : S with module A = A = struct let final_check_ (self:state) si (acts:SI.actions) (trail:_ Iter.t) : unit = Log.debug 5 "(th-lra.final-check)"; + Profile.with_ "lra.final-check" @@ fun () -> let simplex = SimpSolver.create self.gensym in encode_neq self si acts trail; (* first, add definitions *) diff --git a/src/main/dune b/src/main/dune index 77c68d7a..5a8ae94c 100644 --- a/src/main/dune +++ b/src/main/dune @@ -5,7 +5,7 @@ (public_name sidekick) (package sidekick-bin) (libraries containers iter result msat sidekick.core sidekick-arith.base-term - sidekick.msat-solver sidekick-bin.smtlib) + sidekick.msat-solver sidekick-bin.smtlib sidekick.tef) (flags :standard -safe-string -color always -open Sidekick_util)) (rule diff --git a/src/main/main.ml b/src/main/main.ml index fe36465a..5c1cf236 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -127,6 +127,8 @@ let check_limits () = raise Out_of_space let main () = + Sidekick_tef.setup(); + at_exit Sidekick_tef.teardown; CCFormat.set_color_default true; (* Administrative duties *) Arg.parse argspec input_file usage; diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml index 3330099d..5c7ffc3e 100644 --- a/src/msat-solver/Sidekick_msat_solver.ml +++ b/src/msat-solver/Sidekick_msat_solver.ml @@ -587,12 +587,15 @@ module Make(A : ARG) let add_clause (self:t) (c:Atom.t IArray.t) : unit = Stat.incr self.count_clause; Log.debugf 50 (fun k->k "(@[solver.add-clause@ %a@])" (Util.pp_iarray Atom.pp) c); - Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default + let pb = Profile.begin_ "add-clause" in + Sat_solver.add_clause_a self.solver (c:> Atom.t array) P.default; + Profile.exit pb let add_clause_l self c = add_clause self (IArray.of_list c) let mk_model (self:t) (lits:lit Iter.t) : Model.t = Log.debug 1 "(smt.solver.mk-model)"; + Profile.with_ "msat-solver.mk-model" @@ fun () -> let module M = Term.Tbl in let m = M.create 128 in let tst = self.si.tst in @@ -614,6 +617,7 @@ module Make(A : ARG) let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ()) ~assumptions (self:t) : res = + Profile.with_ "msat-solver.solve" @@ fun () -> let do_on_exit () = List.iter (fun f->f()) on_exit; in diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml index 336c130e..a6e72523 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Process.ml @@ -1,6 +1,7 @@ (** {2 Conversion into {!Term.t}} *) module BT = Sidekick_base_term +module Profile = Sidekick_util.Profile open Sidekick_base_term [@@@ocaml.warning "-32"] @@ -153,8 +154,10 @@ let solve let on_progress = if progress then Some (mk_progress()) else None in let res = - Solver.solve ~assumptions ?on_progress s + Profile.with_ "solve" begin fun () -> + Solver.solve ~assumptions ?on_progress s (* ?gc ?restarts ?time ?memory ?progress *) + end in let t2 = Sys.time () in Printf.printf "\r"; flush stdout; @@ -176,11 +179,12 @@ let solve Format.printf "Unsat (%.3f/%.3f/-)@." t1 (t2-.t1); | Solver.Unsat {proof=Some p;_} -> if check then ( - Solver.Proof.check p; + Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p); ); begin match dot_proof with | None -> () | Some file -> + Profile.with_ "dot.proof" @@ fun () -> CCIO.with_out file (fun oc -> Log.debugf 1 (fun k->k "write proof into `%s`" file); diff --git a/src/smtlib/dune b/src/smtlib/dune index e3230bbf..2e0a0136 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -3,5 +3,6 @@ (public_name sidekick-bin.smtlib) (libraries containers zarith msat sidekick.core sidekick.util sidekick.msat-solver sidekick-arith.base-term sidekick.th-bool-static - sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils) + sidekick.mini-cc sidekick.th-data sidekick-arith.lra msat.backend smtlib-utils + sidekick.tef) (flags :standard -warn-error -a+8 -open Sidekick_util)) diff --git a/src/tef/Sidekick_tef.ml b/src/tef/Sidekick_tef.ml new file mode 100644 index 00000000..d7443323 --- /dev/null +++ b/src/tef/Sidekick_tef.ml @@ -0,0 +1,62 @@ + +module P = Sidekick_util.Profile + +let active = lazy ( + match Sys.getenv "TEF" with + | "1"|"true" -> true | _ -> false + | exception Not_found -> false +) + +let program_start = Mtime_clock.now() + +module Make() + : P.BACKEND += struct + let first_ = ref true + let closed_ = ref false + + let teardown_ oc = + if not !closed_ then ( + closed_ := true; + output_char oc ']'; (* close array *) + flush oc; + close_out_noerr oc + ) + + (* connection to subprocess writing into the file *) + let oc = + let oc = Unix.open_process_out "gzip - --stdout > trace.json.gz" in + output_char oc '['; + at_exit (fun () -> teardown_ oc); + oc + + let get_ts () : float = + let now = Mtime_clock.now() in + Mtime.Span.to_us (Mtime.span program_start now) + + let emit_event ~name ~start ~end_ () : unit = + let dur = end_ -. start in + let ts = start in + let pid = Unix.getpid() in + let tid = Thread.id (Thread.self()) in + if !first_ then ( + first_ := false; + ) else ( + output_string oc ",\n"; + ); + Printf.fprintf oc + {json|{"pid": %d,"cat":"","tid": %d,"dur": %.2f,"ts": %.2f,"name":"%s","ph":"X"}|json} + pid tid dur ts name; + flush oc + + let teardown () = teardown_ oc +end + +let setup_ = lazy ( + let lazy active = active in + let b = if active then Some (module Make() : P.BACKEND) else None in + P.Control.setup b +) + +let setup () = Lazy.force setup_ +let teardown = P.Control.teardown diff --git a/src/tef/Sidekick_tef.mli b/src/tef/Sidekick_tef.mli new file mode 100644 index 00000000..33168a57 --- /dev/null +++ b/src/tef/Sidekick_tef.mli @@ -0,0 +1,10 @@ + +(** {1 Tracing Event Format} + + A nice profiling format based on json, useful for visualizing what goes on. + See https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/ +*) + +val setup : unit -> unit + +val teardown : unit -> unit diff --git a/src/tef/dune b/src/tef/dune new file mode 100644 index 00000000..db8f8b5e --- /dev/null +++ b/src/tef/dune @@ -0,0 +1,8 @@ + +(library + (name sidekick_tef) + (public_name sidekick.tef) + (synopsis "profiling backend based on TEF") + (optional) + (flags :standard -warn-error -a+8) + (libraries sidekick.util unix threads mtime mtime.clock.os)) diff --git a/src/util/Profile.ml b/src/util/Profile.ml new file mode 100644 index 00000000..3f0afc96 --- /dev/null +++ b/src/util/Profile.ml @@ -0,0 +1,74 @@ + +module type BACKEND = sig + val get_ts : unit -> float + + val emit_event : + name : string -> + start : float -> + end_ : float -> + unit -> + unit + + val teardown : unit -> unit +end + +type backend = (module BACKEND) + +type probe = + | No_probe + | Probe of { + name: string; + start: float; + } + +(* where to print events *) +let out_ : backend option ref = ref None + +let begin_with_ (module B:BACKEND) name : probe = + Probe {name; start=B.get_ts ()} + +let[@inline] begin_ name : probe = + match !out_ with + | None -> No_probe + | Some b -> begin_with_ b name + +(* slow path *) +let exit_full_ (module B : BACKEND) name start = + let now = B.get_ts() in + B.emit_event ~name ~start ~end_:now () + +let exit_with_ b pb = + match pb with + | No_probe -> () + | Probe {name; start} -> exit_full_ b name start + +let[@inline] exit pb = + match pb, !out_ with + | Probe {name;start}, Some b -> exit_full_ b name start + | _ -> () + +let[@inline] with_ name f = + match !out_ with + | None -> f() + | Some b -> + let pb = begin_with_ b name in + try + let x = f() in + exit_with_ b pb; + x + with e -> + exit_with_ b pb; + raise e + +module Control = struct + let setup b = + assert (!out_ = None); + out_ := b + + let teardown () = + match !out_ with + | None -> () + | Some (module B) -> + out_ := None; + B.teardown() +end diff --git a/src/util/Profile.mli b/src/util/Profile.mli new file mode 100644 index 00000000..d697a39a --- /dev/null +++ b/src/util/Profile.mli @@ -0,0 +1,31 @@ + +(** {1 Profiling probes} *) + +type probe + +val begin_ : string -> probe + +val exit : probe -> unit + +val with_ : string -> (unit -> 'a) -> 'a + +module type BACKEND = sig + val get_ts : unit -> float + + val emit_event : + name : string -> + start : float -> + end_ : float -> + unit -> + unit + + val teardown : unit -> unit +end + +type backend = (module BACKEND) + +module Control : sig + val setup : backend option -> unit + + val teardown : unit -> unit +end diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml index 710e65bf..53b0b2a3 100644 --- a/src/util/Sidekick_util.ml +++ b/src/util/Sidekick_util.ml @@ -12,3 +12,4 @@ module Intf = Intf module Bag = Bag module Stat = Stat module Hash = Hash +module Profile = Profile