research-article

Public Access

Termination-checking for LLVM peephole optimizations

Authors:

David Menendez,

Santosh NagarakatteAuthors Info & Claims

ICSE '16: Proceedings of the 38th International Conference on Software Engineering

Pages 191 - 202

https://doi.org/10.1145/2884781.2884809

Published: 14 May 2016 Publication History

Abstract

Mainstream compilers contain a large number of peephole optimizations, which perform algebraic simplification of the input program with local rewriting of the code. These optimizations are a persistent source of bugs. Our recent research on Alive, a domain-specific language for expressing peephole optimizations in LLVM, addresses a part of the problem by automatically verifying the correctness of these optimizations and generating C++ code for use with LLVM.

This paper identifies a class of non-termination bugs that arise when a suite of peephole optimizations is executed until a fixed point. An optimization can undo the effect of another optimization in the suite, which results in non-terminating compilation. This paper (1) proposes a methodology to detect non-termination bugs with a suite of peephole optimizations, (2) identifies the necessary condition to ensure termination while composing peephole optimizations, and (3) provides debugging support by generating concrete input programs that cause non-terminating compilation. We have discovered 184 optimization sequences, involving 38 optimizations, that cause non-terminating compilation in LLVM with Alive-generated C++ code.

References

[1]

LLVM PatternMatch. http://llvm.org/docs/doxygen/html/PatternMatch_8h.html. Retrieved 2016-02-12.

[2]

A. Balestrat. CCG: A random C code generator. https://github.com/Merkil/ccg/. Retrieved 2016-02-12.

[3]

S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 394--403, 2006.

Digital Library

[4]

S. Buchwald. Optgen: A generator for local optimizations. In Proceedings of the 24th International Conference on Compiler Construction (CC), pages 171--189, 2015.

[5]

J. Burnim, N. Jalbert, C. Stergiou, and K. Sen. Looper: Lightweight detection of infinite loops at runtime. In Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 161--169, 2009.

Digital Library

[6]

M. Carbin, S. Misailovic, M. Kling, and M. C. Rinard. Detecting and escaping infinite loops with Jolt. In Proceedings of the 25th European conference on Object-oriented programming (ECOOP), pages 609--633, 2011.

Digital Library

[7]

B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 415--426, 2006.

Digital Library

[8]

The Coq Development Team. The Coq Proof Assistant Reference Manual, 2013.

[9]

L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337--340, 2008.

Digital Library

[10]

D. C. D'Elia, C. Demetrescu, and I. Finocchi. Mining hot calling contexts in small space. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 516--527, 2011.

Digital Library

[11]

N. Dershowitz. Termination of rewriting. Journal of symbolic computation, 3(1):69--115, 1987.

Digital Library

[12]

J. Giesl, P. Schneider-kamp, and R. Thiemann. AProVE 1.2: Automatic termination proofs in the dependency pair framework. In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR), pages 281--286, 2006.

Digital Library

[13]

A. Gupta, T. Henzinger, R. Majumdar, A. Rybalchenko, and R.-G. Xu. Proving non-termination. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 147--158, 2008.

Digital Library

[14]

S. Z. Guyer and C. Lin. Broadway: A compiler for exploiting the domain-specific semantics of software libraries. Proceedings of the IEEE, 93(2):342--357, Feb. 2005.

[15]

S. Han, Y. Dang, S. Ge, D. Zhang, and T. Xie. Performance debugging in the large via mining millions of stack traces. In Proceedings of the 34th International Conference on Software Engineering (ICSE), pages 145--155, 2012.

Digital Library

[16]

R. Joshi, G. Nelson, and Y. Zhou. Denali: A practical algorithm for generating optimal code. ACM Transactions on Programming Languages and Systems (TOPLAS), 28(6):967--989, Nov. 2006.

Digital Library

[17]

C. Killian, J. W. Anderson, R. Jhala, and A. Vahdat. Life, death, and the critical transition: Detecting liveness bugs in systems code. In Proceedings of the 4th USENIX Symposium on Networked Systems Design & Implementation (NDSI), pages 243--256, 2007.

Digital Library

[18]

S. Kundu, Z. Tatlock, and S. Lerner. Proving optimizations correct using parameterized program equivalence. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 327--337, 2009.

Digital Library

[19]

V. Le, M. Afshari, and Z. Su. Compiler validation via equivalence modulo inputs. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 216--226, 2014.

Digital Library

[20]

S. Lerner, T. Millstein, and C. Chambers. Automatically proving the correctness of compiler optimizations. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI), pages 220--231, 2003.

Digital Library

[21]

S. Lerner, T. Millstein, E. Rice, and C. Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 364--377, 2005.

Digital Library

[22]

X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107--115, July 2009.

Digital Library

[23]

P. Li and J. Regehr. T-check: Bug finding for sensor networks. In Proceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks (IPSN), pages 174--185, 2010.

Digital Library

[24]

C. Lidbury, A. Lascu, N. Chong, and A. F. Donaldson. Many-core compiler fuzzing. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 65--76, 2015.

Digital Library

[25]

N. Lopes, D. Menendez, S. Nagarakatte, and J. Regehr. Alive: Automatic LLVM InstCombine Verifier. http://github.com/nunoplopes/alive. Retrieved 2016-02-12.

[26]

N. Lopes, D. Menendez, S. Nagarakatte, and J. Regehr. Provably correct peephole optimizations with Alive. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 22--32, 2015.

Digital Library

[27]

H. Massalin. Superoptimizer: A look at the smallest program. In Proceedings of the 2nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 122--126, 1987.

