WG211/M19Franchetti - Revision history

Eric at 21:33, 30 April 2019

2019-04-30T21:33:52Z

← Older revision		Revision as of 23:33, 30 April 2019
Line 4:		Line 4:

	See:		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		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		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		2. http://www.spiral.net/doc/papers/08510983_Spiral_IEEE_Final.pdf

Eric at 21:33, 30 April 2019

2019-04-30T21:33:35Z

← Older revision		Revision as of 23:33, 30 April 2019
Line 2:		Line 2:

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

Ups: Created page with "''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 wid..."

2019-04-08T13:53:01Z

Created page with "''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 wid..."

New page

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