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/csymtable.ml | 31 ++++++++++++++++++++-----------
 1 file changed, 20 insertions(+), 11 deletions(-)

(limited to 'kernel/csymtable.ml')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 0129489542..dfe3d8fb1e 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -26,7 +26,9 @@ open Cbytegen
 module NamedDecl = Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 
-external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
+external eval_tcode : tcode -> vm_global -> values array -> values = "coq_eval_tcode"
+
+type global_data = { mutable glob_len : int; mutable glob_val : values array }
 
 (*******************)
 (* Linkage du code *)
@@ -37,21 +39,28 @@ external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
 (* [global_data] contient les valeurs des constantes globales
    (axiomes,definitions), les annotations des switch et les structured
    constant *)
-external global_data : unit -> values array = "get_coq_global_data"
+let global_data = {
+  glob_len = 0;
+  glob_val = Array.make 4096 crazy_val;
+}
 
-(* [realloc_global_data n] augmente de n la taille de [global_data] *)
-external realloc_global_data : int -> unit = "realloc_coq_global_data"
+let get_global_data () = Vmvalues.vm_global global_data.glob_val
 
-let check_global_data n =
-  if n >= Array.length (global_data()) then realloc_global_data n
+let realloc_global_data n =
+  let n = min (n + 0x100) Sys.max_array_length in
+  let ans = Array.make n crazy_val in
+  let src = global_data.glob_val in
+  let () = Array.blit src 0 ans 0 (Array.length src) in
+  global_data.glob_val <- ans
 
-let num_global = ref 0
+let check_global_data n =
+  if n >= Array.length global_data.glob_val then realloc_global_data n
 
 let set_global v =
-  let n = !num_global in
+  let n = global_data.glob_len in
   check_global_data n;
-  (global_data()).(n) <- v;
-  incr num_global;
+  global_data.glob_val.(n) <- v;
+  global_data.glob_len <- global_data.glob_len + 1;
   n
 
 (* table pour les structured_constant et les annotations des switchs *)
@@ -164,7 +173,7 @@ and eval_to_patch env (buff,pl,fv) =
   in
   let tc = patch buff pl slots in
   let vm_env = Array.map (slot_for_fv env) fv in
-  eval_tcode tc vm_env
+  eval_tcode tc (vm_global global_data.glob_val) vm_env
 
 and val_of_constr env c =
   match compile ~fail_on_error:true env c with
-- 
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/csymtable.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/csymtable.ml')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index dfe3d8fb1e..23b4194730 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -26,7 +26,7 @@ open Cbytegen
 module NamedDecl = Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
 
-external eval_tcode : tcode -> vm_global -> values array -> values = "coq_eval_tcode"
+external eval_tcode : tcode -> atom array -> vm_global -> values array -> values = "coq_eval_tcode"
 
 type global_data = { mutable glob_len : int; mutable glob_val : values array }
 
@@ -173,7 +173,7 @@ and eval_to_patch env (buff,pl,fv) =
   in
   let tc = patch buff pl slots in
   let vm_env = Array.map (slot_for_fv env) fv in
-  eval_tcode tc (vm_global global_data.glob_val) vm_env
+  eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
 
 and val_of_constr env c =
   match compile ~fail_on_error:true env c with
-- 
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/csymtable.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/csymtable.ml')

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 23b4194730..4f3cbf289d 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -47,7 +47,7 @@ let global_data = {
 let get_global_data () = Vmvalues.vm_global global_data.glob_val
 
 let realloc_global_data n =
-  let n = min (n + 0x100) Sys.max_array_length in
+  let n = min (2 * n + 0x100) Sys.max_array_length in
   let ans = Array.make n crazy_val in
   let src = global_data.glob_val in
   let () = Array.blit src 0 ans 0 (Array.length src) in
-- 
cgit v1.2.3