Performance optimisation history

Reverse-chronological record of the optimisations that keep the pipeline and prove paths fast. Each entry names the measurement that drove it. Benchmark methodology and current figures are on Performance; the just prove timing table is on Prove timing and the optimisation review.

Optimisation history

Kept in reverse-chronological order. Every entry names the measurement that drove it so the next round of work can see whether the previous assumption still holds.

Parallel pre-build steps + a packed directory memo (1.63.0)

The driver was plan.md P1 and P2: the cold build and cold prove phases each needed a measured verdict, and the 1.61.0 profile put a 13 percent L1 dcache-miss rate beside 14 106 warm newfstatat calls, and the 1.61.0 direction memo put 14 597 warm newfstatat calls beside a 41.7 ms warm pipeline, largely in the directory memo’s slot layout.

  • The five pre-build steps are independent, so they now run at once. The version spec, the CSS 4px gate, the dashboard template, the bundled manual, and the tldr page read different inputs and write different outputs, and the serial recipe paid their sum. The steps measure 463 ms in series and 295 ms as the concurrent bundle at load 2.7-2.8 (36 percent of the step time overlaps), and a paired ten-run sample of a no-op just build reads 609 ms against 732 ms (-16.8 percent). Every exit code is still checked before the compile, and the first failure is the build’s exit code.

  • The phase split is now an instrument, not a one-off script. just bench times each step on its own and the bundle as tools/build.py --steps-only, reads the step list from tools/build.py so the bench cannot measure a step the build no longer runs, and prints the overlap. That is what lets the next cold-phase review start from a table instead of a fresh profile.

  • The memo packs its slots and recalls the busy directories. A slot held a 256-byte path image and up to 64 entries of 72 bytes, and the cap rejected the self tree’s two densest scanned directories (78 and 84 entries), so every walker re-enumerated them. The slot now keeps a 128-byte key and packed 66-byte entries, recalls up to 128 entries, and probes on the insert path so a collision cannot hide a live snapshot. Warm newfstatat falls from 14 597 to 8 142, the memo reports 131 hits and 60 misses against 105 and 86, and warm pipeline reads 46.8 ms against 51.8 ms paired (-9.7 percent). The wider slots cost 1.7 MiB of peak resident set.

  • The negative results are recorded as such. A pinned perf stat sample could not put the L1 dcache-miss rate below the run-to-run spread (22-34 percent both before and after), so the syscall count and the wall time carry the claim. The cold compile is gprbuild’s own parallel work over 79 units at -O2 by design, the workspace sync fetches nothing on a synced tree, and the cold prove row is the solver’s. None of those moved, and the plan’s bar is met by measuring them rather than pretending they were removed.

Deterministic doc bundling + no-op builds (1.50.0)

The driver was the just prove wall: on an unchanged tree it still took seconds, and sometimes tens of seconds, even with a warm result cache. The suspect was the embedded offline manual (tools/gen-docs.py -> src/adacovex-docs_template.ads), and the profile confirmed it:

  • The generated spec was not stable. gen-docs.py collected assets from the incremental Sphinx build directory, so pages that a doc move had left behind stayed in the bundle. A developer tree shipped 217 assets while a fresh clone produced 204 (thirteen dead pages from the pre-1.49.0 layout), and gen-docs.py --check failed on a fresh clone. Because the spec is a proof input, any content change invalidated the cached SPARK proof and made just prove run gnatprove again (a 20-88 s session).

  • The fix removes the failed work. Sphinx now builds clean whenever a SHA-256 fingerprint of docs/ changes, and both generators write their Ada spec only when the content changed. A no-op run keeps the spec’s mtime, so alr build is a true no-op (gprbuild: "adacovex" up to date, ~0.38 s) instead of recompiling the 28k-line unit and relinking.

  • Measured effect. just prove on an unchanged tree fell from seconds (the recompile plus relink; 20-52 s when the spec flipped and the proof re-ran) to ~1.0 s (five runs), with the result cache at 42 hits and 0 misses. The binary-level benchmark shapes are otherwise flat: pipeline warm 46 ms, prove warm 55 ms, warm newfstatat ~6.9k.

  • The proof input stopped carrying the bundle. Even with a stable spec, a real documentation edit changed the bundled manual and therefore the proof-input hash, so every docs edit cost a fresh proof. The two generated bundle specs (adacovex-docs_template.ads, adacovex-dashboard_template.ads) are now excluded from that hash: they are multi-thousand-line string constants with no subprogram and no check. Verified by editing a docs page and re-running just prove: the spec was regenerated and the cache line still read gnatprove inputs unchanged.

  • A second, smaller win. Sphinx itself now runs only when the docs sources changed (the fingerprint stamp): a no-op just build spends ~0.4 s in the generator instead of ~5.9 s in a clean Sphinx rebuild.

  • The payload itself shrank. The asset bodies moved from base64 to base85 (4 bytes to 5 characters instead of 5.33), and the Furo sidebar is stored once per branch under _nav/ instead of once in each of the 191 pages, filled in by resources/js/book-nav.js. Together they take the generated spec from 2.34 MB to 1.93 MB (17.3%) and the stripped binary from ~5.7 MiB to ~5.3 MiB, against the phase’s otherwise flat shapes.

Opt-out marker machinery + the dead proof-probe removal (1.46.0)

The 1.46.0 per-file opt-out markers added two new per-file probes to the cold paths, so the release was profiled before shipping (just perf-bench plus strace over the cold and warm prove shapes):

  • Warm shapes are untouched. The no-covex-spark-proof marker walk runs only after the result-cache lookup misses, so a warm prove hit returns before the walk starts. The table column is flat (prove warm 46 ms, pipeline warm 41 ms).

  • The profile shows cache health. L1-dcache miss rates sit at 0.1-0.7% – far under the ~5% level where data-layout work pays – and the ~6.3k newfstatat per warm run (~67% of syscall time) is the established I/O floor, not a regression.

  • A dead probe was found and removed. The Ada source scanner called the opt-out detector twice per scanned spec – once for the docstring marker and once for the SPARK-proof marker – but the proof flag it wrote (Pkg.Proof_Opt_Out) was never read anywhere: the prove subcommand probes the markers itself for its -u unit list. Removing the redundant probe (and the dead Package_Info field, which bumped Cache_Schema to s11) saves one open plus one header read per scanned spec on every cold scan – measured at ~160 -> ~120 source-file opens on the cold self-assessment. It is sub-millisecond against the ~88 ms cold wall, but it was pure dead work on the hottest per-file path.

Shared directory-snapshot memo + correct-version probe validation (1.45.0)

Two findings drove 1.45.0, both from strace profiles of the warm path after 1.44.0:

  1. Same directory, different memo key. The walkers spelled the same directories differently (".", "src", "/abs/src"), so the 1.44.0 snapshot memo served hits only within one spelling. The memo now resolves every key to its absolute image (the process working directory is read once), and the slot table grew from 64 to 256 (the self tree enumerates ~120 distinct directories). Warm hits rose from 43/82 to 107/58 on the self audit, and Collect_GPR_Files joined the shared-snapshot walkers.

  2. docs/_build was still walked. The shared Skip_Walk_Dir did not exclude it, so the vendored-discovery walk enumerated ~750 Sphinx build-product files per run. A build-product tree can never be a vendored package, so _build joined the shared skip set.

The same release fixed a correctness bug the perf work exposed: cached system-tool versions were keyed only on the tool name and a 7-day TTL, so an upgraded binary kept its old version in the SBOM for up to a week. Both cache layers (the probe store and the tools-set blob) now carry the identity digest of the installed binary (path + size + mtime, SHA-256 folded); a changed digest re-probes exactly once, then serves from cache again. Verified with a PATH shim whose jj --version changes between runs: run 1 probes 0.44.0, run 2 (upgraded shim) re-probes 0.50.0 in a fully warm cache, run 3 serves 0.50.0 from cache (49 ms), run 4 (real binary restored) re-probes 0.45.1.

Net effect on the table: warm syscalls ~6k (docs/_build gone, but the PATH re-resolution and wider memo cost a few stats), warm wall 41 ms (1.44.0’s 23 ms plus the safety work), prove cold unchanged at the solver floor.

Persistent stat-stamp store, learned from language servers (1.44.0)

