Automatically leverage GPUs for your high-performance computation with verified lifting
High-performance codes are prevalent in many domains (image processing, physical simulations, etc). These codes are often manually tuned over long periods of time for performance. Unfortunately, newly emerged architectures and software frameworks render such tuning obsolete, and rewriting legacy codes, either manually for each application or by implementing a new compiler, to leverage the new features offered by the new architectures is a big pain.
Verified lifting is a new technique that automatically rewrites input codes from source to target language. Rather than manually writing rules to translate source language constructs to the target language, verified lifting uses program synthesis to automatically search for rewrites in the target language given a piece of input code. Any found candidate is formally verified using theorem provers to guarantee that it preserves the same program semantics as the original.
Stng is a compiler built using verified lifting. It takes in input codes in Fortran and automatically rewrites them to Halide, a new high-performance domain-specific language that leverages GPUs for computation. We have used Stng to compile real-world high-performance applications consisting of stencil computations and the resulting applications achieved median performance speedups of 4.1x and up to 24x as compared to the original.
Stng is open-source software available on GitHub. Please feel free to submit comments, issues, and pull requests there!
- Our work has been featured in the DoE's Discovery Magazine!
- We presented Stng at PLDI this year. The link includes the presentation video and slides.
 Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, Armando Solar-Lezama,
Verified Lifting of Stencil Computations, PLDI 2016.
If you have any questions, want to keep up-to date, or just like to say hi, please sign up on our mailing list!