The compiled
inference runtime

Evidence key: the first figure is measured; the other two are architectural properties. Cold-start and multi-model gains remain evaluation targets, not published benchmark claims.

From checkpoint to artifact

Most serving stacks repeatedly decide, dispatch, and synchronize work while a request is already waiting. Plow's premise is that if the model, target, and operating profile are known before deployment, the runtime should receive a prepared execution artifact rather than reconstructing a plan for every process or request.

The system therefore splits into two phases. Before deployment, the compiler imports the model, considers equivalent graph forms, chooses a target-specific plan, validates it against a reference, and packages the result. At request time, plowrt loads the artifact and executes it. The important boundary is when the work happens.

What the compiler decides before you deploy

The compile phase reads a HuggingFace checkpoint directory — config, safetensors shards, tokenizer — and lowers it to a shape-inferred operator graph. Every tensor's dimensions are known from that point on, which is what makes the rest of the pipeline possible: a tile graph is assembled, each matrix multiply and attention block is cut into tiles whose shapes are chosen against a hardware cost model, and the tiles are placed with L2-partition-aware scheduling. On chiplet accelerators like CDNA4 each die owns a slice of L2, so tiles and their traffic are mapped to stay resident in a local partition rather than crossing dies.

The scheduler then does the part that has no equivalent in a launch-based runtime. It assigns every dependency in that graph to an atomic counter — producers increment, a consumer proceeds when the count reaches its threshold — and it picks the cheapest scope each counter can legally use: a shared-memory barrier when producer and consumer land on the same SM, a device-scope atomic when they share a GPU, a system-scope atomic only when they do not. It assigns on-chip memory as pages with a lifetime, hoists loads earlier to overlap with prior compute, and resolves every address as an offset into one arena, so there is no allocator on the request path. The emitter writes the result as the packet stream, together with a ladder of compiled buckets — one per (phase, batch, sequence) rung — that the runtime rounds each live shape up into.

There is also an egglog equality-saturation stage: nineteen shape-preserving fusion rules over one e-graph, saturated and extracted by cost, each rule carrying a machine-checked soundness theorem. We should be precise about its status. The search runs and reports what it finds, but it is advisory today — the fusions that reach a packet are the ones the emitter implements directly, and when we measured what routing the search's output through the emitter would buy on a tuned decode path, the answer was below the step-to-step noise. It is a real optimizer on a real e-graph; it is not currently what makes plow fast, and saying otherwise would be easy and wrong.

Every stage above is gated by a Lean oracle: six checkpoints (A–F) covering rule soundness, tile partition and cost, on-chip memory fit, the counter protocol, the wire round-trip, and allocation safety. That deserves more than a sentence — what the proofs actually prove is a section of its own below.

Every phase of a request, in one plan

A request is not one workload. Reading the prompt saturates the arithmetic units; generating each subsequent token barely uses them and is limited instead by how fast weights can be pulled from memory. Serving stacks usually paper over that with one dynamic scheduler that handles both. Plow compiles them as separate buckets of the same bundle, so each phase gets a plan shaped for what actually limits it, and the runtime's job is to pick the rung of the ladder that covers the live shape.

Prefill — chunked, packed, and priced

Long prompts are processed in chunks so that a single request cannot monopolise the device, and the chunks of several waiting requests are packed into one launch under a token budget. The chunk size is not a constant we picked. A launch is not free — it re-reads every layer's weights from memory and pays grid and counter setup — so the compiler prices one launch in padded-row equivalents, measured by regressing time-to-first-token over a prompt-length sweep, and the runtime chooses the chunking that minimises total cost rather than the one that minimises padding. The prompt's keys and values are written straight into the cache at their destination row as part of the attention packet; there is no separate copy pass.

Prefill is also where our honest gap is. It is the phase we have tuned least, and it is first in the auto-tuner's queue. We publish decode results today and will publish prefill results when they have been through the same correctness-gated evaluation, not before.

Decode — one dispatch, and the host is not consulted

