TY - GEN
T1 - Formal verification of SSA-based optimizations for LLVM
AU - Zhao, Jianzhou
AU - Nagarakatte, Santosh
AU - Martin, Milo M.K.
AU - Zdancewic, Steve
PY - 2013
Y1 - 2013
N2 - Modern compilers, such as LLVM and GCC, use a static single assignment (SSA) intermediate representation (IR) to simplify and enable many advanced optimizations. However, formally verifying the correctness of SSA-based optimizations is challenging because SSA properties depend on a function's entire control-flow graph. This paper addresses this challenge by developing a proof technique for proving SSA-based program invariants and compiler optimizations. We use this technique in the Coq proof assistant to create mechanized correctness proofs of several "micro" transformations that form the building blocks for larger SSA optimizations. To demonstrate the utility of this approach, we formally verify a variant of LLVM's mem2reg transformation in Vellvm, a Coq-based formal semantics of the LLVM IR. The extracted implementation generates code with performance comparable to that of LLVM's unverified implementation.
AB - Modern compilers, such as LLVM and GCC, use a static single assignment (SSA) intermediate representation (IR) to simplify and enable many advanced optimizations. However, formally verifying the correctness of SSA-based optimizations is challenging because SSA properties depend on a function's entire control-flow graph. This paper addresses this challenge by developing a proof technique for proving SSA-based program invariants and compiler optimizations. We use this technique in the Coq proof assistant to create mechanized correctness proofs of several "micro" transformations that form the building blocks for larger SSA optimizations. To demonstrate the utility of this approach, we formally verify a variant of LLVM's mem2reg transformation in Vellvm, a Coq-based formal semantics of the LLVM IR. The extracted implementation generates code with performance comparable to that of LLVM's unverified implementation.
KW - Coq
KW - LLVM
KW - Single static assignment
UR - http://www.scopus.com/inward/record.url?scp=84883101134&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84883101134&partnerID=8YFLogxK
U2 - 10.1145/2462156.2462164
DO - 10.1145/2462156.2462164
M3 - Conference contribution
AN - SCOPUS:84883101134
SN - 9781450320146
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 175
EP - 186
BT - PLDI 2013 - Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation
T2 - 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013
Y2 - 16 June 2013 through 19 June 2013
ER -