skip to main content
research-article

Formal verification of SSA-based optimizations for LLVM

Authors Info & Claims
Published:16 June 2013Publication History
Skip Abstract Section

Abstract

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.

References

  1. Static Single Assignment Book, 2012. Working draft available at http://ssabook.gforge.inria.fr/latest/book.pdf.Google ScholarGoogle Scholar
  2. A. W. Appel. SSA is functional programming. SIGPLAN Not., 33(4): 17--20, April 1998. ISSN 0362-1340. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. J. Aycock and N. Horspool. Simple generation of static single assignment form. In CC, 2000. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. G. Barthe, D. Demange, and D. Pichardie. A formally verified SSA-based middle-end - Static Single Assignment meets CompCert. In ESOP, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. J. O. Blech, S. Glesner, J. Leitner, and S. Mülling. Optimizing code generation from SSA form: A comparison between two formal correctness proofs in Isabelle/HOL. Electron. Notes Theor. Comput. Sci., 141(2):33--51, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. The Coq Proof Assistant Reference Manual (Version 8.3pl1). The Coq Development Team, 2011.Google ScholarGoogle Scholar
  7. R. Cytron, J. Ferrante, B. K. Rosen, M. N.Wegman, and F. K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. TOPLAS, 13:451--490, 1991. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. R. A. Kelsey. A correspondence between continuation passing style and static single assignment form. In IR, number 3, 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363--446, December 2009. ISSN 0168-7433. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. The LLVM Reference Manual (Version 3.0). The LLVM Development Team, 2011. http://llvm.org/releases/3.0/docs/LangRef.html.Google ScholarGoogle Scholar
  11. W. Mansky and E. L. Gunter. A framework for formal verification of compiler optimizations. In ITP, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. Y. Matsuno and A. Ohori. A type system equivalent to static single assignment. In PPDP, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. V. S. Menon, N. Glew, B. R. Murphy, A. McCreight, T. Shpeisman, A. Adl-Tabatabai, and L. Petersen. A verifiable SSA program representation for aggressive compiler optimization. In POPL, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. S. S. Muchnick. Advanced compiler design and implementation. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1997. ISBN 1-55860-320-4. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. V. C. Sreedhar and G. R. Gao. A linear time algorithm for placing"-nodes. In POPL, 1995. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. J.-B. Tristan and X. Leroy. Formal verification of translation validators: a case study on instruction scheduling optimizations. In POPL, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. J.-B. Tristan and X. Leroy. Verified validation of lazy code motion. In PLDI, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. J. B. Tristan and X. Leroy. A simple, verified validator for software pipelining. In POPL, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. B. Yakobowski. Étude sémantique dun langage intermédiaire de type Static Single Assignment. Rapport de dea (Master's thesis), ENS Cachan and INRIA Rocquencourt, Sept. 2004.Google ScholarGoogle Scholar
  20. X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In PLDI, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. J. Zhao and S. Zdancewic. Mechanized verification of computing dominators for formalizing compilers. In CPP, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. J. Zhao, S. Nagarakatte, M. M. K. Martin, and S. Zdancewic. For-malizing the LLVM intermediate representation for verified program transformations. In POPL, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Formal verification of SSA-based optimizations for LLVM

        Recommendations

        Comments

        Login options

        Check if you have access through your login credentials or your institution to get full access on this article.

        Sign in

        Full Access

        • Published in

          cover image ACM SIGPLAN Notices
          ACM SIGPLAN Notices  Volume 48, Issue 6
          PLDI '13
          June 2013
          515 pages
          ISSN:0362-1340
          EISSN:1558-1160
          DOI:10.1145/2499370
          Issue’s Table of Contents
          • cover image ACM Conferences
            PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation
            June 2013
            546 pages
            ISBN:9781450320146
            DOI:10.1145/2491956

          Copyright © 2013 ACM

          Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

          Publisher

          Association for Computing Machinery

          New York, NY, United States

          Publication History

          • Published: 16 June 2013

          Check for updates

          Qualifiers

          • research-article

        PDF Format

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader