Repository navigation
Feature/benchmarks - #201
Merged
Merged
Conversation
Per-op rdtsc microbenchmark for the v3 graph store: - Adaptive sampling (riff RE=CV/sqrt(n) criterion, 2% target, batch-means), resolved in-run rather than persisted; auto-sizes iterations per op (~0.1s/run). - Frequency-reference op so comparisons cancel cross-run CPU-turbo drift; median is the headline metric. CI tooling, no committed baselines (nothing for git to churn): - bench-compare: base-vs-head on one runner, freq-corrected median, median of N interleaved runs, soft-fail + PR comment (benchmark.yml). - bench-aggregate + bench-creep: reference-normalized time-series on an orphan bench-history branch + slow-creep detector vs rolling baseline (benchmark-history.yml, on push to master). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EfzTKfjTRRNQ828crWoJf1
fc_graph.c: WP/ACSL proofs (memory-model-clean abstractions, fc_index idiom) of the adjacency edge encoding that every traversal decodes. - adj_pack / adj_pack_injective: the (target<<2)|dir packing is a lossless round-trip and injective for target<2^62, dir<4. Modeled arithmetically as target*4+dir (decode /4, %4 — bit-identical for these field widths); the literal bitwise form is opaque to WP's integer model, the same abstraction boundary fc_index uses for hash32. - read_edges_model: iterating count 24-byte entries at adj+8+i*24 is memory-safe and terminating. 42/42 goals discharged by Alt-Ergo. CI (proofs.yml, path-filtered to proof changes): opam frama-c + alt-ergo, runs `make proofs`. scripts/run-proofs.sh gates the result — frama-c exits 0 even with unproved goals, so it parses "Proved goals: P / T": clean files must be 100%, fc_tree is safety-only (mf_fit_model termination needs an acyclicity measure, the documented free-list-cycle frontier). Verified locally: fc_proofs 25/25, fc_index 27/27, fc_graph 42/42, fc_tree 12/13. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EfzTKfjTRRNQ828crWoJf1
Contributor
Per-op benchmark — p50 cycles (base vs head)base runs: 5, head runs: 5 (median of mins) · freq-correction ×0.9848 · threshold head−base > max(40 cyc, 5%)
* head frequency-corrected to base via the No regressions beyond threshold. |
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.
No description provided.