WG211/M19Franchetti

Formal Software Synthesis of Computational Kernels by Franz Franchetti

In this talk we address the question of how to automatically map computational kernels across a wide range of computing platforms to highly efficient code, and prove the correctness of the synthesized code. This addresses two fundamental problems that software developers are faced with: performance portability across the ever-changing landscape of parallel platforms, and verifiable correctness of sophisticated floating-point code. The problem is attacked as follows: We develop a formal framework to capture computational algorithms, computing platforms, and program transformations of interest, using a unifying mathematical formalism we call operator language (OL). Then we cast the problem of synthesizing highly optimized computational kernels for a given machine as a strongly constrained optimization problem that is solved by a multi-stage rewriting system. Since all rewrite steps are semantics preserving identity operations, our approach allows us to formally prove the equivalence between the kernel specification and the synthesized program. We have implemented this approach as part of the Spiral system where we have formalized a selection of computational kernels from the signal and image processing domain, software-defined radio, and robotic vehicle control. We have targeted platforms spanning from mobile devices as well as desktop and server multicore processors to large high performance and supercomputing systems. Our provably correct synthesized vehicle safety monitors and controllers have been demonstrated on an unmanned ground robot and a passenger car.

See:

1. Franz Franchetti, Tze Meng Low, Doru Thom Popovici, Richard M. Veras, Daniele G. Spampinato, Jeremy R. Johnson, Markus Püschel, James C. Hoe, and José M. F. Moura. SPIRAL: Extreme Performance Portability Proceedings of the IEEE special issue on From High Level Specification to High Performance Code, Vol. 206, No. 11, 2018

2. http://www.spiral.net/doc/papers/08510983_Spiral_IEEE_Final.pdf