From ddd7371dc3b82124c2bb36b93e6c2b185bcc02d2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 31 Aug 2020 08:05:48 +0200
Subject: Reroot primitive arrays on access (fix #12947).

Semi-persistent arrays are supposed to have amortized O(1) complexity.
This commit ensures it, without forcing the user to litter its functions
with explicit calls to reroot.

This commit also makes rerootk faster by carrying the array along the
dependency chain rather than recomputing it at every step.
---
 kernel/parray.ml | 97 ++++++++++++++++++++++++++------------------------------
 1 file changed, 45 insertions(+), 52 deletions(-)

(limited to 'kernel')

diff --git a/kernel/parray.ml b/kernel/parray.ml
index ea314c1883..0953f4b33f 100644
--- a/kernel/parray.ml
+++ b/kernel/parray.ml
@@ -27,45 +27,52 @@ and 'a kind =
 let unsafe_of_array t def = ref (Array (t,def))
 let of_array t def = unsafe_of_array (Array.copy t) def
 
-let rec length_int p =
-  match !p with
-  | Array (t,_) -> Array.length t
-  | Updated (_, _, p) -> length_int p
+let rec rerootk t k =
+  match !t with
+  | Array (a, _) -> k a
+  | Updated (i, v, p) ->
+      let k' a =
+        let v' = Array.unsafe_get a i in
+        Array.unsafe_set a i v;
+        t := !p; (* i.e., Array (a, def) *)
+        p := Updated (i, v', t);
+        k a in
+      rerootk p k'
+
+let reroot t = rerootk t (fun a -> a)
+
+let length_int p =
+  Array.length (reroot p)
 
 let length p = Uint63.of_int @@ length_int p
 
-let rec get p n =
-  match !p with
-  | Array (t,def) ->
-      let l = Array.length t in
-      if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then
-        Array.unsafe_get t (length_to_int n)
-      else def
-  | Updated (k,e,p) ->
-     if Uint63.equal n (Uint63.of_int k) then e
-     else get p n
+let get p n =
+  let t = reroot p in
+  let l = Array.length t in
+  if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then
+    Array.unsafe_get t (length_to_int n)
+  else
+    match !p with
+    | Array (_, def) -> def
+    | Updated _ -> assert false
 
 let set p n e =
-  let kind = !p in
-  match kind with
-  | Array (t,_) ->
-      let l = Uint63.of_int @@ Array.length t in
-      if Uint63.le Uint63.zero n && Uint63.lt n l then
-        let res = ref kind in
-        let n = length_to_int n in
-        p := Updated (n, Array.unsafe_get t n, res);
-        Array.unsafe_set t n e;
-        res
-      else p
-  | Updated _ ->
-      if Uint63.le Uint63.zero n && Uint63.lt n (length p) then
-        ref (Updated((length_to_int n), e, p))
-      else p
-
-let rec default p =
+  let a = reroot p in
+  let l = Uint63.of_int (Array.length a) in
+  if Uint63.le Uint63.zero n && Uint63.lt n l then
+    let i = length_to_int n in
+    let v' = Array.unsafe_get a i in
+    Array.unsafe_set a i e;
+    let t = ref !p in (* i.e., Array (a, def) *)
+    p := Updated (i, v', t);
+    t
+  else p
+
+let default p =
+  let _ = reroot p in
   match !p with
   | Array (_,def) -> def
-  | Updated (_,_,p) -> default p
+  | Updated _ -> assert false
 
 let make n def =
   ref (Array (Array.make (trunc_size n) def, def))
@@ -75,33 +82,19 @@ let init n f def =
   let t = Array.init n f in
   ref (Array (t, def))
 
-let rec to_array p =
+let to_array p =
+  let _ = reroot p in
   match !p with
   | Array (t,def) -> Array.copy t, def
-  | Updated (n,e,p) ->
-      let (t,_) as r = to_array p in
-      Array.unsafe_set t n e; r
+  | Updated _ -> assert false
 
 let copy p =
   let (t,def) = to_array p in
   ref (Array (t,def))
 
-let rec rerootk t k =
-  match !t with
-  | Array _ -> k ()
-  | Updated (i, v, t') ->
-      let k' () =
-        begin match !t' with
-        | Array (a,_def) as n ->
-            let v' = a.(i) in
-            Array.unsafe_set a i v;
-            t := n;
-            t' := Updated (i, v', t)
-        | Updated _ -> assert false
-        end; k() in
-      rerootk t' k'
-
-let reroot t = rerootk t (fun () -> t)
+let reroot t =
+  let _ = reroot t in
+  t
 
 let map f p =
   let p = reroot p in
-- 
cgit v1.2.3


From e3764e1e857fce9b6d4cb018db676db3612c00a0 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 31 Aug 2020 08:52:05 +0200
Subject: Remove occurrences of Parray.reroot.

---
 kernel/cPrimitives.ml   | 9 +--------
 kernel/cPrimitives.mli  | 1 -
 kernel/nativevalues.ml  | 9 ---------
 kernel/nativevalues.mli | 4 ----
 kernel/parray.mli       | 1 -
 kernel/primred.ml       | 5 -----
 kernel/vmbytegen.ml     | 1 -
 kernel/vmemitcodes.ml   | 2 +-
 kernel/vmsymtable.ml    | 2 --
 kernel/vmvalues.ml      | 1 -
 kernel/vmvalues.mli     | 1 -
 11 files changed, 2 insertions(+), 34 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 314cb54d1d..5cd91b4e74 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -58,7 +58,6 @@ type t =
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength
 
 let parse = function
@@ -110,7 +109,6 @@ let parse = function
   | "array_set" -> Arrayset
   | "array_length" -> Arraylength
   | "array_copy" -> Arraycopy
-  | "array_reroot" -> Arrayreroot
   | _ -> raise Not_found
 
 let equal (p1 : t) (p2 : t) =
@@ -164,8 +162,7 @@ let hash = function
   | Arraydefault -> 45
   | Arrayset -> 46
   | Arraycopy -> 47
-  | Arrayreroot -> 48
-  | Arraylength -> 49
+  | Arraylength -> 48
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -216,7 +213,6 @@ let to_string = function
   | Arraydefault -> "arraydefault"
   | Arrayset -> "arrayset"
   | Arraycopy -> "arraycopy"
-  | Arrayreroot -> "arrayreroot"
   | Arraylength -> "arraylength"
 
 type const =
@@ -302,7 +298,6 @@ let types =
   | Arraydefault -> [array_ty; PITT_param 1]
   | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty]
   | Arraycopy -> [array_ty; array_ty]
-  | Arrayreroot -> [array_ty; array_ty]
   | Arraylength -> [array_ty; int_ty]
 
 let one_param =
@@ -360,7 +355,6 @@ let params = function
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength -> one_param
 
 let nparams x = List.length (params x)
@@ -414,7 +408,6 @@ let univs = function
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength -> one_univ
 
 type arg_kind =
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 41b3bff465..0db643faf4 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -56,7 +56,6 @@ type t =
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength
 
 (** Can raise [Not_found].
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 9e17f97a56..05c98e4b87 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -739,15 +739,6 @@ let arraycopy accu vA t =
     no_check_arraycopy t
   else accu vA t
 
-let no_check_arrayreroot t =
-  of_parray (Parray.reroot (to_parray t))
-[@@ocaml.inline always]
-
-let arrayreroot accu vA t =
-  if is_parray t then
-    no_check_arrayreroot t
-  else accu vA t
-
 let no_check_arraylength t =
   mk_uint (Parray.length (to_parray t))
 [@@ocaml.inline always]
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 08c5bd7126..b9b75a9d7c 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -344,7 +344,6 @@ val arrayget : t -> t -> t -> t -> t (* accu A t n *)
 val arraydefault : t -> t -> t (* accu A t *)
 val arrayset : t -> t -> t -> t -> t -> t (* accu A t n v *)
 val arraycopy : t -> t -> t -> t (* accu A t *)
-val arrayreroot : t -> t -> t -> t (* accu A t *)
 val arraylength : t -> t -> t -> t (* accu A t *)
 val arrayinit : t -> t -> t -> t (* accu A n f def *)
 val arraymap : t -> t -> t (* accu A B f t *)
@@ -364,8 +363,5 @@ val no_check_arrayset : t -> t -> t -> t
 val no_check_arraycopy : t -> t
 [@@ocaml.inline always]
 
-val no_check_arrayreroot : t -> t
-[@@ocaml.inline always]
-
 val no_check_arraylength : t -> t
 [@@ocaml.inline always]
diff --git a/kernel/parray.mli b/kernel/parray.mli
index 0276278bd0..8b6565c159 100644
--- a/kernel/parray.mli
+++ b/kernel/parray.mli
@@ -19,7 +19,6 @@ val default : 'a t -> 'a
 val make    : Uint63.t -> 'a -> 'a t
 val init    : Uint63.t -> (int -> 'a) -> 'a -> 'a t
 val copy    : 'a t -> 'a t
-val reroot  : 'a t -> 'a t
 
 val map : ('a -> 'b) -> 'a t -> 'b t
 
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 90eeeb9be7..f158cfacea 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -365,11 +365,6 @@ struct
       let t = get_parray evd args 1 in
       let t' = Parray.copy t in
       E.mkArray env u t' ty
-    | Arrayreroot ->
-      let ar = E.get args 1 in
-      let t = E.get_parray evd ar in
-      let _ = Parray.reroot t in
-      ar
     | Arraylength ->
       let t = get_parray evd args 1 in
       E.mkInt env (Parray.length t)
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 375b1aface..16a0f42664 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -508,7 +508,6 @@ let is_caml_prim = let open CPrimitives in function
   | Arraydefault
   | Arrayset
   | Arraycopy
-  | Arrayreroot
   | Arraylength -> true
   | _ -> false
 
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index f913cb906c..ec8601edc9 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -262,7 +262,7 @@ let check_prim_op = function
   | Arraymake -> opISINT_CAML_CALL2
   | Arrayget -> opISARRAY_INT_CAML_CALL2
   | Arrayset -> opISARRAY_INT_CAML_CALL3
-  | Arraydefault | Arraycopy | Arrayreroot | Arraylength ->
+  | Arraydefault | Arraycopy | Arraylength ->
       opISARRAY_CAML_CALL1
 
 let emit_instr env = function
diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
index 4ad830a298..9d80dc578b 100644
--- a/kernel/vmsymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -69,7 +69,6 @@ let parray_get = set_global Vmvalues.parray_get
 let parray_get_default = set_global Vmvalues.parray_get_default
 let parray_set = set_global Vmvalues.parray_set
 let parray_copy = set_global Vmvalues.parray_copy
-let parray_reroot = set_global Vmvalues.parray_reroot
 let parray_length = set_global Vmvalues.parray_length
 
 (* table pour les structured_constant et les annotations des switchs *)
@@ -135,7 +134,6 @@ let slot_for_caml_prim =
   | Arraydefault -> parray_get_default
   | Arrayset -> parray_set
   | Arraycopy -> parray_copy
-  | Arrayreroot -> parray_reroot
   | Arraylength -> parray_length
   | _ -> assert false
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 0678f37a0b..2068133b10 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -700,5 +700,4 @@ let parray_get = Obj.magic Parray.get
 let parray_get_default = Obj.magic Parray.default
 let parray_set = Obj.magic Parray.set
 let parray_copy = Obj.magic Parray.copy
-let parray_reroot = Obj.magic Parray.reroot
 let parray_length = Obj.magic Parray.length
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 6632dc46b2..d15595766a 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -204,5 +204,4 @@ val parray_get : values
 val parray_get_default : values
 val parray_set : values
 val parray_copy : values
-val parray_reroot : values
 val parray_length : values
-- 
cgit v1.2.3