The 1.43.0 warm profile still showed ~2k stats per file per run: every adacovex invocation re-opened and re-hashed every unchanged file (sources for scan keys, manifests and vendored trees for graph keys) because the 1.28.0 stamp map dies with the process. Language servers solved this class of problem years ago: the Ada Language Server keeps a persistent indexed file set and re-parses only files whose on-disk state changed between sessions (lsp-ada_file_sets.ads, studied in the local checkout), and tree-sitter keeps its parse input in a single reusable buffer (TSInput, tree_sitter/api.h). adacovex adopts the first technique directly:

  • Hash_File gained a second fast path backed by a persistent stat-stamp store at <cache>/stamps/ (machine-local, like the probe and meta stores, so --cache-dir wipes never cost re-hashes). A record is <sha-256-of-path> holding size, mtime, record time, and the digest; a lookup is one open + four short reads and validates two stats (size + mtime) against the stored pair.

  • The store is size-gated at 16 KiB. Measured on the self-audit tree, stamping the 38 small .ads sources made warm runs slower (a lookup costs more than re-hashing a 10 KB file); the gate keeps the store for the payloads where re-hashing actually dominates – vendored manifests, lockfiles, generated assets. This is the same cost model language servers apply when deciding whether dirty-tracking pays.

  • Two git-proven safety rules keep a stale digest from ever being served: the size AND mtime must both match, and a file modified during the second the record was written is never recorded (git’s racy-clean rule). A Reset_Process_Stamps diagnostic lets tests (and long-lived --serve processes) re-walk files as a fresh run would.

  • Result: warm syscalls ~12k -> ~2k (newfstatat ~26.8k -> ~2k on a stamped tree), pipeline warm 35 -> 23 ms, pipeline cold 86 -> 60 ms (a wiped result cache re-serialises instead of re-hashing). Persistent_Stamp_Hits / Persistent_Stamp_Misses counters make the fast path testable (Result-cache tests 22+).

Walker-skip completion + cached-proof restore (1.43.0)

The 1.43.0 strace profile of a warm run showed ~21k newfstatat calls, and 13.3k of them (~53%) hit docs/_build – the Sphinx build tree of the bundled offline manual, a gitignored build product with 461 files. Fourteen distinct walkers re-enumerated it per run: the tools-key source tree hash, the vendored discovery walk, the graph-key language probe and vendored hash, the GPR collection walk, and more. Four changes cut the warm syscall count to ~12k and warm wall to ~35 ms:

  • The shared Skip_Walk_Dir-governed walks (tools scan, graph key, vendored hash) plus the scanner, GPR-collection, and vendored-component walks now skip _build explicitly. Skip_Walk_Dir itself deliberately does not skip node_modules: the generic vendored discovery descends into it to find package manifests, and its own vendor-scan skip list is unchanged. A build-product tree is a per-walker decision, not a global one – vendor roots must stay discoverable.

  • The Vendored_Hash internal tree hash now honours Skip_Walk_Dir, so the graph-key walk never descends into .venv/alire/build trees either.

  • The prove-input walk skips _build (its skip set already covered docs/ and the installer trees).

  • Restore_Proof_Output (see the table notes above): a warm prove hit writes the cached gnatprove.out content back to <target>/obj/gnatprove/, so a wiped session store no longer turns a cache hit into a Stone/0-VC assessment failure.

just perf-bench itself had two reporting bugs fixed while profiling this: perf stat writes its counter table to stderr, which the old capture_output + print(stdout) shape discarded (the perf sections printed adacovex output but no counters), and the strace ... 2>&1 | tail -20 pipe interleaved the workload’s stdout with the table and cut the header rows. Both tables now print in full, and a missing perf or strace fails loudly instead of silently printing nothing.

Deploying a manifest-pinned gnatprove prints a progress line (deploy: gnatprove <v> not in the toolchain cache -- downloading via alr (one-time, may take a minute)...) – the first deployment downloads a ~130 MB bundle through alr -n get and a silent minute of nothing read as a hang. The deployment is one-time per version; every later run reuses the deployed crate with no download.

SIMD and other optimisation candidates (1.46.0)

An optimisation review in 1.46.0 asked whether SIMD or other low-level speed-ups could improve the pipeline. The measurements say no:

  • A cold self-assessment (no result cache, ~250 source files) completed in ~88 ms and a warm one in ~41 ms on the dev machine (hyperfine, 1.46.0), even with an unoptimised local build profile. The pipeline is I/O-bound and cache-bound, not compute-bound. A prove run is dominated by the gnatprove solver floor (~39 s cold), and its adacovex-side share is about a second.

  • just perf-bench (perf + strace over the same tree, 1.46.0) showed a healthy cache: L1-dcache miss rates of 0.1-0.7% sit far under the ~5% level where data-layout work pays, so no struct packing or prefetching is warranted. The I/O story is unchanged: ~6.3k newfstatat on a warm run (~67% of syscall time) is the walk floor.

  • The per-byte scanning loops (comment stripping, decision counting, HLR tags) are the only SIMD candidates. They process short lines one byte at a time; auto-vectorisation needs -O3 (or -ftree-vectorize) and gains little on data this small, at the cost of the zero-dependency build’s simplicity.

Conclusion: no SIMD or assembly is added. The sanctioned path to more speed is the existing one: higher optimisation in release profiles, the shared directory snapshot memo, and the content-hashed result cache. If a future profile shows the scanner hot, the first move is whole-file buffered reads.