Repository navigation
ci: track the one-thread cases at 4 and 8 threads too - #531
Merged
kevaundray merged 1 commit intoOct 7, 2026
Merged
Conversation
leanxmss-100, aggregate-leanxmss-100-2to1 and aggregate-leanxmss-100-4to1 are now also proven on 4 and 8 threads (`-4thread`, `-8thread`), so each is reported at 1, 4, 8 and all threads on both testbeds. `ONE_THREAD` becomes `THREADS`, a list of (case, threads): the CLI proves such a case in a child with `LEANVM_NUM_THREADS` set to its count unless its own pool already has that many performance workers. The `-1thread` cases keep their names and behaviour, and `--cycles-only` is unchanged (its JSON is identical to leanEthereum#530's head). Smoke, `bench --only <case> --repeat 5 --cooldown 0` on a Ryzen 9 7950X3D (32 threads), `/usr/bin/time`'s CPU: leanxmss-100-1thread 100%, -4thread 360%, -8thread 646%, leanxmss-100 1905%; aggregate-leanxmss-100-4to1-4thread 343%, -8thread 597%.
Benchmarks: base against this PR, on one runner4c7e325 merged into its base, against the base 40f22fc: each benchmark run in turns on one runner, base and PR 5 times each. A size is shown when it changed; a time or a peak memory when it moved the same way in every round and its median by at least 1% (the change is the median ratio, with the rounds' range). Proving time
Prover stages
Verifying time
Proof size
Peak memory
allocations
heap-peak
Every resultProving time
Prover stages
Verifying time
Time per operation
Proof size
Peak memory
allocations
heap-peak
|
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.
What is tracked
The three cases proven on one thread (#461, #470, #530) are now also proven on 4 and 8 threads, so CI reports each at 1, 4, 8 and all threads on both testbeds:
leanxmss-100-1threadleanxmss-100-4threadleanxmss-100-8threadleanxmss-100aggregate-leanxmss-100-2to1-1threadaggregate-leanxmss-100-2to1-4threadaggregate-leanxmss-100-2to1-8threadaggregate-leanxmss-100-2to1aggregate-leanxmss-100-4to1-1threadaggregate-leanxmss-100-4to1-4threadaggregate-leanxmss-100-4to1-8threadaggregate-leanxmss-100-4to1Each new case reports the same metrics as its one-thread twin (a tree's as
-firstand-node), and is its own matrix job on both testbeds. The-1threadcases keep their names and behaviour, so their comparisons carry on.--cycles-onlyis unchanged: its JSON is identical to #530's head.Mechanism
ONE_THREADinbins/leanvm/src/tracked.rsbecomesTHREADS, a list of (case, threads). The pool readsLEANVM_NUM_THREADSonce per process, so the CLI proves such a case in a child (itself again, with--only <case>andLEANVM_NUM_THREADS=<threads>) unless its own pool already has that many performance workers (parallel::topology().perf, which on Linux is the whole pool; comparing the performance count rather than the total keeps a child on Apple silicon from re-running itself), and merges the child's JSON as before.No CPU pinning, as for the one-thread cases: each job runs on a fresh VM it has to itself, and base and PR alternate within that one job, so both sides see the same scheduler and the same idle cores.
CI time
Estimated before the run, from #530's Bench run: a job costs about 90 s (x86-64) or 82 s (arm64) before its runs (setup and building both sides), a 4- or 8-thread run 1 to 3 s on x86-64 and about 1.5 times that on arm64, so the six new jobs per testbed would add about 11 runner-minutes each to the 26.5 (x86-64) and 26.8 (arm64) of today's 17 jobs, and none of them would be the longest job.
Measured in this PR's Bench run, where the base lacks the new cases, so each ran 5 times (head only):
aggregate-leanxmss-100-4to1-1thread)aggregate-leanxmss-100-4to1-1thread)Once the base has them, each new job adds the base's 5 runs: about 54 s more over the six on x86-64 and 72 s on arm64, so about 11.4 runner-minutes added on x86-64 and 10.5 on arm64 per PR. Each new job would then take 1.5 to 2 min, below the longest (the one-thread 4-to-1 tree, 3 to 3.8 min), so the run's wall time grows only if the runner pools cannot start the extra jobs at once. In this run each pool started all but one or two jobs within 4 min of the first; the last x86-64 job and the last two arm64 jobs started about 10 min later, as three arm64 jobs did in #530's run with 17 jobs, and those stragglers set the run's wall time (20 min here, 16 min for #530). That is modest, so this keeps
ROUNDSas it is for these cases.Results
Proving latency, the median of this run's 5 head runs per case, with the speedup over one thread. x86-64, Intel Xeon Gold 6548N (32 vCPUs, so all threads is 32):
leanxmss-100aggregate-leanxmss-100-2to1-firstaggregate-leanxmss-100-2to1-nodeaggregate-leanxmss-100-4to1-firstaggregate-leanxmss-100-4to1-nodearm64, Neoverse-V2 (16 vCPUs, so all threads is 16):
leanxmss-100aggregate-leanxmss-100-2to1-firstaggregate-leanxmss-100-2to1-nodeaggregate-leanxmss-100-4to1-firstaggregate-leanxmss-100-4to1-nodeJob durations in this run (the 1-thread and all-thread jobs ran 10 times, base and head; the new ones 5, head only):
x86-64:
leanxmss-100aggregate-leanxmss-100-2to1aggregate-leanxmss-100-4to1arm64:
leanxmss-100aggregate-leanxmss-100-2to1aggregate-leanxmss-100-4to1Smoke
cargo leanvm bench --only <case> --repeat 1 --cooldown 0for each case ofTHREADS, undersystemd-run --user --scope -p MemoryMax=16G -p MemorySwapMax=0on a Ryzen 9 7950X3D (16 cores, 32 threads), all exit 0, with the proving latency:/usr/bin/time's CPU with--repeat 5(the rest of a run is serial setup and verification):Under
strace -f, each pinned case execs one child, which spawns 0, 3 or 7 workers for 1, 4 or 8 threads; withLEANVM_NUM_THREADS=4already set,--only leanxmss-100-4threadproves in place with no child.cargo leanvm benchwith no--onlyproves all 10 cases and 8 trees and prints all 26 benchmarks.Checks:
cargo fmt --all --check;cargo clippyallfor haswell on 1.97 and 1.99 and native on 1.99;cargo test --release -p leanvm-cli -p bench;cargo docall; actionlint onbench.yml.