Lightweight Formal Methods for LLVM Verification

Peephole optimizations  perform local rewriting to improve the efficiency of the code input to the compiler. These optimizations are a persistent source of bugs.  The talk will present Alive and Alive-FP, domain-specific languages for writing integer and floating-point related peephole optimizations in LLVM, respectively.  A transformation expressed in these DSLs is shown to be correct automatically by encoding the transformation into constraints whose validity is checked using a Satisfiability Modulo Theory (SMT) solver. Furthermore, an optimization expressed in the DSL can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass.

These DSL’s  are based on an attempt to balance usability and formal methods. We have discovered numerous bugs in the LLVM compiler and the Alive tool is actively used by LLVM developers to check new optimizations. I will also highlight  the challenges in incorporating lightweight formal methods in the tool-chain of the compiler developer and the lessons learned in this project. I will conclude by briefly describing other active projects in my group on approximation, parallel program testing, and verification.

Bio: Santosh Nagarakatte is an Assistant Professor of Computer Science at Rutgers University. He obtained his PhD from the University of Pennsylvania in 2012. His research interests are in Hardware-Software Interfaces spanning Programming Languages, Compilers, Software Engineering, and Computer Architecture. His papers have been selected as IEEE MICRO TOP Picks papers of computer architecture conferences in 2010 and 2013. He has received the NSF CAREER Award in 2015, ACM SIGPLAN PLDI 2015 Distinguished Paper Award, ACM SIGSOFT ICSE 2016 Distinguished Paper Award, and the Google Faculty Research Award in 2014 for his research on  LLVM compiler verification.