Add hashcons weak-pointer/ephemeron benchmarks (bench_bdd, bench_lambda)#4
Open
udesou wants to merge 1 commit into
Open
Add hashcons weak-pointer/ephemeron benchmarks (bench_bdd, bench_lambda)#4udesou wants to merge 1 commit into
udesou wants to merge 1 commit into
Conversation
Add backtracking's quick-and-dirty hash-consing benchmarks from ocaml-hashcons#19 to simple/hashcons/, filling a weak-pointer/ephemeron coverage gap in the suite. hashcons.ml/.mli are vendored as a local library so only the runtime varies across compiler comparisons. - bench_bdd -de-bruijn N: hash-consed BDD for a de Bruijn tautology; the workload ocaml/ocaml#13580 (mark-delay, 5.5) targets. At N=800 it shows ~1.46x speedup and ~41% lower peak heap on 5.5 vs 5.4, and is highly space_overhead-sensitive. - bench_bdd -pigeon N: pigeonhole tautology; milder hash-consing stressor. - bench_lambda N: lambda-calculus quicksort over hash-consed terms; CPU-bound short micro. Reads its term file from $QUICKSORT_TERM (the run cwd is a temp dir) with a fallback to the upstream relative default. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds
backtracking's quick-and-dirty hash-consing benchmarks from ocaml-hashcons#19 undersimple/hashcons/, filling a weak-pointer / ephemeron coverage gap in the suite (Frama-C etc. don't exercise this path).hashcons.ml/.mliare vendored frombacktracking/ocaml-hashcons(LGPL-2.1, J-C Filliâtre) as a local library, pinned so that only the runtime varies across compiler comparisons.Benchmarks
bench_bdd -de-bruijn800bench_bdd -pigeon12bench_lambda6Notes / verification
-de-bruijnis the GC-pacing showcase. Verified locally atN=800: 5.4.1 → 5.5(d8bb46c) gives ~1.46× speedup (2.24s → 1.53s) and ~41% lower peak heap (46.8M → 27.7M words). Highly sensitive tospace_overhead— a good candidate for the(s,o)sweeps. Runtime and peak RSS both scale withN(N=800≈ 2s / ~370 MB on 5.4).-pigeonbarely moves under #13580 (~7%) — kept for coverage, not as a PR demonstrator.bench_lambdais CPU-bound (heap ~8 MB regardless ofN) and has a combinatorial runtime cliff (N=6≈ 0.8s,N=7≈ 60s), so it stays a short micro.bench_lambdareads its marshalled term from$QUICKSORT_TERM(absolute path) with a fallback to the upstream relativequicksort.term, because the running-ng run cwd is a temp dir. The config must pointQUICKSORT_TERMatsimple/hashcons/quicksort.term.Default inputs chosen for ~2–3s on modern hardware; the running-ng config tunes
Nand thespace_overheadsweep separately.🤖 Generated with Claude Code