AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
We have shown that an important class of optimizations in LLVM— peephole optimizations—can be formalized in Alive, a new language that makes optimizations much more concise than when they are embedded in C++ code, while supporting automated proofs of correctness

Provably correct peephole optimizations with alive

PLDI, no. 6 (2015): 22-32

Cited by: 92|Views219
EI

Abstract

Compilers 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 presence of undefined behavior; taken together they represent a persistent source of bugs. T...More

Code:

Data:

0
Introduction
  • Compiler optimizations should be efficient, effective, and correct— but meeting all of these goals is difficult.
  • Random testing [15, 23, 37] is one approach to improve the correctness of compilers; it has been shown to be effective, but testing misses bugs.
  • Creating CompCert required several person-years of proof engineering and the resulting tool does not provide a good value proposition for many real-world use cases: it implements a subset of C, optimizes only lightly, and does not yet support x86-64 or the increasingly important vector extensions to x86 and ARM.
  • Production compilers are constantly improved to support new language standards and to obtain the best possible performance on emerging architectures
Highlights
  • Compiler optimizations should be efficient, effective, and correct— but meeting all of these goals is difficult
  • We have shown that an important class of optimizations in LLVM— peephole optimizations—can be formalized in Alive, a new language that makes optimizations much more concise than when they are embedded in C++ code, while supporting automated proofs of correctness
  • After an Alive transformation has been proved correct, it can be automatically translated into C++ that can be included in an optimization pass
  • Our first goal was to create a tool that is useful for LLVM developers
  • We would like to see a large part of InstCombine replaced with code generated by Alive; we are still working towards that goal
Results
  • The authors translated hundreds of peephole optimizations from LLVM into Alive. The authors verified them, the authors inferred optimal nsw/nuw/exact attributes for them, and the authors translated the Alive optimizations into C++ that the authors linked into LLVM and used the resulting optimizer to build LLVM’s test suite and the SPEC INT 2000 and 2006 benchmarks.

    6.1 Translating and Verifying InstCombine

    LLVM’s InstCombine pass rewrites expression trees to reduce their cost, but does not change the control-flow graph.
  • The authors translated hundreds of peephole optimizations from LLVM into Alive.
  • The authors inferred optimal nsw/nuw/exact attributes for them, and the authors translated the Alive optimizations into C++ that the authors linked into LLVM and used the resulting optimizer to build LLVM’s test suite and the SPEC INT 2000 and 2006 benchmarks.
  • Table 3 summarizes the 334 InstCombine transformations that the authors translated to Alive.
  • Eight (2.4%) of these could not be proved correct; the authors reported these erroneous transformations to the LLVM developers, who confirmed and fixed them.
  • The authors re-translated the fixed optimizations to Alive and proved them correct.
  • Out of the remaining 694 transformations that the authors did not translate, some cannot yet be expressed in Alive and the rest the authors have not had time to translate
Conclusion
  • The authors have shown that an important class of optimizations in LLVM— peephole optimizations—can be formalized in Alive, a new language that makes optimizations much more concise than when they are embedded in C++ code, while supporting automated proofs of correctness.
  • The authors' first goal was to create a tool that is useful for LLVM developers.
  • The authors believe this goal has been accomplished.
  • The authors would like to see a large part of InstCombine replaced with code generated by Alive; the authors are still working towards that goal
Tables
  • Table1: The constraints for Alive’s arithmetic instructions to be defined. <u is unsigned less-than. B is the bitwidth of the operands in the Alive instruction. INT MIN is the smallest signed integer value for a given bitwidth
  • Table2: The constraints for Alive’s arithmetic instructions to be poison-free. >>u and ÷u are the unsigned shift and division operations. B is the bitwidth of the operands in the Alive instruction. SExt(a, n) sign-extends a by n bits; ZExt(a, n) zero-extends a by n bits
  • Table3: The total number of optimizations, the number of optimizations that we translated into Alive, and the number of translated optimizations that were wrong, for each file in InstCombine expression with one that is defined for a smaller range of inputs than was the original expression. There were four bugs in this category. We also found two bugs where the value of an expression was incorrect for some inputs, and two bugs where a transformation would generate a poison value for inputs that the original expression did not
