Tree traversal synthesis using domain-specific symbolic compilation

Compilers and browser layout engines compute attributes over trees in several passes, and fusing those passes into few traversals, or splitting them to run in parallel, is a scheduling puzzle that humans get wrong (Servo has layout bugs open for years) and existing automatic schedulers solve in only one fixed way — Hecate lets the programmer write a traversal template with holes, fills the holes with a solver so every attribute is computed once and after its inputs, and, by translating the schedule into a time-free trace of reads and writes that becomes an integer linear program instead of an SMT formula, synthesizes 3 times faster than the generic solver-aided approach and orders of magnitude faster on real CSS grammars while opening up vector-based and parallel traversals that make rendering 2 times faster.

The argument in one glance

Problem

Scheduling tree computations into traversals is where layout engines break

A browser computes widths, heights, fonts and positions for a render tree; a compiler desugars, propagates constants and folds them over an AST. Each is a set of attribute rules, and running them efficiently means fusing rules into a small number of tree traversals and running independent subtrees in parallel. Every rule must run after the attributes it reads and exactly once. Done by hand, this produces bugs: Servo has layout bugs open for over five years because its architecture does not match its intended semantics.
What people did

Automatic schedulers: rewrite rules, automata, or Prolog

TreeFuser and Grafter analyze dependencies statically, build access automata, and apply deterministic fusion rules. FTL expresses layout as an attribute grammar and asks a Prolog engine to find a schedule with parallel traversals. Solver-aided languages such as Rosette can, in principle, turn an interpreter for traversals into a synthesizer automatically.
Why it fell short

One answer, one data structure, or one exploding formula

Grafter always fuses whenever possible, supports only linked lists of children because of its static analysis, and cannot produce parallel traversals, so it cannot explore the space of legal schedules. FTL needs experts to hand-translate layout semantics into Prolog and is tied to that solver and encoding. And the generic Rosette route, symbolically running the interpreter, threads every scheduling choice through every later time step: with n nodes, k slots per node and q candidate rules per slot, up to q to the power of n times k symbolic states, which the paper measures as constraints that take far too long to solve.
This paper's idea

A traversal template with holes, filled by CEGIS, encoded as an ILP through a trace language

Hecate takes an attribute grammar, a symbolic traversal whose slots each hold at most one rule, and an example tree. A counterexample-guided loop asks a solver to fill the slots so that on the example every attribute is written once and read only after it is written, then verifies the result on all trees up to a depth and feeds back any failing tree. The key is how the constraints are built: a domain-specific layer under the interpreter rewrites each candidate rule placement into a short trace of read and write actions, and a dependency operator maps those to 0-1 integer linear constraints that never mention time steps, at most (1 + n squared) times q times k states. Hecate reproduces all five Grafter benchmarks 3.1 times faster than the generic encoding and 8 times faster than Grafter, synthesizes vector-based and parallel traversals that cut rendering time about 70 percent against the unfused baseline and 40 percent against Grafter, and schedules real CSS grammars in 39 seconds where FTL needs 189 and the generic encoding does not finish in 30 minutes.

Why this problem is worth solving

A render tree node has a default width w0 and height h0, a final width w and height h, and two helpers: w1, the maximum width among a node and its later siblings, and h1, the summed height. An inner box’s width is the larger of its default and its first child’s w1; its height is the larger of its default and its first child’s h1. Computing width and height as two separate passes visits every node twice. The fused version in the paper’s Figure 1 visits each node once and does both, but only because someone worked out that the width rules and height rules can interleave safely. Real engines have hundreds of such rules. The paper’s CSS-full grammar has 244; the AST benchmark has 136.

The cost of getting this wrong is measured in years. One Servo bug, a mismatch between the intended layout semantics and the traversal architecture chosen to implement them, had been open for five years at submission; a developer wrote that it took three weeks to realize the actual complexity of the problem, and the team resolved to leave it until a complete rewrite. An

