Tata Institute of Fundamental Research
Lightweight Formal Methods for LLVM Verification
STCS Seminar
Speaker:
Santosh Nagarakatte (Rutgers University
Department of Computer Science
New Brunswick
United States of America)
Organiser:
Ashutosh Gupta
Date:
Friday, 5 Aug 2016, 15:00 to 16:00
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
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.
| Speaker: | Santosh Nagarakatte (Rutgers University Department of Computer Science New Brunswick United States of America) |
| Organiser: | Ashutosh Gupta |
| Date: | Friday, 5 Aug 2016, 15:00 to 16:00 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
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.
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.