Skip to content

fix(instruments): restore the rounds 2-4 phase span and make the prover report honest - #893

Merged
ColoCarletti merged 5 commits into
gpu-opt-table-schedulerfrom
gpu-opt-877-review-fixes
Aug 3, 2026
Merged

fix(instruments): restore the rounds 2-4 phase span and make the prover report honest#893
ColoCarletti merged 5 commits into
gpu-opt-table-schedulerfrom
gpu-opt-877-review-fixes

Conversation

@MauroToscano

@MauroToscano MauroToscano commented Aug 3, 2026

Copy link
Copy Markdown
Contributor

Review fixes for the per-table scheduler, targeting gpu-opt-table-scheduler so they land with it. No scheduler behaviour changes: the fused chain, gate semantics, heaviest-first ordering and the cores * 2 / 3 constant are untouched.

1. The rounds 2–4 phase wall vanished from the timeline

This is the one that matters, because it is the instrument the GPU campaign reads its numbers from.

On origin/main, rounds_2to4 was one span wrapping the chunk loop (prover.rs:3503), so it measured the phase. The scheduler moved it inside the per-table closure (:3568), one instance per table. scripts/profiling/phase_table.py:129 does e["wall_ns"] += s["wall_ns"] — it sums spans that share a label — so that row became the sum of N concurrent tables, up to k× the real wall clock and able to print >100%. And with the span consumed per table, nothing was left measuring the phase at all. Same story for r1_aux_build and r1_aux_commit, which were also phase-level spans on main (:3143, :3225).

Fix (2fa9d75e): reopen rounds_2to4 on the calling thread around the whole fused region (prover.rs:3611-3619, dropped at :3664), and rename the per-table spans to r1_aux_build_table / r1_aux_commit_table / rounds_2to4_table so a per-instance label can never be summed into a phase row.

This also repairs LAMBDA_VM_NSYS_CAPTURE_SPAN=rounds_2to4 (scripts/profiling/README.md:115): with the label on the per-table span, N concurrent driver threads each called cuProfilerStart/Stop, and the first table to finish stopped the capture while the rest were still running. One phase span means one capture range again.

Verified on prove(fib_iterative_1M) with --features instruments — phase spans sum to their parent exactly:

  proving                                     11.585s   96.4%
    r1_prepass                              148.229ms    1.2%
    r1_main_commit                             2.493s   20.8%
    rounds_2to4                                8.943s   74.5%      <- restored
r1_aux_build_table                          408.711ms    3.4%      <- per instance
rounds_2to4_table                              2.946s   24.5%
...

0.148 + 2.493 + 8.943 = 11.584 vs proving 11.585.

The span depth field is not the problem, and is deliberately left alone. Worker-thread spans do record depth = 0, but phase_table.py:121 takes its denominator from max(s["wall_ns"] for _, s in pathed) — the longest span, not the root of the ancestor stack — so the "% of total" column was always correct and README.md:77 stays accurate. And prover/src/continuation.rs has recorded spans off worker threads since before this PR (:1146, :1205, :1299, :1328, :1415), with the comment at :1051-1053 saying so outright. So instruments.rs:5-14's claim that spans "do not overlap and sum to their parent" was already inaccurate on main. It is rewritten to describe what the data actually is — including the label-summing trap that caused this bug.

2. The timing report was self-inconsistent (same commit — compile-coupled)

aux_build_elapsed / aux_commit_elapsed were pinned to Duration::ZERO. That was deliberate (prover.rs:3250-3251 documents the folding); the report just never got updated to match. Consequences, all in the terminal report every --features instruments user sees:

  • prover/src/instruments.rs:74 computed round1 = main_commits + aux_build + aux_commit, so :77 "Round 1" and :78 " Main trace commits" printed the identical number.
  • :89 / :110 printed a plausible 0.00s for the two aux buckets while accum_r1_aux kept their children populated (prover.rs:3410, :3449, :3497) — nonzero children under zero parents, and a fabricated zero rather than a missing row.
  • "Round 1" understated by the whole aux stage while "Rounds 2–4" absorbed it.

