Abstract
Domain-specific languages (DSLs) are prevalent across many application domains. Such languages let developers easily express computations using high-level abstractions that result in performant implementations. To leverage DSLs, however, application developers need to master the DSL’s syntax and manually rewrite existing code. Compilers can aid in this effort, but building them requires designing and implementing syntax transformation rules, which is often a tedious and error-prone process.
In this talk, I will discuss how we view compilation as program synthesis: given source code to compile, our goal is to synthesize a program written in the target DSL that is the most performant (in terms of execution time, etc) and is semantically equivalent to the input. As searching for all possible programs in the target language is intractable, I will describe verified lifting, where we first "lift" the source code into a high-level summary that captures the semantics of the input, and subsequently generate executable code in the target language from the summary. Much of these two steps is driven by synthesis. I will argue that this approach makes compilers much easier to construct and maintain, and will illustrate verified lifting using a number of DSL compilers we have constructed. This includes Dexter (dexter.uwplse.org), which translates C++ image processing codes into the Halide DSL, with the translated code now shipping with Adobe Photoshop.