The Semantics of SPIRAL
Seminar Modèles et Algorithmes Déterministes: CASYS
11/06/2015 - 09:30 Mr Jérémy Johnson Salle 1 - Tour IRMA
In this talk we review the SPIRAL algorithm and code generation system and outline several ideas for defining and verifying the semantics of SPIRAL expressions. The SPIRAL (www.spiral.net) system generates state-of-the-art code for various digital signal processing algorithms on a variety of computing platforms and has been used by Intel for their IPP and MKL libraries. SPIRAL uses rewrite rules, at multiple levels, to transform mathematical expressions into code. At the highest level SPIRAL specifies a computation with a high-level mathematical description and then transforms the specification into mathematically equivalent expressions capturing different algorithm for performing the desired computation. Further mathematical transformations are performed to enhance parallelism and vectorization. Then the resulting mathematical expression is transformed into a lower level mathematical expression that allows various optimizations such as loop merging. Finally, the lower level expression is, in a fairly straightforward way, transformed into code which is then further optimized using code level transformations. The important point, is that at each level there is a well defined mathematical semantics and it is possible, using this semantics, to prove correctness of the rules at each level. Verification proofs are carried out formally using the rewrite system Maude and the proof assistant Isabelle. In this talk we outline and show examples of how this is done. Bio: Jeremy Johnson is Professor of Computer Science and Electrical and Computer Engineering at Drexel University. He served as the first Department Head for the newly formed Computer Science department from 2002-2012. His research interests include algebraic algorithms, computer algebra systems, computer verification, programming languages and compilers, high performance computing, and automated performance tuning. He directs Drexel's Applied Symbolic Computation lab which focuses on the use of symbolic computation to derive and optimize the implementation of algorithms with mathematical structure. He recently completed a term as chair of the ACM special interest group on symbolic and algebraic manipulation (SIGSAM) and serves on the editorial board of the journal of Applicable Algebra in Engineering, Communication and Computing. He, along with colleagues at CMU and UIUC, initiated the SPIRAL project on the automatic generation and optimization of digital signal processing algorithms and was a key part of the DARPA funded Very High Dimensionality Study, which developed the mathematical framework and a prototype domain specific language (Tensor Product Language) and special purpose compiler that led to the SPL language used by SPIRAL. He is currently working on a DARPA supported project to develop a high assurance version of SPIRAL that produces efficient and verified controllers and monitors, that are safe under various attacks, for cyber physical systems.