The fused stages genuinely have no wall-clock phase of their own any more, so rather than resurrect separate timers the report now shows the two phases that remain, with the aux CPU-time rows grouped under the fused phase behind headers that say they are summed over tables:

  Round 1 (main trace commits)            1.41s   12.9%
      Main LDE (fused GPU: …)             2.29s   20.9%
      Main commit (Merkle, CPU only)      1.88s   17.2%
  Rounds 2–4 (aux build+commit fused in)  9.25s   84.4%
      ── aux build (CPU, summed over tables) ──
      LogUp fingerprint (CPU)             2.65s   24.2%
      …
      ── aux commit (CPU, summed over tables) ──
      Aux LDE (fused GPU: …)              3.02s   27.6%
      …
      ── per table (R2–4 wall) ──

The dead MultiProveTiming::aux_build / aux_commit fields are removed, which is why this lands in the same commit as fix 1.

3. Bench script rows whose sources no longer exist (e6bf4a8a)

scripts/bench_prover_scaling.sh still parsed, printed and ran heap-growth regressions on snap("After aux build") / snap("After aux commit"), which the scheduler deleted (present on origin/main at prover.rs:3216, :3486). Not silent — regress skips a missing key and prints "(insufficient data)", print_row prints - — but two guards were comparing nothing. Re-adding the snapshots is impossible: with k tables in flight there is no single moment at which either stage has finished. Removed, with a NOTE saying why and naming the guards that still bracket the fused region ("After main commits", "Peak heap"). Kept deliberately minimal — this script has no Makefile target and no workflow referencing it.

4. Stale comments (5221d655, comments only)

The one a reviewer would be actively misled by: prover.rs:3134-3135 and :3266 said the GPU LDE handles stay paired with their table via "Phase D's zip chain … by construction". That mechanism is gone — pairing is index-keyed mutex cells (gpu_main_cells, filled at :3311, taken at :3534), and the aux handle never leaves its own table's task.

Also: the orphaned plan_table_chunks doc that VramGate's rustdoc had absorbed (:618-623VramGate is private so cargo doc won't render it by default, but it is still wrong); Lde's "all N tables' LDE columns are live simultaneously" (:263-266), now stating the real asymmetric bound — main LDEs all-N, aux LDEs ≤ k because each is created in aux_stage, moved by value into rounds_stage and dropped in build_round1 inside one task, except under debug-checks where the two-pass split holds all N across run_debug_checks; the "Split into two passes" block contradicting the comment two lines below it (:3219-3221); table_parallelism's single-arm doc (:568-570); and the "Phase D" sweep — 7 references with no definition left, its banner deleted while A/B/C kept theirs.

prover/src/auto_storage.rs is not touched: origin/main...gpu-opt-table-scheduler is crypto/stark/src/prover.rs and nothing else, so its stale comments are pre-existing and out of scope here. Verifier-side "Phase A/B/C" naming is likewise left alone.

5. CI: exercise the scheduler concurrently (e843d328)