attribute grammar

A formal description of a tree computation: node types with attributes and rules that define each attribute from attributes of the node and its children or siblings, each assigned exactly once.

makes the rules explicit; what is missing is a way to turn the rules into traversals that is both automatic and flexible enough to explore serial versus parallel, list versus vector.

What people did before, and where it broke

Manual scheduling. Engine developers choose the passes and their order. Where it broke. Fine control, but the complexity of CSS semantics makes the schedule hard to maintain and the source of long-lived bugs.
Grafter and TreeFuser. Static dependence analysis over visitors, access automata, and deterministic fusion rules. Where it broke. Fast, but each produces exactly one schedule that fuses whenever it can; extending to a new kind of traversal means devising new fusion theory; Grafter’s analysis supports only linked lists of children, not the vectors real compilers such as Clang use, and it cannot emit parallel traversals. The paper shows unconditional fusion can be slower than de-fusing into a parallel loop plus a sequential reduction.
FTL. Attribute grammars plus a Prolog-based search for parallel schedules of layout engines. Where it broke. Translating semantics into Prolog is expert, error-prone work; FTL is specialized to one solver, encoding, grammar language and schedule language, and is no longer maintained.
General-purpose solver-aided synthesis. Write the traversal interpreter in Rosette and let symbolic execution produce constraints. Where it broke. Faithful interpretation carries every earlier choice into every later assertion; the number of symbolic states grows exponentially with nodes times slots, and the resulting SMT constraints are slow even with Rosette’s state merging. On the CSS grammars it did not terminate within 30 minutes.
The gap. No tool combined automatic synthesis, user-definable traversal templates including vectors and parallel visits, and constraints that scale to real grammars.

Where Hecate sits

The Hecate CEGIS loop

Inputs new

An attribute grammar (classes, children, rules), a symbolic traversal with slots, and an example tree.
↓ →
Domain-specific interpreter new

Executes the traversal; for each slot, emits a trace program of read and write actions per candidate rule instead of raw assertions.
↓ →
Trace to ILP new

A dependency operator maps traces to 0-1 integer linear constraints without time steps; slot and rule constraints enforce validity.
↓ →
ILP solver

CPLEX or Z3 returns an assignment of rules to slots: a concrete traversal.
↓ →
Verifier new

Symbolically checks the concrete traversal on all trees up to depth k via Rosette; a failing tree becomes a new example.
↓ →
Output

A concrete traversal in the tree language, translated to C++ for benchmarking.

The loop repeats until the verifier finds no counterexample. Replacing the trace-to-ILP box with direct Rosette assertions gives HecateG, the general-purpose baseline the paper measures against.

The idea

Three small languages. The attribute grammar language declares interfaces with typed attributes, classes with named children, and rules of the form self.attr := expression over access paths such as fc.h1 or nx.w1, with folds over vectors of children. The

tree traversal language

A program that visits tree nodes and, at each node type, recurses into children, iterates or parallelizes over a list of children, and evaluates attribute rules in order.

has cases per node type containing recur, iterate, parallel, eval, and a

slot

A hole in a symbolic traversal that the synthesizer fills with zero or one attribute rule.

ι that holds zero or one rule. A traversal with slots is symbolic; the synthesizer’s job is to make it concrete. Because the programmer writes the template, new kinds of traversal, post-order, vector iteration, parallel children, are a few lines rather than new theory.

Correctness as a total order. A traversal induces a total order over every location, every node-attribute pair, in the tree. It is correct if every attribute is computed exactly once and each rule runs after every location it reads has been written. The synthesis problem is to fill the slots so this holds for every tree the grammar can generate, which Hecate approximates by checking the initial example and then verifying on all trees up to a bounded depth, adding counterexamples until none remain.

