TY - GEN
T1 - Termination analysis without the tears
AU - Zhu, Shaowei
AU - Kincaid, Zachary
N1 - Publisher Copyright:
© 2021 ACM.
PY - 2021/6/18
Y1 - 2021/6/18
N2 - Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis may be classified into two groups: (1) algorithms with strong behavioral guarantees that work in limited circumstances (e.g., complete synthesis of linear ranking functions for polyhedral loops), and (2) algorithms that are widely applicable, but have weak behavioral guarantees (e.g., Terminator). This paper investigates the space in between: how can we design practical termination analyzers with useful behavioral guarantees? This paper presents a termination analysis that is both compositional (the result of analyzing a composite program is a function of the analysis results of its components) and monotone ("more information into the analysis yields more information out"). The paper has two key contributions. The first is an extension of Tarjan's method for solving path problems in graphs to solve infinite path problems. This provides a foundation upon which to build compositional termination analyses. The second is a collection of monotone conditional termination analyses based on this framework. We demonstrate that our tool ComPACT (Compositional and Predictable Analysis for Conditional Termination) is competitive with state-of-the-art termination tools while providing stronger behavioral guarantees.
AB - Determining whether a given program terminates is the quintessential undecidable problem. Algorithms for termination analysis may be classified into two groups: (1) algorithms with strong behavioral guarantees that work in limited circumstances (e.g., complete synthesis of linear ranking functions for polyhedral loops), and (2) algorithms that are widely applicable, but have weak behavioral guarantees (e.g., Terminator). This paper investigates the space in between: how can we design practical termination analyzers with useful behavioral guarantees? This paper presents a termination analysis that is both compositional (the result of analyzing a composite program is a function of the analysis results of its components) and monotone ("more information into the analysis yields more information out"). The paper has two key contributions. The first is an extension of Tarjan's method for solving path problems in graphs to solve infinite path problems. This provides a foundation upon which to build compositional termination analyses. The second is a collection of monotone conditional termination analyses based on this framework. We demonstrate that our tool ComPACT (Compositional and Predictable Analysis for Conditional Termination) is competitive with state-of-the-art termination tools while providing stronger behavioral guarantees.
KW - Algebraic program analysis
KW - algebraic path problems
KW - loop summarization
KW - termination analysis
UR - http://www.scopus.com/inward/record.url?scp=85108902566&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85108902566&partnerID=8YFLogxK
U2 - 10.1145/3453483.3454110
DO - 10.1145/3453483.3454110
M3 - Conference contribution
AN - SCOPUS:85108902566
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 1296
EP - 1311
BT - PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
A2 - Freund, Stephen N.
A2 - Yahav, Eran
PB - Association for Computing Machinery
T2 - 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021
Y2 - 20 June 2021 through 25 June 2021
ER -