From b5aed34bb8bbdda27646720db29a8d47c79653b9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 2 Mar 2018 15:41:50 +0100
Subject: Moving the VM global data to a ML reference.

---
 kernel/vmvalues.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/vmvalues.ml')

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 0e0cb4e584..6377e947f3 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -43,6 +43,7 @@ let fix_val v = (Obj.magic v : values)
 let cofix_upd_val v = (Obj.magic v : values)
 
 type vm_env
+type vm_global
 let fun_env v = (Obj.magic v : vm_env)
 let fix_env v = (Obj.magic v : vm_env)
 let cofix_env v = (Obj.magic v : vm_env)
@@ -51,6 +52,8 @@ type vstack = values array
 
 let fun_of_val v = (Obj.magic v : vfun)
 
+let vm_global (v : values array) = (Obj.magic v : vm_global)
+
 (*******************************************)
 (* Machine code *** ************************)
 (*******************************************)
-- 
cgit v1.2.3


From fd5dc5b37e765bdb864e874c451d42d03d737792 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 3 Mar 2018 19:43:02 +0100
Subject: Moving the VM global atom table to a ML reference.

---
 kernel/vmvalues.ml | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

(limited to 'kernel/vmvalues.ml')

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 6377e947f3..cbe8c9187a 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -410,13 +410,20 @@ let check_fix f1 f2 =
     else false
   else false
 
-external atom_rel : unit -> atom array = "get_coq_atom_tbl"
-external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
+let atom_rel : atom array ref =
+  let init i = Aid (RelKey i) in
+  ref (Array.init 40 init)
+
+let get_atom_rel () = !atom_rel
+
+let realloc_atom_rel n =
+  let n = min (n + 0x100) Sys.max_array_length in
+  let init i = Aid (RelKey i) in
+  let ans = Array.init n init in
+  atom_rel := ans
 
 let relaccu_tbl =
-  let atom_rel = atom_rel() in
-  let len = Array.length atom_rel in
-  for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done;
+  let len = Array.length !atom_rel in
   ref (Array.init len mkAccuCode)
 
 let relaccu_code i =
@@ -425,9 +432,7 @@ let relaccu_code i =
   else
     begin
       realloc_atom_rel i;
-      let atom_rel = atom_rel () in
-      let nl = Array.length atom_rel in
-      for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done;
+      let nl = Array.length !atom_rel in
       relaccu_tbl :=
         Array.init nl
           (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
-- 
cgit v1.2.3


From 93c8e14d0c9bc233b2dcf213485b62a533b34580 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Mar 2018 12:03:47 -0300
Subject: More efficient reallocation of VM global tables.

The previous code was mimicking what the C implementation was doing, which
was a quadratic algorithm. We simply use the good old exponential reallocation
strategy that is amortized O(1).
---
 kernel/vmvalues.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/vmvalues.ml')

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index cbe8c9187a..6a41efac24 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -417,7 +417,7 @@ let atom_rel : atom array ref =
 let get_atom_rel () = !atom_rel
 
 let realloc_atom_rel n =
-  let n = min (n + 0x100) Sys.max_array_length in
+  let n = min (2 * n + 0x100) Sys.max_array_length in
   let init i = Aid (RelKey i) in
   let ans = Array.init n init in
   atom_rel := ans
-- 
cgit v1.2.3