CaT: A Solver-Aided Compiler for Packet-Processing Pipelines

A high-speed programmable switch runs a packet through a short fixed line of hardware stages, and fitting a network program into that line — while a stateful update must finish in a single clock cycle and the whole program either fits and runs at full speed or does not run at all — is an NP-hard packing puzzle that today's compilers either solve slowly or fail; this paper (NYU, Princeton, Rutgers) builds CaT, which splits the puzzle into three phases and hands each to the solver best suited to it, compiling programs prior tools could not and doing so about three times faster with fewer resources.

Why this problem is worth solving

These pipelines are the substrate of programmable networking, and their constraints are unusually unforgiving.

The technique CaT leans on to cope with that hardness is one more often seen in hardware design than in networking.

What people did before, and where it broke

• Rewrite the program with classical compiler passes. The standard P4 compiler and the Tofino compiler apply rewrites like common-subexpression elimination and constant folding, and tools like Cetus merge tables to save stages. Where it broke. Their dependency analysis is conservative — it treats writes to the same field as conflicting even when the branches that make them can never both run — so it misses rewrites that would collapse several stages into one, forcing programmers to restructure code by hand.
• Synthesize each action exhaustively (Chipmunk). Use program synthesis to search the full space of ALU configurations for an action, guaranteeing a fit if one exists. Where it broke. The search is enormous, so compilation takes many minutes to hours and needs a grid of machines running a parallel search over pipeline geometries; and it handles only a single transaction, with no global allocation across actions.
• Synthesize only the stateful parts, rewrite the rest (Domino). Use fast rewrite rules for most of an action and program synthesis just for the stateful update. Where it broke. It is brittle — a minor, semantics-preserving change to the input program can make compilation fail — and it targets only one ALU family.
• Allocate resources with an integer linear program. Frame the placement of match memory into stages as an ILP or SMT constraint problem, which beats greedy heuristics. Where it broke. These formulations model memory but not the ALU computation inside actions, and not multi-stage or multiple transactions, so they optimize only part of the layout.
• Invent a new higher-level language. DSLs like Lyra and Flightplan raise the abstraction and even split a program across many devices. Where it broke. They solve a different, complementary problem — network-wide partitioning — and still must ultimately compile down to a single device, which is the piece left unsolved.
• The gap. Every tool owned one slice of an NP-hard problem — rewriting, or synthesis, or allocation — and none combined them into an end-to-end flow that could optimize globally while staying fast. What was missing was a decomposition of the whole puzzle into pieces small enough for solvers yet arranged so their local answers add up to a good global fit.

How CaT is put together

The idea

The dependencies that force extra stages are often not real once you look at the conditions. A pipeline compiler serializes two statements into different stages whenever it thinks one depends on the other — and a write to a field followed by another write to the same field looks exactly like such a dependency. But consider three statements that each add to the same counter, each guarded by a different, mutually exclusive test on a packet field. A naive analysis sees three writes to one field and demands three stages; in truth at most one branch ever runs, so there is no ordering to respect and all three can live in one stage. CaT makes this precise with guarded dependencies: it attaches to each apparent dependency a guard, the condition under which both statements could actually execute on the same packet, and asks an SMT solver — or a cheap depth-first walk of the branch conditions — whether that guard is even satisfiable. When it is not, the dependency is a phantom and is dropped, and the disjoint branches collapse into a single match-action table keyed on the conditions. Discovering that a constraint everyone treated as fundamental is an artifact of looking too coarsely, and that removing it unlocks parallelism the hardware could always have exploited, is the same move the non-blocking automata-processing work covered elsewhere on this site makes when it finds that the barrier serializing the computation belonged to the data structure, not to the problem, and dissolves it.

Do not hand the solver one giant question — cut it into many small ones. The reason exhaustive synthesis is slow is that it asks a single enormous question: find an implementation of this whole action across the ALU grid. The search space is the product of every choice at once. CaT’s synthesis phase instead breaks an action into a computation graph, condenses each atomic read-modify-write into one stateful node, and then poses a separate, small synthesis query for each stateful update and each output — with stateful and stateless queries kept apart, because a stateful ALU must be handled as an indivisible one-cycle unit while stateless code can be spread out and minimized for depth. Each query is tiny and fast, and because they are independent they compose into a resource graph. That graph is then the input to a second, global decomposition: synthesize every action locally in Phase 2, then allocate all of them together in Phase 3. The compiler never faces the whole NP-hard problem at once; it faces a swarm of small ones and one global placement. Taming a combinatorial layout by decomposing it into subproblems sized for a solver, rather than presenting the solver with the monolith, is the same discipline the on-chip memory-allocation work covered elsewhere on this site relies on, carving a hard packing problem into pieces a constraint solver can dispatch quickly.

Use the solver that fits each phase, and describe the hardware so the same machinery retargets. The thread tying the design together is that each phase is expressed in the form some mature solver already solves well: satisfiability for deciding whether a guard can hold, program synthesis for fitting an action into ALUs, and integer linear programming for placing everything into stages under capacity constraints. CaT is thus less a hand-written compiler than an orchestration of solver engines, which is what its authors mean by solver-aided. Crucially, the synthesis queries are parameterized by an ALU grammar — a description of exactly what one target’s ALUs can compute — so the identical procedure retargets to the Tofino, to Banzai, or to Menshen just by swapping the grammar, no compiler rewrite required. Building a compiler as a thin layer that poses each subproblem to a general solver and stays retargetable by describing the hardware in a reusable specification, rather than encoding one chip’s rules in bespoke code, is the same philosophy the retargetable synthesis-based compiler work covered elsewhere on this site is built on, generating backends from machine descriptions instead of writing them by hand.

Following one action through the three phases

A lightweight version skips the solver entirely: a depth-first walk of the control-flow graph pushes and pops branch conditions on a stack, so each statement carries the AND of its enclosing conditions, and two disjoint conditions AND to false.

Why it works

• Removing phantom dependencies frees stages the hardware could always use. A conservative analysis serializes writes that can never co-occur → but proving the guard between them unsatisfiable shows there is no real ordering to keep → so disjoint branches fold into one stage and programs that needed too many stages suddenly fit.
• Many small synthesis queries beat one huge one. Exhaustive synthesis of a whole action explodes because every choice multiplies → but splitting the action into small, independent stateful and stateless queries makes each search tiny and fast → which is why CaT compiles about 2.75 to 3.94 times faster on average, and up to roughly 49 times, than exhaustive synthesis.
• Local synthesis plus global allocation stays tractable and still fits well. Solving the whole program at once is NP-hard, but so is ignoring the global picture → so CaT synthesizes each action locally where the problem is small, then feeds those resource graphs to one global allocation → getting stage counts on par with exhaustive search while using a single machine instead of a grid.
• An ALU grammar makes the same compiler retarget. Encoding one chip’s ALU rules in bespoke code locks a compiler to that chip → but posing synthesis against a swappable grammar of the target’s ALU capabilities keeps the procedure unchanged → so CaT already targets Tofino, Banzai, and Menshen and can take on more by writing a grammar.
• Each phase is posed in a solved form. Deciding guards, fitting ALUs, and placing resources are three different hard problems → but they map cleanly onto satisfiability, program synthesis, and integer linear programming respectively → so CaT inherits decades of solver engineering instead of hand-coding search, turning an NP-hard whole into practically solvable pieces.

What it costs (trade-offs and scope)

• The hardest programs are still slow, and the fast number needs a special trick. SipHash, with a deep four-stage action and 32-bit bitvector operations, took about 40 hours in the base procedure. It drops to under two minutes only with a constrain-and-verify enhancement — synthesize on a narrowed input space, then separately verify the result for the full space — which is not the default flow, and deep multi-stage actions are named as open future work.
• The decomposition can cost optimality. Separating stateful from stateless queries occasionally uses an extra stage — the STFQ benchmark compiles to three stages where exhaustive synthesis found two — so the speed comes with an occasional resource penalty that predecessor packing only sometimes recovers.
• The Tofino backend is not real machine code. Because the Tofino’s instruction format is proprietary and undocumented, CaT emits low-level P4 as a best-effort encoding rather than machine code, so the strongest commercial target is reached only indirectly.
• The benchmarks are small and partly borrowed. Resource transformation is shown on three extracted examples, synthesis on the fourteen benchmarks (and their mutations) from the tool it compares against, and allocation on subsets of switch.p4 with two to six tables — evidence of capability, not a study of large production programs.
• Target expressiveness limits coverage. The open Menshen ALU could not express six of the fourteen Domino benchmark programs, so the fully open, end-to-end tested path covers a subset of the workloads.
• The dependency analysis is deliberately conservative. The lightweight guarded-dependency pass gives up and does no rewriting when an assignment updates a variable used in an if-condition, to avoid the harder write-after-read cases, so some legitimate rewrites are left unfound.
• Scope is one device, exact matches, no sharing across queries. CaT compiles a program for a single device and does not do the network-wide partitioning that Lyra and Flightplan address; table partitioning currently supports only exact matches; and, like the tool it improves on, its independent synthesis queries cannot share common subcomputations.
• The all-or-nothing nature bounds the payoff. Because a program either fits and runs at line rate or does not run at all, CaT’s value is largely binary per program — it makes more programs fit and compiles them faster, but there is no partial credit for a program that still does not fit.

The evaluation

Check yourself

Sources

The paper is “CaT: A Solver-Aided Compiler for Packet-Processing Pipelines” by Xiangyu Gao, Divya Raghunathan, Ruijie Fang, Tao Wang, Xiaotong Zhu, Anirudh Sivaraman, Srinivas Narayana, and Aarti Gupta, published at ASPLOS 2023, pages 72-88, DOI 10.1145/3582016.3582036. The authors are at New York University, Princeton University, and Rutgers University.

This explainer is written from the full 17-page text. Everything above comes from the paper’s own sections: the introduction framing compilation to RMT pipelines as an NP-hard combinatorial problem with multiple resource types, transactional guarantees, and all-or-nothing fit, and the high-level-synthesis inspiration; the background on match-action pipelines and the survey of prior work (p4c, Cetus, Lyra, Domino, Chipmunk, Jose et al., P4All, Flightplan) unified in Table 1; the motivation with the SipHash and rate-enforcer examples that programmers pipelined by hand; Phase 1 resource transformation with guarded dependencies and the lightweight path-condition analysis and the rewrites to match-action tables; Phase 2 resource synthesis with its preprocessing, computation graph, decomposition into small stateful and stateless SKETCH queries, minimum-depth synthesis, predecessor packing, ALU grammars, and the detailed comparison with Chipmunk; Phase 3 resource allocation with its ILP/SMT constraint formulation for ALUs, multi-stage actions, multiple transactions, and output propagation; and the evaluation covering resource-transformation stage reductions (Table 4), the synthesis comparison against Chipmunk and Domino on Tofino and Banzai ALUs with the reported 2.75x and 3.94x geometric-mean speedups and the SipHash 40-hours-to-2-minutes result (Table 5), the controlled optimization studies, and the resource-allocation experiments comparing Gurobi and Z3.