CS-Kolloquium: Franz Franchetti

Die Fakultät für Informatik der Universität Wien lädt Sie herzlich ein zum CS-Kolloquium

„Formal Software Synthesis of Computational Kernels“
Franz Franchetti
Associate Research Professor, ECE Department, Carnegie Mellon University, USA

27. Mai 2015, 15:00 Uhr, Hörsaal 3
(Der Vortrag wird in englischer Sprache stattfinden)

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

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.