table_parallelism() defaults to (cores / 3).max(1), and every job in pr_main.yaml is runs-on: ubuntu-latest with no larger-runner label, so PR CI proves with exactly one driver thread today — the concurrent path never runs, and VramGate is additionally inert on non-cuda builds (vram_budget = u64::MAX makes acquire's condition always true).

TABLE_PARALLELISM: 6 on shard 1 only of the 4-way "Prover tests" matrix is the smallest change that puts several real table closures in flight concurrently on a PR. The other three shards keep default-k coverage; the expression yields an empty string there, which fails to parse and falls back to the default, so it is inert. prover/Cargo.toml:8 is default = ["parallel"], so the env arm is the live one.

This is not a substitute for GPU coverage — gpu-tests.yml on merge_group rents a ≥16-core RTX 5090, taking the cuda arm (cores * 2 / 3, k≈10) with a finite VRAM budget, so both the concurrent and blocking paths already run before merge. The gap this closes is PR-time only.

No unit tests were added for VramGate / run_admitted / heaviest_first: the properties worth pinning are either structural (heaviest_first is (0..n).collect() + sort_by_key), already covered end-to-end (a slot mixup in run_admitted is schedule-independent and trips one of the three .expect("run_admitted fills every slot") sites or fails multi_verify), or unreachable from the call sites (k is .max(1)'d, order is always a full permutation). The one property with teeth — an over-budget table being admitted alone — hangs rather than fails if it regresses, which on an 8-10 minute shard burns to the job timeout.

Verified locally — none of it GPU-verified

No CUDA on this machine (math-cuda builds via nvcc stubs), and gpu-tests does not run on PRs, so nothing here has been exercised on a real device.

  • cargo check -p stark with each of instruments, debug-checks, disk-spill, cuda, and combined instruments,cuda,debug-checks,disk-spill; same for -p lambda-vm-prover — all clean.
  • cargo clippy -p stark --features cuda --all-targets — 30 warnings, the same set as the base branch (pre-existing "needlessly taken reference" noise in tests/fri_tests.rs, tests/prover_tests.rs, tests/row_pair_opening_tests.rs, lookup.rs, logup_gpu.rs). cargo clippy -p lambda-vm-prover --features instruments is warning-free — the new separator lines are plain literals, and the one pre-existing print_literal on the adjacent "sub-operation totals" separator was inlined to match.
  • cargo fmt --all then --check — clean.
  • cargo test --release -p stark --lib — 202 passed, 0 failed.
  • cargo test --release -p lambda-vm-prover --features instruments --test bench_single -- --ignored --nocapture for the timeline and report above, on CPU with k = 5.
  • bash -n scripts/bench_prover_scaling.sh; workflow YAML parsed with yq to confirm the env landed on the right step.

The per-table scheduler moved `r1_aux_build`, `r1_aux_commit` and
`rounds_2to4` inside closures that run on `std::thread::scope` worker
threads. `SPAN_DEPTH` is thread-local and a fresh OS thread starts at 0,
so all three were stamped `depth = 0` and recorded as root siblings of
`prove_total` instead of children of `proving`. That happens even at
k = 1.

Downstream, `scripts/profiling/phase_table.py` reconstructs the tree with
`del stack[d:]`, so a depth-0 span empties the ancestor stack and
`prove_total` stops being an ancestor of anything — the "% of total"
column documented in `scripts/profiling/README.md` becomes meaningless.

`run_admitted` now reads the spawning thread's depth and seeds each
driver with it via new `instruments::current_depth` / `enter_depth`.
Both call sites are `#[cfg(feature = "instruments")]`, so non-instrumented
builds are byte-identical.

Also correct the module contract doc: per-table spans genuinely do
overlap now — that is inherent to running one driver per in-flight table,
not a bug to code around. Only the top-level phase spans remain a strict
latency breakdown.
`aux_build_elapsed` / `aux_commit_elapsed` were hardcoded to
`Duration::ZERO`, but `prover/src/instruments.rs` still computed
`round1 = main_commits + aux_build + aux_commit` and still printed the
"Aux trace build" / "Aux trace commit" rows. Since `accum_r1_aux` keeps
firing, the report showed nonzero LogUp and Aux-LDE/Merkle children under
zero parents, and all the aux time silently landed in "Rounds 2-4".

Time both stages inside the fused chain and sum them across drivers
(`instruments::accum_aux_phases` / `take_aux_phases`), then restructure
the report to match what the scheduler actually does:

  - "Round 1 (main trace commits)" is now exactly the main commits — the
    last phase-wide barrier, since the main roots must all be in the
    transcript before the shared LogUp challenges are sampled.
  - Aux build, aux commit and rounds 2-4 sit under one wall-clock parent,
    "Rounds 2-4 (aux build+commit fused)", with the aux rows marked as
    summed across concurrent drivers — they may exceed that wall, the same
    convention the existing accum_* sub-rows already use.

No zero parents over nonzero children remain. Verified on
fib_iterative_1M: Round 1 1.68s, Rounds 2-4 6.89s wall, aux build 2.91s
and aux commit 3.38s summed over 5 drivers.
The scheduler removed `instruments::snap("After aux build")` and
`snap("After aux commit")`. `bench_prover_scaling.sh` still parsed them,
printed them and ran heap-growth regressions on them, so two regression
guards were comparing nothing and dropping out without complaint.

Re-adding a snapshot inside a per-table task would be meaningless — with
k tables in flight there is no single moment at which aux build or aux
commit has finished — so remove the two rows and their `regress` calls,
with a NOTE recording why and pointing at the guards that still cover the
fused region ("After main commits" and "Peak heap").

Also repoint the timing regexes at the labels the report actually prints.
`Main expand_columns_to_lde` / `Aux expand_columns_to_lde` and
`Main commit (Merkle)` / `Aux commit (Merkle)` had not matched since the
labels gained their GPU/CPU suffixes, so t_main_lde, t_aux_lde,
t_main_merkle and t_aux_merkle silently printed blank. All four populate
again — checked by running the script's own awk over a real report.
Nothing functional. All of these described structure the scheduler
removed:

- `VramGate`'s rustdoc opened with the deleted `plan_table_chunks`'s doc
  comment ("Plan contiguous table chunks... Returns (start, end) half
  open ranges"), left behind and contiguous with `VramGate`'s own.
- `Lde`'s doc claimed all N tables' LDE columns are live simultaneously.
  Only the main LDEs still are — the Round 1 main commit is a phase-wide
  barrier. Each aux LDE is produced and consumed inside one fused task,
  so at most k coexist. That is a memory improvement the PR made and did
  not claim; state the real, asymmetric bound.
- A "Split into two passes for parallelism: Pass 1 ... Pass 2 ..." block
  sat two lines above the new comment saying the opposite.
- `table_parallelism`'s doc still gave only `num_cores / 3`. Document
  both arms, that `TABLE_PARALLELISM` overrides both, and that without
  the `parallel` feature it is hardcoded to 1.
- `run_debug_checks` said "called once after Phase C commits"; it now
  runs between two `run_admitted` passes. Document that, and the
  "each driver locks only its own index" contract its new
  `&[Mutex<AirTracePair>]` parameter relies on.
- `auto_storage::peak_bytes` described phase D and a "worst possible
  chunk assignment". With `heaviest_first` the top-k is the set actually
  admitted first, not a worst case. Also document that
  `table_parallelism()` is not only the prover's k: `decide` feeds it
  into the RAM-vs-Disk choice, so the cuda arm's `cores * 2 / 3` doubles
  that transient term and makes `Disk` likelier. The direction is safe
  (it over-estimates) but was undocumented.
- Remaining "Phase A/B/D" references, plus the "chunks of K" banner and
  the "Phase D's zip chain" handle comments.
These three had zero direct tests, and PR CI never exercises them
concurrently: `ubuntu-latest` has 2-4 vCPU so `cores / 3` floors to
k = 1, and `VramGate` is inert on non-cuda builds because
`vram_budget = u64::MAX` makes `acquire`'s admit condition always true,
so the condvar is never waited on.

They are free functions over `&[u64]` with no field, AIR or GPU
dependency, so a plain `#[cfg(test)] mod` pins them without a device:

- `heaviest_first` returns a permutation of `0..n`, descending by
  estimate, with ties broken by index (stable sort — so the admission
  order does not vary run to run).
- `run_admitted` fills every slot exactly once, including `order.len()
  == 0`, `workers > order.len()`, `workers == 1` and `workers == 0`.
- `VramGate` admits an over-budget request alone rather than deadlocking,
  never lets concurrent admissions push `used` past the budget, and wakes
  waiters on permit drop.
- A `u64::MAX` budget never blocks, including when the byte sum saturates.
- `run_admitted` seeds its drivers' span depth, which guards the
  regression fixed earlier in this branch. Reads the depth directly
  rather than the global span timeline, which other tests in this binary
  also write to.

Deterministic and fast: no sleeps as synchronization: channel rendezvous
for ordering, and `recv_timeout` only as a failure deadline so a
regression fails instead of hanging.
@ColoCarletti
ColoCarletti merged commit 8f91e7c into gpu-opt-table-scheduler Aug 3, 2026
13 checks passed
@ColoCarletti
ColoCarletti deleted the gpu-opt-877-review-fixes branch August 3, 2026 20:42
@MauroToscano MauroToscano changed the title fix(prover): repair the instruments span tree and timing report under the per-table scheduler fix(instruments): restore the rounds 2-4 phase span and make the prover report honest Aug 3, 2026
MauroToscano added a commit that referenced this pull request Aug 3, 2026
#893 also repointed four timing regexes in
`scripts/bench_prover_scaling.sh` that had gone stale earlier and
independently of this branch. That is unrelated churn in a script with no
Makefile target and no workflow referencing it, so it is reverted.

What stays removed: the two dead heap rows and their `regress` calls
(their `snap()` sources no longer exist and cannot be recreated with k
tables in flight) and the two aux timing rows, which follow the report.
The NOTE explaining why is kept.

Nothing here was failing silently, contrary to the original review note:
`regress` prints "(insufficient data)" for a missing key and `print_row`
prints "-".
MauroToscano added a commit that referenced this pull request Aug 3, 2026
Comments only. #893 rewrote these docs correctly on the substance —
"phase D" is a dangling label with no definition left on this branch, and
the `table_parallelism` coupling it documented is real
(`decide` -> `peak_bytes(.., table_parallelism())` -> `.take(k)`). Both
stay. But two clauses in it are wrong:

- "the `cuda` arm's `cores * 2 / 3` DOUBLES the transient term". It does
  not: the per-table terms are sorted descending and only the top `k` are
  summed, so each extra slot adds the next SMALLEST remaining table.
  Growth in `k` is sub-linear, not proportional.
- "with the scheduler's heaviest-first admission that top-k is also the
  set actually admitted first". Also false, and for a sharper reason than
  it looks: `transient_per_table` destructures `(rows, _, _, _)` and
  ignores column counts entirely, while `heaviest_first` orders by
  `estimate_table_vram_bytes`, which weighs `main_cols` and `aux_cols`.
  The two orderings diverge for equal-row tables of differing width —
  exactly the shape of this table set. It is a bound, not the admitted
  set, so the comment now says so.
MauroToscano added a commit that referenced this pull request Aug 3, 2026
Replaces the `VramGate` / `run_admitted` / `heaviest_first` unit tests
added in #893 (removed in the previous commit). Every assertion they made
was guaranteed by construction, already covered end to end, or
unreachable from the call sites: `heaviest_first` is `(0..n).collect()`
plus `sort_by_key`; a slot mixup in `run_admitted` is schedule
independent, so it trips one of the three
`.expect("run_admitted fills every slot")` sites or fails `multi_verify`
on every PR today; `order.len() == 0` and `workers > order.len()` cannot
happen, since `k` is `.max(1)`'d and `order` is always a full
permutation. The one property with teeth — an over-budget table admitted
alone — HANGS rather than fails if it regresses, which on an 8-10 minute
shard burns to the job timeout unless wrapped in a watchdog. That was
~50 lines of permanent maintenance against approximately zero risk.

The actual PR-time gap is that the scheduler never runs concurrently.
`table_parallelism()` defaults to `(cores / 3).max(1)` and every job in
this workflow is `runs-on: ubuntu-latest` with no larger-runner label, so
PR CI proves with exactly one driver thread; `VramGate` is additionally
inert on non-cuda builds, where `vram_budget` is `u64::MAX` and
`acquire`'s condition always holds.

`TABLE_PARALLELISM: 6` on shard 1 only is the smallest change that puts
several real table closures in flight at once. The other three shards
keep default-k coverage — the expression yields an empty string there,
which fails to parse and falls back to the default. `prover/Cargo.toml:8`
is `default = ["parallel"]`, so the env arm is the live one.

Not a substitute for GPU coverage: `gpu-tests.yml` on merge_group rents a
>=16-core RTX 5090, taking the cuda arm (`cores * 2 / 3`) with a finite
VRAM budget, so both the concurrent and blocking paths already run before
merge. This closes the PR-time gap only.
MauroToscano added a commit that referenced this pull request Aug 3, 2026
Replaces the `VramGate` / `run_admitted` / `heaviest_first` unit tests
added in #893 (removed in the previous commit). Every assertion they made
was guaranteed by construction, already covered end to end, or
unreachable from the call sites: `heaviest_first` is `(0..n).collect()`
plus `sort_by_key`; a slot mixup in `run_admitted` is schedule
independent, so it trips one of the three
`.expect("run_admitted fills every slot")` sites or fails `multi_verify`
on every PR today; `order.len() == 0` and `workers > order.len()` cannot
happen, since `k` is `.max(1)`'d and `order` is always a full
permutation. The one property with teeth — an over-budget table admitted
alone — HANGS rather than fails if it regresses, which on an 8-10 minute
shard burns to the job timeout unless wrapped in a watchdog. That was
~50 lines of permanent maintenance against approximately zero risk.

The actual PR-time gap is that the scheduler never runs concurrently.
`table_parallelism()` defaults to `(cores / 3).max(1)` and every job in
this workflow is `runs-on: ubuntu-latest` with no larger-runner label, so
PR CI proves with exactly one driver thread; `VramGate` is additionally
inert on non-cuda builds, where `vram_budget` is `u64::MAX` and
`acquire`'s condition always holds.

`TABLE_PARALLELISM: 6` on shard 1 only is the smallest change that puts
several real table closures in flight at once. The other three shards
keep default-k coverage — the expression yields an empty string there,
which fails to parse and falls back to the default. `prover/Cargo.toml:8`
is `default = ["parallel"]`, so the env arm is the live one.

Not a substitute for GPU coverage: `gpu-tests.yml` on merge_group rents a
>=16-core RTX 5090, taking the cuda arm (`cores * 2 / 3`) with a finite
VRAM budget, so both the concurrent and blocking paths already run before
merge. This closes the PR-time gap only.
ColoCarletti pushed a commit that referenced this pull request Aug 3, 2026
…timing report honest (#895)

* fix(instruments): restore the rounds 2-4 phase span instead of plumbing depth

Supersedes the approach in #893. Adversarial review showed the depth
field was never the defect.

`phase_table.py:121` takes its denominator from
`max(s["wall_ns"] for _, s in pathed)` — the longest span, not the root
of the ancestor stack — so depth-0 records never broke the "% of total"
column, and `scripts/profiling/README.md:77` was accurate all along.
`prover/src/continuation.rs` has also recorded spans from worker threads
since long before this branch (:1146, :1205, :1299, :1328, :1415), with
the comment at :1051-1053 saying so. Seeding worker depth was therefore
work that bought nothing, and it would have left overlapping siblings
looking like a clean tree — a subtler lie. Removed
(`instruments::current_depth` / `enter_depth` / `DepthGuard` and the
seeding in `run_admitted`).

The real defect is label collision under summing. `phase_table.py:129`
does `e["wall_ns"] += s["wall_ns"]`, so spans sharing a label are summed.
On origin/main `rounds_2to4` was ONE span around the chunk loop
(prover.rs:3503) and measured the phase; this branch made it one span per
table, so the row became the sum of N concurrent tables — up to k times
the real wall, able to exceed 100% — and no span measured the phase at
all. `r1_aux_build` and `r1_aux_commit` were phase spans on main too
(:3143, :3225).

So: reopen `rounds_2to4` on the calling thread around the whole fused
region, and rename the per-table spans `*_table` so a per-instance label
can never be summed into a phase row. This also repairs
`LAMBDA_VM_NSYS_CAPTURE_SPAN=rounds_2to4` (README.md:115), which with the
label on the per-table span had N driver threads calling
cuProfilerStart/Stop, the first to finish ending the capture.

The report follows, and is compile-coupled to the same change. #893 added
per-driver aux timers to fill the zeroed `aux_build` / `aux_commit`
buckets; the fused stages have no wall-clock phase of their own any more,
so reporting one invites exactly the misreading the label summing caused.
Both timers and both `MultiProveTiming` fields are gone. The report now
shows only the two phases that remain — "Round 1 (main trace commits)"
and "Rounds 2-4 (aux build+commit fused in)" — with the aux CPU-time rows
grouped under the fused phase behind headers stating they are summed over
tables. That still fixes what #893 set out to fix: no row prints a
fabricated 0.00s over live children, and "Round 1" no longer duplicates
its own child.

Verified on fib_iterative_1M: phase spans sum to their parent
(r1_prepass 0.148 + r1_main_commit 2.493 + rounds_2to4 8.943 = 11.584 vs
proving 11.585).

* revert: trim the bench script back to the minimum

#893 also repointed four timing regexes in
`scripts/bench_prover_scaling.sh` that had gone stale earlier and
independently of this branch. That is unrelated churn in a script with no
Makefile target and no workflow referencing it, so it is reverted.

What stays removed: the two dead heap rows and their `regress` calls
(their `snap()` sources no longer exist and cannot be recreated with k
tables in flight) and the two aux timing rows, which follow the report.
The NOTE explaining why is kept.

Nothing here was failing silently, contrary to the original review note:
`regress` prints "(insufficient data)" for a missing key and `print_row`
prints "-".

* test: drop the scheduler unit tests

* ci: force k > 1 on one prover shard so the scheduler runs concurrently

Replaces the `VramGate` / `run_admitted` / `heaviest_first` unit tests
added in #893 (removed in the previous commit). Every assertion they made
was guaranteed by construction, already covered end to end, or
unreachable from the call sites: `heaviest_first` is `(0..n).collect()`
plus `sort_by_key`; a slot mixup in `run_admitted` is schedule
independent, so it trips one of the three
`.expect("run_admitted fills every slot")` sites or fails `multi_verify`
on every PR today; `order.len() == 0` and `workers > order.len()` cannot
happen, since `k` is `.max(1)`'d and `order` is always a full
permutation. The one property with teeth — an over-budget table admitted
alone — HANGS rather than fails if it regresses, which on an 8-10 minute
shard burns to the job timeout unless wrapped in a watchdog. That was
~50 lines of permanent maintenance against approximately zero risk.

The actual PR-time gap is that the scheduler never runs concurrently.
`table_parallelism()` defaults to `(cores / 3).max(1)` and every job in
this workflow is `runs-on: ubuntu-latest` with no larger-runner label, so
PR CI proves with exactly one driver thread; `VramGate` is additionally
inert on non-cuda builds, where `vram_budget` is `u64::MAX` and
`acquire`'s condition always holds.

`TABLE_PARALLELISM: 6` on shard 1 only is the smallest change that puts
several real table closures in flight at once. The other three shards
keep default-k coverage — the expression yields an empty string there,
which fails to parse and falls back to the default. `prover/Cargo.toml:8`
is `default = ["parallel"]`, so the env arm is the live one.

Not a substitute for GPU coverage: `gpu-tests.yml` on merge_group rents a
>=16-core RTX 5090, taking the cuda arm (`cores * 2 / 3`) with a finite
VRAM budget, so both the concurrent and blocking paths already run before
merge. This closes the PR-time gap only.

* fix(bench): drop the row killed by the Round 1 relabel

"Round 1 (main trace commits)" is lowercase, so `/Main trace commits/`
stopped matching, and the row would have printed "-". It is also now
redundant: with the aux stages fused out of round 1, `t_main_commits`
and `t_round1` are the same number by construction.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants