A practical analysis of non-termination in large logic programs

A large body of work has been dedicated to termination analysis of logic programs but relatively little has been done to analyze non-termination. In our opinion, explaining non-termination is a much more important task because it can dramatically improve a user's ability to effectively debug large, complex logic programs without having to abide by punishing syntactic restrictions. Non-termination analysis examines program execution history when the program is suspected to not terminate and informs the programmer about the exact reasons for this behavior. In Liang and Kifer (2013), we studied the problem of non-termination in tabled logic engines with subgoal abstraction, such as XSB, and proposed a suite of algorithms for non-termination analysis, called Terminyzer. These algorithms analyze forest logging traces and output sequences of tabled subgoal calls that are the likely causes of non-terminating cycles. However, this feedback was hard to use in practice: the same subgoal could occur in multiple rule heads and in even more places in rule bodies, so Terminyzer left too much tedious, sometimes combinatorially large amount of work for the user to do manually. Here we propose a new suite of algorithms, Terminyzer(+), which closes this usability gap. Terminyzer+ can detect not only sequences of subgoals that cause non-termination, but, importantly, the exact rules where they occur and the rule sequences that get fired in a cyclic manner, thus causing non-termination. This makes Terminyzer(+) suitable as a back-end for user-friendly graphical interfaces on top of Terminyzer(+), which can greatly simplify the debugging process. Terminyzer(+) back-ends exist for the SILK system as well as for the open-source Flora-2 system. A graphical interface has been developed for SILK and is currently underway for Flora-2. We also report experimental studies, which confirm the effectiveness of Terminyzer(+) on a host of large real-world knowledge bases. All tests used in this paper are available online.(1) In addition, we make a step towards automatic remediation of non-terminating programs by proposing an algorithm that heuristically fixes some causes of misbehavior. Furthermore, unlike Terminyzer, Terminyzer(+) does not require the underlying logic engine to support subgoal abstraction, although it can make use of it.