A decode step is a single dispatch. Inside it, a persistent kernel walks a few hundred counter-gated packets: the bandwidth-bound linear layers, attention split across workers with a merge step so that a batch of one still occupies the whole GPU, the router and expert arithmetic if the model is a mixture of experts, and the output projection. Then it samples. Greedy sampling is a reduction fused into the output-projection packet; temperature, top-k, top-p and min-p run in a device sampler with per-row parameters, so a batch can mix greedy and stochastic requests. Either way the chosen token id is written on the device directly into the tensor the next step's embedding lookup reads. An optional multi-step mode advances a fixed quantum of tokens with one host round trip instead of one per token.

The key-value cache is a paged block pool with per-request page tables, in the manner PagedAttention established. Plow stores it head-major, so a shared prompt prefix is not one block but a set of strided runs at the same offset in every head's slot — which is what its prefix cache indexes. Above that, a shared prefix can be held once in physical memory and multi-mapped into each sharing sequence's virtual window, so the second and later users of a long shared prompt cost address space rather than gigabytes. Cache precision is bf16 by default; an fp8 key-value mode exists, is opt-in, and is lossy — we say so rather than quoting the memory saving alone.

The serving loop around them

Each model has a dispatcher holding a slot table sized to the largest compiled batch. Between decode ticks it admits new arrivals into free slots, so a request that arrives mid-generation gets its first token without waiting for the in-flight ones to finish. Tokens stream out as incremental detokenized deltas, and a client that disconnects frees its slot on the next tick.

Admission control is where being static pays off in an unexpected place. Queueing theory needs a service-time distribution, and a dynamic runtime can only estimate one by observing itself. Plow knows the packet count and the byte cost of a decode step before any request arrives, so the service time is a lookup — and because a compiled step is deterministic to well under a percent step-to-step on the model and card we measured it on, the arrival model that applies is the deterministic-service one rather than the exponential-service one usually assumed. The batch-formation window becomes the minimiser of a latency function instead of a tuned constant. That is the mechanism behind the predictable-tail claim, and it is a design property we can point at rather than a number we would like to be true.

What the plan has to cover

"Compile the model" is only interesting if the compiler covers the shapes models actually take. Modern architectures are not uniform stacks of the same attention block, and a compiled runtime has to express the variation without a special case per checkpoint.

Where each model family actually stands

Coverage claims are easy to inflate, so here is the ladder we hold ourselves to. Served and measured on real accelerators: Gemma-4 (12B and 31B dense, 26B-A4B mixture-of-experts), Qwen3, Llama-3.1, and Kimi-K3 — a hybrid that mixes latent attention with linear-attention layers and 4-bit experts, brought up and measured across eight CDNA4 accelerators. Compiles a block at a time, not yet a served model: other latent-attention checkpoints of the DeepSeek lineage, and Mamba-2 hybrids, which have a device operation but no model-level validation.

Graph only, with no device path: vision towers and image-diffusion transformers. Their graphs build and shape-infer, and several of the fusion rules exist specifically for them — adaptive layer-norm modulation, gated residuals, group-norm-and-activation chains. But there is no device operation for convolution or group normalisation, no image decoder, and no diffusion sampler, so nothing about them runs. Design only: speech recognition and synthesis. The multi-stage pipeline abstraction that would carry an encoder into a decoder on-device exists in the runtime and is not yet reachable from the serving loop. We describe those as where the architecture is going, and we do not describe them as features.

What the proofs actually prove

GPU coordination bugs have a specific and unpleasant character. A counter with the wrong threshold does not throw; it produces slightly wrong tokens, or it hangs, and which one it does depends on timing. Unit tests do not find that class, because the failing interleaving is the one the test machine did not happen to run. So plow carries a Lean 4 library that proves the properties instead of sampling them.

It works by proving universal theorems once and applying them per compilation. For each check the compiler serialises a payload — the counter graph with its producers, thresholds and scopes; the tile shapes; the on-chip memory timeline; the encoded packet bytes; the address map — and invokes a separate Lean binary that checks this instance's preconditions and returns a certificate naming the theorems it applied. Running it as its own process rather than a linked library means a prover crash cannot corrupt a compile, and it means the checks can be switched on and off. They are opt-in at the command line and always on in continuous integration. There is a deliberately broken schedule in the test suite whose job is to be rejected; a verifier that only ever says yes is not a verifier.