Download tables as Excel
Related work
  • Prior research on improving compiler correctness can be broadly classified into compiler testing tools, formal reasoning frameworks for compilers, and domain specific languages (DSLs). DSLs for compiler optimizations are the most closely related work to Alive. These include languages based on graph rewriting [2, 21, 27], regular expressions [12], computation tree logic (CTL) [14], type systems [28], and rewrite rules [16, 36]. While Alive is perhaps most similar to high-level rewrite patterns [13, 20], it differs in its extensive treatment of undefined behavior, which is heavily exploited by LLVM and other aggressive modern compilers.

    Peephole optimization patterns for a particular ISA can be generated from an ISA specification [6]. In contrast to compiler optimizations, optimized code sequences can be synthesized either with peephole pattern generation or through superoptimization [3, 11, 22, 30, 33].
Funding
  • This paper is based upon work supported in part by NSF CAREER Award CCF–1453086, NSF Award CNS–1218022, and a Google Faculty Award
Reference
  • W. Ackermann. Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics, 1954.
    Google ScholarLocate open access versionFindings
  • U. Aßmann. How to uniformly specify program analysis and transformation with graph rewrite systems. In Proc. of the 6th International Conference on Compiler Construction, pages 121–135, 1996.
    Google ScholarLocate open access versionFindings
  • S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. In Proc. of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 394–403, 2006.
    Google ScholarLocate open access versionFindings
  • S. Buchwald. Optgen: A generator for local optimizations. In Proc. of the 24th International Conference on Compiler Construction (CC), pages 171–189, Apr. 2015.
    Google ScholarLocate open access versionFindings
  • 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. ACM Trans. Program. Lang. Syst., 13(4):451–490, Oct. 1991.
    Google ScholarLocate open access versionFindings
  • J. W. Davidson and C. W. Fraser. Automatic generation of peephole optimizations. In Proc. of the 1984 SIGPLAN Symposium on Compiler Construction, pages 111–116, 1984.
    Google ScholarLocate open access versionFindings
  • L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340, 2008.
    Google ScholarLocate open access versionFindings
  • S. Dissegna, F. Logozzo, and F. Ranzato. Tracing compilation by abstract interpretation. In Proc. of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 47–59, 2014.
    Google ScholarLocate open access versionFindings
  • S. Guyer and C. Lin. Broadway: A compiler for exploiting the domainspecific semantics of software libraries. Proceedings of the IEEE, 93 (2), 2005.
    Google ScholarLocate open access versionFindings
  • C. Hawblitzel, S. K. Lahiri, K. Pawar, H. Hashmi, S. Gokbulut, L. Fernando, D. Detlefs, and S. Wadsworth. Will you still compile me tomorrow? Static cross-version compiler validation. In Proc. of the 9th Joint Meeting on Foundations of Software Engineering (FSE), 2013.
    Google ScholarLocate open access versionFindings
  • R. Joshi, G. Nelson, and Y. Zhou. Denali: A practical algorithm for generating optimal code. ACM Trans. Program. Lang. Syst., 28(6): 967–989, Nov. 2006.
    Google ScholarLocate open access versionFindings
  • D. Kozen and M.-C. Patron. Certification of compiler optimizations using Kleene algebra with tests. In Proc. of the 1st International Conference on Computational Logic, pages 568–582, 2000.
    Google ScholarLocate open access versionFindings
  • S. Kundu, Z. Tatlock, and S. Lerner. Proving optimizations correct using parameterized program equivalence. In Proc. of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 327–337, 2009.
    Google ScholarLocate open access versionFindings
  • D. Lacey, N. D. Jones, E. Van Wyk, and C. C. Frederiksen. Compiler optimization correctness by temporal logic. Higher Order Symbol. Comput., 17(3):173–206, Sept. 2004.
    Google ScholarLocate open access versionFindings
  • V. Le, M. Afshari, and Z. Su. Compiler validation via equivalence modulo inputs. In Proc. of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 216–226, 2014.
    Google ScholarLocate open access versionFindings
  • S. Lerner, T. Millstein, E. Rice, and C. Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. In Proc. of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 364–377, 2005.
    Google ScholarLocate open access versionFindings
  • X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009.
    Google ScholarLocate open access versionFindings
  • LLVM Developers. LLVM Language Reference Manual. Available from http://llvm.org/docs/LangRef.html, 2014.
    Findings
  • N. P. Lopes and J. Monteiro. Weakest precondition synthesis for compiler optimizations. In Proc. of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation, pages 203–221, 2014.
    Google ScholarLocate open access versionFindings
  • N. P. Lopes and J. Monteiro. Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. Int. J. Softw. Tools Technol. Transf., 2015.
    Google ScholarLocate open access versionFindings
  • W. Mansky and E. Gunter. A cross-language framework for verifying compiler optimizations. In Proc. of the 5th Workshop on Syntax and Semantics of Low-Level Languages, 2014.
    Google ScholarLocate open access versionFindings
  • H. Massalin. Superoptimizer: A look at the smallest program. In Proc. of the 2nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 122–126, 1987.
    Google ScholarLocate open access versionFindings
  • W. M. McKeeman. Differential testing for software. Digital Technical Journal, 10(1):100–107, Dec. 1998.
    Google ScholarLocate open access versionFindings
  • R. Morisset, P. Pawan, and F. Z. Nardelli. Compiler testing via a theory of sound optimisations in the C11/C++11 memory model. In Proc. of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 187–196, 2013.
    Google ScholarLocate open access versionFindings
  • G. C. Necula. Translation validation for an optimizing compiler. In Proc. of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, pages 83–94, 2000.
    Google ScholarLocate open access versionFindings
  • A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Proc. of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 151–166, 1998.
    Google ScholarLocate open access versionFindings
  • N. Ramsey, J. Dias, and S. P. Jones. Hoopl: A modular, reusable library for dataflow analysis and transformation. In Proc. of the 3rd ACM Symposium on Haskell, 2010.
    Google ScholarLocate open access versionFindings
  • A. Saabas and T. Uustalu. Program and proof optimizations with type systems. The Journal of Logic and Algebraic Programming, 77(1–2): 131–154, 2008.
    Google ScholarLocate open access versionFindings
  • H. Samet. Proving the correctness of heuristically optimized code. In Communications of the ACM, 1978.
    Google ScholarLocate open access versionFindings
  • E. Schkufza, R. Sharma, and A. Aiken. Stochastic superoptimization. In Proc. of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2013.
    Google ScholarLocate open access versionFindings
  • T. A. L. Sewell, M. O. Myreen, and G. Klein. Translation validation for a verified OS kernel. In Proc. of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 471– 482, 2013.
    Google ScholarLocate open access versionFindings
  • M. Stepp, R. Tate, and S. Lerner. Equality-based translation validator for LLVM. In Proc. of the 23rd International Conference on Computer Aided Verification, pages 737–742, 2011.
    Google ScholarLocate open access versionFindings
  • R. Tate, M. Stepp, and S. Lerner. Generating compiler optimizations from proofs. In Proc. of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010.
    Google ScholarLocate open access versionFindings
  • J.-B. Tristan, P. Govereau, and G. Morrisett. Evaluating value-graph translation validation for LLVM. In Proc. of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 295–305, 2011.
    Google ScholarLocate open access versionFindings
  • V. Vafeiadis, T. Balabonski, S. Chakraborty, R. Morisset, and F. Z. Nardelli. Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In Proc. of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015.
    Google ScholarLocate open access versionFindings
  • D. L. Whitfield and M. L. Soffa. An approach for exploring code improving transformations. ACM Trans. Program. Lang. Syst., 19(6): 1053–1084, Nov. 1997.
    Google ScholarLocate open access versionFindings
  • X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In Proc. of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 283– 294, 2011.
    Google ScholarLocate open access versionFindings
  • A. Zaks and A. Pnueli. CoVaC: Compiler validation by program analysis of the cross-product. In Proc. of the 15th International Symposium on Formal Methods, pages 35–51, 2008.
    Google ScholarLocate open access versionFindings
  • J. Zhao, S. Nagarakatte, M. M. Martin, and S. Zdancewic. Formalizing the LLVM intermediate representation for verified program transformations. In Proc. of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 427–440, 2012.
    Google ScholarLocate open access versionFindings
  • J. Zhao, S. Nagarakatte, M. M. Martin, and S. Zdancewic. Formal verification of SSA-based optimizations for LLVM. In Proc. of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 175–186, 2013.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科