Repository navigation
ci: track the 4-to-1 aggregation proven on one thread - #530
Merged
kevaundray merged 1 commit intoOct 7, 2026
Merged
kevaundray merged 1 commit into
kevaundray merged 1 commit into
Conversation
A new proven_trees() case, aggregate-leanxmss-100-4to1-1thread: the tree of aggregate-leanxmss-100-4to1 (a leanXMSS 100 leaf, a first-level node over 4 copies of its proof, a node over 4 copies of that) proven whole on one thread through ONE_THREAD's re-exec with LEANVM_NUM_THREADS=1, reporting -first and -node with the multi-threaded entry's measures. A bench.yml matrix job on both testbeds; AGENTS.md names it. --cycles-only is unchanged (identical JSON against the base). Local smoke (AMD Ryzen 9 7950X3D, loaded): --only aggregate-leanxmss-100-4to1-1thread --repeat 1 --cooldown 0 took 7.5 s wall at CPU 99%; first-level node 0.98 s and node 1.06 s against 0.25 s and 0.24 s on all threads, proof sizes equal (283,331 and 285,027 bytes).
Benchmarks: base against this PR, on one runner5f2c1fc merged into its base, against the base 651735f: 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
|
kevaundray
added a commit
that referenced
this pull request
Oct 7, 2026
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 #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%.
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
A new
proven_trees()case,aggregate-leanxmss-100-4to1-1thread: the same tree asaggregate-leanxmss-100-4to1(a leanXMSS 100 leaf proven once, a first-level node over 4 copies of its proof, a node over 4 copies of that), proven on one thread. It prints the two benchmarks the multi-threaded entry prints, with the same measures (latency,proof-size,verify,stage.<name>,peak-memory,heap-peak,allocations):aggregate-leanxmss-100-4to1-1thread-first: the first-level node (the RISC-V verifier in rows over 4 leaf proofs).aggregate-leanxmss-100-4to1-1thread-node: the node above it (the recursion verifier in rows over 4 first-level proofs).This sits next to
aggregate-leanxmss-100-2to1-1thread(#470), so both tracked tree shapes now show what one core costs per level, apart from how the prover scales over the testbed's cores.How
Exactly as the 2-to-1 one-thread case: the name is added to
ONE_THREADand toproven_trees()inbins/leanvm/src/tracked.rs, and to thebench.ymlmatrix (both testbeds). When the pool has more than one thread, the CLI runs itself again with--only <case>andLEANVM_NUM_THREADS=1and merges the child's JSON; the child proves the whole tree, leaf included. AGENTS.md's CI paragraph names it.--cycles-onlyis unchanged: its JSON is byte-identical to the base's.CI time
Estimate, from the latest Bench run on the self-hosted testbeds (#528): a run of
aggregate-leanxmss-100-2to1-1threadtakes 6.0 s on x86-64 (Xeon Gold 6548N) and 9.4 s on arm64 (Neoverse-V2), and the rest of the job (checkout, cache, the two builds) about 65 s; those jobs took 2.2 and 2.6 minutes. Locally, a 4-to-1 one-thread run takes about 1.35 times a 2-to-1 one (6.8 to 7.7 s against 5.2 to 6.0 s), so a run should take about 8 s on x86-64 and 13 s on arm64, and a job with 10 runs about 2.5 minutes on x86-64 and 3.2 minutes on arm64.Measured, in this PR's Bench run (the base cannot run the new entry, so each new job proved the head's 5 runs only): a one-thread 4-to-1 run took 8.1 s on x86-64 and 14.2 s on arm64, and the new jobs took 2.1 minutes (128 s) and 2.6 minutes (158 s). Once the base has the entry, each job proves 5 more runs: about 2.8 minutes on x86-64 and 3.8 minutes on arm64. The longest job in the same run is the 2-to-1 one-thread job on arm64 (3.0 minutes), so the new arm64 job becomes the longest by under a minute; jobs run in parallel, so a PR's Bench wall time grows by at most that. I would leave
ROUNDSas is; if the arm64 job's length matters, the change would be a per-case round count inscripts/ab.sh(3 rounds for this case would save about 57 s on arm64), not fewer rounds for every benchmark.CI numbers
Medians of the 5 rounds, latency, from this PR's run; each pair of columns is one CPU (x86-64 Xeon Gold 6548N, 32 vCPUs; arm64 Neoverse-V2, 16 vCPUs).
Proof sizes match the multi-threaded entry (283,331 and 285,027 bytes); peak memory on one thread is 1.43 GiB on x86-64 and 2.23 GiB on arm64. For reference, the 2-to-1 one-thread entry in the same run: 0.630 s and 0.658 s on x86-64, 1.065 s and 1.119 s on arm64.
Local smoke (AMD Ryzen 9 7950X3D, 32 threads, under other load)
/usr/bin/time cargo leanvm bench --only aggregate-leanxmss-100-4to1-1thread --repeat 1 --cooldown 0: 7.5 s wall, 7.4 s user, CPU 99% (the parent idles while the child proves), so it ran on one thread.--only aggregate-leanxmss-100-4to1for comparison: 2.3 s wall, CPU 709%.Proof sizes match the multi-threaded entry; peak memory 1.53 GB. The base refuses the new name (
no tracked case is named aggregate-leanxmss-100-4to1-1thread), so this PR's own Bench jobs prove the head's 5 runs only.Checks
cargo fmt --all --checkcargo clippyallwithRUSTFLAGS="-C target-cpu=haswell"on 1.97 and 1.99, native on 1.99cargo test --release -p leanvm-cli -p benchcargo docallactionlint .github/workflows/bench.yml