Optimizing array mapping in the kernel.

We unroll the map operation by hand in two performance-critical cases so as
not to call the generic array allocation function in OCaml, and allocate
directly on the minor heap instead. The generic array function is slow because
it needs to discriminate between float and non-float arrays. The unrolling
replaces this by a simple increment to the minor heap pointer and moves from
the stack.

The quantity of unrolling was determined by experimental measures on various Coq
developments. It looks like most of the maps are for small arrays of size lesser
or equal to 4, so this is what is implemented here. We could probably extend it
to an even bigger number, but that would result in ugly code. From what I've seen,
virtually all maps are of size less than 16, so that we could probably be almost
optimal by going up to 16 unrollings, but the code tradeoffs are not obvious. Maybe
when we have PPX?

1 files changed, 12 insertions, 1 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1ae89347ad..0d7f77edae 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -71,6 +71,17 @@ let rec zlapp v = function
     Zlapp v2 :: s -> zlapp (Array.append v v2) s
   | s -> Zlapp v :: s
 
+(** Hand-unrolling of the map function to bypass the call to the generic array
+    allocation. Type annotation is required to tell OCaml that the array does
+    not contain floats. *)
+let map_lift (l : lift) (v : fconstr array) = match v with
+| [||] -> assert false
+| [|c0|] -> [|(l, c0)|]
+| [|c0; c1|] -> [|(l, c0); (l, c1)|]
+| [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|]
+| [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|]
+| v -> CArray.Fun1.map (fun l t -> (l, t)) l v
+
 let pure_stack lfts stk =
   let rec pure_rec lfts stk =
     match stk with
@@ -80,7 +91,7 @@ let pure_stack lfts stk =
               (Zupdate _,lpstk)  -> lpstk
             | (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
             | (Zapp a, (l,pstk)) ->
-                (l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
+                (l,zlapp (map_lift l a) pstk)
 	    | (Zproj (n,m,c), (l,pstk)) ->
 		(l, Zlproj (c,l)::pstk)
             | (Zfix(fx,a),(l,pstk)) ->