@INPROCEEDINGS{asplos22-hecate,
  title     = "Tree Traversal Synthesis Using {Domain-Specific} Symbolic
               Compilation",
  booktitle = "Proceedings of the 27th {ACM} International Conference on
               Architectural Support for Programming Languages and Operating
               Systems",
  author    = "Chen, Yanju and Liu, Junrui and Feng, Yu and Bodik, Rastislav",
  abstract  = "Efficient computation on tree data structures is important in
               compilers, numeric computations, and web browser layout engines.
               Efficiency is achieved by statically scheduling the computation
               into a small number of tree traversals and by performing the
               traversals in parallel when possible. Manual design of such
               traversals leads to bugs, as observed in web browsers. Automatic
               schedulers avoid these bugs but they currently cannot explore a
               space of legal traversals, which prevents exploring the
               trade-offs between parallelism and minimizing the number of
               traversals. We describe Hecate, a synthesizer of tree traversals
               that can produce both serial and parallel traversals. A key
               feature is that the synthesizer is extensible by the programmer
               who can define a template for new kinds of traversals. Hecate is
               constructed as a solver-aided domain-specific language, meaning
               that the synthesizer is generated automatically by translating
               the tree traversal DSL to an SMT solver that synthesizes the
               traversals. We improve on the general-purpose solver-aided
               architecture with a scheduling-specific symbolic evaluation that
               maintains the engineering advantages solver-aided design but
               generates efficient ILP encoding that is much more efficient to
               solve than SMT constraints. On the set of Grafter problems,
               Hecate synthesizes traversals that trade off traversal fusion to
               exploit parallelism. Additionally, Hecate allows defining a tree
               data structure with an arbitrary number of children. Together,
               parallelism and data structure improvements accelerate the
               computation 2$\times$ on a tree rendering problem. Finally,
               Hecate's domain-specific symbolic compilation accelerates
               synthesis 3$\times$ compared to the general-purpose compilation
               to an SMT solver; when scheduling a CSS engine traversal, this
               ILP-based synthesis executes orders of magnitude faster.",
  publisher = "Association for Computing Machinery",
  pages     = "1030--1042",
  series    = "ASPLOS '22",
  year      =  2022,
  address   = "New York, NY, USA",
  keywords  = "tree traversal, program synthesis, symbolic compilation",
  location  = "Lausanne, Switzerland"
}