From: Kim Nguyễn <kim.nguyen@lri.fr>
Date: Tue, 18 Apr 2017 12:44:43 +0000 (+0200)
Subject: Further improve the jit.
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=6bf7e46a9e33989261c349cbe532c6eec1585427

Further improve the jit.
---

diff --git a/src/run.ml b/src/run.ml
index 89aae12..00f19d3 100644
--- a/src/run.ml
+++ b/src/run.ml
@@ -28,42 +28,6 @@ type stats = { mutable pass : int;
                mutable nodes_per_run : int list;
              }
 
-module NodeSummary =
-struct
-  (* Pack into an integer the result of the is_* and has_ predicates
-     for a given node *)
-  type t = int
-  let dummy = -1
-  (*
-    ...44443210
-    ...4444 -> kind
-    3 -> has_right
-    2 -> has_left
-    1 -> is_right
-    0 -> is_left
-  *)
-  let is_left (s : t) : bool =
-    s land 1 != 0
-
-  let is_right (s : t) : bool =
-    s land 0b10 != 0
-
-  let has_left (s : t) : bool =
-    s land 0b100 != 0
-
-  let has_right (s : t) : bool =
-    s land 0b1000 != 0
-
-  let kind (s : t) : Tree.NodeKind.t =
-    Obj.magic (s lsr 4)
-
-  let make is_left is_right has_left has_right kind =
-    (int_of_bool is_left) lor
-      ((int_of_bool is_right) lsl 1) lor
-      ((int_of_bool has_left) lsl 2) lor
-      ((int_of_bool has_right) lsl 3) lor
-      ((Obj.magic kind) lsl 4)
-end
 
 let dummy_set = StateSet.singleton State.dummy_state
 
@@ -106,7 +70,6 @@ type ('tree, 'node) 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: Bytes.t;
   stats : stats;
 }
 
@@ -142,7 +105,7 @@ let eval_form phi fcs nss ps ss summary =
     | Boolean.True -> true
     | Boolean.Atom (a, b) ->
       begin
-        let open NodeSummary in
+        let open Tree.NodeSummary in
         match a.Atom.node with
         | Move (m, q) ->
           b && StateSet.mem q (
@@ -205,7 +168,7 @@ let eval_trans run trans_cache tag summary fcs nss ps ss todo action_builder =
     Cache.N6.add trans_cache tagid summary ssid fcsid nssid psid new_action;
     new_action
 
-
+module NodeSummary = Tree.NodeSummary
 module Make (T : Tree.S)  =
 struct
   module Tree : Tree.S with type node = T.node = T
@@ -215,7 +178,6 @@ struct
 
   let make auto tree =
     let len = Tree.size tree in
-    let ba = Bytes.make len '\000' in
     {
       tree = tree;
       auto = auto;
@@ -225,7 +187,6 @@ struct
       fetch_trans_cache = Cache.N2.create dummy_form;
       td_cache = Cache.N6.create dummy_action;
       bu_cache = Cache.N6.create dummy_action;
-      node_summaries = ba;
       stats = {
         pass = 0;
         tree_size = len;
@@ -254,27 +215,14 @@ struct
     let last_run = i >= Array.length states_by_rank - 2 in
 
     let rec common node parent parent_sat action_builder =
-      if node == Tree.nil then StateSet.empty
-      else begin
+      begin
         incr num_visited;
         let tag = Tree.tag tree node in
         let node_id = Tree.preorder tree node in
+        let summary = Tree.summary 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 = Char.code (Bytes.unsafe_get run.node_summaries node_id) in
-          if  s != 0 then s else
-            let s =
-              NodeSummary.make
-                (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
-            Bytes.unsafe_set run.node_summaries node_id (Char.chr 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 *)
@@ -314,24 +262,82 @@ struct
            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
-      action node node_id
+        )
+    and td_and_bu_action_builder parent_sat summary tag status1  =
+      match NodeSummary.(has_left summary, has_right summary) with
+        false, false ->
+        (fun node node_id fc ns ->
+           let action =
+             eval_trans run run.bu_cache tag summary StateSet.empty StateSet.empty
+               parent_sat status1 bu_todo bu_action_builder
+           in
+           action node node_id)
+      | true, false ->
+        (fun node node_id fc ns ->
+           let fcs1 = loop_td_and_bu fc node status1 in
+           let action =
+             eval_trans run run.bu_cache tag summary fcs1 StateSet.empty
+               parent_sat status1 bu_todo bu_action_builder
+           in
+           action node node_id
+        )
+      | false, true ->
+        (fun node node_id fc ns ->
+           let nss1 = loop_td_and_bu ns node status1 in
+           let action =
+             eval_trans run run.bu_cache tag summary StateSet.empty nss1
+               parent_sat status1 bu_todo bu_action_builder
+           in
+           action node node_id
+        )
+      | _ ->
+        (fun 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
+           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 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
-      action node node_id
+    and td_and_bu_last_action_builder parent_sat summary tag status1 =
+      match NodeSummary.(has_left summary, has_right summary) with
+        false, false ->
+        (fun node node_id fc ns ->
+           let action =
+             eval_trans run run.bu_cache tag summary StateSet.empty StateSet.empty
+               parent_sat status1 bu_todo bu_last_action_builder
+           in
+           action node node_id)
+      | true, false ->
+        (fun node node_id fc ns ->
+           let fcs1 = loop_td_and_bu_last fc node status1 in
+           let action =
+             eval_trans run run.bu_cache tag summary fcs1 StateSet.empty
+               parent_sat status1 bu_todo bu_last_action_builder
+           in
+           action node node_id
+        )
+      | false, true ->
+        (fun node node_id fc ns ->
+           let nss1 = loop_td_and_bu_last ns node status1 in
+           let action =
+             eval_trans run run.bu_cache tag summary StateSet.empty nss1
+               parent_sat status1 bu_todo bu_last_action_builder
+           in
+           action node node_id
+        )
+      | _ ->
+        (fun 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
+           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 ->
@@ -380,7 +386,7 @@ struct
            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 (fun n -> ResultSet.push_back n res; f_acc n)
            else f_acc) sat (fun _ -> ())),
     (fun () -> res_mapper)
 
diff --git a/src/tatoo.ml b/src/tatoo.ml
index 5e8144d..2b901d4 100644
--- a/src/tatoo.ml
+++ b/src/tatoo.ml
@@ -72,6 +72,14 @@ let main () =
       Gc.compact();
       Gc.set (tuned_gc)
   in
+  let () =
+    let rec loop node = if node == Runtime.Tree.nil then () else
+        let i = Runtime.Tree.preorder doc node in
+        let () = loop (Runtime.Tree.first_child doc node) in
+        loop (Runtime.Tree.next_sibling doc node)
+    in
+    time loop (Runtime.Tree.root doc) "calibrating full traversal"
+  in
   let queries =
     time
       (fun l ->