The interesting part is not the first column of the table below. Proving a compiler's output legal is the expected use of a theorem prover. The second column is the one that changes how the compiler is written: a proof that an optimisation is safe is a licence to take it without re-arguing it per model, and a proof that an optimisation cannot pay is permission to stop working on it. Both kinds are in the library, and the second kind has saved us more engineering time than the first.

Counters: proving a dataflow, then pruning it

The verification side is the part you would expect. A counter protocol is well-formed when every dependency edge in the task graph is covered by some counter whose threshold is exactly the number of producers assigned to it, and the relation those gates induce is acyclic. From that, deadlock-freedom is a theorem rather than a soak test, and it holds for every schedule the compiler can emit, not just the ones we ran.

The optimisation side is where the proofs earn their place. Three passes rewrite the counter graph after scheduling. One removes counters whose dependency is already implied by the order two tasks occupy on the same resource. One merges counters that carry the same dependency. One hoists loads earlier so they overlap with prior compute. Each of those is a transformation that could silently break the dataflow, and each has a theorem saying the coverage property survives it — so the pass is written once and trusted, rather than re-validated per model with benchmarks that would not detect the failure anyway.

Then there is a result that told us not to build something. The natural next idea is finer counters: instead of one gate saying "all producers of this operator are done", give each consumer slice its own gate so it can start as soon as its own producers finish. The collapse theorem says that for a chain of counter-gated stages ending in a barrier, the finish time is the latest arrival plus the total work, and that expression does not mention which producers each consumer waited on. The straggler's slack reaches the barrier regardless. Fine counters can only win when the consumer slices do unequal work — and the library carries the smallest witness of that too, so the rule is not vacuously true. The compiler runs the corollary as an executable decision: it asks whether the cost model gives this operator's slices differing costs, and on a model whose attention heads are all identical the answer is no on every edge, so it emits the coarse counters. That matches what we measure. On a mixture-of-experts model the answer can be yes, and the finer counters remain available.

A measurement closes the loop. On a 48-layer 12B model compiled in fp8, the emitted graph has exactly one counter per operation, and its transitive reduction is itself — 717 dependency edges, 717 after reduction, and a single dead counter in the whole model. The passes that the proofs made safe to run have nothing left to remove. That is a negative result, and it is worth more than a speedup, because it closed a line of work instead of starting one.

Tiles: proving a partition, then pricing it

On the tile side, the legality question is whether the chosen tile shape actually covers the matrix multiply it claims to. The theorem is a completeness statement: the tile steps cover the whole index space. It is stated to permit an over-sized tile on a small operator — a router with eight output columns compiled against a minimum tile width of sixteen — where one tile covers the axis with masked waste and the coverage argument still holds. That case is common enough that a theorem which quietly excluded it would be worse than none. Alongside it is a soundness result for the executable check the compiler calls, so the fast decision procedure and the proved property cannot drift apart. On-chip memory gets a temporal argument: if a producer's window closes before its consumer's opens and each side individually fits the page budget, then occupancy never exceeds the budget at any cycle — with a counterexample proving both halves of that hypothesis are load-bearing.

The optimisation side is a proved cost model. The work a tiling is charged is never less than the arithmetic it really performs, so choosing the cheaper-looking tiling is choosing the cheaper one. Above that sit lower bounds on the schedule's makespan from the memory bandwidth and the arithmetic throughput of the machine, and their contrapositives: a plan needing more bandwidth or more compute than the hardware has is rejected at compile time with a reason, rather than built and measured. That is what makes exploring a large tile space affordable — most candidates are eliminated by arithmetic, not by running them. The same file proves the weight-traffic argument for decode that justifies keeping the plan resident, and separate modules prove that writing in place, streaming a value rather than materialising it, splitting a reduction across workers, and the interleaved layout the fused gated-MLP uses are all equalities. Those are exactly the rewrites where a heuristic would be plausible and wrong.

And what the proofs do not do

Lean proves the plan is legal. It does not prove the plan is fast — speed is a separate, measured gate, and a schedule can pass every checkpoint and still lose to a better one. It does not prove the kernels themselves compute the right function; those are gated numerically against a reference, and a family without a correctness oracle cannot produce a qualified measurement at all. The on-chip memory checkpoint is defence in depth over a scheduler pass that already enforces the same invariant, which is why it is opt-in and expensive rather than always on. And the argument for splitting the instruction stream into segments with different occupancy is written down and not yet mechanised — it is stated in the design notes as a proof obligation, and until it is discharged we describe it as an argument, not a theorem.

