diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-07 12:03:47 -0300 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-03-26 08:57:39 +0200 |
| commit | 93c8e14d0c9bc233b2dcf213485b62a533b34580 (patch) | |
| tree | dcf1e391ebf9e87947294eb3a822829c7d26381a | |
| parent | fd5dc5b37e765bdb864e874c451d42d03d737792 (diff) | |
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).
| -rw-r--r-- | kernel/csymtable.ml | 2 | ||||
| -rw-r--r-- | kernel/vmvalues.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 23b419473..4f3cbf289 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 diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index cbe8c9187..6a41efac2 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 |