STNG

"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."

http://stng.uwplse.org/

https://github.com/uwplse/stng

http://halide-lang.org/

http://uwplse.org/#projects