Why the generic encoding explodes. The straightforward interpreter, Figure 8a in the paper, asserts at each rule that its inputs are ready and its target is not, using a readiness predicate δ(node, attribute, time). A slot becomes a choose over candidate rules, and Rosette compiles each choice as a guarded implication: σ(rule, slot) implies the readiness facts at this time step. The trouble is that readiness at time t depends on which rules were chosen at all earlier steps, so the guards nest, and the number of symbolic states climbs as q to the power of n times k: the paper’s Figure 9 counts 26, 806, 3,206, 10,406, 94,406, 374,406 and 1,214,406 states as a small traversal proceeds.

The trace language. Hecate inserts a layer between the interpreter and Rosette. Instead of asserting, the interpreter transpiles each candidate placement into a program in a tiny

trace language

Hecate's intermediate language of four operations, choose, alloc, read and write, that records which locations a rule reads and writes without any notion of when.

: assume σ(Inner.h, ι2), read n1.h0, read n3.h1, write n1.h. The trace says what a placement depends on and produces, and nothing about time.

From traces to an ILP. A

dependency operator

The operator κ(location, time) that names the 0-1 variable saying whether a location was written at a given step; a write sets it to the placement variable σ, and a read requires the sum of κ over earlier steps to be at least σ.

κ links reads to writes. A write at step t guarded by σ(a, ι) sets κ(n.a, t) to σ(a, ι). A read at step t guarded by σ(a, ι) requires that the attribute was written somewhere earlier: σ(a, ι) is at most the sum of κ(n.a, t′) over t′ before t. Because the traversal fixes a total order of locations, every time step corresponds to a known location, so the sums can be rewritten as sums over the σ variables of the slots that could have written that location, and the time variables vanish. The read constraint for computing n1.h at slot ι2 becomes σ(Inner.h, ι2) ≤ σ(Inner.h0, ι0) + σ(Inner.h0, ι1), and similarly over the four leaf slots that could have produced n3.h1. Add that each slot holds at most one rule and each rule fills exactly one slot, and the whole problem is a 0-1

integer linear program

An optimization problem over integer variables with linear constraints; the 0-1 case restricts every variable to zero or one and is what off-the-shelf solvers such as CPLEX handle well.

. The state count is bounded by (1 + n²) times q times k, polynomial rather than exponential.

Design choices become template edits. With children as a vector cs rather than a first-child/next-sibling list, the rules become folds: self.w := fold(max, self.w0, cs.w). Marking the child loop parallel asks Hecate to verify that children’s computations are independent and, if so, to emit a parallel schedule, falling back to iterate otherwise. Grafter’s fusion heuristic, always merge, can lose here: a fused loop that recurses and accumulates per child can be de-fused into a parallel recursion followed by a sequential reduction, which costs more node visits but wins when child work dominates.

Tracing the rendering example through Hecate

Filling the height slot on an inner box

The paper's running example: tree with root n0, children n1 and n2, and n1's children n3 and n4. Inner nodes have rules for w, w1, h, h1; leaves likewise. The symbolic post-order traversal has slots ι0..ι3 on Inner and ι4..ι7 on Leaf after the recursive calls.

Step 1 of 6

The template

For an Inner node: recur fc; recur nx; then four slots. For a Leaf: recur nx; then four slots. Each slot may hold one of the node type's rules or nothing. The synthesizer must decide which rule goes where.

case Inner { recur fc; recur nx; ι0; ι1; ι2; ι3 } | case Leaf { recur nx; ι4; ι5; ι6; ι7 }

Why it works

