Termination is a crucial program property. Non-termination bugs can be subtle to detect, and may remain hidden for long before they take effects. Many real-world programs still suffer from vast consequences (e.g., no response) caused by non-termination bugs. As a classic problem, termination proving has been studied for many years. Many termination checking tools and techniques have been developed and demonstrated effective on existing well-established benchmarks. However, the capability of these tools in finding practical non-termination bugs has yet to be tested on real-world projects. To fill in this gap, in this paper, we conducted the first large-scale empirical study of non-termination bugs in real-world OSS projects. Specifically, we first devoted substantial manual efforts in collecting and analyzing 445 non-termination bugs from 3,142 GitHub commits, and provided a systematic classification of the bugs based on their root causes. We constructed a new benchmark set characterizing the real-world bugs with simplified programs, including a non-termination dataset with 56 real and reproducible non-termination bugs and a termination dataset with 58 fixed programs. With the constructed benchmark, we evaluated five state-of-the-art termination analysis tools. The results show that the capabilities of the tested tools to make correct verdicts have obviously dropped compared with the existing benchmarks. Meanwhile, we identified the challenges and limitations that these tools face by analyzing the root causes of their unhandled bugs. Finally, we summarized the challenges and future research directions for detecting non-termination bugs in real-world projects. This website provides further supplementary descriptions of our paper.
In the website, we provide more details include the example illustration for each category, related data for reproducibility (manually labelling of each bug and the extracted benchmark) and more experimental results. Please see more details as follows:
Taxonomy of Infinite Loop: We introduce the corresponding examples for each category of infinite loop.
Taxonomy of Infinite Recursion: We introduce the example for each category of infinite recursion.
Data and Benchmarks: We provide all data and benchmarks and make therm public available.
Experiment Results: We provide more experiment results and analysis.