[28]

R. Morisset, P. Pawan, and F. Z. Nardelli. 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 (PLDI), pages 187--196, 2013.

Digital Library

[29]

G. C. Necula. Translation validation for an optimizing compiler. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI), pages 83--94, 2000.

Digital Library

[30]

A. Nistor, P.-C. Chang, C. Radoi, and S. Lu. CARAMEL: Detecting and fixing performance problems that have non-intrusive fixes. In Proceedings of the 37th International Conference on Software Engineering (ICSE), pages 902--912, 2015.

Digital Library

[31]

M. Rinard. Credible compilation. Technical Report MIT-LCS-TR-776, Massachusetts Institute of Technology, Mar. 1999.

[32]

H. Samet. Proving the correctness of heuristically optimized code. Communications of the ACM, 21(7):570--582, July 1978.

Digital Library

[33]

E. Schkufza, R. Sharma, and A. Aiken. Stochastic superoptimization. In Proceedings of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 305--316, 2013.

Digital Library

[34]

F. Spoto, F. Mesnard, and É. Payet. A termination analyzer for Java bytecode based on path-length. ACM Transactions on Programming Languages and Systems (TOPLAS), 32(3):8:1--8:70, Mar. 2010.

Digital Library

[35]

J. Steinbach. Simplification orderings: History of results. Fundamenta Informaticae, 24(1-2):47--87, Apr. 1995.

Digital Library

[36]

D. L. Whitfield and M. L. Soffa. An approach for exploring code improving transformations. ACM Transactions on Programming Languages and Systems (TOPLAS), 19(6):1053--1084, Nov. 1997.

Digital Library

[37]

H. Xi. Towards automated termination proofs through "freezing". In Rewriting Techniques and Applications, pages 271--285. Springer, 1998.

Digital Library

[38]

X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 283--294, 2011.

Digital Library

[39]

J. Zhao, S. Nagarakatte, M. M. K. Martin, and S. Zdancewic. Formalizing the LLVM intermediate representation for verified program transformations. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 427--440, 2012.

Digital Library

[40]

L. Zuck, A. Pnueli, Y. Fang, and B. Goldberg. VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science, 9(3):223--247, 2003.

Cited By

Zang ZThimmaiah AGligoric MRoychoudhury APaiva AAbreu RStorey M(2024)JOG: Java JIT Peephole Optimizations and Tests from PatternsProceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings10.1145/3639478.3640040(11-15)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3639478.3640040
Zang ZThimmaiah AGligoric MJust RFraser G(2023)Pattern-Based Peephole Optimizations with Java JIT TestsProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598038(64-75)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598038
Shi XXie XLi YZhang YChen SLi XRoychoudhury ACadar CKim M(2022)Large-scale analysis of non-termination bugs in real-world OSS projectsProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549129(256-268)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549129
Show More Cited By

Index Terms

Termination-checking for LLVM peephole optimizations

Recommendations

Provably correct peephole optimizations with alive
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

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 ...
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 Implementation

Peephole 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 ...
Provably correct peephole optimizations with alive
PLDI '15

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICSE '16: Proceedings of the 38th International Conference on Software Engineering

May 2016

1235 pages

ISBN:9781450339001

DOI:10.1145/2884781

General Chair:
Laura Dillon
Michigan State University
,
Program Chairs:
Willem Visser
Stellenbosch University, South Africa
,
Laurie Williams
North Carolina State University

Copyright © 2016 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]

Sponsors

ACM: Association for Computing Machinery
SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS\TCSE: TC on Software Engineering
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 May 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

ICSE '16

Sponsor:

ACM
SIGSOFT
IEEE-CS\TCSE
IEEE-CS\DATC

ICSE '16: 38th International Conference on Software Engineering

May 14 - 22, 2016

Texas, Austin

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
587
Total Downloads

Downloads (Last 12 months)99
Downloads (Last 6 weeks)25

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zang ZThimmaiah AGligoric MRoychoudhury APaiva AAbreu RStorey M(2024)JOG: Java JIT Peephole Optimizations and Tests from PatternsProceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings10.1145/3639478.3640040(11-15)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3639478.3640040
Zang ZThimmaiah AGligoric MJust RFraser G(2023)Pattern-Based Peephole Optimizations with Java JIT TestsProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598038(64-75)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598038
Shi XXie XLi YZhang YChen SLi XRoychoudhury ACadar CKim M(2022)Large-scale analysis of non-termination bugs in real-world OSS projectsProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549129(256-268)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549129
Nishida NWinkler S(2018)Loop Detection by Logically Constrained Term RewritingVerified Software. Theories, Tools, and Experiments10.1007/978-3-030-03592-1_18(309-321)Online publication date: 24-Nov-2018
https://doi.org/10.1007/978-3-030-03592-1_18
Menendez DNagarakatte S(2017)Alive-Infer: data-driven precondition inference for peephole optimizations in LLVMACM SIGPLAN Notices10.1145/3140587.306237252:6(49-63)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3140587.3062372
Menendez DNagarakatte SCohen AVechev M(2017)Alive-Infer: data-driven precondition inference for peephole optimizations in LLVMProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3062341.3062372(49-63)Online publication date: 14-Jun-2017
https://dl.acm.org/doi/10.1145/3062341.3062372
Menendez DNagarakatte SGupta A(2016)Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVMStatic Analysis10.1007/978-3-662-53413-7_16(317-337)Online publication date: 31-Aug-2016
https://doi.org/10.1007/978-3-662-53413-7_16

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

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

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents