The Pivot to Deficit-Based Dispatch: Replacing a Semaphore with a P-Controller in the GPU Pipeline

Introduction

In the course of optimizing a GPU-accelerated zero-knowledge proof system, a single edit to a dispatcher loop marked a fundamental shift in scheduling philosophy. Message [msg 3365] is deceptively brief — the assistant simply reports "Now update the dispatcher loop:" followed by a successful edit to /tmp/czk/extern/cuzk/cuzk-core/src/engine.rs. But this laconic message conceals the culmination of an extensive design deliberation, the replacement of a semaphore-based throttle with a proportional controller (P-controller), and the beginning of a weeks-long iterative refinement of GPU pipeline scheduling that would ultimately yield a sophisticated PI-controlled pacer with synthesis throughput caps. This article unpacks what that single edit meant, why it was necessary, the reasoning that led to it, and the assumptions — some incorrect — that shaped its implementation.

The Problem: Why Permits Were the Wrong Abstraction

The context for this message begins with the user's critique at [msg 3356]. The existing dispatch mechanism used a tokio::sync::Semaphore with N permits. The dispatcher would acquire a permit before starting a synthesis task, and the GPU finalizer would release a permit after completing a proof. This limited the total number of in-flight partitions — those being synthesized, waiting for GPU, or currently executing on GPU — to N.

The user identified a fundamental flaw in this design: it controlled the wrong variable. Limiting total in-flight partitions did not guarantee a stable pipeline. If synthesis was fast and GPU was slow, the queue of synthesized partitions waiting for GPU could grow unboundedly within the permit budget, causing memory pressure. Conversely, if GPU was fast and synthesis was slow, the GPU would starve even though permits were available. The semaphore could not distinguish between "work being synthesized" and "work waiting for GPU" — it treated both as consuming the same resource.

The user's proposed alternative was elegant: instead of limiting total in-flight work, target a specific number of partitions waiting for the GPU. When a GPU job finishes, check how many synthesized partitions are sitting in the GPU work queue. If that number exceeds the target (N, default 8), don't start new syntheses. If it's below the target, start enough new syntheses to fill the gap. This creates a self-regulating loop where the system naturally converges to the right number of concurrent synthesis jobs to maintain a stable GPU queue depth, minimizing memory pressure and preserving budget for PCE/SRS caching.

The Design Journey: From Semaphore to Notify

The assistant's reasoning in [msg 3357] and [msg 3361] reveals a careful exploration of the design space. The core insight was that the dispatcher needed to shift from a push model (acquire permit, dispatch work) to a pull model (GPU completion triggers dispatch of deficit). This required replacing the semaphore with a notification mechanism — specifically, tokio::sync::Notify.

The assistant considered several edge cases during the design:

In-flight synthesis tracking: When the dispatcher sends work to a synthesis worker, that work is "in-flight" and won't appear in the GPU queue until synthesis completes. If the dispatcher checks the deficit based only on items already in the queue, it could over-dispatch during ramp-up — sending N items, then immediately sending N more because none have reached the queue yet. The assistant initially considered an atomic counter for in-flight work, but ultimately decided that the budget semaphore and worker pool would naturally bound concurrency, and that the user's model of counting only waiting items was correct.
Notification semantics: The assistant chose Notify over a channel or event because only the dispatcher task waits on it. The notify_one() method stores one notification if the dispatcher hasn't called notified() yet, preventing lost wakeups. If multiple GPU completions occur before the dispatcher checks, only one notification is stored, but that's acceptable because the dispatcher re-evaluates the deficit on each loop iteration — it will keep dispatching until the deficit is filled.
Edge case — empty synthesis queue: If the synthesis queue is empty, the dispatcher should wait for new work regardless of the GPU queue depth. The dispatcher loop handles this by checking both conditions: wait for GPU completion if the queue is full enough, or wait for new work if the synthesis queue is empty.
Disabled throttle: If max_gpu_queue_depth is set to 0 (disabled), the dispatcher should fall back to the old behavior of dispatching as quickly as possible without deficit logic.

The Edit in Message 3365

Message [msg 3365] itself applies the second of three planned edits. The first edit ([msg 3364]) replaced the semaphore declaration with a Notify and updated the GPU finalizer to call notify_one() instead of add_permits(1). The third edit ([msg 3366]) would update the GPU worker clone paths.

The edit in [msg 3365] rewrites the dispatcher loop itself. The new loop structure is:

Check the current length of gpu_work_queue.
Calculate the deficit: target_queue_depth - gpu_work_queue.len().
If the deficit is positive, dispatch that many items from the synthesis queue (respecting budget and worker availability).
If the deficit is zero or negative (queue is at or above target), wait for a GPU completion notification before checking again.
If the synthesis queue is empty, wait for new work regardless. This is a textbook proportional controller: the control output (number of syntheses to dispatch) is proportional to the error (deficit between target and actual queue depth). The system measures the process variable (GPU queue length) on each GPU completion event and adjusts the control input (synthesis dispatch) to drive the error toward zero.

Assumptions and Incorrect Predictions

The implementation in [msg 3365] rested on several assumptions, some of which proved incorrect:

Assumption 1: The GPU queue length is a clean feedback signal. The assistant assumed that checking gpu_work_queue.len() would give an accurate, low-latency measurement of the system state. In practice, the deep synthesis pipeline introduced significant delay between dispatching a synthesis task and seeing its result appear in the GPU queue. This made the raw waiting count a noisy and delayed feedback signal, causing the P-controller to overshoot.

Assumption 2: Dispatching the full deficit in one burst is safe. The assistant designed the loop to dispatch deficit items each time a GPU completion occurs. This means that at startup, with a deficit of 8, the dispatcher would immediately dispatch 8 synthesis tasks. The assumption was that the budget semaphore and worker pool would naturally limit concurrency. However, the first deployment (cuzk-pctrl1) proved too aggressive, instantly filling all allocation slots. The user later requested a dampening factor, capping the burst size at max(1, min(3, deficit * 0.75)) to limit the expansion rate per GPU event.

Assumption 3: The system would converge to a steady state. The user's vision was that "eventually we'll just be spawning synthesis one by one in a stable manner." In practice, the combination of a noisy feedback signal (delayed queue depth) and a proportional controller with no integral term or damping meant the system oscillated rather than converging. This led to the eventual development of a PI-controlled pacer with EMA smoothing and synthesis throughput caps in the subsequent chunk (<msg id=3390+>).

The Broader Arc: From P-Controller to PI Pacer

The edit in [msg 3365] represents the first step in a months-long journey of control system refinement. The semaphore was replaced by a P-controller (this edit), which was then dampened with a burst cap (cuzk-pctrl2), then replaced by a PI-controlled pacer with EMA feed-forward (pacer1), and finally extended with a synthesis throughput cap and anti-windup to handle CPU-bound scenarios. Each iteration addressed a failure mode exposed by the previous design.

The pinned memory pool fix — the original reason for the GPU underutilization investigation — remained deployed and effective throughout. The dispatch scheduling was always a secondary optimization, but it proved surprisingly complex. The fundamental challenge was that the system had two coupled resources (CPU for synthesis, GPU for proving) with different dynamics, and controlling one based on measurements of the other required careful handling of delays, noise, and saturation.

Conclusion

Message [msg 3365] is a turning point in the GPU pipeline optimization effort. It marks the moment when the team abandoned the simple semaphore model and embraced control theory — even if they didn't yet know they were doing control theory. The P-controller implemented in this edit was the first step toward a sophisticated scheduling system that would eventually incorporate proportional-integral control, exponential moving averages, feed-forward rate estimation, and anti-windup mechanisms. The edit itself is small, but the thinking behind it — the careful analysis of feedback signals, the consideration of edge cases, the shift from push to pull dispatch — represents a deep understanding of the system dynamics and a willingness to redesign from first principles when the existing abstraction proved inadequate.