Research Article
Loopster++: Termination Analysis for Multi-path Linear Loop
@INPROCEEDINGS{10.1007/978-3-030-92635-9_28, author={Hui Jin and Weimin Ge and Yao Zhang and Xiaohong Li and Zhidong Deng}, title={Loopster++: Termination Analysis for Multi-path Linear Loop}, proceedings={Collaborative Computing: Networking, Applications and Worksharing. 17th EAI International Conference, CollaborateCom 2021, Virtual Event, October 16-18, 2021, Proceedings, Part I}, proceedings_a={COLLABORATECOM}, year={2022}, month={1}, keywords={Termination analysis Multi-path linear loop Path dependency automaton}, doi={10.1007/978-3-030-92635-9_28} }- Hui Jin
Weimin Ge
Yao Zhang
Xiaohong Li
Zhidong Deng
Year: 2022
Loopster++: Termination Analysis for Multi-path Linear Loop
COLLABORATECOM
Springer
DOI: 10.1007/978-3-030-92635-9_28
Abstract
Loop structure is widely adopted in many applications,e.g. collaborative applications, social network applications, and edge computing. And the termination of the loop is of great significance to the correctness of the program. Most of the previous relative studies focused on determining the termination of a loop program by synthesizing the ranking functions, but not every ranking function can be synthesized. Although a class of linear loop program termination has been proven to be decidable, it is always difficult to analyze the termination of a multi-path linear loop. Xie et al. [20] presented Loopster to quickly check the termination of the multi-path loop program by analyzing the termination of each path and the dependency between paths. But it relies on the monotonicity of variables which is very complicated to check when the variables increase.
To this end, we extend Loopster, named Loopster++, to analyze the termination of multi-path linear loops. In Loopster++, 1) we convert the iterable path into a single path linear loop to analyze its termination. 2) We also propose a novel method to analyze the dependency between linear loop paths. 3) For the cycle constituted by alternate execution between paths, we classify all cycles and give the termination method of the corresponding category cycle. We finally evaluate Loopster++ by analyzing the termination of the benchmarks from the competition on software verification and compare it with the state-of-the-art tools. The empirical results demonstrate the superiority of Loopster++ by achieving high accuracy of 83% in the shortest time.
