Is there a reasonable synthetic benchmark of `ocaml-hcons` usage I could use when working on weak pointers in the runtime?

[gasche]

Hi @backtracking and @sim642,

@sim642 recently posted intriguing results on the performance of the Goblint static analyser (which uses ocaml-hashcons) over recent OCaml versions. I am working on the OCaml runtime, and recently I have been hacking on weak pointers and ephemerons. I am interested in benchmarks I could use to understand the performance of the runtime and see if some aspects could be improved. (For example I notice that ocaml-hashcons uses Weak.blit on bucket resizing, how good is its implementation and would improvements there have measurable impact?) Unfortunately "running all SV-COMP 2026 benchmarks on Goblint" is a bit scary, it would be nice to have a simpler way to evaluate runtime changes that could be relevant to hashconsing users.

What would be a simple synthetic benchmark of using ocaml-hashcons, that would maybe run for ~1s on a typical machine, which I could use for profiling and evaluating runtime changes? Would it be reasonable to provide such a benchmark as part of the ocaml-hashcons distribution, or somewhere else?

[backtracking]

Hi @gasche,

I can provide benchmarks quite easily (based on simple implementations of reduction of lambda-terms and BDDs that we used when we were writing Type-Safe Modular Hash-Consing with Sylvain). I need a few hours to prepare that, and I can provide it here if this is convenient.

But I have no idea is this will be representative of the use of hash-consing in Goblint.

[gasche]

Thanks! This sounds great. There is no urgency, so please take your time.

Re. were to place the benchmarks: here or anything else that you think is better. (I will probably move things around to include them directly in the compiler sources as I am hacking on it, so the build system stuff does not matter too much, the simpler the better.)

(Completely unrelated, but while I am writing to you: under the soon-to-be-released 5.5, let f (module M : Map.S) = M.empty type-checks correctly: val f : (module M : Map.S) -> 'a M.t. The keyword is "module-dependent function", also known as "modular explicits". )

[sim642]

As I just happened to mention here #18 (comment), the way Goblint uses hashconsing is kind of non-standard because it's not applied recursively.
The benefit of hashconsing to Goblint runtime can be quite hit and miss too: there are cases where it significantly hurts performance. And in some cases I've profiled the bottleneck is probably not the implementation of weak pointers but the expensive hash and equal operations, especially when hashconsing values which are never looked up again.

So I don't think Goblint is a very good benchmark for weak pointers. And given the monolithic nature of how it uses hashconsing, it's kind of impossible to extract something small and synthetic which is still representative of the use case.
My hunch is that the usual hashconsing examples probably show the impact of weak pointer changes better than Goblint, given how central hashconsing is to them.
However, what those usual examples might not show is how things perform when there's also a lot of non-hashconsing-related allocations and GC happening (which the very hashconsing-focused examples might be low on). But I don't really understand these possible interferences.

Goblint static analyser (which uses ocaml-hashcons)

That's actually not true right now. Goblint uses BatHashcons from batteries, which currently includes an old copy of ocaml-hashcons. As I've recently ported some upstream Weak improvements over to ocaml-hashcons, I've also done that in my fork of batteries to benchmark Goblint w.r.t. each one. I should have some results about that soon.

[backtracking]

bench-hash-consing.zip

Here is a small archive with two quick-and-dirty benchmark programs (bench_bdd and bench_lambda) and a dune file to compile them, assuming an installed ocaml-hashcons library. A README.md provides brief instructions.

@gasche Let me know if you have questions, and if this is what you were looking for.

[backtracking]

FYI, here are the timings I get on my machine with hyperfine:

Benchmark 1: ./bench_bdd.exe -de-bruijn 350
  Time (mean ± σ):      1.126 s ±  0.042 s    [User: 1.084 s, System: 0.043 s]
  Range (min … max):    1.097 s …  1.227 s    10 runs

Benchmark 1: ./bench_bdd.exe -pigeon 11
  Time (mean ± σ):      1.858 s ±  0.032 s    [User: 1.796 s, System: 0.062 s]
  Range (min … max):    1.796 s …  1.924 s    10 runs

Benchmark 1: ./bench_lambda.exe 5
  Time (mean ± σ):      1.124 s ±  0.013 s    [User: 1.120 s, System: 0.003 s]
  Range (min … max):    1.115 s …  1.159 s    10 runs

(but my machine is pretty old).

I'm using OCaml 5.4.0.

[gasche]

This looks very nice, thanks! (I may try to adapt the programs to become multi-domain, by doing the embarrassingly parallel thing of running a fully independent copy of the benchmark on each domain.)