Hydride: A Retargetable and Extensible Synthesis-based Compiler for Modern Hardware Architectures

Every new vector instruction a chip vendor ships requires a human to read a thousand-page manual, invent a matching operation for the compiler's internal language, and hand-write the rules that recognise when to use it — which is why compilers lag hardware by years; Hydride (UIUC and AWS) reads the vendor pseudocode instead, proves with an SMT solver which instructions differ only in their numbers, and collapses 3,557 instructions across x86, ARM and Hexagon into 397 parameterised operations that a program synthesiser targets directly.

Why this problem is worth solving

The lag between hardware and compilers is a structural property, not an oversight.

There is an alternative to matching patterns: searching for programs.

What people did before, and where it broke

• Expose each new instruction as a target-specific intrinsic. The pragmatic route taken by production compilers, and it works: no neutral operation has to be designed, and the instruction becomes reachable immediately. Where it broke. An intrinsic named for one chip cannot be lowered to another, so nothing retargets, and the compiler infrastructure gains no ability to evolve with the hardware.
• Write a separate backend for each target inside each language compiler. Performance-sensitive image and tensor languages do exactly this, with hand-crafted rules mapping their own IR directly to chip intrinsics. Where it broke. It reimplements a complex part of a general compiler for the benefit of a single language, once per target, and every one of those backends must be updated by hand as instruction sets grow.
• Generate the matching rules automatically from instruction semantics. A prior system does this for one architecture, removing the most tedious part of the manual work. Where it broke. It generates one pattern variant per instruction, so any deviation in the input code shape means a miss; it does not handle the cross-lane shuffles that matter most for tensor and stencil code; and its IR is still fixed, so nothing evolves.
• Use program synthesis for instruction selection. Several systems search for provably equivalent instruction sequences rather than matching templates, which is the right idea and finds code no rule anticipated. Where it broke. They cover a few hundred instructions rather than thousands, and their neutral IR is designed by hand, so the scalability problem simply moves. One of them also requires the programmer to restructure source code so the patterns are visible to the synthesiser, which pushes work back onto the user and breaks the separation between what a program computes and how it is scheduled.
• Hand-write the formal semantics each of these approaches needs. Unavoidable if the semantics are the input to the tooling. Where it broke. It is enormous, and it is wrong in places — this paper found five semantics bugs in the prior synthesis system it compares against, all involving unmasked shift operands.
• The gap. Every approach assumed the description of the hardware is something a person writes. But the vendors already publish executable descriptions of every instruction, in their own manuals, and nobody was using them as the foundation of the compiler.

How 3,557 instructions become 397

The idea

An instruction set is much smaller than its instruction count, once you stop looking at the numbers. Two x86 instructions that add sixteen-bit elements in 512-bit registers and eight-bit elements in 256-bit registers are documented separately, named separately, and pattern-matched separately, and they are the same operation. The move here is to make that observation mechanical: normalise each instruction description into a loop over lanes containing a loop over elements, pull every constant out into a symbolic parameter, and ask a solver whether two descriptions become identical under the same assignment. What survives is an equivalence class, and one parameterised operation represents the whole class — so lowering to any member is a matter of filling in the parameters, not matching a pattern. The compression is severe: 2,029 x86 instructions become 136 operations, 1,221 ARM instructions become 177, and all 3,557 instructions across three architectures become 397, about one in nine. Discovering that a space which looks impossibly large collapses to a small parameterised basis once the incidental details are abstracted away is the same reasoning the reconfigurable array work covered elsewhere on this site applies to dataflow graphs, where every three-node fragment turns out to be one of exactly three shapes.

