diff options
| -rw-r--r-- | checker/check.mllib | 1 | ||||
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | lib/ephemeron.ml | 87 | ||||
| -rw-r--r-- | lib/ephemeron.mli | 50 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 |
5 files changed, 140 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 759be8729..08196d27f 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -23,6 +23,7 @@ CString CArray CStack Util +Ephemeron Future CUnix System diff --git a/dev/printers.mllib b/dev/printers.mllib index 1eb3aa4bb..1fc249eef 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -38,6 +38,7 @@ Heap Dnet Genarg Stateid +Ephemeron Future RemoteCounter diff --git a/lib/ephemeron.ml b/lib/ephemeron.ml new file mode 100644 index 000000000..ee763086c --- /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 000000000..bc34c5c66 --- /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 f45c34610..f641e68f0 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -17,6 +17,7 @@ Heap Dnet Unionfind Genarg +Ephemeron Future RemoteCounter Dag |