Developments in hardware have delivered formidable computing power. Yet, the increased hardware complexity has made it a real challenge to develop software that exploits hardware to its full potential. Numerous approaches have been explored to help programmers turn naive code into high-performance code, finely tuned for the targeted hardware. However, these approaches have inherent limitations, and it remains common practice for programmers seeking maximal performance to follow the tedious and error-prone route of writing optimized code by hand.
In this talk I will present OptiTrust, an interactive source-to-source optimization framework. The programmer develops a script describing a series of code transformations. The framework provides continuous feedback in the form of human-readable diff s over conventional C code. OptiTrust supports advanced code transformations, including transformations exploited by the state-of-the-art DSL tools Halide and TVM, and transformations beyond the reach of existing tools. OptiTrust also supports user-defined transformations, as well as defining complex transformations by composition of simpler transformations.
Crucially, to check the validity of code transformations, OptiTrust leverages a static resource analysis in a simplified form of Separation Logic. Our analysis exploits user-provided annotations on functions and loops, and deduces precise resource usage throughout the code. Through three representative case studies, we demonstrate how OptiTrust can be employed to produce state-of-the-art, high-performance programs.
