open hash tables with linear probing

[gasche]

This commit reimplements the weak hash tables of ocaml-hashcons using open-adressing hash tables with linear probing. The implementation is loosely inspired from François Pottier's hachis library ( https://github.com/fpottier/hachis/ ), from which the suggestion comes that open-addressing hash tables can be competitive with the array-of-buckets design commonly found in OCaml libraries.

One interesting aspect of open-addressing hash tables is that we can use a single large weak array, instead of many smaller weak arrays of buckets. (At this point I don't know whether this difference should make things faster or slower.)

(This is joint work with @iuliadmtru, we worked on this during the Rocq'n'share 2026 in Lausanne.)

The 'hashcons' library comes with three benchmarks representing three very different workloads:

1. quicksort: 'test_qs.exe', which reduces a large lambda-calculus term implementing a quicksort, has a hit rate of 99.8%, that is, virtually all 'hashcons' call succeed by finding a value already in the hash set. Terms get collected very slowly.

   The new implementation struggles on this workload: on my machine it is around 1.1x slower than the previous implementation, with similar memory usage. (We had to implement specific logic to avoid a 2x slowdown on this benchmark.)

2. pigeons: 'bench_bdd.exe -pigeon 11' is more balanced, with a hit rate of 44.6%, but terms that are largely long-lived -- the number of distinct live elements grows over time so the table needs to be resized repeatedly.

   The new implementation is 1.21x faster on this benchmark, with similar memory usage.

3. indices; 'bench_bdd.exe -de-bruijn 400' has a hit rate of 1.2%: most terms in the table are new, and in fact most terms are relatively short-lived and get collected quickly.

   The new implementation uses 7x less memory and is 2.85x faster on this benchmark.

These results suggest that the new implementation could be an improvement over the previous one for certain workloads.

We wrote this with the intention of adopting the same approach in the hash-consing layer of Rocq (moving from an array-of-buckets design to an open-addressing design); but at this point we don't know to which of the three workloads Rocq is closer to. (We suspect that it is in-betwen (1) and (2), so it is really unclear what the gains would be for Rocq.)

[gasche]

cc @sim642 who may be interested in experiments with hash-consing implementations

[gasche]

In typical @fpottier fashion the implementation comes with a verbose variable which is statically set to false, but if you set it to true you see statistics about the data structure.

Verbose output for the quicksort benchmark (excerpt)

$ dune build --profile=release && time ./_build/default/test_qs.exe

[01] Compression: occupation 2805=>2154
[02] Compression: occupation 3216=>2553
[03] Compression: occupation 4025=>3066
[...]
[31] Compression: occupation 7388=>6266
[32] Compression: occupation 7056=>6315
[33] Compression: occupation 6936=>6438
Hachcons calls 17432513: hits 17395893 (99.7899%), misses 36620 (0.210067%).
Hashcons locate: calls 17599089, average travel 1.3292/call

There are regular "compression" events to remove from the (weak) table values that have been deleted by the GC. Each compression does not reduce the occupation by a lot, but doing them regularly is key to having good performance on this benchmark.

If we remove the logic in the PR to do regular compressions even in absence of the need to resize, we see the following instead:

[01] Compression: occupation 13441=>4523
[02] Compression: occupation 13441=>5448
[03] Compression: occupation 13441=>5942
Hachcons calls 17345844: hits 17309397 (99.7899%), misses 36447 (0.210119%).
Hashcons locate: calls 17361757, average travel 5.41509/call

The compression kicks in when 13441 slots are used (or occupied by dead values), only three times, but this results in much longer probe travel on each access to the table, and the benchmark takes 1.7s rather than 1.3s.

(The periodic compressions discussed above mostly do not fire in the other benchmarks discussed below, because their tables grow fast enough for the resizing logic to kick in.)

Pigeons

$ dune build --profile=release && time ./_build/default/bench_bdd.exe -pigeon 11

[01] Resize: size 256=>512, occupation 211=>211
[02] Resize: size 512=>1024, occupation 421=>421
[03] Resize: size 1024=>2048, occupation 841=>841
[04] Compression: occupation 1669=>171
[05] Compression: occupation 1681=>619
[06] Resize: size 2048=>4096, occupation 1681=>1681
[07] Compression: occupation 3361=>1280
[08] Resize: size 4096=>8192, occupation 3361=>2668
[09] Resize: size 8192=>16384, occupation 6721=>6666
[10] Resize: size 16384=>32768, occupation 13441=>12765
[11] Resize: size 32768=>65536, occupation 26881=>26826
[12] Resize: size 65536=>131072, occupation 53761=>53706
[13] Resize: size 131072=>262144, occupation 107521=>106628
[14] Resize: size 262144=>524288, occupation 215041=>213969
Hachcons calls 433376: hits 193567 (44.6649%), misses 239809 (55.3351%).
Hashcons locate: calls 861828, average travel 2.70208/call

A "resize" events doubles the size of the backing array, and also removes dead values (so occupation also decreases temporarily).

We can see that the table steadily grows with this test.

Indices

$ dune build --profile=release && time ./_build/default/bench_bdd.exe -de-bruijn 400

[01] Resize: size 256=>512, occupation 211=>211
[02] Resize: size 512=>1024, occupation 421=>421
[03] Resize: size 1024=>2048, occupation 841=>841
[04] Resize: size 2048=>4096, occupation 1681=>1681
[05] Resize: size 4096=>8192, occupation 3361=>3361
[06] Compression: occupation 6721=>2272
[07] Compression: occupation 6721=>949
[08] Resize: size 8192=>16384, occupation 6721=>6721
[09] Compression: occupation 13441=>2522
[10] Compression: occupation 13441=>5259
[11] Compression: occupation 13441=>5520
[12] Compression: occupation 13441=>5478
[13] Compression: occupation 13441=>5671
[14] Compression: occupation 13441=>6039
[15] Resize: size 16384=>32768, occupation 13441=>13395
[16] Resize: size 32768=>65536, occupation 26881=>26809
[17] Resize: size 65536=>131072, occupation 53761=>53632
[18] Compression: occupation 107521=>30402
[19] Compression: occupation 107521=>52383
[20] Compression: occupation 107521=>48266
[21] Compression: occupation 107521=>47064
[22] Compression: occupation 107521=>44248
[23] Compression: occupation 107521=>43732
[24] Compression: occupation 107521=>44414
[25] Compression: occupation 107521=>43198
Hachcons calls 652813: hits 8006 (1.22638%), misses 644807 (98.7736%).
Hashcons locate: calls 1147302, average travel 4.94342/call

The number of live values in the table grows over time, but somewhat slowly, and the GC can collect existing values at almost the same speed. Whenever we would need to resize we first check if a compression suffices to free half the table, and here most resizing events are replaced by compressions.