From 2af07a38c94296187fd345f387eb2595e0af93ab Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Tue, 18 Apr 2017 10:37:39 +0200 Subject: [PATCH] Implement a pseudo jit (store closures in the look-up table instead of data) --- src/run.ml | 207 +++++++++++++++++++++++++---------------------------- 1 file changed, 98 insertions(+), 109 deletions(-) diff --git a/src/run.ml b/src/run.ml index 0d0e7e9..89aae12 100644 --- a/src/run.ml +++ b/src/run.ml @@ -18,7 +18,6 @@ INCLUDE "debug.ml" open Format open Misc -open Bigarray type stats = { mutable pass : int; tree_size : int; @@ -83,12 +82,16 @@ let unsafe_get a i = if i < 0 then StateSet.empty else Array.unsafe_get (IFHTML(List.hd a, a)) i -let unsafe_set a i v old_v = - if v != old_v then +let unsafe_set a i v = + (* if v != old_v then *) Array.unsafe_set (IFHTML(List.hd a, a)) i v -type 'a run = { - tree : 'a ; +type 'node td_action = 'node -> int -> 'node -> 'node -> StateSet.t +type 'node bu_action = 'node -> int -> StateSet.t +let dummy_action = fun _ _ -> assert false + +type ('tree, 'node) run = { + tree : 'tree ; (* The argument of the run *) auto : Ata.t; (* The automaton to be run *) @@ -98,12 +101,11 @@ type 'a run = { (* Number of run we have performed *) mutable fetch_trans_cache : Ata.Formula.t Cache.N2.t; (* A cache from states * label to list of transitions *) - mutable td_cache : StateSet.t Cache.N6.t; - mutable bu_cache : StateSet.t Cache.N6.t; + mutable td_cache : 'node td_action Cache.N6.t; + mutable bu_cache : 'node bu_action Cache.N6.t; (* 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: Bytes.t; stats : stats; } @@ -182,7 +184,7 @@ let rec eval_trans_fix run tag summary fcs nss ps sat todo = eval_trans_fix run tag summary fcs nss ps new_sat todo -let eval_trans run trans_cache tag summary fcs nss ps ss todo = +let eval_trans run trans_cache tag summary fcs nss ps ss todo action_builder = let stats = run.stats in let fcsid = (fcs.StateSet.id :> int) in let nssid = (nss.StateSet.id :> int) in @@ -192,14 +194,16 @@ let eval_trans run trans_cache tag summary fcs nss ps ss todo = 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 + if res != dummy_action then res - else let new_sat = if todo == StateSet.empty then ss else - eval_trans_fix run tag summary fcs nss ps ss todo + else + let new_sat = + eval_trans_fix run tag summary fcs nss ps ss todo in stats.eval_trans_cache_miss <- 1 + stats.eval_trans_cache_miss; - Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_sat; - new_sat + let new_action = action_builder ps summary tag new_sat in + Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_action; + new_action module Make (T : Tree.S) = @@ -211,8 +215,6 @@ struct let make auto tree = 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; @@ -221,8 +223,8 @@ struct IFHTML([a], a)); pass = 0; fetch_trans_cache = Cache.N2.create dummy_form; - td_cache = Cache.N6.create dummy_set; - bu_cache = Cache.N6.create dummy_set; + td_cache = Cache.N6.create dummy_action; + bu_cache = Cache.N6.create dummy_action; node_summaries = ba; stats = { pass = 0; @@ -236,7 +238,7 @@ struct } - let top_down2 run update_res = + let top_down run mk_update_res = let num_visited = ref 0 in let i = run.pass in let tree = run.tree in @@ -250,7 +252,8 @@ struct in let run_sat = run.sat in let last_run = i >= Array.length states_by_rank - 2 in - let rec common node parent parent_sat kont = + + let rec common node parent parent_sat action_builder = if node == Tree.nil then StateSet.empty else begin incr num_visited; @@ -275,56 +278,73 @@ struct 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 = + let action = eval_trans run run.td_cache tag summary (unsafe_get run_sat (Tree.preorder tree fc)) (unsafe_get run_sat (Tree.preorder tree ns)) parent_sat - status0 td_todo + status0 td_todo action_builder in - kont summary tag parent_sat status0 status1 fc ns node node_id + action node node_id fc ns 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 + and td_action_builder parent_sat summary tag status1 = + let update_res = mk_update_res false status1 in + match NodeSummary.(has_left summary, has_right summary) with + false, false -> + (fun node node_id fc ns -> + unsafe_set run_sat node_id status1; + update_res node; + StateSet.empty) + | true, false -> + (fun node node_id fc ns -> + unsafe_set run_sat node_id status1; + update_res node; + loop_td fc node status1) + | false, true -> + (fun node node_id fc ns -> + unsafe_set run_sat node_id status1; + update_res node; + loop_td ns node status1) + | _ -> + (fun node node_id fc ns -> + unsafe_set run_sat node_id status1; (* write the td_states *) + update_res node; + ignore (loop_td fc node status1); + loop_td ns node status1 (* tail call *) + ) + and td_and_bu_action_builder parent_sat summary tag status1 node node_id fc ns = + let fcs1 = loop_td_and_bu fc node status1 in + let nss1 = loop_td_and_bu ns node status1 in + let action = + eval_trans run run.bu_cache tag summary fcs1 nss1 parent_sat status1 bu_todo bu_action_builder in - unsafe_set run_sat node_id status2 status0; + action node node_id + and bu_action_builder parent_sat summary tag status2 node node_id = + unsafe_set run_sat node_id status2; 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 + and td_and_bu_last_action_builder parent_sat summary tag status1 node node_id fc ns = + let nss1 = loop_td_and_bu_last ns node status1 in + let fcs1 = loop_td_and_bu_last fc node status1 in + let action = + eval_trans run run.bu_cache tag summary fcs1 nss1 parent_sat status1 bu_todo bu_last_action_builder in - unsafe_set run_sat node_id status2 status0; - if status2 != StateSet.empty then update_res true status2 node; - status2 + action node node_id + and bu_last_action_builder parent_sat summary tag status2 = + let update_res = mk_update_res true status2 in + (fun node node_id -> + unsafe_set run_sat node_id status2; + update_res node; + status2) and loop_td node parent parent_sat = - common node parent parent_sat kont_pure_td + common node parent parent_sat td_action_builder and loop_td_and_bu node parent parent_sat = - common node parent parent_sat kont_td_and_bu + common node parent parent_sat td_and_bu_action_builder and loop_td_and_bu_last node parent parent_sat = - common node parent parent_sat kont_td_and_bu_last + common node parent parent_sat td_and_bu_last_action_builder in - let _ = if bu_todo == StateSet.empty then loop_td (Tree.root tree) Tree.nil dummy_set @@ -338,62 +358,31 @@ struct 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 = 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*)), + (fun prepend sat -> + if StateSet.intersect sat sel_states then + if prepend then (fun n -> ResultSet.push_front n res) + else (fun n -> ResultSet.push_back n res) + else (fun _ -> ())), (fun () -> res) let mk_update_full_result auto = - 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) (ResultSet.create())) - (Ata.get_selecting_states auto) + let sel_states = Ata.get_selecting_states auto in + let res_mapper = + StateSet.fold_right (fun q acc -> (q, ResultSet.create())::acc) sel_states [] in - (fun prepend sat node -> - StateSet.iter - (fun q -> - let res = Cache.N1.find res_mapper (q :> int) in - if res != dummy then begin - if prepend then ResultSet.push_front node res - else ResultSet.push_back node res - end - ) sat), - (fun () -> - StateSet.fold_right - (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc) - (Ata.get_selecting_states auto) []) + (fun prepend sat -> + StateSet.fold (fun q f_acc -> + if StateSet.mem q sel_states then + let res = List.assoc q res_mapper in + if prepend then (fun n -> ResultSet.push_front n res; f_acc n) + else (fun n -> ResultSet.push_front n res; f_acc n) + else f_acc) sat (fun _ -> ())), + (fun () -> res_mapper) let prepare_run run list = let tree = run.tree in @@ -405,15 +394,15 @@ struct sat.(node_id) <- sat0) list - let compute_run auto tree nodes update_res = + let compute_run auto tree nodes mk_update_res = let run = make auto tree in prepare_run run nodes; let rank = Ata.get_max_rank auto in while run.pass <= rank do - top_down2 run update_res; + top_down run mk_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; + run.td_cache <- Cache.N6.create dummy_action; + run.bu_cache <- Cache.N6.create dummy_action; done; IFHTML((run.sat <- List.tl run.sat), ()); IFHTML(Html_trace.gen_trace auto run.sat (module T : Tree.S with type t = Tree.t) tree ,()); @@ -423,14 +412,14 @@ struct let last_stats = ref None let full_eval auto tree nodes = - let update_full,get_full = mk_update_full_result auto in - let run = compute_run auto tree nodes update_full in + let mk_update_full,get_full = mk_update_full_result auto in + let run = compute_run auto tree nodes mk_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 run = compute_run auto tree nodes update_res in + let mk_update_res,get_res = mk_update_result auto in + let run = compute_run auto tree nodes mk_update_res in last_stats := Some run.stats; get_res () -- 2.17.1