From e56b9fbeaed04c1f2fb7019de34f7d8e87d6db73 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Sun, 1 Dec 2013 21:14:54 +0100 Subject: [PATCH] Split the formula cache into a top-down and bottom-up cache. --- Remakefile.in | 12 ++- src/run.ml | 224 +++++++++++++++++++++++++++++--------------------- src/run.mli | 8 +- src/tatoo.ml | 8 +- 4 files changed, 148 insertions(+), 104 deletions(-) diff --git a/Remakefile.in b/Remakefile.in index b3b1168..a4fe1c9 100644 --- a/Remakefile.in +++ b/Remakefile.in @@ -17,7 +17,7 @@ OCAMLDEP = @OCAMLDEP@ ODEPS = tools/odeps.sh $(OCAMLDEP) OCAMLC = @OCAMLC@ OCAMLOPT = @OCAMLOPT@ -OCAMLFLAGS = @OCAMLFLAGS@ +OCAMLFLAGS = @OCAMLFLAGS@ OCAMLOPTFLAGS = @OCAMLOPTFLAGS@ OCAMLCFLAGS = @OCAMLCFLAGS@ OCAMLYACC = @OCAMLYACC@ @@ -59,9 +59,12 @@ distclean: clean test_clean javac $< %.native$(EXE): %.cmx %.depx + if test -f $@".flags"; then + FLAGS=`cat $@".flags"` + fi objects=`cat $*.depx | xargs | sed 's/[.]depx/.cmx/g'` $(REMAKE) OCAMLNATIVE="-native" $objects #ensure all objects have been built - $(OCAMLOPT) -o $@ $(OCAMLFLAGS) $(OCAMLOPTFLAGS) $(OCAMLFINDLINKFLAGS) $(OCAMLFINDFLAGS) $objects $< + $(OCAMLOPT) -o $@ $(OCAMLFLAGS) $(OCAMLOPTFLAGS) $(OCAMLFINDLINKFLAGS) $(OCAMLFINDFLAGS) $FLAGS $objects $< %.byte$(EXE): %.cmo %.depo objects=`cat $*.depo | xargs | sed 's/[.]depo/.cmo/g'` @@ -85,7 +88,10 @@ distclean: clean test_clean REMAKE="$(REMAKE) OCAMLNATIVE=$NATIVE" OCAMLDEP="$(OCAMLDEP) $(OCAMLFINDFLAGS)" SRC=$(SRC) - COMPILE="$(OCAMLOPT) $(OCAMLFLAGS) $(OCAMLOPTFLAGS) $(OCAMLFINDFLAGS)" + if test -f "$base".flags; then + FLAGS=`cat "$base".flags` + fi + COMPILE="$(OCAMLOPT) $(OCAMLFLAGS) $(OCAMLOPTFLAGS) $(OCAMLFINDFLAGS) $FLAGS" . tools/ocamldriver.sh %.cmo %.depo: diff --git a/src/run.ml b/src/run.ml index 7677af1..1f59ef8 100644 --- a/src/run.ml +++ b/src/run.ml @@ -21,21 +21,21 @@ open Misc type stats = { run : int; tree_size : int; - cache2_access : int; - cache2_hit : int; - cache5_access : int; - cache5_hit : int; + fetch_trans_cache_access : int; + fetch_trans_cache_hit : int; + eval_trans_cache_access : int; + eval_trans_cache_hit : int; } -let cache2_hit = ref 0 -let cache2_access = ref 0 -let cache5_hit = ref 0 -let cache5_access = ref 0 +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 () = - cache2_hit := 0; - cache2_access := 0; - cache5_hit := 0; - cache5_access := 0 + fetch_trans_cache_hit := 0; + fetch_trans_cache_access := 0; + eval_trans_cache_hit := 0; + eval_trans_cache_access := 0 module Make (T : Tree.S) = @@ -48,44 +48,40 @@ module Make (T : Tree.S) = type t = int let dummy = -1 (* - 4444444444443210 - 4 -> kind - 3 -> is_left - 2 -> is_right + 333333333333333210 + 3333 -> kind + 2 -> has_right 1 -> has_left - 0 -> has_right + 0 -> is_left/is_right *) + let is_left (s : t) : bool = + s land 1 == 1 - let has_right (s : t) : bool = - Obj.magic (s land 1) + let is_right (s : t) : bool = + s land 1 == 0 let has_left (s : t) : bool = - Obj.magic ((s lsr 1) land 1) - - let is_right (s : t) : bool = - Obj.magic ((s lsr 2) land 1) + (s lsr 1) land 1 == 1 - let is_left (s : t) : bool = - Obj.magic ((s lsr 3) land 1) + let has_right (s : t) : bool = + (s lsr 2) land 1 == 1 let kind (s : t) : Tree.NodeKind.t = - Obj.magic (s lsr 4) + Obj.magic (s lsr 3) - let make is_left is_right has_left has_right kind = - ((Obj.magic kind) lsl 4) lor - ((int_of_bool is_left) lsl 3) lor - ((int_of_bool is_right) lsl 2) lor + let make is_left has_left has_right kind = + (int_of_bool is_left) lor ((int_of_bool has_left) lsl 1) lor - (int_of_bool has_right) - + ((int_of_bool has_right) lsl 2) lor + ((Obj.magic kind) lsl 3) end type node_status = { rank : int; sat : StateSet.t; (* States that are satisfied at the current node *) todo : StateSet.t; (* States that remain to be proven *) - (* For every node_status and automaton a, - a.states - (sat U todo) = unsat *) + (* For every node_status and automaton a, + a.states - (sat U todo) = unsat *) summary : NodeSummary.t; (* Summary of the shape of the node *) } (* Describe what is kept at each node for a run *) @@ -132,19 +128,13 @@ module Make (T : Tree.S) = (* The automaton to be run *) status : NodeStatus.t array; (* A mapping from node preorders to NodeStatus *) - mutable redo : bool; - (* A boolean indicating whether the run is incomplete *) mutable pass : int; - (* The number of times this run was updated *) - mutable cache2 : Ata.Formula.t Cache.N2.t; + mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t; (* A cache from states * label to list of transitions *) - mutable cache5 : NodeStatus.t Cache.N5.t; + mutable td_cache : NodeStatus.t Cache.N5.t; + mutable bu_cache : NodeStatus.t Cache.N5.t; } - let pass r = r.pass - let stable r = not r.redo - let auto r = r.auto - let tree r = r.tree let dummy_form = Ata.Formula.stay State.dummy @@ -155,10 +145,10 @@ module Make (T : Tree.S) = tree = tree; auto = auto; status = Array.create len dummy_status; - redo = true; pass = 0; - cache2 = Cache.N2.create dummy_form; - cache5 = Cache.N5.create dummy_status; + fetch_trans_cache = Cache.N2.create dummy_form; + td_cache = Cache.N5.create dummy_status; + bu_cache = Cache.N5.create dummy_status; } let get_status a i = @@ -193,21 +183,21 @@ END StateSet.print config.todo i - let get_form cache2 auto tag q = + let get_form fetch_trans_cache auto tag q = let phi = - incr cache2_access; - Cache.N2.find cache2 (tag.QName.id :> int) (q :> int) + incr fetch_trans_cache_access; + Cache.N2.find fetch_trans_cache (tag.QName.id :> int) (q :> int) in if phi == dummy_form then let phi = Ata.get_form auto tag q in let () = Cache.N2.add - cache2 + fetch_trans_cache (tag.QName.id :> int) (q :> int) phi in phi else begin - incr cache2_hit; + incr fetch_trans_cache_hit; phi end @@ -276,7 +266,7 @@ DEFINE AND_(t1,t2) = loop phi - let eval_trans_aux auto cache2 tag fcs nss ps old_status = + let eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status = let { sat = old_sat; todo = old_todo; summary = old_summary } as os_node = old_status.NodeStatus.node @@ -284,7 +274,7 @@ DEFINE AND_(t1,t2) = let sat, todo = StateSet.fold (fun q ((a_sat, a_todo) as acc) -> let phi = - get_form cache2 auto tag q + get_form fetch_trans_cache auto tag q in let v = eval_form phi fcs nss ps old_status old_summary in @@ -299,43 +289,44 @@ DEFINE AND_(t1,t2) = else old_status - let eval_trans auto cache2 cache5 tag fcs nss ps ss = - let rec loop old_status = - let new_status = - eval_trans_aux auto cache2 tag fcs nss ps old_status - in - if new_status == old_status then old_status else loop new_status + let rec eval_trans_fix auto fetch_trans_cache tag fcs nss ps old_status = + let new_status = + eval_trans_aux auto fetch_trans_cache tag fcs nss ps old_status in + if new_status == old_status then old_status else + eval_trans_fix auto fetch_trans_cache tag fcs nss ps new_status + + + let eval_trans auto fetch_trans_cache td_cache tag fcs nss ps ss = let fcsid = (fcs.NodeStatus.id :> int) in let nssid = (nss.NodeStatus.id :> int) in let psid = (ps.NodeStatus.id :> int) in let ssid = (ss.NodeStatus.id :> int) in let tagid = (tag.QName.id :> int) in - let res = Cache.N5.find cache5 tagid ssid fcsid nssid psid in - incr cache5_access; - if res != dummy_status then begin incr cache5_hit; res end - else let new_status = loop ss in - Cache.N5.add cache5 tagid ssid fcsid nssid psid new_status; + let res = Cache.N5.find td_cache tagid ssid fcsid nssid psid in + incr eval_trans_cache_access; + if res != dummy_status then begin incr eval_trans_cache_hit; res end + else let new_status = eval_trans_fix auto fetch_trans_cache tag fcs nss ps ss in + Cache.N5.add td_cache tagid ssid fcsid nssid psid new_status; new_status - - let top_down run = let i = run.pass in let tree = run.tree in let auto = run.auto in let status = run.status in - let cache2 = run.cache2 in - let cache5 = run.cache5 in + let fetch_trans_cache = run.fetch_trans_cache in + let td_cache = run.td_cache in + let bu_cache = run.bu_cache 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 + 1 = Array.length states_by_rank then StateSet.empty else states_by_rank.(i+1) in - let rec loop node = - let node_id = T.preorder tree node in - if node != T.nil then begin + let rec loop_td_and_bu node = + if node == T.nil then () else begin + let node_id = T.preorder tree node in let parent = T.parent tree node in let fc = T.first_child tree node in let fc_id = T.preorder tree fc in @@ -351,16 +342,15 @@ DEFINE AND_(t1,t2) = { rank = i; sat = c.NodeStatus.node.sat; todo = td_todo; - summary = let summary = c.NodeStatus.node.summary - in - if summary != NodeSummary.dummy then summary - else - 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 *) + summary = + let summary = c.NodeStatus.node.summary in + if summary != NodeSummary.dummy then summary + else + NodeSummary.make + (node != T.next_sibling tree parent) + (fc != T.nil) (* has_left *) + (ns != T.nil) (* has_right *) + (T.kind tree node) (* kind *) } else c in @@ -372,14 +362,14 @@ DEFINE AND_(t1,t2) = let status1 = if status0.NodeStatus.node.todo == StateSet.empty then status0 else begin - let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in + let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in (* update the cache if the status of the node changed *) if status1 != status0 then status.(node_id) <- status1; status1 end in (* recursively traverse the first child *) - let () = loop fc in + let () = loop_td_and_bu fc in (* here we re-enter the node from its first child, get the new status of the first child *) let fcs1 = unsafe_get_status status fc_id in @@ -394,19 +384,64 @@ DEFINE AND_(t1,t2) = let status2 = if status1.NodeStatus.node.todo == StateSet.empty then status1 else begin - let status2 = eval_trans auto cache2 cache5 tag fcs1 nss ps status1 in + let status2 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss ps status1 in if status2 != status1 then status.(node_id) <- status2; status2 end in - let () = loop ns in + let () = loop_td_and_bu ns in let nss1 = unsafe_get_status status ns_id in if status2.NodeStatus.node.todo != StateSet.empty then - let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in + let status3 = eval_trans auto fetch_trans_cache bu_cache tag fcs1 nss1 ps status2 in if status3 != status2 then status.(node_id) <- status3 end + and loop_td_only node = + if node == T.nil then () else begin + let node_id = T.preorder tree node in + let parent = T.parent tree node in + let fc = T.first_child tree node in + let fc_id = T.preorder tree fc in + let ns = T.next_sibling tree node in + let ns_id = T.preorder tree ns in + let tag = T.tag tree node in + (* We enter the node from its parent *) + let status0 = + let c = unsafe_get_status status node_id in + if c.NodeStatus.node.rank < i then + (* first time we visit the node during this run *) + NodeStatus.make + { rank = i; + sat = c.NodeStatus.node.sat; + todo = td_todo; + summary = + let summary = c.NodeStatus.node.summary in + if summary != NodeSummary.dummy then summary + else + NodeSummary.make + (node != T.next_sibling tree parent) + (fc != T.nil) (* has_left *) + (ns != T.nil) (* has_right *) + (T.kind tree node) (* kind *) + } + else c + in + (* get the node_statuses for the first child, next sibling and parent *) + let ps = unsafe_get_status status (T.preorder tree parent) in + let fcs = unsafe_get_status status fc_id in + let nss = unsafe_get_status status ns_id in + (* evaluate the transitions with all this statuses *) + if status0.NodeStatus.node.todo != StateSet.empty then begin + let status1 = eval_trans auto fetch_trans_cache td_cache tag fcs nss ps status0 in + (* update the cache if the status of the node changed *) + if status1 != status0 then status.(node_id) <- status1; + end; + (* recursively traverse the first child *) + loop_td_only fc; + loop_td_only ns + end in - loop (T.root tree) + if bu_todo == StateSet.empty then loop_td_only (T.root tree) + else loop_td_and_bu (T.root tree) let get_results run = @@ -478,8 +513,7 @@ DEFINE AND_(t1,t2) = todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto); summary = NodeSummary.make - (node == T.first_child tree parent) (* is_left *) - (node == T.next_sibling tree parent) (* is_right *) + (node != T.next_sibling tree parent) (* is_left *) (fc != T.nil) (* has_left *) (ns != T.nil) (* has_right *) (T.kind tree node) (* kind *) @@ -497,7 +531,9 @@ DEFINE AND_(t1,t2) = prepare_run run nodes; for i = 0 to Ata.get_max_rank auto do top_down run; - run.pass <- run.pass + 1 + run.pass <- run.pass + 1; + run.td_cache <- Cache.N5.create dummy_status; + run.bu_cache <- Cache.N5.create dummy_status; done; pass := Ata.get_max_rank auto + 1; IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree); @@ -515,10 +551,10 @@ DEFINE AND_(t1,t2) = let stats () = { tree_size = !tree_size; run = !pass; - cache2_access = !cache2_access; - cache2_hit = !cache2_hit; - cache5_access = !cache5_access; - cache5_hit = !cache5_hit; + 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; } end diff --git a/src/run.mli b/src/run.mli index 579dd8a..725192e 100644 --- a/src/run.mli +++ b/src/run.mli @@ -14,10 +14,10 @@ (***********************************************************************) type stats = { run : int; tree_size : int; - cache2_access : int; - cache2_hit : int; - cache5_access : int; - cache5_hit : int; + fetch_trans_cache_access : int; + fetch_trans_cache_hit : int; + eval_trans_cache_access : int; + eval_trans_cache_hit : int; } module Make (T : Tree.S) : sig diff --git a/src/tatoo.ml b/src/tatoo.ml index 485d8e1..6464cb4 100644 --- a/src/tatoo.ml +++ b/src/tatoo.ml @@ -15,6 +15,8 @@ open Format + + let time f arg msg = let t1 = Unix.gettimeofday () in let r = f arg in @@ -123,10 +125,10 @@ let main () = let s = Naive.stats () in Run.( Logger.msg `STATS - "@[tree size: %d@\ntraversals: %d@\ncache2 hit ratio: %f@\ncache5 hit ratio: %f@]" + "@[tree size: %d@\ntraversals: %d@\ntransition fetch cache hit ratio: %f@\ntransition eval cache hit ratio: %f@]" s.tree_size s.run - (float s.cache2_hit /. float s.cache2_access) - (float s.cache5_hit /. float s.cache5_access)); + (float s.fetch_trans_cache_hit /. float s.fetch_trans_cache_access) + (float s.eval_trans_cache_hit /. float s.eval_trans_cache_access)); time (fun () -> let count = ref 1 in List.iter (fun results -> -- 2.17.1