The Semantics of SPIRAL

français

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.