Nuno P. Lopes
Santosh Nagarakatte
Abstract
Compilers should not miscompile. Peephole optimizations, which perform local rewriting of the input program to improve the efficiency of generated code, are a persistent source of compiler bugs. We created Alive, a domain-specific language for writing optimizations and for automatically either proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures---but largely hides---the detailed semantics of the various kinds of undefined behavior. Alive has found numerous bugs in the LLVM compiler and is being used by LLVM developers.
- Bansal, S., Aiken, A. Automatic generation of peephole superoptimizers. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2006), 394--403. Google Scholar
Digital Library
- Buchwald, S. Optgen: A generator for local optimizations. In Proceedings of the 24th International Conference on Compiler Construction (CC) (2015).Google ScholarCross Ref
- Davidson, J.W., Fraser, C.W. Automatic generation of peephole optimizations. In Proceedings of the 1984 SIGPLAN Symposium on Compiler Construction (1984). Google ScholarDigital Library
- De Moura, L., Bjørner, N. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2008), 337--340. Google ScholarDigital Library
- Joshi, R., Nelson, G., Zhou, Y. Denali: A practical algorithm for generating optimal code. ACM Trans. Program. Lang. Syst. 28, 6 (Nov. 2006), 967--989. Google ScholarDigital Library
- Kundu, S., Tatlock, Z., Lerner, S. Proving optimizations correct using parameterized program equivalence. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (2009). Google ScholarDigital Library
- Le, V., Afshari, M., Su, Z. Compiler validation via equivalence modulo inputs. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (2014). Google ScholarDigital Library
- Lee, J., Kim, Y., Song, Y., Hur, C.-K., Das, S., Majnemer, D., Regehr, J., Lopes, N.P. Taming undefined behavior in LLVM. In Proceedings of the 38th annual ACM SIGPLAN conference on Programming Language Design and Implementation (2017). Google ScholarDigital Library
- Leroy, X. Formal verification of a realistic compiler. Commun. of the ACM 52, 7 (2009), 107--115. Google ScholarDigital Library
- Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J. Provably correct peephole optimizations with Alive. In Proceedings of the 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI) (2015). Google ScholarDigital Library
- Lopes, N.P., Monteiro, J. Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. Int. J. Softw. Tools Technol. Transf. 18, 4 (2016), 359--374. Google ScholarDigital Library
- Massalin, H. Superoptimizer: A look at the smallest program. In Proceedings of the 2nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (1987). Google ScholarCross Ref
- Menendez, D., Nagarakatte, S. Alive-infer: Data-driven precondition inference for peephole optimizations in LLVM. In Proceedings of the 38th annual ACM SIGPLAN conference on Programming Language Design and Implementation (2017). Google ScholarDigital Library
- Menendez, D., Nagarakatte, S., Gupta, A. Alive-FP: Automated verification of floating point based peephole optimizations in LLVM. In Proceedings of the 23rd International Symposium on Static Analysis (2016).Google ScholarCross Ref
- Morisset, R., Pawan, P., Nardelli, F.Z. Compiler testing via a theory of sound optimisations in the C11/C++11 memory model. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (2013). Google ScholarDigital Library
- Nötzli, A., Brown, F. LifeJacket: Verifying precise floating-point optimizations in LLVM. In Proceedings of the 5th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis (2016). Google ScholarDigital Library
- Pnueli, A., Siegel, M., Singerman, E. Translation validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (1998), 151--166. Google ScholarDigital Library
- Samet, H. Proving the correctness of heuristically optimized code. In Communications of the ACM (1978). Google ScholarDigital Library
- Schkufza, E., Sharma, R., Aiken, A. Stochastic superoptimization. In Proceedings of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2013). Google ScholarDigital Library
- Yang, X., Chen, Y., Eide, E., Regehr, J. Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (2011). Google ScholarDigital Library
- Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S. Formalizing the LLVM intermediate representation for verified program transformations. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2012). Google ScholarDigital Library
Index Terms
- Practical verification of peephole optimizations with Alive
Recommendations
Provably correct peephole optimizations with alive
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationCompilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the efficiency of LLVM code. These optimizations are individually difficult to get right, particularly in the ...
Provably correct peephole optimizations with alive
PLDI '15Compilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the efficiency of LLVM code. These optimizations are individually difficult to get right, particularly in the ...
Alive-Infer: data-driven precondition inference for peephole optimizations in LLVM
PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and ImplementationPeephole optimizations are a common source of compiler bugs. Compiler developers typically transform an incorrect peephole optimization into a valid one by strengthening the precondition. This process is challenging and tedious. This paper proposes ...
Comments