perf: count only user-mode instructions in benchmarks - #14908
Draft
Kha wants to merge 1 commit into
Draft
Conversation
This PR restricts the `instructions` benchmark metric to user mode, making it far less noisy and independent of the machine it is measured on. Reported instruction counts drop by a one-time step of roughly 5% on elaboration-heavy benchmarks and considerably more on short, load-dominated ones; comparisons from this commit onwards are unaffected. `tests/measure.py` requested the bare `instructions` perf event, which counts user and kernel mode together wherever `perf_event_paranoid` permits it. Kernel-mode instructions track page cache state, memory pressure and kernel version rather than anything Lean does, and they carry practically all of the variance: measured over repeated runs of `elab_bench/big_match`, the total has a relative standard deviation of 2.01% while its user-mode part has 0.02% and its kernel-mode part 11.41%. Their cost is already covered, more directly and more quietly, by `task-clock`, `wall-clock`, `maxrss` and the `bytes .olean` metrics. Requesting `instructions:u` explicitly also pins down what the metric means. `perf` silently degrades an unrestricted counter to its user-mode variant when it lacks permission, and `get_perf_result` accepts that under the same metric name, so the quantity being recorded depended on the measuring machine and a change in its configuration would have registered as a large improvement across every series at once. The `:u` modifier is available at every `perf_event_paranoid` level, so the metric is now comparable between the benchmark machine, CI and developer machines. `cycles` deliberately keeps counting both modes, alongside the other cost metrics. Co-Authored-By: Claude <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for d75ee59 against 16e77c4 are in. There are significant results. @Kha
Large changes (48✅)
Medium changes (40✅)
Small changes (2532✅)
|
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
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
3 participants
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.
This PR restricts the
instructionsbenchmark metric to user mode, which should further reduce noise.