Termination analysis without the tears
Termination analysis without the tears
复制标题
不流泪的终结分析
DOI：
10.1145/3453483.3454110
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Kincaid, Zachary
中科院分区：
文献类型：
--
作者：
Zhu, Shaowei;Kincaid, Zachary
确定给定程序是否终止是典型的不可判定问题。用于终止性分析的算法可分为两组：(1)具有在有限情况下工作的强行为保证的算法(例如，用于多面体循环的线性排序函数的完全合成)，以及(2)广泛适用但具有弱行为保证的算法(例如，终结符)。本文探讨了介于两者之间的问题：如何设计具有有用行为保证的实用终止分析器？本文提出了一种终止性分析，它既是组合的(分析组合程序的结果是其组件分析结果的函数)，也是单调的(“进入分析的信息越多，输出的信息就越多”)。这篇论文有两个主要贡献。第一个是将Tarjan求解图中的路问题的方法推广到求解无限路问题。这为建立成分终止分析提供了基础。第二种是基于该框架的单调条件终止分析集合。我们证明，我们的工具COMPACT(条件终止的成分和可预测分析)在提供更强大的行为保证的同时，与最先进的终止工具竞争。
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 bothcompositional(the result of analyzing a composite program is a function of the analysis results of its components) andmonotone(“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 solveinfinitepath 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.