The Semaphore That Saved the GPU: Reactive Backpressure in a Zero-Knowledge Proving Pipeline

On its surface, message 3319 of this opencode session appears unremarkable: a single-line confirmation that a code edit was applied. [edit] /tmp/czk/extern/cuzk/cuzk-core/src/engine.rs Edit applied successfully. But this terse output marks the precise moment when a fundamental architectural flaw in a GPU proving pipeline was corrected — the replacement of a poll-based throttle with a semaphore-based reactive dispatch mechanism. The edit itself was the culmination of a diagnostic chain that traced GPU underutilization through three interrelated failure modes: a dispatch burst problem, pinned memory pool thrashing, and cudaHostAlloc serialization blocking GPU activity. Understanding why this single edit was the turning point requires reconstructing the reasoning that led to it.

The Problem: A Thundering Herd of Syntheses

The context for this message begins with the user's observation in [msg 3310]: when the GPU queue depth dropped below its threshold of 8, all ~20 pending synthesis jobs would dispatch simultaneously. This burst of activity triggered a cascade of cudaHostAlloc calls — CUDA's pinned memory allocation, which requires GPU driver synchronization — that effectively stalled the GPU. The user noted that "when all 20+ synths run there is almost zero GPU activity," and suggested a reactive modulation scheme: "start a job only after a gpu consumed a slot."

The assistant's response in [msg 3311] synthesized the user's observations into three distinct but interconnected issues. First, the dispatch burst: the poll-based throttle checked every 250ms whether the GPU queue had room, and when it did, it released all waiting syntheses at once. Second, pinned pool thrashing: the assistant suspected buffers were being allocated and freed without reuse, forcing constant cudaHostAlloc calls. Third, cudaHostAlloc stalls: concurrent pinned allocations serialized through the CUDA driver, blocking GPU kernel execution.

The assistant immediately recognized that fixing the dispatch burst would also fix the other two problems: "if we only dispatch one synthesis per GPU completion, pinned allocations trickle in instead of bursting."

The Diagnostic Evidence

Before implementing the fix, the assistant gathered quantitative evidence. In [msg 3312], a log query revealed the pinned pool's catastrophic reuse ratio:

474 new allocations
447 checkins (buffers returned to pool)
12 reuses This was the smoking gun. The pool was allocating nearly 500 pinned buffers (totaling over 1 TiB of cudaHostAlloc calls) but only reusing them 12 times. The checkins were happening — buffers were being returned — but they weren't available when new syntheses requested them. The assistant's reasoning in [msg 3313] identified the root cause: the burst dispatch pattern meant all syntheses requested buffers simultaneously, before any GPU partition had finished and returned its buffers to the pool. By the time a buffer was checked in, no synthesis worker was waiting for it — they had already allocated fresh. This insight was critical. The pinned pool itself was not buggy; the dispatch pattern was preventing it from working. The fix had to change when syntheses were started, not how the pool operated.

The Semaphore Design

The assistant's reasoning in [msg 3311] and [msg 3313] converged on a clean solution: a tokio Semaphore initialized to max_gpu_queue_depth (8). The mechanism would work as follows:

Acquire: Before dispatching a synthesis job, the dispatcher acquires a permit from the semaphore. If no permits are available (i.e., the GPU queue is full), the dispatcher blocks — exactly one synthesis per permit.
Forget: The permit is intentionally forgotten (not dropped), so it remains consumed even after synthesis completes. This decouples the permit lifecycle from Rust's normal drop semantics.
Release: When the GPU finalizer finishes processing a partition — after gpu_prove_finish completes and the reservation is dropped — it calls semaphore.add_permits(1) to release a permit back. This signals the dispatcher that exactly one slot has opened.
Self-modulation: Each GPU completion triggers exactly one new dispatch. If two partitions finish simultaneously, two permits are released, and two new syntheses start. The system naturally matches the GPU's consumption rate. This design directly implements the user's suggestion: "if we went from N → N-1, start one job, if from N → N-2 start two." The semaphore's internal counter tracks the available queue depth precisely, and the acquire/release pattern creates a 1:1 correspondence between GPU completions and new dispatches.