The escalation over hand-written semantics is the whole practical difference. Using synthesis for instruction selection was not new — the immediately preceding work covered elsewhere on this site made precisely this argument, that pattern matchers only ever find what somebody thought to write down, and beat a backend that two large companies had spent years tuning. What limited it was that a human had to write the formal semantics of every target instruction by hand, which is why it covered 164 Hexagon and 200 ARM instructions, why its neutral IR was designed manually and could not grow, and why this paper was able to find five bugs in those hand-written semantics, all of them missing operand masks on shift operations. Taking the vendor pseudocode as the source removes that ceiling: one parser per architecture, then the semantics for the entire instruction set follow, giving roughly twice the Hexagon coverage and six times the ARM coverage. It also removes a second imposition — the earlier system asked programmers to rewrite their source so that dot-product and data-movement patterns were visible to the synthesiser, which violates the whole premise of a language that separates what is computed from how it is scheduled.

Everything that makes synthesis tractable is where the engineering actually went. Handing a synthesiser all 2,029 x86 instructions runs out of memory. Restricting it to the fifty best-scoring instructions still exceeds a four-hour timeout without finishing. The system only works because of a stack of prunings applied before the search begins: drop an entire equivalence class if none of its underlying bit-vector operations appear in the input, drop instructions whose element size is smaller than anything in the input since they would lose information, then score the remainder by how much they resemble the input and keep only the best three or four from each class. On top of that, the search exploits the fact that vector computations repeat across lanes, so equivalence is asserted on a few lanes and verified on the rest afterwards, and the register widths are scaled down before searching and scaled back up after — solver time grows exponentially in bit-vector size, which matters enormously for a chip with 2048-bit registers. Together these turn intractable into 86 seconds for x86 and 48 for Hexagon. Confronting a design space that cannot be explored because the tooling for each point is too expensive is the same obstacle the automated tile design work covered elsewhere on this site identifies when it notes that every candidate architecture needs a new compiler before it can even be judged.

Following one Halide expression down to machine instructions

Also generated offline: an interpreter for those operations, a cost model summing instruction latencies, the grammar generator, and the near-trivial one-to-one rules that lower each parameterised operation to a real chip intrinsic.

Why it works

• Vendors already publish what the compiler needs to know. Every approach before this treated the formal description of an instruction as something a person writes, which caps coverage at what a person has time for → but the manuals contain executable pseudocode for every instruction already → so one parser per architecture yields semantics for the whole instruction set, giving twice the Hexagon coverage and six times the ARM coverage of the hand-written alternative.
• Most of what distinguishes two instructions is a number. Element size, register width, lane offset and shift amount are what the names and the documentation emphasise → but abstracting them into symbols and asking a solver for equivalence reveals that instructions differing only in those values are one operation → collapsing 3,557 instructions into 397 classes, about one in nine.
• A parameterised operation makes lowering trivial in both directions. Pattern matching exists because a neutral operation and a chip instruction are related only by a human-written correspondence → whereas here each class member is exactly the parameterised operation with particular values, and the system remembers which → so instruction selection becomes filling in arguments, and a front end can pick target-optimal values at synthesis time.
• Searching finds sequences no rule anticipated. A pattern matcher fires only on the shapes someone wrote down, and misses on any deviation → whereas a synthesiser asked for the cheapest provably equivalent program will assemble cross-lane shuffles and dot products that no template covers → which is where the wins over a decade-old production backend come from, largest on matrix multiplication at over 1.30 times.
• Pruning before searching is what makes searching possible. The search is doubly exponential, and even the fifty best-scoring instructions exceed a four-hour timeout → so classes are dropped wholesale when their operations do not appear in the input, lanes are constrained on a subset and verified afterwards, and register widths are scaled down and back up → turning intractable into 86 seconds on x86 and 48 on Hexagon.

What it costs (trade-offs and scope)

