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

@@ -18,6 +18,7 @@ depends: [
   "smtlib-utils" { >= "0.1" & < "0.3" }
   "sidekick" { = version }
   "menhir"
+  "mtime"
   "msat" { >= "0.8" < "0.9" }
   "ocaml" { >= "4.03" }
 ]

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 *)

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

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;

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

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);

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))

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

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

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))

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

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

src/util/Sidekick_util.ml

@@ -12,3 +12,4 @@ module Intf = Intf
 module Bag = Bag
 module Stat = Stat
 module Hash = Hash
+module Profile = Profile