Repository navigation
perf-benchcomp: count solver invocations and judge solver time against noise #4822
Description
Requested feature: make the perf-benchcomp regression check robust to variation that is not a regression, by recording the number of solver invocations per harness and by judging solver time against a noise estimate rather than a fixed 1.5x on a single run per side.
Use case: the error_on_regression step of perf-regression.yaml fails a PR when a harness's summed solver time is 1.5x its main-side value. In the fourteen executed runs of the job between 2026-09-15 and 2026-09-19 the main-side solver time of inet::checksum::tests::differential, one unchanging formula (8,763 VCCs on every run), ranged from 40 s to 148 s; within a run the two sides usually agree, but they diverged 0.42x on one PR and 4.6x, 1.85x and 1.45x on three others, with identical VCC and step counts on both sides every time. The only two runs that tripped the check were on PRs that do not touch the code those harnesses use (#4801, #4804), and both failures reproduce locally on the unchanged main commit: two compilations of the same commit give slice::tests::vectored_copy_fuzz_test 5 and 8 external-solver calls of 21 s each (see #4821), which is 0.61x or 1.64x depending on which side runs which. Meanwhile the compile-timer jobs in the same workflow already label such changes ProbablyNoise under a threshold of max(2 x std_dev, 5%).
Link to relevant documentation (Rust reference, Nomicon, RFC): n/a (tools/benchcomp, configs/perf-regression.yaml, parsers/kani_perf.py, which sums the Runtime Solver: lines per harness).
Test case:
# two full runs of the suite on one commit, e5f2e75a4, checked out twice as old/ and new/
$ tools/benchcomp/bin/benchcomp --config tools/benchcomp/configs/perf-regression.yaml run
$ tools/benchcomp/bin/benchcomp --config tools/benchcomp/configs/perf-regression.yaml collate
$ tools/benchcomp/bin/benchcomp --config tools/benchcomp/configs/perf-regression.yaml visualize --except dump_markdown_results_table
benchcomp: WARNING: Benchmark 's2n-quic/quic/s2n-quic-core/slice::tests::vectored_copy_fuzz_test' regressed on metric 'solver_runtime' (105.89 -> 173.42)
Two small changes would cover the cases seen: parse the number of Solving with ... calls as a metric and skip the solver-time rule when it differs between the sides (the per-call time is the comparable quantity), and give the rule a floor in absolute terms and a noise margin like the compile-timer's. I can send either.
Activity
srivatsansamraj commentedon Sep 21, 2026
Another instance, this time on @feliperodri's #4820: the run tripped on
inet::checksum::tests::differentialat 2.24x (56.8 s to 127.5 s) with the same 8,763 VCCs on both sides and symex unchanged, for an autoharness-side change that touches no perf harness.feliperodri commentedon Sep 24, 2026
You're right, and I measured how bad it is. Pulling the metrics out of seven
mainruns and keeping only the pairs where VCC and step counts match on both sides — the same formula, by construction — gives 910 (benchmark, run) pairs: median ratio 0.99×, p90 1.08×, range 0.41× to 2.41×. So the sides normally agree closely, and then occasionally don't, by more than the threshold. The 2.41× pair failed a run;inet::checksum::tests::differentialranged 38.8s–116.0s on themainside alone, matching your 40–148s.#4846 takes both of your suggestions, with one addition: since identical VCC and step counts mean both sides are solving the same problem, the solver-time rule now only applies when one of those counts moved. That alone removes every false positive in the seven runs I replayed, while a synthetic change that grows the formula and triples solver time is still caught.
The call count is in there too, as
solver_callsplus a derivedsolver_runtime_per_call, and the count shows up in the results table — a differing sum then explains itself rather than looking like a regression.What it gives up: a change that makes the same formula slower no longer fails the job. That seemed the right trade, but it is worth a second opinion on the PR.
benchcomp: scale the solver-time threshold to whether the SAT instanc…