Scheduling is a placement problem, not an execution problem. What matters is which slot computes which attribute, not the moment it happens. Because the traversal fixes the order of locations, every “before time t” can be rewritten as “in one of these slots,” and time disappears from the constraints.
Time-free constraints are linear. A read requirement becomes “the placement variable is at most the sum of the placement variables that could have produced the input,” which is a linear inequality over 0-1 variables. That is exactly what ILP solvers are built for, and the state count drops from exponential to (1 + n²) q k.
The solver-aided architecture is preserved. The programmer still writes an ordinary interpreter in Rosette; the trace layer is a syntax-directed transpilation inserted below it, so the engineering advantages of solver-aided languages remain while the encoding changes.
Templates make the search space the programmer’s. Serial or parallel, list or vector, which rules are even eligible for a slot: all are expressed in the symbolic traversal, so exploring a design choice is editing a few lines and re-running.
CEGIS keeps examples small. Synthesis runs on one example tree; the verifier’s bounded symbolic tree catches shapes the example missed and adds them, so the solver rarely needs a large instance.

What it costs

Bounded verification. Correctness is checked on all trees up to depth k, following prior synthesis work; deeper or differently shaped trees are not covered by the proof.
The programmer supplies the template. A symbolic traversal must be written; a wrong template yields no solution. The HecateA variant auto-tunes templates and matches Hecate on four Grafter benchmarks but takes over 30 minutes on the AST benchmark.
An ILP solver, ideally commercial. The domain-specific path targets CPLEX; the artifact notes the free edition can fail on larger instances and that Z3 works with a slowdown.
Slots hold at most one rule. The paper notes the semantics could be extended to several rules per slot, but the presented system is one-rule-per-slot.
Parallelism is opt-in and checked, not discovered. The template must mark a child loop parallel; Hecate verifies independence and falls back to sequential iteration if it fails.
Performance of synthesized code depends on the template, not the tool. Hecate’s fused traversals match Grafter’s; gains beyond that come from choosing vectors or parallel loops, which the paper shows pay off only as trees grow past overhead.

The evaluation

Synthesis time in seconds on the Grafter benchmarks (Table 2)

Property	Rules	Grafter	HecateG (general-purpose)	Hecate
BinaryTree	16	2.6	3.2	1.1
FMM	14	7.6	1.6	1.0
Piecewise	12	12.6	3.1	2.1
AST	136	151.7	73.4
RenderTree	50	62.0	10.1	4.1
Average	—

Times are synthesis plus verification. Hecate supports every Grafter benchmark and emits C++ via syntax-directed translation so the traversals can be benchmarked under Grafter's own workloads.Underlined values explain themselves when clicked.

Three further results show what the flexibility buys. RenderTree. Five rendering passes over a document tree of pages and nested containers. HecateL, the linked-list variant, matches Grafter’s fused traversal at over 50 percent running-time reduction versus unfused. HecateV switches children to vectors with a few lines of grammar change, which Grafter’s analysis cannot express, and reaches about 70 percent reduction, roughly 40 percent faster than Grafter. HecateP marks the child loop parallel; its overhead is visible on small trees but as tree size grows toward a billion nodes it adds a further 23 percent over HecateV. AST. Six desugaring and optimization passes over a small imperative language with 136 rules: HecateL matches Grafter at about 50 percent, HecateV adds 10 percent, and HecateP, exploiting independence between functions, exceeds 75 percent reduction on large trees. FTL. On three real CSS attribute grammars that Grafter cannot handle, CSS-float with 192 rules, CSS-margin with 178, and CSS-full with 244 including absolute positioning, margin collapse and floats, Hecate takes 39 seconds where FTL takes 189 on CSS-float and stays about 5 times faster on CSS-full, while the general-purpose HecateG does not terminate within 30 minutes on any of the three.

In an actual implementation

Why fusing everything can be the wrong answer

Grafter’s heuristic is to merge computations on the same node whenever dependencies allow, minimizing node visits. The paper’s Figure 14 shows the counter-case. A fused loop over a vector of children calls each child’s fused computation and, in the same iteration, folds the child’s result into a running maximum. The recursive calls are independent of one another, but the fold is sequential, so the loop as a whole cannot run in parallel. De-fusing it into two loops, a parallel one that recurses into every child and a sequential one that folds, visits each child twice. When the cost of the child subtree dwarfs the cost of the fold, the extra visit is negligible and the parallel loop wins. Hecate can express both and let measurement decide; Grafter can express only the first.