A runtime built to stay out of the way

The serve-time surface is deliberately narrow, but the consequences span the serving system. The diagram shows where each property lives in the stack; the cards below distinguish what is measured today from what is still a hypothesis under test.

Every kernel is ours

Plow has no vendor math or collective library underneath it. There is no cuBLAS, cuDNN, CUTLASS, NCCL, or ROCm/RCCL anywhere in the serving path. Every kernel plow runs — the GEMMs, attention, the Mixture-of-Experts routing, and the cross-GPU all-reduce — is written by us. On NVIDIA they compile with nvcc; on AMD, with AMD's clang. The runtime binds directly to the CUDA driver API on NVIDIA and to the HSA runtime on AMD — nothing else sits between plow and the accelerator.

This is a deliberate cost, and it is the point. The same compiled execution plan, the same counter protocol, and the same collectives run on both vendors with no dependency on a library we don't control — which is why AMD is a first-class target rather than a port, and why a collective in plow is just another entry in the resident kernel's stream instead of a launched library call.

How we evaluate it

A systems rewrite is only useful if it survives comparison. We report results by workload phase because prefill and decode stress different parts of the machine, and we avoid collapsing latency, throughput, startup, and efficiency into one headline number.

1. 01
   Fix the workload.

   Model, precision, context, batch size, tensor-parallel degree, hardware, and software versions are recorded per run.

2. 02
   Gate on correctness.

   Output is checked against a reference before performance data is accepted.

3. 03
   Separate the surfaces.

   Raw execution, serving overhead, cold start, host utilization, and end-to-end pipeline latency are measured independently.

4. 04
   Publish limits.

   Untuned paths, crossovers, and unmeasured design goals are stated next to the results rather than hidden in footnotes.

The first published decode studies follow this protocol. On Blackwell, serving overhead measured +0.9% on the 12B model and below noise on larger models. On 8× MI350X, Plow's per-token latency grew 1.40–1.52× from 1k to 128k context, compared with 1.9–2.9× for the tested vLLM configurations. Those results support a low-overhead execution path; they do not yet prove the cold-start or multi-model hypotheses.

What we are not claiming

• Plow does not make data transfer, weight loading, or device initialization disappear.
• Ahead-of-time compilation shifts work earlier; it does not make compilation free.
• Lower host involvement does not mean zero host CPU use across networking, tokenization, and the serving API.
• Multi-model support is a runtime design property today; production co-residency results are still pending.
• Current public measurements cover LLM decode. Diffusion, voice, prefill, and multi-user throughput will be published only after the same correctness-gated evaluation.
• The e-graph rewrite search runs and is proved sound, but it does not currently produce the fusions in a shipped packet — those are implemented in the emitter. We describe it as a working optimizer that is advisory today, not as the thing making plow fast.
• Vision and diffusion architectures build as graphs and have fusion rules; they have no device path, so they are not served. Speech is a design, not code.
• The Lean checkpoints prove the compiler's own output legal. They say nothing about whether a kernel computes the right function — that is a separate numerical gate against a reference.

Research context

Plow is our implementation, but the motivation is broader than one runtime. The relevant direction across the field is consistent: describe repeated work earlier, reduce request-time coordination, and keep multi-stage data on the serving side when possible.

• Hazy Research — Look Ma, No Bubbles! Designing a Low-Latency Megakernel for Llama-1B: fusing an entire forward pass into a single kernel to remove the per-kernel launch and setup/teardown bubbles — the same premise as plow's persistent kernel.
• NVIDIA CUDA Programming Guide — CUDA Graphs: why defining repeated work in advance reduces CPU launch costs.
• PyTorch — Ahead-of-Time Compilation: moving compilation out of the production cold-start path.
• Tate et al. — Equality Saturation: exploring equivalent program forms before selecting an optimized result.
• NVIDIA Triton — Ensemble Models: the latency motivation for server-side multi-model pipelines.