The Edit Itself

Message 3319 is the application of this design to engine.rs. While the message text does not show the diff, the preceding messages reveal the edit locations. In [msg 3318], the assistant identified that the semaphore should be created alongside the existing work queues (synth_work_queue and gpu_work_queue) at approximately line 1175 of engine.rs. The permit release point was identified at line 2796, where the GPU reservation is dropped after gpu_prove_finish — the natural place to also release the semaphore permit.

The edit touched three areas of the codebase:

Semaphore creation: Initializing an Arc<tokio::sync::Semaphore> with max_gpu_queue_depth permits, alongside the existing priority work queues.
Dispatcher logic: Replacing the polling loop that checked gpu_work_queue.len() < max_depth with a semaphore.acquire().await call. The permit is acquired but intentionally forgotten to keep it consumed.
GPU finalizer: Adding semaphore.add_permits(1) after the reservation is dropped, ensuring the permit is released only after the GPU has fully finished processing the partition.

Assumptions and Input Knowledge

The assistant made several assumptions that proved correct. The key assumption was that the pinned pool's low reuse ratio was caused by the dispatch timing mismatch — not by a bug in the pool's checkin/checkout logic. This was validated by the log data showing 447 checkins occurring but only 12 reuses, which strongly suggested temporal misalignment rather than a code defect. The assistant also assumed that cudaHostAlloc serialization was a consequence of concurrent calls, not a fundamental CUDA driver limitation — an assumption validated when the serialized dispatch pattern eliminated the GPU stalls.

The input knowledge required to understand this message is substantial. One must understand CUDA's pinned memory model (cudaHostAlloc creates page-locked host memory that enables direct GPU DMA but requires driver synchronization), the tokio async runtime and its Semaphore primitive, the architecture of the CuZK proving pipeline (synthesis → GPU queue → GPU worker → finalizer), and the budget system that tracks memory reservations. The assistant also needed familiarity with the existing poll-based throttle implementation and the PriorityWorkQueue data structure.

Output Knowledge Created

This message produced several forms of knowledge. Most concretely, it created a working implementation of reactive backpressure in a high-performance GPU proving pipeline. The design pattern — using a semaphore to create 1:1 modulation between GPU completions and synthesis dispatches — is a reusable solution for any pipeline where a fast producer threatens to overwhelm a slower consumer.

The edit also validated a design principle: when a resource pool (like the pinned memory pool) shows poor reuse, the problem may not be in the pool itself but in the consumption pattern. The 12:474 reuse ratio was not a bug in checkin() or checkout() — it was a symptom of burst dispatch overwhelming the temporal buffer lifecycle.

The Results

The subsequent messages tell the story of the fix's impact. In [msg 3337], after deploying the pinned4 binary, the metrics showed a transformation:

| Metric | Before (pinned3) | After (pinned4) | |---|---|---| | ntt_kernels H2D transfer | 1,300–12,000 ms | 0 ms | | Total per-partition GPU time | 2,000–12,700 ms | 934–994 ms | | Pinned pool allocations | 474 | 24 | | Pinned pool reuses | 12 | 48 | | Budget headroom | 5 GiB | 288 GiB |

The ntt_kernels=0ms result was particularly striking — the H2D transfer that had dominated GPU time was now so fast it rounded to zero. The pinned pool reuse ratio flipped from 12:474 (2.5% reuse) to 48:24 (200% reuse — more reuses than allocations). Budget headroom ballooned from 5 GiB to 288 GiB, indicating that the pipeline was no longer holding massive amounts of memory waiting for GPU processing.

Conclusion

Message 3319 is a case study in how a small, precisely targeted code change can resolve a complex performance problem. The edit itself was minimal — replacing a polling loop with a semaphore acquire, adding a permit release in the GPU finalizer — but the reasoning behind it required tracing a chain of causality from dispatch bursts to pinned pool thrashing to GPU stalls. The semaphore-based reactive dispatch pattern that emerged is a textbook application of backpressure in a producer-consumer pipeline, and its success validates the principle that controlling when work starts can be more impactful than optimizing how work executes.