Where this stops working

Hecate proves correctness only up to a bounded tree depth, and only for the traversal template the programmer wrote, so a poor template produces no schedule and an unusual tree shape beyond the bound is unverified. The ILP path relies on a solver such as CPLEX, whose free edition fails on the larger instances in the artifact. Parallel traversals are validated rather than invented: the programmer must guess where parallelism might be legal. Performance results reuse Grafter’s workloads and show gains only past a tree size where parallel overhead is amortized, on the order of millions of nodes. Finally, the paper compares against FTL on the three grammars FTL can still run, since FTL is unmaintained, and against Grafter only on Grafter’s own five benchmarks.

Background

Solver-aided languages, and what domain-specific means here

Rosette lets a programmer write an ordinary interpreter for a language and obtain, for free, a verifier and a synthesizer for that language by executing the interpreter symbolically. The price of that generality is that the symbolic execution mirrors the interpreter’s control flow, so any program whose later behavior depends on earlier choices generates nested, history-guarded constraints. Hecate’s observation is that traversal scheduling has extra structure the generic engine cannot see: the order of locations is fixed by the template, and correctness is entirely about read-before-write. A layer that knows this can restate every assertion in a relational form that does not mention time, and the constraints that come out happen to be linear. The technique is domain-specific symbolic compilation: keep the interpreter, replace the encoding.

If you remember only three things

1. Efficient tree computation means scheduling attribute rules into few traversals, or parallel ones, without ever reading an attribute before it is written. Browser engines do this by hand and accumulate multi-year layout bugs; Grafter does it automatically but produces one always-fused, linked-list, serial answer; FTL needs experts to write Prolog; and the generic solver-aided approach of symbolically executing a traversal interpreter generates history-guarded constraints whose count grows as q to the power of n times k.
2. Hecate takes an attribute grammar, a symbolic traversal template with slots, and an example tree, and fills the slots with a CEGIS loop on Rosette. Its domain-specific symbolic compilation transpiles each candidate placement into a time-free trace of reads and writes, and a dependency operator turns traces into 0-1 integer linear constraints, at most (1 + n squared) q k states, that an ILP solver handles directly. Templates let the programmer express vector children and parallel visits, which Hecate verifies rather than discovers.
3. On Grafter's five benchmarks Hecate is 3.1 times faster than its own general-purpose encoding and 8 times faster than Grafter, with equivalent traversals; vector and parallel variants cut rendering time about 70 percent against unfused and 40 percent against Grafter, with parallelism adding 23 percent on large trees and over 75 percent total reduction on the AST benchmark; on real CSS grammars of 178 to 244 rules it needs 39 seconds where FTL needs 189 and the generic encoding never finishes. Limits: bounded verification depth, programmer-written templates, and a commercial ILP solver for the largest instances.

Check yourself

Check your understanding

1. What makes a concrete traversal correct in Hecate's formulation?
2. Why does the general-purpose symbolic compilation produce constraints that are hard to solve?
3. Predict what happens to the constraint "n1.h0 must be written before ι2 of n1 reads it" under the trace-to-ILP encoding.
4. What does the HecateV versus Grafter comparison on RenderTree show?
5. Why can a fully fused traversal be slower than a de-fused one?

Sources

The paper is “Tree Traversal Synthesis Using Domain-Specific Symbolic Compilation” by Yanju Chen, Junrui Liu, Yu Feng and Rastislav Bodík, University of California, Santa Barbara and University of Washington, published at ASPLOS 2022, pages 1030 to 1042, DOI 10.1145/3503222.3507751, under a Creative Commons Attribution licence. This explainer was written from the full text of the author-hosted copy, including its AST case-study appendix. Numbers are taken from Table 2 and Figures 9, 11, 15 and 16. The artifact, with both the domain-specific and general-purpose encodings, is archived on Zenodo (record 5748202).