ocaml/ocaml — pull request #22 by bobot (2014-03-25 18:10:10+00:00)
Title: Add Ephemerons to OCaml

#### Ephemerons
The current OCaml runtime proposes two kinds of pointers:

- `A` points hardly to `B`: if `A` is alive, `B` is alive (usual pointers)
- `A` points weakly to `B`: when the GC decide that `B` stops to be alive, `A` stops to point to `B`

Weak pointers are very handy when you want to be able to access a data without creating memory leaks. For example hashconsing can be done using the weaksets defined in `Weak.Make`. However you can't create general weaktable with the current runtime: associative table that keep a data until the key is not needed anymore. The problematic case is when the data points to the key(cf [10]).

Barry Hayes proposed in 1997 (cf [9]) the notion of ephemerons which allow to code such table. In its simplest form an ephemeron `A` with key `K` and data `D` keeps `D` alive while `A` **and** `K` are alive. To sum up ephemerons add the possibility to express conjunctions where you normally have only disjunctions.

#### Request for Comment and Merge-Request
This merge-request adds ephemerons to ocaml with particularly a modification of the runtime, [4], and a new module in the standard library, [6]. An untyped API with an arbitrary number of keys is given in `Ephemerons.Obj` and two specialized API for one and two keys are provided in `Ephemerons.K1` and `Ephemerons.K2`. Each of these three APIs define a functor for constructing weaktables with the same signature than `Hashtbl`.

Before an actual review of the C or OCaml implementation parts, comments about the OCaml interface are more than welcomed.

The modifications are splitted as follows:

- [1], [2]: code factorization that can be removed from the merge request but at the end without them some functions start to be very big
- [3]: A correction of the behavior of the weak pointer when more than one weak array points to one value
- [4]: Add the ephemerons in the runtime (simple but inefficient way). The stdlib is modified in another commit in order to simplify rebase and bootstrapping.
- [5]: just add a getter for Hashtbl.randomized
- [6]: Add the module Ephemeron in the stdlib and some tests in the testsuites
- [7]: Shortcut clean phase if possible (can be removed from the merge request)
- [8]: Optimize the implementation of the ephemerons and mitigate the worst case

The code have been evaluated on Why3, "don't use" correspond to why3 commit [11] and "use" to why3 commit [12] that replace the half-satisfying weak-table solution by weak-table provided by Ephemeron.

| | [0] | [1] | [2] | [3] | [4] | [5] | [6] | [7] | [8] |
|:----------|:------------:|:------------:|:------------:|:------------:|:------------:|:------------:|:------------:|:------------:|:------------:|
| don't use | 12.96 (0.02) | 12.96 (0.13) | 12.93 (0.03) | 13.26 (0.06) | 13.70 (0.27) | 13.87 (0.16) | 13.30 (0.04) | 13.37 (0.10) | 13.10 (0.09) |
| use | NA | NA | NA | NA | NA | NA | 12.08 (0.06) | 12.02 (0.05) | 11.88 (0.05) |

We can see that the slowdown for a code that heavily use weak pointers is of 1-2%, and the speedup when using weak-pointers (weaksets) and weaktable is of 8% without counting the fact that the weaktable is "perfect" and simple to use.

*nb: the branch is not directly mergeable because of `boot/ocaml...`, but at the end of the review process I will rebase the branch and doing the bootstrap.*

#### How to reproduce the bench
clone why3, `configure --enable-local`, `bin/why3config --detect`. Add this section to `why3.conf`:

```
[prover]
command = "/bin/true %t %f"
driver = "drivers/null_smt.drv"
editor = ""
in_place = false
interactive = false
name = "null"
version = "0"
```

Bench with the command:

```
(exec bin/why3session.opt output --output /tmp --filter-prover null $(git ls-files "examples/**/why3session.xml") -L examples/bitvectors -F -L examples/vacid_0_binary_heaps/) >& /dev/null
```

[0]: ccf516168fc5c2570c77ed3dfe8ec973c342e97e
[1]: 3caeca0b32c45e7200e692c49a90555c641abbe7
[2]: 3a27d09a2938cf872880c03e1e849fefe3d0edfd
[3]: e1dac1c1b563ae44f5255d2166d81ba641a4f66d
[4]: 85e173203df770d443cf74c5eede969cc339fd4a
[5]: 99db66f3e86bca69c68407d42b4e5727a421c3fe
[6]: 47e1e6730acd39529b63a8345a4b9c4c5f659a8c
[7]: a75d8130323e378a89a348de56f537a0c86c6448
[8]: b83f7bbd415dea05127bd11c0fadae965b88cf37
[9]: http://pdf.aminer.org/000/522/273/ephemerons_a_new_finalization_mechanism.pdf
[10]: http://forge.ocamlcore.org/plugins/mediawiki/wiki/ocaml-meeting/index.php/OCamlMeeting2011#The_Eternal_Solution_for_Memoisation:_Ephemerons.2C_by_Fran.C3.A7ois_Bobot
[11]: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=why3/why3.git;a=commitdiff;h=838ea132ad07ddd9c4a6a2843b5023b82caa5bfd
[12]: https://gforge.inria.fr/plugins/scmgit/cgi-bin/gitweb.cgi?p=why3/why3.git;a=commitdiff;h=f17551ce9d36035ef8d0ffae256872611e798b29