Ephemeron: marshaling friendly keys

Ideally all unmarshallable content in the state should be
stocked using Ephemeron keys.  In this way the state becomes
always marshallable (because the unmarshallable content is magically
dropped).  The mli contains more detailed doc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16891 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 138 insertions, 0 deletions

diff --git a/lib/ephemeron.ml b/lib/ephemeron.ml
new file mode 100644
index 0000000000..ee763086c9
--- /dev/null
+++ b/lib/ephemeron.ml
@@ -0,0 +1,87 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type key_type = int
+
+type boxed_key = key_type ref ref
+
+let mk_key : unit -> boxed_key =
+  (* TODO: take a random value here. Is there a random function in OCaml? *) 
+  let bid = ref 0 in
+  (* According to OCaml Gc module documentation, Pervasives.ref is one of the
+     few ways of getting a boxed value the compiler will never alias. *)
+  fun () -> incr bid; Pervasives.ref (Pervasives.ref !bid)
+
+(* A phantom type to preserve type safety *)
+type 'a key = boxed_key
+
+(* Comparing keys with == grants that if a key is unmarshalled (in the same
+   process where it was created or in another one) it is not mistaken for
+   an already existing one (unmarshal has no right to alias).  If the initial
+   value of bid is taken at random, then one also avoids potential collisions *)
+module HT = Hashtbl.Make(struct
+  type t = key_type ref
+  let equal k1 k2 = k1 == k2
+  let hash id = !id
+end)
+
+(* A key is the (unique) value inside a boxed key, hence it does not
+   keep its corresponding boxed key reachable (replacing key_type by boxed_key
+   would make the key always reachable) *)
+let values : Obj.t HT.t = HT.create 1001
+
+(* To avoid a race contidion between the finalization function and
+   get/create on the values hashtable, the finalization function just
+   enqueues in an imperative list the item to be collected.  Being the list
+   imperative, even if the Gc enqueue an item while run_collection is operating,
+   the tail of the list is eventually set to Empty on completion.
+   Kudos to the authors of Why3 that came up with this solution for their
+   implementation of weak hash tables! *)
+type imperative_list = cell ref
+and cell = Empty | Item of key_type ref * imperative_list
+
+let collection_queue : imperative_list ref = ref (ref Empty)
+
+let enqueue x = collection_queue := ref (Item (!x, !collection_queue))
+
+let run_collection () =
+  let rec aux l = match !l with
+    | Empty -> ()
+    | Item (k, tl) -> HT.remove values k; aux tl in
+  let l = !collection_queue in
+  aux l;
+  l := Empty
+
+(* The only reference to the boxed key is the one returned, when the user drops
+   it the value eventually disappears from the values table above *)
+let create (v : 'a) : 'a key =
+  run_collection ();
+  let k = mk_key () in
+  HT.add values !k (Obj.repr v);
+  Gc.finalise enqueue k;
+  k
+
+(* Avoid raising Not_found *)
+exception InvalidKey
+let get (k : 'a key) : 'a =
+  run_collection ();
+  try Obj.obj (HT.find values !k)
+  with Not_found -> raise InvalidKey
+
+(* Simple utils *)
+let default k v =
+  try get k
+  with InvalidKey -> v
+
+let iter_opt k f =
+  match
+    try Some (get k)
+    with InvalidKey -> None
+  with
+  | None -> ()
+  | Some v -> f v
diff --git a/lib/ephemeron.mli b/lib/ephemeron.mli
new file mode 100644
index 0000000000..bc34c5c66f
--- /dev/null
+++ b/lib/ephemeron.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Use case:
+     You have a data structure that needs to be marshalled but it contains
+     unmarshallable data (like a closure, or a file descriptor).  Actually
+     you don't need this data to be preserved by marshalling, it just happens
+     to be there.
+     You could produced a trimmed down data structure, but then, once
+     unmarshalled, you can't used the very same code to process it, unless you
+     re-inject the trimmed down data structure into the standard one, using
+     dummy values for the unmarshallable stuff.
+     Similarly you could change your data structure turning all types [bad]
+     into [bad option], then just before marshalling you set all values of type
+     [bad option] to [None].  Still this pruning may be expensive and you have
+     to code it.
+
+   Desiderata:
+     The marshalling operation automatically discards values that cannot be
+     marshalled or cannot be properly unmarshalled.
+
+   Proposed solution:
+     Turn all occurrences of [bad] into [bad key] in your data structure.
+     Use [crate bad_val] to obtain a unique key [k] for [bad_val], and store
+     [k] in the data structure.  Use [get k] to obtain [bad_val].
+
+     An ['a key] can always be marshalled.  When marshalled, a key loses its
+     value.  The function [get] raises Not_found on unmarshalled keys.
+     
+     If a key is garbage collected, the corresponding value is garbage
+     collected too (unless extra references to it exist).
+     In short no memory management hassle, keys can just replace their
+     corresponding value in the data structure.  *)
+
+type 'a key
+
+val create : 'a -> 'a key
+
+(* May raise InvalidKey *)
+exception InvalidKey
+val get : 'a key -> 'a
+
+(* These never fail. *)
+val iter_opt : 'a key -> ('a -> unit) -> unit
+val default : 'a key -> 'a -> 'a
diff --git a/lib/lib.mllib b/lib/lib.mllib
index f45c34610a..f641e68f0e 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -17,6 +17,7 @@ Heap
 Dnet
 Unionfind
 Genarg
+Ephemeron
 Future
 RemoteCounter
 Dag