Gilles Barthe
David Pichardie
Skip Abstract Section
Abstract
CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler, faster optimizers. In fact, it has remained an open problem to verify formally an SSA-based compiler. We report on a formally verified, SSA-based middle-end for CompCert. In addition to providing a formally verified SSA-based middle-end, we address two problems raised by Leroy in [2009]: giving an intuitive formal semantics to SSA, and leveraging its global properties to reason locally about program optimizations.
- Alpern, B., Wegman, M. N., and Zadeck, F. K. 1988. Detecting equality of variables in programs. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’88). ACM Press, New York, 1--11. Google Scholar
Digital Library
- Appel, A. W. 1998a. Modern Compiler Implementation: In ML. Cambridge University Press, New York. Google ScholarDigital Library
- Appel, A. W. 1998b. SSA is functional programming. SIGPLAN Not. 33, 17--20. Google ScholarDigital Library
- Aycock, J. and Horspool, N. 2000. Simple generation of static single-assignment form. In Proceedings of the 9th International Conference on Compiler Construction, held as part of the Joint European Conferences on Theory and Practice of Software (CC/ETAPS’00). Lecture Notes in Computer Science, vol. 1781, Springer, 110--124. Google ScholarDigital Library
- Barthe, G., Demange, D., and Pichardie, D. 2012. A formally verified SSA-based middle-end-static single assignment meets compcert. In Proceedings of the 21st European Conference on Programming Languages and Systems (ESOP’12). Lecture Notes in Computer Science, vol. 7211, Springer, 47--66. Google ScholarDigital Library
- Blech, J. O., Glesner, S., Leitner, J., and Mülling, S. 2005. Optimizing code generation from SSA form: A comparison between two formal correctness proofs in isabelle/hol. J. Electron. Theor. Comput. Sci. 141, 2, 33--51. Google ScholarDigital Library
- Boissinot, B., Hack, S., Grund, D., Dupont De Dinechin, B., and Rastello, F. 2008. Fast liveness checking for ssa form programs. In Proceedings of the 6th Annual IEEE/ACM International Symposium on Code Generation and Optimization (CGO’08). ACM Press, New York, 35--44. Google ScholarDigital Library
- Boissinot, B., Darte, A., Rastello, F., Dupont De Dinechin, B., and Guillon, C. 2009. Revisiting out-of-ssa translation for correctness, code quality and efficiency. In Proceeding of the 7th Annual IEEE/ACM International Symposium on Code Generation and Optimization (CGO’09). IEEE Computer Society, 114--125. Google ScholarDigital Library
- Brandis, M. M. and Mössenböck, H. 1994. Single-pass generation of static single-assignment form for structured languages. ACM Trans. Program. Lang. Syst. 16, 6, 1684--1698. Google ScholarDigital Library
- Briggs, P., Cooper, K. D., and Simpson, L. T. 1997. Value numbering. Softw. Pract. Exper. 27, 6, 701--724. Google ScholarDigital Library
- Briggs, P., Cooper, K. D., Harvey, T. J., and Simpson, L. T. 1998. Practical improvements to the construction and destruction of static single assignment form. Softw. Pract. Exper. 28, 8, 859--881. Google ScholarDigital Library
- Brisk, P. 2006. Advances in static single assignment form and register allocation. Ph.D. dissertation AAI3254798, University of California, Los Angeles, CA. Google ScholarDigital Library
- Chlipala, A. 2008. Parametric higher-order abstract syntax for mechanized semantics. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP’08). ACM Press, New York, 143--156. Google ScholarDigital Library
- Chlipala, A. 2010. A verified compiler for an impure functional language. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10). ACM Press, New York, 93--106. Google ScholarDigital Library
- Chow, F., Chan, S., Kennedy, R., Liu, S.-M., Lo, R., and Tu, P. 1997. A new algorithm for partial redundancy elimination based on ssa form. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’97). ACM Press, New York, 273--286. Google ScholarDigital Library
- CompCertSSA. 2012. Companion web page. http://compcertssa.gforge.inria.fr.Google Scholar
- Cooper, K. D., Harvey, T. J., and Kennedy, K. 2000. A simple, fast dominance algorithm. Tech. rep., Rice University. www.cs.rice.edu/~keith/Embed/dom.pdf.Google Scholar
- Cytron, R., Ferrante, J., Rosen, B. K., Wegman, M. N., and Zadeck, F. K. 1991. Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13, 4, 451--490. Google ScholarDigital Library
- Dargaye, Z. and Leroy, X. 2007. Mechanized verification of CPS transformations. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’07). 211--225. Google ScholarDigital Library
- Hack, S., Grund, D., and Goos, G. 2006. Register allocation for programs in SSA form. In Proceedings of the 15th International Conference on Compiler Construction (CC’06). 247--262. Google ScholarDigital Library
- Knoop, J., Rüthing, O., and Steffen, B. 1992. Lazy code motion. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’92). ACM Press, New York, 224--234. Google ScholarDigital Library
- Knoop, J., Koschützkil, D., and Steffen, B. 1998. Basic-block graphs: Living dinosaurs? In Proceedings of the 7th International Conference on Compiler Construction, held as part of the Joint European Conferences on Theory and Practice of Software (CC/ETAPS’98). 65--79. Google ScholarDigital Library
- Lengauer, T. and Tarjan, R. E. 1979. A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst. 1, 1, 121--141. Google ScholarDigital Library
- Leroy, X. 2009. A formally verified compiler back-end. J. Autom. Reason. 43, 4, 363--446. Google ScholarDigital Library
- Mansky, W. and Gunter, E. 2010. A framework for formal verification of compiler optimizations. In Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP’10). 371--386. Google ScholarDigital Library
- Matsuno, Y. and Ohori, A. 2006. A type system equivalent to static single assignment. In Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’06). ACM Press, New York, 249--260. Google ScholarDigital Library
- Menon, V., Glew, N., Murphy, B. R., Mccreight, A., Shpeisman, T., Adl-Tabatabai, A. R., and Petersen, L. 2006. A verifiable ssa program representation for aggressive compiler optimization. In Proceedings of the Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’06). ACM Press, New York, 397--408. Google ScholarDigital Library
- Necula, G. 2000. Translation validation for an optimizing compiler. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’00). ACM Press, New York, 83--94. Google ScholarDigital Library
- Pnueli, A., Siegel, M., and Singerman, E. 1998. Translation validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’98). 151--166. Google ScholarDigital Library
- Rideau, L., Serpette, B. P., and Leroy, X. 2008. Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves. J. Autom. Reason. 40, 4, 307--326. Google ScholarDigital Library
- Samet, H. 1975. Automatically proving the correctness of translations involving optimized code. Ph.D. dissertation STAN-CS-75-498, Computer Science Department, Stanford University. Google ScholarDigital Library
- Schneider, S. 2013. Semantics of an intermediate language for program transformation. Master’s thesis, Saarland University.Google Scholar
- Sreedhar, V. C., Ju, R., Gillies, D. M., and Santhanam, V. 1999. Translating out of static single assignment form. In Proceedings of the 6th International Symposium on Static Analysis (SAS’99). 194--210. Google ScholarDigital Library
- Stepp, M., Tate, R., and Lerner, S. 2011. Equality-based translation validator for LLVM. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11). 737--742. Google ScholarDigital Library
- Tate, R., Stepp, M., Tatlock, Z., and Lerner, S. 2009. Equality saturation: A new approach to optimization. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’09). ACM Press, New York, 264--276. Google ScholarDigital Library
- Tristan, J. B. and Leroy, X. 2009. Verified validation of lazy code motion. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’09). ACM Press, New York, 316--326. Google ScholarDigital Library
- Tristan, J. B. and Leroy, X. 2010. A simple, verified validator for software pipelining. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10). ACM Press, New York, 83--92. Google ScholarDigital Library
- Tristan, J. B., Govereau, P., and Morrisett, G. 2011. Evaluating value-graph translation validation for llvm. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’11). ACM Press, New York, 295--305. Google ScholarDigital Library
- Zhao, J. 2013. Formalizing an SSA-based compiler for verified advanced program transformations. Ph.D. dissertation, University of Pennsylvania. http://www.cis.upenn.edu/~stevez/vellvm/Zhao13.pdf.Google Scholar
- Zhao, J. and Zdancewic, S. 2012. Mechanized verification of computing dominators for formalizing compilers. In Proceedings of the 2nd International Conference on Certified Programs and Proofs (CPP’12). 27--42. Google ScholarDigital Library
- Zhao, J., Zdancewic, S., Nagarakatte, S., and Martin, M. 2012. Formalizing the LLVM intermediate representation for verified program transformation. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12). ACM Press, New York, 427--440. Google ScholarDigital Library
- Zhao, J., Nagarakatte, S., Martin, M., and Zdancewic, S. 2013. Formal verification of SSA-based optimizations for LLVM. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’13). ACM Press, New York, 175--186. Google ScholarDigital Library
Index Terms
- Formal Verification of an SSA-Based Middle-End for CompCert
Recommendations
Formal verification of SSA-based optimizations for LLVM
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and ImplementationModern 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 ...
Formal verification of SSA-based optimizations for LLVM
PLDI '13Modern 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 ...
A formally verified SSA-Based middle-end: Static single assignment meets compcert
ESOP'12: Proceedings of the 21st European conference on Programming Languages and SystemsCompCert is a formally verified compiler that generates compact and efficient PowerPC, ARM and x86 code for a large and realistic subset of the C language. However, CompCert foregoes using Static Single Assignment (SSA), an intermediate representation ...
Comments