From 84751fead39221a8e01d20a4692faf0b63a7c996 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Mon, 17 Apr 2017 14:19:07 +0200 Subject: [PATCH 1/1] Add a new option to choose tree model at runtime. --- src/options.ml | 20 ++++-- src/run.ml | 174 +++++++++++++++++++++++++++++++------------------ src/run.mli | 15 +++-- src/tatoo.ml | 42 ++++++++---- 4 files changed, 164 insertions(+), 87 deletions(-) diff --git a/src/options.ml b/src/options.ml index b8c5730..c303c80 100644 --- a/src/options.ml +++ b/src/options.ml @@ -7,30 +7,38 @@ let queries = ref [] let stats = ref false let compose = ref false let parallel = ref false +let supported_models = [ "naive", (module Naive_tree : Tree.S); + "compact",(module Compact_tree : Tree.S); + ] +let tree_model = ref (fst (List.hd supported_models)) +let set_model s = tree_model := s let set_string_option r s = r := Some s let specs = align [ "-c", Set count, - " write the number of results only"; + " write the number of results only"; "--count", Set count, " "; "-s", Set stats, - " display timing and various statistics"; + " display timing and various statistics"; "--stats", Set stats, " "; "-d", String (set_string_option input_file), - " specify the input document file [default stdin]"; + " specify the input document file [default stdin]"; "--doc", String (set_string_option input_file), " "; "-o", String (set_string_option output_file), - " specify the output file [default stdout]"; + " specify the output file [default stdout]"; "--out", String (set_string_option output_file), " "; "-C", Set compose, - " compose queries: each query is applied to the results of the \ + " compose queries: each query is applied to the results of the \ previous one [default run all queries from the root node]"; "--compose", Set compose, " "; "-p", Set parallel, - " run all queries in parallel [default run all queries \ + " run all queries in parallel [default run all queries \ sequentially]"; "--parallel", Set parallel, " "; + "-m", Symbol (List.map fst supported_models, set_model), + " specify tree model (naive or compact, default to naive)"; + "--model", Symbol (List.map fst supported_models, set_model), " "; ] let usage_msg = diff --git a/src/run.ml b/src/run.ml index 887eb35..0d0e7e9 100644 --- a/src/run.ml +++ b/src/run.ml @@ -103,7 +103,8 @@ type 'a run = { (* Two 6-way caches used during the top-down and bottom-up phase label * self-set * fc-set * ns-set * parent-set * node-shape -> self-set *) - node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t; + (*node_summaries: (int, int16_unsigned_elt, c_layout) Array1.t; *) + node_summaries: Bytes.t; stats : stats; } @@ -193,7 +194,7 @@ let eval_trans run trans_cache tag summary fcs nss ps ss todo = stats.eval_trans_cache_access <- 1 + stats.eval_trans_cache_access; if res != dummy_set then res - else let new_sat = + else let new_sat = if todo == StateSet.empty then ss else eval_trans_fix run tag summary fcs nss ps ss todo in stats.eval_trans_cache_miss <- 1 + stats.eval_trans_cache_miss; @@ -201,13 +202,18 @@ let eval_trans run trans_cache tag summary fcs nss ps ss todo = new_sat -module Make (T : Tree.S) (L : Deque.S with type elem = T.node) = +module Make (T : Tree.S) = struct + module Tree : Tree.S with type node = T.node = T + module ResultSet : Deque.S with type elem = Tree.node = + Deque.Make (struct type t = Tree.node end) + let make auto tree = - let len = T.size tree in - let ba = Array1.create int16_unsigned c_layout len in - Array1.fill ba 0; + let len = Tree.size tree in + (* let ba = Array1.create int16_unsigned c_layout len in + Array1.fill ba 0; *) + let ba = Bytes.make len '\000' in { tree = tree; auto = auto; @@ -230,7 +236,7 @@ struct } - let top_down run update_res = + let top_down2 run update_res = let num_visited = ref 0 in let i = run.pass in let tree = run.tree in @@ -242,95 +248,137 @@ struct else states_by_rank.(i+1) in + let run_sat = run.sat 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 + let rec common node parent parent_sat kont = + if node == Tree.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 tag = Tree.tag tree node in + let node_id = Tree.preorder tree node in + let fc = Tree.first_child tree node in + let ns = Tree.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 + let s = Char.code (Bytes.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 *) + (node == (Tree.first_child tree parent)) (*is_left *) + (node == (Tree.next_sibling tree parent)) (*is_right *) + (fc != Tree.nil) (* has_left *) + (ns != Tree.nil) (* has_right *) + (Tree.kind tree node) (* kind *) in - run.node_summaries.{node_id} <- s; s + Bytes.unsafe_set run.node_summaries node_id (Char.chr s); s in - let status0 = unsafe_get run.sat node_id 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 run run.td_cache tag summary - (unsafe_get run.sat (T.preorder tree fc)) - (unsafe_get run.sat (T.preorder tree ns)) + (unsafe_get run_sat (Tree.preorder tree fc)) + (unsafe_get run_sat (Tree.preorder tree ns)) parent_sat status0 td_todo in - (* update the cache if the status of the node changed - unsafe_set run.sat node_id status1 status0;*) - if bu_todo == StateSet.empty then begin - unsafe_set run.sat node_id status1 status0; (* write the td_states *) - update_res false status1 node; - let _ = loop_td_and_bu fc node status1 in - loop_td_and_bu ns node status1 (* tail call *) - end else - let fcs1, nss1 = - if last_run then - let nss1 = loop_td_and_bu ns node status1 in - let fcs1 = loop_td_and_bu fc node status1 in - fcs1, nss1 - else - let fcs1 = loop_td_and_bu fc node status1 in - let nss1 = loop_td_and_bu ns node status1 in - fcs1, nss1 - in - let status2 = - eval_trans run run.bu_cache tag - summary fcs1 - nss1 - parent_sat - status1 bu_todo - in - unsafe_set run.sat node_id status2 status0; - if last_run && status2 != StateSet.empty then update_res true status2 node; - status2 + kont summary tag parent_sat status0 status1 fc ns node node_id end + + and kont_pure_td summary tag parent_sat status0 status1 fc ns node node_id = + unsafe_set run_sat node_id status1 status0; (* write the td_states *) + update_res false status1 node; + if fc != Tree.nil then ignore (loop_td fc node status1); + if ns == Tree.nil then StateSet.empty else loop_td ns node status1 (* tail call *) + and kont_td_and_bu summary tag parent_sat status0 status1 fc ns node node_id = + let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu fc node status1 in + let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu ns node status1 in + let status2 = + eval_trans run run.bu_cache tag + summary fcs1 + nss1 + parent_sat + status1 bu_todo + in + unsafe_set run_sat node_id status2 status0; + status2 + and kont_td_and_bu_last summary tag parent_sat status0 status1 fc ns node node_id = + let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu_last ns node status1 in + let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu_last fc node status1 in + let status2 = + eval_trans run run.bu_cache tag + summary fcs1 + nss1 + parent_sat + status1 bu_todo + in + unsafe_set run_sat node_id status2 status0; + if status2 != StateSet.empty then update_res true status2 node; + status2 + and loop_td node parent parent_sat = + common node parent parent_sat kont_pure_td + and loop_td_and_bu node parent parent_sat = + common node parent parent_sat kont_td_and_bu + and loop_td_and_bu_last node parent parent_sat = + common node parent parent_sat kont_td_and_bu_last + in + + let _ = + if bu_todo == StateSet.empty then + loop_td (Tree.root tree) Tree.nil dummy_set + else if last_run then + loop_td_and_bu_last (Tree.root tree) Tree.nil dummy_set + else + loop_td_and_bu (Tree.root tree) Tree.nil dummy_set in - let _ = loop_td_and_bu (T.root tree) T.nil dummy_set in run.pass <- run.pass + 2; run.stats.pass <- run.stats.pass + 1; run.stats.nodes_per_run <- !num_visited :: run.stats.nodes_per_run + type res_op = Dummy | Prepend | Append | Nothing let mk_update_result auto = let sel_states = Ata.get_selecting_states auto in - let res = L.create () in + let res = ResultSet.create () in + let cache = Cache.N2.create Dummy in (fun prepend sat node -> + let sat_id = (sat.StateSet.id :> int) in + let prep_id : int = Obj.magic prepend in + let op = Cache.N2.find cache prep_id sat_id in + let op = + if op == Dummy then + let op = + if StateSet.intersect sel_states sat then + if prepend then + Prepend + else Append + else Nothing + in + let () = Cache.N2.add cache prep_id sat_id op in + op + else op + in + match op with + Dummy | Nothing -> () + | Prepend -> ResultSet.push_front node res + | Append -> ResultSet.push_back node res + (* if StateSet.intersect sel_states sat then begin if prepend then L.push_front node res else L.push_back node res - end), + end*)), (fun () -> res) let mk_update_full_result auto = - let dummy = L.create () in + let dummy = ResultSet.create () in let res_mapper = Cache.N1.create dummy in let () = StateSet.iter - (fun q -> Cache.N1.add res_mapper (q :> int) (L.create())) + (fun q -> Cache.N1.add res_mapper (q :> int) (ResultSet.create())) (Ata.get_selecting_states auto) in (fun prepend sat node -> @@ -338,8 +386,8 @@ struct (fun q -> let res = Cache.N1.find res_mapper (q :> int) in if res != dummy then begin - if prepend then L.push_front node res - else L.push_back node res + if prepend then ResultSet.push_front node res + else ResultSet.push_back node res end ) sat), (fun () -> @@ -352,8 +400,8 @@ struct let auto = run.auto in let sat = IFHTML((List.hd run.sat), run.sat) in let sat0 = Ata.get_starting_states auto in - L.iter (fun node -> - let node_id = T.preorder tree node in + ResultSet.iter (fun node -> + let node_id = Tree.preorder tree node in sat.(node_id) <- sat0) list @@ -362,13 +410,13 @@ struct prepare_run run nodes; let rank = Ata.get_max_rank auto in while run.pass <= rank do - top_down run update_res; + top_down2 run update_res; IFHTML((run.sat <- (Array.copy (List.hd run.sat)) :: run.sat), ()); run.td_cache <- Cache.N6.create dummy_set; run.bu_cache <- Cache.N6.create dummy_set; done; IFHTML((run.sat <- List.tl run.sat), ()); - IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = T.t) tree ,()); + IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = Tree.t) tree ,()); run diff --git a/src/run.mli b/src/run.mli index 705b44f..c67f2d1 100644 --- a/src/run.mli +++ b/src/run.mli @@ -23,9 +23,12 @@ type stats = private { mutable pass : int; mutable nodes_per_run : int list; } -module Make (T : Tree.S) (L : Deque.S with type elem = T.node) : - sig - val eval : Ata.t -> T.t -> L.t -> L.t - val full_eval : Ata.t -> T.t -> L.t -> (State.t * L.t) list - val stats : unit -> stats - end +module Make (T : Tree.S) : +sig + module Tree : Tree.S with type node = T.node + module ResultSet : Deque.S with type elem = Tree.node + + val eval : Ata.t -> Tree.t -> ResultSet.t -> ResultSet.t + val full_eval : Ata.t -> Tree.t -> ResultSet.t -> (State.t * ResultSet.t) list + val stats : unit -> stats +end diff --git a/src/tatoo.ml b/src/tatoo.ml index 5dec2f6..5e8144d 100644 --- a/src/tatoo.ml +++ b/src/tatoo.ml @@ -14,6 +14,13 @@ (***********************************************************************) open Format +let default_gc = Gc.get() +let tuned_gc = { default_gc with + Gc.minor_heap_size = 32*1024*1024; + Gc.major_heap_increment = 8*1024*1024; + Gc.max_overhead = 1000000; + Gc.space_overhead = 100; +} let time f arg msg = let t1 = Unix.gettimeofday () in @@ -44,15 +51,27 @@ let restart_sequential run auto_list tree nodes () = let main () = let () = Options.parse () in + let tree_model = List.assoc !Options.tree_model + Options.supported_models + in + let module T = (val tree_model) in + let module Runtime = Run.Make(T) + in + let doc = let fd, close_fd = match !Options.input_file with None | Some "-" | Some "/dev/stdin" -> stdin, ignore | Some input -> let fd = open_in input in fd, fun () -> close_in fd in - let d = time Compact_tree.load_xml_file fd "parsing xml document" in + let d = time Runtime.Tree.load_xml_file fd "parsing xml document" in close_fd (); d in + let () = + Gc.full_major(); + Gc.compact(); + Gc.set (tuned_gc) + in let queries = time (fun l -> @@ -104,24 +123,23 @@ let main () = Logger.msg `STATS "@[Automaton: @\n%a@]" Ata.print auto) auto_list; end; - let module Naive = Run.Make(Compact_tree)(Compact_node_list) in let result_list = - let root = Compact_node_list.create () in - let () = Compact_node_list.add (Compact_tree.root doc) root in + let root = Runtime.ResultSet.create () in + let () = Runtime.ResultSet.add (Runtime.Tree.root doc) root in let f, msg = match !Options.parallel, !Options.compose with true, true -> - compose_parallel Naive.eval auto_list doc root, "parallel/compose" + compose_parallel Runtime.eval auto_list doc root, "parallel/compose" | true, false -> - restart_parallel Naive.full_eval auto_list doc root, "parallel/restart" + restart_parallel Runtime.full_eval auto_list doc root, "parallel/restart" | false, true -> - compose_sequential Naive.eval auto_list doc root , "sequential/compose" + compose_sequential Runtime.eval auto_list doc root , "sequential/compose" | false, false -> - restart_sequential Naive.eval auto_list doc root, "sequential/restart" + restart_sequential Runtime.eval auto_list doc root, "sequential/restart" in time f () ("evaluating query in " ^ msg ^ " mode") in - let s = Naive.stats () in + let s = Runtime.stats () in Run.( Logger.msg `STATS "@[tree size: %d@\ntraversals: %d@\ntransition fetch cache miss ratio: %f@\ntransition eval cache miss ratio: %f@\nNumber of visited nodes per pass: %a@]" @@ -138,11 +156,11 @@ let main () = output_string output (string_of_int !count); output_string output "\" >\n"; if !Options.count then begin - output_string output (string_of_int (Compact_node_list.length results)); + output_string output (string_of_int (Runtime.ResultSet.length results)); output_char output '\n'; end else - Compact_node_list.iter (fun n -> - Compact_tree.print_xml output doc n; + Runtime.ResultSet.iter (fun n -> + Runtime.Tree.print_xml output doc n; output_char output '\n' ) results; output_string output "\n"; -- 2.17.1