From: Kim Nguyễn Date: Sat, 11 Jan 2014 20:56:59 +0000 (+0100) Subject: Refactor the statistics gathering code in run.ml X-Git-Tag: v0.1~2 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=836d6ea0aebf1f947faa74db1d78168afb882930;ds=sidebyside Refactor the statistics gathering code in run.ml --- diff --git a/src/run.ml b/src/run.ml index 53f48c3..bc6518a 100644 --- a/src/run.ml +++ b/src/run.ml @@ -20,25 +20,15 @@ open Format open Misc open Bigarray -type stats = { run : int; +type stats = { mutable pass : int; tree_size : int; - fetch_trans_cache_access : int; - fetch_trans_cache_hit : int; - eval_trans_cache_access : int; - eval_trans_cache_hit : int; + mutable fetch_trans_cache_access : int; + mutable fetch_trans_cache_hit : int; + mutable eval_trans_cache_access : int; + mutable eval_trans_cache_hit : int; + mutable nodes_per_run : int list; } -let fetch_trans_cache_hit = ref 0 -let fetch_trans_cache_access = ref 0 -let eval_trans_cache_hit = ref 0 -let eval_trans_cache_access = ref 0 -let reset_stat_counters () = - fetch_trans_cache_hit := 0; - fetch_trans_cache_access := 0; - eval_trans_cache_hit := 0; - eval_trans_cache_access := 0 - - module NodeSummary = struct (* Pack into an integer the result of the is_* and has_ predicates @@ -114,14 +104,17 @@ END label * self-set * fc-set * ns-set * parent-set * node-shape -> self-set *) node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t; - + stats : stats; } let dummy_form = Ata.Formula.stay State.dummy - let get_form fetch_trans_cache auto tag q = + let get_form run tag q = + let auto = run.auto in + let fetch_trans_cache = run.fetch_trans_cache in + let stats = run.stats in let phi = - incr fetch_trans_cache_access; + stats.fetch_trans_cache_access <- stats.fetch_trans_cache_access + 1; Cache.N2.find fetch_trans_cache (tag.QName.id :> int) (q :> int) in if phi == dummy_form then @@ -133,7 +126,7 @@ END (q :> int) phi in phi else begin - incr fetch_trans_cache_hit; + stats.fetch_trans_cache_hit <- stats.fetch_trans_cache_hit + 1; phi end @@ -169,10 +162,10 @@ END loop phi - let eval_trans_aux auto trans_cache tag summary fcs nss ps sat todo = + let eval_trans_aux run tag summary fcs nss ps sat todo = StateSet.fold (fun q (a_sat) -> let phi = - get_form trans_cache auto tag q + get_form run tag q in if eval_form phi fcs nss ps a_sat summary then StateSet.add q a_sat @@ -180,28 +173,32 @@ END ) todo sat - let rec eval_trans_fix auto trans_cache tag summary fcs nss ps sat todo = + let rec eval_trans_fix run tag summary fcs nss ps sat todo = let new_sat = - eval_trans_aux auto trans_cache tag summary fcs nss ps sat todo + eval_trans_aux run tag summary fcs nss ps sat todo in if new_sat == sat then sat else - eval_trans_fix auto trans_cache tag summary fcs nss ps new_sat todo + eval_trans_fix run tag summary fcs nss ps new_sat todo - let eval_trans auto fetch_trans_cache eval_cache tag summary fcs nss ps ss todo = + let eval_trans run trans_cache tag summary fcs nss ps ss todo = + let stats = run.stats in let fcsid = (fcs.StateSet.id :> int) in let nssid = (nss.StateSet.id :> int) in let psid = (ps.StateSet.id :> int) in let ssid = (ss.StateSet.id :> int) in let tagid = (tag.QName.id :> int) in - let res = Cache.N6.find eval_cache tagid summary ssid fcsid nssid psid in - incr eval_trans_cache_access; - if res != dummy_set then begin incr eval_trans_cache_hit; res end - else let new_sat = - eval_trans_fix auto fetch_trans_cache tag summary fcs nss ps ss todo - in - Cache.N6.add eval_cache tagid summary ssid fcsid nssid psid new_sat; - new_sat + + let res = Cache.N6.find trans_cache tagid summary ssid fcsid nssid psid in + stats.eval_trans_cache_access <- 1 + stats.eval_trans_cache_access; + if res != dummy_set then begin + stats.eval_trans_cache_hit <- 1 + stats.eval_trans_cache_hit; + res + end else let new_sat = + eval_trans_fix run tag summary fcs nss ps ss todo + in + Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_sat; + new_sat module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = @@ -209,6 +206,8 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = let make auto tree = let len = T.size tree in + let ba = Array1.create int16_unsigned c_layout len in + Array1.fill ba 0; { tree = tree; auto = auto; @@ -218,50 +217,60 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = fetch_trans_cache = Cache.N2.create dummy_form; td_cache = Cache.N6.create dummy_set; bu_cache = Cache.N6.create dummy_set; - node_summaries = let ba = Array1.create int16_unsigned c_layout len in - Array1.fill ba 0; ba + node_summaries = ba; + stats = { + pass = 0; + tree_size = len; + fetch_trans_cache_access = 0; + fetch_trans_cache_hit = 0; + eval_trans_cache_access = 0; + eval_trans_cache_hit = 0; + nodes_per_run = []; + } } let top_down run update_res = - let i = run.pass in - let tree = run.tree in - let auto = run.auto in - let states_by_rank = Ata.get_states_by_rank auto in - let td_todo = states_by_rank.(i) in - let bu_todo = - if i == Array.length states_by_rank - 1 then StateSet.empty - else - states_by_rank.(i+1) - in - let last_run = i >= Array.length states_by_rank - 2 in - let rec loop_td_and_bu node parent parent_sat = - if node == T.nil then StateSet.empty - else begin - let tag = T.tag tree node in - let node_id = T.preorder tree node in - let fc = T.first_child tree node in - let ns = T.next_sibling tree node in - (* We enter the node from its parent *) - let summary = - let s = Array1.unsafe_get run.node_summaries node_id in - if s != 0 then s else - let s = + let num_visited = ref 0 in + let i = run.pass in + let tree = run.tree in + let auto = run.auto in + let states_by_rank = Ata.get_states_by_rank auto in + let td_todo = states_by_rank.(i) in + let bu_todo = + if i == Array.length states_by_rank - 1 then StateSet.empty + else + states_by_rank.(i+1) + in + let last_run = i >= Array.length states_by_rank - 2 in + let rec loop_td_and_bu node parent parent_sat = + if node == T.nil then StateSet.empty + else begin + incr num_visited; + let tag = T.tag tree node in + let node_id = T.preorder tree node in + let fc = T.first_child tree node in + let ns = T.next_sibling tree node in + (* We enter the node from its parent *) + let summary = + let s = Array1.unsafe_get run.node_summaries node_id in + if s != 0 then s else + let s = NodeSummary.make (node == (T.first_child tree parent)) (*is_left *) (node == (T.next_sibling tree parent))(*is_right *) (fc != T.nil) (* has_left *) (ns != T.nil) (* has_right *) (T.kind tree node) (* kind *) - in - run.node_summaries.{node_id} <- s; s - in + in + run.node_summaries.{node_id} <- s; s + in let status0 = unsafe_get run.sat node_id in (* get the node_statuses for the first child, next sibling and parent *) (* evaluate the transitions with all this statuses *) let status1 = - eval_trans - auto run.fetch_trans_cache run.td_cache tag + eval_trans run + run.td_cache tag summary (unsafe_get run.sat (T.preorder tree fc)) (unsafe_get run.sat (T.preorder tree ns)) @@ -289,7 +298,7 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = fcs1, nss1 in let status2 = - eval_trans auto run.fetch_trans_cache run.bu_cache tag + eval_trans run run.bu_cache tag summary fcs1 nss1 parent_sat @@ -301,7 +310,10 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = end in let _ = loop_td_and_bu (T.root tree) T.nil dummy_set in - run.pass <- run.pass + 2 + run.pass <- run.pass + 2; + run.stats.pass <- run.stats.pass + 1; + run.stats.nodes_per_run <- !num_visited :: run.stats.nodes_per_run + let mk_update_result auto = @@ -346,12 +358,8 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = let node_id = T.preorder tree node in sat.(node_id) <- sat0) list - let tree_size = ref 0 - let pass = ref 0 let compute_run auto tree nodes update_res = - pass := 0; - tree_size := T.size tree; let run = make auto tree in prepare_run run nodes; let rank = Ata.get_max_rank auto in @@ -362,29 +370,26 @@ module Make (T : Tree.S) (L : Node_list.S with type node = T.node) = run.bu_cache <- Cache.N6.create dummy_set; done; IFHTML((run.sat <- List.tl run.sat), ()); - pass := Ata.get_max_rank auto + 1; IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = T.t) tree ,()); run + let last_stats = ref None let full_eval auto tree nodes = let update_full,get_full = mk_update_full_result auto in - let _ = compute_run auto tree nodes update_full in + let run = compute_run auto tree nodes update_full in + last_stats := Some run.stats; get_full () let eval auto tree nodes = let update_res,get_res = mk_update_result auto in - let _ = compute_run auto tree nodes update_res in + let run = compute_run auto tree nodes update_res in + last_stats := Some run.stats; get_res () - let stats () = { - tree_size = !tree_size; - run = !pass; - fetch_trans_cache_access = !fetch_trans_cache_access; - fetch_trans_cache_hit = !fetch_trans_cache_hit; - eval_trans_cache_access = !eval_trans_cache_access; - eval_trans_cache_hit = !eval_trans_cache_hit; - } + let stats () = match !last_stats with + Some s -> s.nodes_per_run <- List.rev s.nodes_per_run;s + | None -> failwith "Missing stats" end diff --git a/src/run.mli b/src/run.mli index e124e8a..c942277 100644 --- a/src/run.mli +++ b/src/run.mli @@ -12,13 +12,17 @@ (* ../LICENSE. *) (* *) (***********************************************************************) -type stats = { run : int; + + +type stats = private { mutable pass : int; tree_size : int; - fetch_trans_cache_access : int; - fetch_trans_cache_hit : int; - eval_trans_cache_access : int; - eval_trans_cache_hit : int; + mutable fetch_trans_cache_access : int; + mutable fetch_trans_cache_hit : int; + mutable eval_trans_cache_access : int; + mutable eval_trans_cache_hit : int; + mutable nodes_per_run : int list; } + module Make (T : Tree.S) (L : Node_list.S with type node = T.node) : sig val eval : Ata.t -> T.t -> L.t -> L.t diff --git a/src/tatoo.ml b/src/tatoo.ml index 0987b6d..e0f29ee 100644 --- a/src/tatoo.ml +++ b/src/tatoo.ml @@ -124,10 +124,13 @@ let main () = let s = Naive.stats () in Run.( Logger.msg `STATS - "@[tree size: %d@\ntraversals: %d@\ntransition fetch cache hit ratio: %f@\ntransition eval cache hit ratio: %f@]" - s.tree_size s.run + "@[tree size: %d@\ntraversals: %d@\ntransition fetch cache hit ratio: %f@\ntransition eval cache hit ratio: %f@\nNumber of visited nodes per pass: %a@]" + s.tree_size s.pass (float s.fetch_trans_cache_hit /. float s.fetch_trans_cache_access) - (float s.eval_trans_cache_hit /. float s.eval_trans_cache_access)); + (float s.eval_trans_cache_hit /. float s.eval_trans_cache_access) + (let i = ref 0 in + Pretty.print_list ~sep:"," (fun fmt n -> Format.fprintf fmt "%i: %i" !i n;incr i)) + s.nodes_per_run); time (fun () -> let count = ref 1 in List.iter (fun results ->