Abstract
In this short course 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. Students will learn how abstraction of algorithms, computer architectures, and program transformations enable full automation of the production of highly tuned computational software. Abstraction and representation are core issues we address and we will extract lessons on how to make the correct design choices, which require a thorough understanding of the problem domain. The goal is that students will be able to apply these lessons to their application areas of interest.
Bio
Franz Franchetti is an Associate Research Professor with the Department of Electrical and Computer Engineering at Carnegie Mellon University. He received the Dipl.-Ing. (M.Sc.) degree in Technical Mathematics and the Dr. techn. (Ph.D.) degree in Computational Mathematics from the Vienna University of Technology in 2000 and 2003, respectively. In 2006 he received the Gordon Bell Prize (Peak Performance Award) and in 2010 he won the HPC Challenge Class II Award (most productive system). In 2013 he was awarded the CIT Dean's Early Career Fellowship by the College of Engineering of Carnegie Mellon University. Dr. Franchetti's research focuses on automatic performance tuning and program generation for emerging parallel platforms and algorithm/hardware co-synthesis. He leads two DARPA projects in the HACMS and PERFECT program and is PI/Co-PI on a number of federal and industry grants. He is one of the principal designers of the Spiral system.