• Integer instructions only. Floating point is left to future work, which is a substantial exclusion for image processing and deep learning, and it means the comparison against production backends covers a subset of what those backends must handle.
• No memory instructions. Loads and stores are not synthesised — as with the prior work. This cuts both ways: it is missing functionality, and it is also why changing a schedule usually does not force resynthesis, since schedules mostly affect memory access patterns.
• The vendor pseudocode needed manual correction. The x86 and Hexagon specifications do not distinguish logical from arithmetic right shifts and do not make operand widening explicit for saturating left shifts, so the authors edited the vendor pseudocode by hand in those cases. The resulting semantics are validated by random fuzz testing against the vendors’ own C builtins, which raises confidence rather than establishing correctness.
• Compile times are measured in tens of minutes. Geometric means from a cold cache are 18 minutes on x86, 39 on Hexagon and 9 on ARM, and individual benchmarks run far longer — a depthwise convolution takes over sixteen hours on Hexagon. Even with everything cached, recompilation is a few minutes.
• The cache itself is slow enough to dominate. Cache-lookup overhead reaches 5.5 to 60 minutes in the largest cases, which the paper attributes to the hash tables and start-up cost of the host language.
• The lane-shuffle patterns are a hand-written list of five. They are always included in the grammar because a general permutation makes synthesis intractable, and a chip with a genuinely novel shuffle would need it added manually — a manual step inside a system whose argument is the elimination of manual steps.
• Bounded windows cause real, structural losses. One Hexagon benchmark runs at 0.54 times the production compiler because the pattern that yields a four-way dot product spans more code than the synthesiser can take in at once, and another at 0.78 times because interleave and de-interleave pairs cannot be moved across basic blocks the way a specialised pass does. These are limits of window-bounded synthesis, not tuning gaps.
• The engineering-effort comparison is not like for like. Three students in a year against backends maintained for a decade is a striking framing, and the production backends also handle floating point, memory operations, more targets, and years of accumulated correctness in production.
• The largest speedup is on the target the authors tuned themselves. The benchmarks were hand-tuned by the authors for x86 and by Qualcomm and Adobe for ARM and Hexagon — and the x86 result is the strongest at 8 percent, with the vendor-tuned targets at 3 percent and parity.
• Several baselines could not be run. The prior synthesis system failed to compile 28 of the benchmarks on Hexagon and every benchmark on ARM despite claiming support, and the standard compiler backend fails register allocation on two Hexagon benchmark families, so those comparison points are absent rather than unfavourable.
• Hexagon results come from a simulator, a cycle-accurate one supplied by the vendor, not from hardware.
• Tuning parameters remain. Window size, output sequence length and the number of operations kept per class — three or four here — are set empirically, and the pruning heuristics are load-bearing rather than incidental.

The evaluation

Check yourself

Sources

The paper is “Hydride: A Retargetable and Extensible Synthesis-based Compiler for Modern Hardware Architectures” by Akash Kothari, Abdul Rafae Noor, Muchen Xu, Hassam Uddin, Dhruv Baronia, Stefanos Baziotis, Vikram Adve, Charith Mendis and Sudipta Sengupta, published at ASPLOS 2024, pages 514-529, DOI 10.1145/3620665.3640385. The authors are at the University of Illinois Urbana-Champaign and Amazon Web Services.

This explainer is written from the full 16-page text. Everything above comes from the paper’s own sections: the statement of the three challenges facing compilers for evolving instruction sets and the analysis of why intrinsics, per-language backends, automatically generated pattern rules and existing synthesis-based selectors each fail to address all of them; the automatic IR generator, covering the parsing of vendor pseudocode into a solver-aided intermediate language, the canonicalisation into a two-level loop nest, the extraction of constants with bit-width analysis to avoid conflating parameters, the formal definition of instruction similarity and the equivalence-checking algorithm with its argument permutation, hole-synthesis refinement and dead-argument elimination steps, and the generation of parameterised compiler intrinsics with their one-to-one lowering rules; the code synthesiser, covering the automatically generated interpreter, cost model, grammar generator and memoisation cache, the counterexample-guided synthesis procedure with its lane-wise constraints and width scaling, the three-stage grammar pruning, and the five supported lane-shuffle patterns; the implementation notes on the parsers, the fuzz testing of generated semantics and the manual corrections required for ambiguous specifications; and the evaluation covering the equivalence-class counts per architecture and in combination, the five semantics bugs found in the prior system, the case study on adding a third architecture, the per-target performance against production backends and against a standard compiler backend with the per-benchmark exceptions and their causes, the compile-time tables under four caching scenarios, and the sensitivity analysis isolating each synthesis heuristic.