The Synthesis Algorithm Behind Dexter
Translating Image Processing Code
How Does Dexter Work?
Unlike traditional compilers that rely on syntax-driven rules to translate code, Dexter uses program synthesis to re-write the input code. In other words, Dexter constructs and solves a search problem to discover semantically equivalent programs in the target language.
Unfortunately, this process is prohibitively expensive: even if we limit our scope to programs that involve only a handful of operations, the number of Halide programs to be considered orders in the tens of thousands.
Modular Search
Our key insight to make the search problem tractable in Dexter is to exploit domain-specific knowledge about image and array processing operations. In particular, we observe that we can decompose many such operations into three components:
- A Region of Interest (ROI) that describes the dimensionality of the operation and the bounds for each dimension within which the output is realized.
- The set of terminals used to compute the value of each location within the ROI. Such terminals can consist of numeric constants, program variables, or array reads.
- The computation performed using the aforementioned set of terminals to compute the values inside the ROI.
Dexter exploits this insight to decompose the overall synthesis problem into three separate synthesis sub-problems, each targeting one component above. To learn more about our 3-stage synthesis algorithm, read our paper.
Next Steps
See: Customize Duo.
Dexter is a compiler that rejuvenates legacy image and array processing C++ code by re-writing it to the Halide DSL, thus enabling cross-platform optimization and portability. Given an operation implemented in C++, Dexter uses Verified Lifting, a combination of program synthesis and verification, to discover the algorithm hidden in the low-level code. Once discovered, the algorithm is then automatically compiled to new hardware using Halide, avoiding manual reimplementation.
Publication: SIGGRAPH ASIA 2019
Presentation: Slide deck
Source Code: uwplse/dexter