Dexter

A Compiler for Lifting C++ Code to Halide

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.

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:

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