Phase 12's Split GPU Proving API: From Compilation to Memory Backpressure

Introduction

In the high-stakes world of Filecoin proof generation, where a single Groth16 proof consumes hundreds of gigabytes of memory and takes over thirty seconds to compute, every optimization is a battle against physical constraints. This article synthesizes the complete arc of Segment 30 of the cuzk SNARK proving engine optimization campaign — a multi-day debugging and optimization journey that began with a broken build, progressed through a successful 2.4% throughput improvement, discovered a critical use-after-free concurrency bug, encountered a hard memory wall at 668 GiB RSS, built the instrumentation needed to understand the problem, and ultimately resolved the tension between memory pressure and throughput through a nuanced understanding of pipeline backpressure.

The narrative of this segment follows a classic pattern in systems engineering: a successful architectural optimization (Phase 12's split GPU proving API, delivering 37.1 seconds per proof) exposes a hidden bottleneck (OOM at higher parallelism), which triggers a diagnostic investigation (building a global buffer tracker with atomic counters), which reveals a structural flaw (the semaphore permit released too early), which leads to a fix (holding the permit until channel delivery), which introduces a new problem (throughput regression to 39.9 seconds per proof), which requires a second-order optimization (increasing channel capacity to balance memory and throughput). Each step builds on the previous one, and the entire sequence is a masterclass in instrumentation-driven debugging and iterative refinement.

This article traces the threads that connect the compilation fixes, the concurrency bug, the memory investigation, and the final resolution. It is a story about how complex systems are built — not in a straight line from specification to delivery, but through a recursive cycle of hypothesis, experiment, failure, measurement, and refinement.

The State of Play: A Broken Build and a Plan

The segment opens with a comprehensive status document ([msg 2910]) that the assistant produces at a critical juncture. Phase 11 has been successfully committed, achieving 38.0 seconds per proof through memory-bandwidth interventions. Phase 12 — the split GPU proving API — is partially implemented but broken. The assistant's message is a masterclass in engineering transparency: it documents every file that has been modified, every function that exists, every compilation error, and every remaining task.

The core idea of Phase 12 is elegant in its simplicity. In the existing architecture, each GPU worker follows a cycle: acquire the GPU lock, run GPU kernels (~1.8 seconds), release the GPU lock, run b_g2_msm (~1.7 seconds), run the epilogue (~0 ms), and loop back for the next partition. The 1.7 seconds spent on b_g2_msm — a CPU-side multi-scalar multiplication on the G2 curve — blocks the GPU worker from picking up the next synthesized partition. If synthesis is producing partitions faster than the GPU workers can consume them, the pipeline backs up, and the GPU eventually starves.

The Phase 12 split API decouples these operations. The GPU worker calls gpu_prove_start, which runs the GPU kernels, releases the GPU lock, and spawns a background C++ thread (prep_msm_thread) to compute b_g2_msm. The worker immediately loops back to pick up the next partition. A separate Rust tokio task (the finalizer) later joins the background thread, runs the epilogue, and routes the result. The goal is to hide the 1.7-second b_g2_msm latency behind the GPU worker's next cycle.

But the status document reveals that the implementation is incomplete. The PendingGpuProof type alias doesn't exist. The helper functions process_partition_result and process_monolithic_result — which encapsulate ~300 lines of inline result-processing logic — haven't been extracted. The trait bounds on prove_start are mismatched. The continue statements inside async blocks are incorrect. The build is thoroughly broken.

This status document is not a confession of failure; it is a strategic pause. By writing down the exact state of every file, the assistant creates a navigable map of the remaining work. The subsequent messages in the segment will systematically address each item on this map.

The Compilation Gauntlet: Seven Errors and Their Fixes

The next 45 messages (approximately [msg 2916] through [msg 2955]) document a systematic triage of compilation errors. The assistant runs cargo build and iteratively fixes each error that emerges. The errors span multiple layers of the system:

Missing types and structs. The SynthesisCapacityHint struct is missing from the Rust code — it is needed by the C++ FFI but hasn't been defined yet. The assistant adds it. The PendingGpuProof type alias is missing from pipeline.rs — the assistant defines it as a tuple type (PendingProofHandle<Bls12>, Option<usize>, Instant).

Unused generic parameters. The start_groth16_proof FFI function has an unused generic parameter E that causes a compilation error. The assistant removes it, recognizing that the FFI boundary does not need the generic — the C++ code works with a concrete curve type.

Trait bound mismatches. The prove_start method's parameter params has a trait bound that does not match how it is used. The assistant changes it from params: &P (by reference) to params: P (by value), resolving the mismatch. This is a subtle fix — the trait bound P: Parameters<E> was being satisfied by &P in one context but P in another, and the compiler's error message required careful interpretation.

Async control flow bugs. The spawned finalizer task contains continue statements that were intended to exit the task early under certain conditions. But in Rust, continue inside an async block or closure does not work the same way as in a loop body — it attempts to continue the enclosing loop, which does not exist. The assistant replaces them with return, which properly exits the spawned task.

Each of these fixes is individually small, but collectively they represent a deep engagement with the Rust type system, the FFI boundary, and the async runtime. The assistant is not just making the code compile — it is ensuring that the type-level invariants are correct, that ownership is properly managed across the language boundary, and that the async control flow matches the intended execution model.

The moment of clean compilation arrives at [msg 2955], and the assistant's message reads simply: "Build succeeded. No errors." After dozens of messages of debugging, the code finally compiles. But as the assistant knows, compilation is only the first gate. Runtime correctness is a separate, more demanding test.

The Use-After-Free: A Bug Within a Bug

With a clean build achieved, the assistant launches the Phase 12 benchmark at [msg 2961]. The configuration matches the Phase 11 baseline: gw=2 (two GPU workers), pw=10 (ten partition workers), gt=32 (32 GPU threads), j=15 (15 concurrent jobs). The daemon starts, and the benchmark runs 20 proofs.

The result is 37.1 seconds per proof — a 2.4% improvement over the Phase 11 baseline of 38.0 seconds. The split API works. The b_g2_msm offloading is delivering the expected throughput gain.

But while analyzing the benchmark results, the assistant makes a discovery that changes the trajectory of the debugging session. At [msg 3011], while tracing whether Rust-owned memory must remain alive during the background b_g2_msm thread, the assistant realizes that the C++ provers array itself — a stack-local variable in generate_groth16_proofs_start_c — is captured by reference in the prep_msm_thread lambda.

The lambda capture [&, num_circuits] captures all automatic variables by reference. The provers parameter — a C-style array that decays to a stack pointer — is captured by reference. When generate_groth16_proofs_start_c returns, that stack variable is destroyed. The background thread continues running b_g2_msm, reading through a dangling reference. This is textbook undefined behavior.

The assistant's analysis is meticulous. It traces through the C++ code with grep and awk to identify every reference to provers inside the thread lambdas. It distinguishes between references that are safe (the GPU thread, which runs inside a lock that is joined before function return) and references that are unsafe (the prep_msm_thread, which runs after the function returns). It traces the Rust FFI chain in lib.rs to confirm the full picture of how provers flows from Rust through the FFI boundary into C++.

The fix, implemented across [msg 3017] through [msg 3034], is to copy the provers array into the heap-allocated groth16_pending_proof struct as provers_owned — a std::vector<Assignment<fr_t>> that lives on the heap and outlives the function call. The background thread references provers_owned instead of the stack-allocated provers. This is a small change in terms of lines of code, but it represents a fundamental understanding of C++ lambda capture semantics, stack lifetime, and the ownership model required for safe concurrency across the Rust/C++ boundary.

The assistant initially wonders whether this use-after-free bug might be causing the OOM — perhaps the undefined behavior is corrupting heap metadata and preventing proper deallocation. But after fixing the bug and re-running the benchmark at [msg 3043], the OOM persists. The UB fix was necessary for correctness, but it was not the cause of the memory pressure. The hypothesis is cleanly rejected, and the assistant pivots back to structural analysis.

The Memory Wall: Probing the Ceiling

The natural next step after the successful 37.1-second benchmark is to increase parallelism. If pw=10 works, perhaps pw=12 or pw=15 will yield even better throughput by reducing queueing. The assistant tries this at [msg 2974] and beyond, and the results are dramatic — but not in the way expected.

With pw=12, the daemon is killed by the OOM (Out of Memory) killer. The assistant, having set up an RSS monitoring loop, collects the trace and discovers the peak: 668 GiB on a system with 755 GiB total ([msg 3044]). The five highest RSS measurements are 653.1, 655.3, 665.5, 666.4, and 668.3 GiB. With only ~87 GiB of headroom, the system simply cannot sustain the additional memory pressure.

The user's response at [msg 2990] — "It's not 400GB tho, something is leaking somewhere" — pushes back against the assistant's initial hypothesis that the OOM is simply a capacity issue. The user suspects a memory leak. The assistant, despite having initial evidence that the memory returns to baseline after the benchmark completes (RSS drops to 71 GiB), takes the user's skepticism seriously and begins a deeper investigation.

The assistant's first attempt to address the memory pressure is to look for memory that can be freed earlier. The PendingProofHandle — the heap-allocated struct that bridges prove_start and prove_finish — holds the massive a, b, c NTT evaluation vectors (~12 GiB per partition). By tracing data dependencies through the C++ prep_msm_thread with precise grep commands, the assistant confirms that these vectors are only accessed by the GPU kernel region, which completes before prove_start returns. The prep_msm_thread only uses the b vector's G2 representation, not the original NTT evaluation vectors.

This is the critical insight: the 12 GiB of NTT evaluation vectors can be freed immediately after prove_start returns, without waiting for prove_finish. The assistant implements this early deallocation by dropping the Rust references to these vectors at the appropriate point in the pipeline. But the early deallocation, while a valid optimization, only saves approximately 18 GiB — far short of the ~300 GiB gap between pw=10 and pw=12 memory usage. The OOM at pw=12 persists.

The Pivot: Building a Global Buffer Tracker

The user's question at [msg 3076] — "Can we count and report number of each large buffer in flight and maybe the stage?" — triggers a critical instrumentation effort. The assistant builds a global buffer tracker with atomic counters (buf_synth_start, buf_abc_freed, buf_dealloc_done) integrated across the pipeline and engine modules.

The design choices embedded in the buffer tracker reveal the assistant's mental model of the pipeline:

The Discovery: 28 Provers and the Semaphore That Didn't

When the assistant runs the instrumented benchmark at pw=12 and greps the buffer log for peak values, the data is devastating:

BUFFERS[synth_done]: synth=3 provers=28 aux=97 shells=69 pending=0 est=727GiB
BUFFERS[synth_done]: synth=2 provers=28 aux=98 shells=70 pending=0 est=732GiB
BUFFERS[synth_done]: synth=1 provers=27 aux=99 shells=72 pending=0 est=724GiB

provers=28 — twenty-eight ProvingAssignment sets alive simultaneously, each holding ~12 GiB of a/b/c evaluation vectors. That is ~336 GiB just for these structures. With partition_workers=12, the theoretical maximum should have been 12. The fact that 28 are alive means something is fundamentally wrong with the concurrency control.

The assistant traces the problem to a single line of code in engine.rs:

let _permit = permit; // held until synth complete

This line is inside a tokio::task::spawn_blocking closure. The permit is indeed held until synthesis completes — but it is dropped inside the spawn_blocking closure. After the closure returns, the code continues with an asynchronous synth_tx.send(job).await — but the permit is already released.

The consequence is devastating: as soon as a partition finishes synthesis, the semaphore permit is returned to the pool, allowing another synthesis task to start. But the just-completed partition's SynthesizedJob — holding ~16 GiB of data — is still sitting in memory, blocked on the synth_tx.send() call because the GPU channel has capacity for only one item. The semaphore was supposed to limit the number of in-flight partitions, but because it releases before the data is delivered to the next pipeline stage, it effectively only limits the number of actively synthesizing partitions — not the number of synthesized-but-not-yet-GPU-processed partitions.

This is a classic pitfall in pipeline design: the semaphore's scope is too narrow. It controls the entry to the synthesis stage but not the exit from it. The pipeline can have up to pw partitions actively synthesizing, plus an unbounded number of completed partitions waiting to be sent through the channel. With pw=12 and a GPU that processes ~3 partitions in the time it takes 12 to synthesize, the backlog grows at roughly 9 partitions per cycle, quickly reaching 28 and consuming 336 GiB of memory just for the a/b/c vectors.

The Semaphore Fix: Holding the Permit

The fix is conceptually simple but structurally significant: move the permit out of the spawn_blocking closure so that it remains alive until after the synth_tx.send().await completes. This changes the semaphore from limiting "number of partitions being synthesized" to limiting "number of partitions between start-of-synthesis and acceptance-into-GPU-channel."

The assistant applies the edit with surgical precision, reasoning through Rust's ownership semantics to ensure the permit will not be dropped prematurely. The permit — an OwnedSemaphorePermit — is acquired at lines 1125-1131 of engine.rs. It is then moved into a spawn_blocking(move || { let _permit = permit; ... }) closure. By removing it from the closure and keeping it in the outer tokio::spawn(async move { ... }) block, the permit's lifetime extends across both the CPU-bound synthesis and the channel delivery.

The result is dramatic: peak RSS drops from 668 GiB to 294.7 GiB, and pw=12 runs without OOM for the first time. The buffer tracker confirms the fix: provers=12 max — exactly the pw=12 limit.

The Trade-Off Revealed: Throughput Regression

But the very next benchmark reveals the cost. Throughput regresses from 37.1 seconds to 39.9 seconds per proof — a 7.5% slowdown. Even worse, when the assistant tests pw=10 with the same semaphore fix, throughput drops to 40.5 seconds per proof.

The reasoning is clear: "The semaphore holding through channel send means synthesis is now throttled by GPU throughput." The semaphore, by holding the permit through the entire channel delivery window, is serializing synthesis and GPU consumption. A partition cannot begin synthesis until the previous partition's synthesized output has been fully accepted by the channel. This eliminates the natural overlap between CPU-bound synthesis and GPU-bound proving, effectively turning the pipeline back into a sequential process.

The assistant now faces a fundamental trade-off: the semaphore fix solves the memory crisis but introduces a throughput regression that wipes out the Phase 12 gains and more. The system is stable but slower than before the optimization.

The Second Pivot: Channel Capacity Instead of Semaphore

The assistant's response to this trade-off is methodical and scientific. Rather than accepting the regression or reverting the fix entirely, the assistant explores the design space with the clarity of empirical data.

The key insight is that the problem is not the semaphore itself but the channel capacity. With synthesis_lookahead=1 (the default), the GPU channel can buffer at most one completed job. When a synthesis task finishes and finds the channel full, it blocks on send() while still holding its ~16 GiB of data. The semaphore fix solves this by preventing new synthesis from starting until the channel has room — but it does so by eliminating overlap entirely.

The assistant considers three approaches:

  1. Accept the pw=10 constraint — declare victory at the working configuration and move on.
  2. Add a separate queue-depth semaphore — create two independent throttles, one for CPU pressure and one for memory pressure. But that is complex.
  3. Increase the channel capacity from 1 to partition_workers — a one-line configuration change that would allow up to pw completed jobs to be buffered in the channel without blocking. The assistant chooses option 3. The reasoning is elegant: by setting the channel capacity equal to partition_workers, up to pw completed jobs can be buffered in the channel without blocking. When the channel is full, the (pw+1)th completion will block on send(), naturally capping memory at approximately 2×pw synthesis outputs — pw actively being synthesized plus pw waiting in the channel. The channel itself becomes the backpressure mechanism, and the semaphore can continue to release early, preserving synthesis overlap with GPU work. This approach separates the concerns: the semaphore controls CPU pressure (how many tasks can synthesize concurrently), while the channel capacity controls memory pressure (how many completed jobs can be buffered). Both are bounded, and neither introduces new synchronization primitives.

The Commit: Sealing Phase 12 into History

Despite the memory ceiling, Phase 12 is a success. The split API works, the benchmark shows a measurable improvement, and a critical concurrency bug has been fixed. At [msg 3051], the assistant commits the Phase 12 implementation to the feat/cuzk branch with a detailed changelog:

feat(cuzk): Phase 12 — split (async) GPU proving API

Decouple b_g2_msm CPU computation from the GPU worker loop so the GPU worker
can pick up the next synthesized partition ~1.7s faster.

Key changes:
- C++: generate_groth16_proofs_start_c / finalize_groth16_proof_c split
- C++: prep_msm_thread runs b_g2_msm in background
- C++: groth16_pending_proof struct holds all shared state
- Rust: PendingProofHandle<E> in bellperson
- Rust: PendingGpuProof type alias in pipeline.rs
- Rust: gpu_prove_start / finish_pending_proof in engine.rs
- Fix use-after-free: prep_msm_thread now reads provers_owned (heap copy)
- Fix compilation errors: missing structs, unused generics, trait bounds
- Benchmark: 37.1s/proof (2.4% improvement over Phase 11 baseline of 38.0s)

The commit adds 1,275 lines and deletes 439 across 6 files. It is the culmination of the entire segment's work.

The todo list at [msg 3053] completes the narrative. Four items are marked completed: the compilation fixes, the pw=10 benchmark (37.1 seconds per proof), the pw=12/15 OOM diagnosis (memory capacity, not leak), and the use-after-free fix. The todo list is not just a status update — it is a compressed narrative of the entire Phase 12 journey, from broken build to successful commit.

Themes That Bind the Segment

Several themes recur throughout this segment, connecting the compilation fixes, the concurrency bug, and the memory investigation into a coherent narrative.

The Primacy of Measurement

The assistant's debugging methodology is grounded in empirical measurement. When the OOM strikes, the assistant does not guess at the cause — it sets up an RSS monitoring loop, collects data, and analyzes the trace. When the user suspects a leak, the assistant builds a global buffer tracker with atomic counters to get real-time visibility into memory state. When the use-after-free is discovered, the assistant traces every reference with grep to confirm the analysis. Every hypothesis is tested against data.

The Fragility of Cross-Language Boundaries

The Phase 12 split API spans three language boundaries: Rust async code (engine.rs, pipeline.rs), Rust FFI declarations (lib.rs, supraseal.rs), and C++ CUDA kernels (groth16_cuda.cu). Each boundary introduces its own failure modes. The Rust type system catches some errors at compile time (missing types, trait bound mismatches), but the most dangerous bugs — the use-after-free, the memory accumulation — are invisible to the compiler. They require runtime observation and careful reasoning about lifetimes.

The Nonlinearity of Memory Scaling

The assistant's mental model of memory scaling is linear: 2 more workers = 2 more partitions × ~16 GiB = ~32 GiB more memory. The actual increase from pw=10 to pw=12 is 301 GiB — nearly 10× the expected value. This nonlinearity reveals complex interactions in the pipeline: faster synthesis (more workers) causes more proofs to be parsed from the queue, more PendingProofHandle objects to accumulate, and more partitions to be queued waiting for the GPU channel. The semaphore, designed to limit concurrency, releases too early, allowing the queue to grow unboundedly.

The Semaphore Scope Fallacy

The most important technical lesson is that a semaphore's scope must match the resource it is protecting. The partition semaphore was intended to limit memory usage by capping concurrent synthesis. But because the permit was released before the synthesized data was delivered to the next pipeline stage, the semaphore only limited active synthesis, not in-flight data. The scope was too narrow. This is a general principle: when using semaphores to bound concurrent work in a pipeline, the permit must cover the entire critical section where the resource is held, including any asynchronous handoff to the next stage.

The Memory-Throughput Trade-Off

The segment vividly demonstrates that in pipelined systems, memory pressure and throughput are often inversely related. Buffering completed work allows the pipeline to run ahead, improving throughput by keeping all stages busy. But buffering consumes memory. The art of pipeline design is finding the right balance — enough buffering to absorb variability and maintain throughput, but not so much that memory becomes the bottleneck.

The Power of a Single Configuration Change

The final solution — increasing channel capacity from 1 to partition_workers — is a one-line change that reuses existing infrastructure. It does not introduce new synchronization primitives, new code paths, or new failure modes. It simply tunes an existing parameter to match the system's actual concurrency model. This is the hallmark of a well-designed system: the communication primitive doubles as a resource control primitive.

Iterative Refinement

The segment follows a classic optimization cycle: measure → hypothesize → implement → measure → analyze → repeat. Each iteration reveals new information that refines the assistant's mental model. The early deallocation fix is correct but insufficient. The semaphore fix is correct but has side effects. The channel capacity increase is the third iteration, building on the knowledge gained from the first two. This is not a sign of failure — it is the normal pattern of systems optimization, where each attempt reveals more about the system's behavior.

The Broader Significance

This segment of work in the cuzk SNARK proving engine optimization is a masterclass in systems engineering under constraint. It begins with a successful architectural optimization (Phase 12's split GPU API), encounters a hard memory wall (OOM at pw=12), builds the instrumentation needed to understand the problem (the global buffer tracker), identifies a structural flaw (the semaphore permit released too early), applies a fix (holding the permit until channel delivery), discovers a trade-off (throughput regression), and iterates to a balanced solution (increasing channel capacity).

The final state of the system is not perfect — there is no such thing in high-performance computing. But it is understood. The assistant knows exactly where memory goes, exactly how the pipeline's throttles interact, and exactly what trade-offs are being made. The buffer tracker remains in the code, providing ongoing visibility. The channel capacity is tuned to match the system's concurrency model. And the semaphore now correctly bounds the resource it was designed to protect.

In the broader narrative of the cuzk optimization campaign, this segment represents the transition from Phase 12 (the split API) to the diagnostic and architectural work that enabled Phase 12 to actually function at scale. The 37.1-second per proof throughput target is still achievable — but only with the right backpressure configuration. And the lessons learned here — about instrumentation, semaphore scope, and the memory-throughput trade-off — will inform every subsequent optimization in the project.

Conclusion

The 144+ messages of this segment trace a complete engineering cycle: from a broken build and a comprehensive status document, through a systematic gauntlet of compilation fixes, to a successful benchmark, a critical concurrency bug discovery, a memory capacity diagnosis, a semaphore fix, a throughput regression, and finally a channel capacity optimization that balances the competing demands of memory and throughput.

The Phase 12 split GPU proving API is now committed. It delivers a 2.4% throughput improvement — 37.1 seconds per proof versus 38.0 seconds — while fixing a dangerous use-after-free bug that could have caused corrupted proofs or crashes in production. The memory ceiling at 668 GiB is documented and understood, and the backpressure fix ensures that the pipeline can operate at higher parallelism without OOM.

But the deeper story of this segment is about the engineering process itself. It is about how complex systems are built through iteration, measurement, and the willingness to confront failure. It is about the value of writing things down — the status document at [msg 2910] and the todo list at [msg 3053] bookend the segment, providing structure and clarity at the beginning and closure at the end. It is about the interplay between human intuition (the user's "something is leaking somewhere") and empirical data (the RSS trace, the buffer counters). And it is about the quiet satisfaction of a clean build, a working benchmark, and a commit that captures the accumulated understanding of dozens of debugging hours.

In the end, Phase 12 is not just a code change. It is a documented journey through the challenges of high-performance GPU proving — a journey that reveals as much about the system's architecture as about the engineering discipline required to improve it.

References

[1] From Compilation to Capacity: The Full Arc of Phase 12's Split GPU Proving API — The foundational Phase 12 chunk article covering compilation fixes, use-after-free bug, and benchmark results.

[2] The Memory Wall and the Backpressure Fix: How Instrumentation Unlocked the GPU Proving Pipeline — The second chunk article covering the buffer tracker, semaphore fix, throughput regression, and channel capacity optimization.