Title: A System for Faster Software Verification and Better Compiler Optimizations through Symbiosis
Date: Tuesday, May 7th, 2024
Time: 3:00 - 5:00 PM EDT
Location: Klaus 2100
Virtual Link: Teams (Link)
Sharjeel Khan
Ph.D. Student
School of Computer Science
College of Computing
Georgia Institute of Technology
Committee:
Dr. Santosh Pande (Advisor) – School of Computer Science, Georgia Institute of Technology
Dr. Vivek Sarkar – School of Computer Science, Georgia Institute of Technology
Dr. Qirun Zhang – School of Computer Science, Georgia Institute of Technology
Dr. Vijay Ganesh – School of Computer Science, Georgia Institute of Technology
Abstract:
Despite numerous advancements over the years, both compilers and software verification have limitations in terms of their abilities. Due to the conservative nature of static data-flow analysis, compiler optimizations are restricted in terms of their applicability and effectiveness. On the other hand, whole-program software verification takes a long time on some real-life applications and does not seem to scale. Current approaches to optimizations do not seem to leverage verification and vice versa. In this work, we showcase the symbiotic relationship between compiler analyses and software verification, where each uses the other's advancements to improve its own techniques.
This proposal shows both directions of the symbiotic relationship are extremely valuable. We first present a framework called VICO that converts conservative dependence or alias constraints into invariants that are verified in a demand-driven way. These verified invariants lead to better auto-parallelization and loop transformations at the source level, and better register allocation and global value numbering (GVN), at the IR level. In the second work, we present a framework called CompVerif which leverages smart compiler analysis and reinforcement learning to speed up software verification. Specifically, we use a novel bi-directional dataflow analysis to detect variables affecting the verifier constructs like asserts, errors, or non-determinism variables. This analysis is used by our inliner to perform smart inlining for verification. At the verifier level, we use reinforcement learning to guide counterexample-guided abstraction and refinement (CEGAR) used by software verification.
In the last work, we propose a more complete framework that combines both directions of the symbiotic relationship seen in VICO and CompVerif. Specifically, we utilize MLIR as the bridge point between compiler analyses and software verification. By utilizing MLIR’s many dialects and lowering scheme, our goal is twofold: (1) to leverage domain-specific compiler analyses and optimizations at each stage of lowering to simplify programs for general software verification or domain-specific verification and (2) to verify domain-specific properties for better domain-specific optimizations. Building on our current results, we hope to demonstrate the significant benefits of such a symbiotic approach.