«Abstract. Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check is ...»
Termination Analysis with
Compositional Transition Invariants
Daniel Kroening1, Natasha Sharygina2,4,
Aliaksei Tsitovich2, and Christoph M. Wintersteiger3
Oxford University, Computing Laboratory, UK
Formal Veriﬁcation and Security Group, University of Lugano, Switzerland
Computer Systems Institute, ETH Zurich, Switzerland
School of Computer Science, Carnegie Mellon University, USA
Abstract. Modern termination provers rely on a safety checker to construct disjunctively well-founded transition invariants. This safety check is known to be the bottleneck of the procedure. We present an alternative algorithm that uses a light-weight check based on transitivity of ranking relations to prove program termination. We provide an experimental evaluation over a set of 87 Windows drivers, and demonstrate that our algorithm is often able to conclude termination by examining only a small fraction of the program. As a consequence, our algorithm is able to outperform known approaches by multiple orders of magnitude.
1 Introduction Automated termination analysis of systems code has advanced to a level that permits industrial application of termination provers. One possible way to obtain a formal argument for termination of a program is to rank all states of the program with natural numbers such that for any pair of consecutive states si, si+1 the rank is decreasing, i.e., rank(si+1 ) rank(si ). In other words, a program is terminating if there exists a ranking function for every program execution.
Substantial progress towards the applicability of procedures that compute ranking arguments to industrial code was achieved by an algorithm called Binary Reachability Analysis (BRA), proposed by Cook, Podelski, and Rybalchenko .
This approach combines detection of ranking functions for program paths with a procedure for checking safety properties, e.g., a Model Checker. The key idea of the algorithm is to encode an intermediate termination argument into a program annotated with an assertion, which is then passed to the safety checker. Any counterexample for the assertion produced by the safety checker contains a path that violates the intermediate termination argument. The counterexample path is then used to compute a better termination argument with the help of methods that discover ranking functions for program paths.
Supported by the Swiss National Science Foundation under grant no. 200020-122077, by EPSRC grant no. EP/G026254/1, by the EU FP7 STREP MOGENTES, and by the Tasso Foundation.
A broad range of experiments with diﬀerent implementations have shown that the bottleneck of this approach is the safety check [1, 2]: Cook et al.  report more than 30 hoursof runtime for some of their benchmarks. The time for computing the ranking function for a given program path is insigniﬁcant in comparison. Part of the reason for the diﬃculty of the safety checks is their dual role: they ensure that a disjunctively composed termination argument is correct and they need to provide suﬃciently deep counterexamples for the generation of further ranking arguments.
We propose a new algorithm for termination analysis that addresses these challenges as follows: 1) We use a light-weight criterion for termination based on compositionality of transition invariants. 2) Instead of using full counterexample paths, the algorithm applies the path ranking procedure directly to increasingly deep unwindings of the program until a suitable ranking argument is found. We prove soundness and completeness (for ﬁnite-state programs) of our approach and support it by an extensive evaluation on a large set of Windows device drivers. Our algorithm performs up to 3 orders of magnitude faster than BRA, as it avoids the bottleneck of safety checking in the iterative construction of a termination argument.
2 Background Preliminaries We deﬁne notation for programs and record some basic properties we require later on. Programs are modeled as transition systems.
Deﬁnition 1 (Transition System). A transition system (program) P is a three tuple S, I, R, where – S is a (possibly inﬁnite) set of states, – I ⊆ S is the set of initial states, – R ⊆ S × S is the transition relation.
A computation of a transition system is a maximal sequence of states s0, s1,... such that s0 ∈ I and (si, si+1 ) ∈ R for all i ≥ 0. A program is terminating iﬀ all computations of the program eventually reach a ﬁnal state. The non-reﬂexive transitive closure of R is denoted by R+, and the reﬂexive transitive closure of R is denoted by R∗. The set of reachable states is R∗ (I).
Podelski and Rybalchenko  use Transition Invariants to prove termination
Deﬁnition 2 (Transition Invariant ). A transition invariant T for program P = S, I, R is a superset of the transitive closure of R restricted to the reachable state space, i.e., R+ ∩ (R∗ (I) × R∗ (I)) ⊆ T.
A well-founded relation is a relation that does not contain inﬁnite descending
chains. Podelski and Rybalchenko deﬁne a weaker notion as follows:
Deﬁnition 3 (Disjunctive Well-foundedness ). A relation T is disjunctively well-founded (d.wf.) if it is a ﬁnite union T = T1 ∪... ∪ Tn of well-founded (wf.) relations.
A program is terminating if it does not have inﬁnite computations, and Podelski and Rybalchenko show that disjunctive well-foundedness is enough to prove
termination of a program:
Theorem 1 (Termination ). A program P is terminating iﬀ there exists a d.wf. transition invariant for P.
The literature presents a broad range of methods to obtain transition invariants. Usually, this is accomplished via synthesis of ranking functions, which deﬁne well-founded ranking relations [2, 4–6]. We refer to such methods as ranking procedures.
Binary Reachability Analysis . Theorem 1 gives rise to an algorithm for proving termination that constructs a d.wf. transition invariant in an incremental fashion. Initially, an empty termination argument is used, i.e., T0 = ∅. Then, a Model Checker is used to search the reachable state space for a counterexample to termination argument Ti. If there is none, termination is proven. Otherwise, let π be the counterexample path. The counterexample may be genuine, i.e., demonstrate a preﬁx of a non-terminating computation. Otherwise, a wellfounded relation T that includes π is constructed (via a ranking procedure).
Finally, the current termination argument is updated, i.e., Ti+1 = Ti ∪ T and the process is repeated.
This principle has been put to the test in various tools, most notably in Terminator , ARMC , and in an experimental version of SatAbs .
3 Compositional Termination Analysis The literature contains a broad range of reports of experiments with multiple implementations that indicate that the bottleneck of Binary Reachability Analysis is that the safety checks are often diﬃcult to decide by means of the currently available software Model Checkers [1, 2]. This problem unfortunately applies to both cases of ﬁnding a counterexample to an intermediate termination argument and to proving that no such counterexample exists.
As an example, consider a program that contains a trivial loop. The d.wf. transition invariant for the loop can be constructed in a negligible amount of time, but the computation of a path to the beginning of the loop may already exceed the computational resources available.
In this section, we describe a new algorithm for proving program termination that achieves the same result while avoiding excessively expensive safety checks.
We ﬁrst deﬁne the usual relational composition operator ◦ for two relations A, B : S × S as
Note that a relation R is transitive if it is closed under relational composition, i.e., when R ◦ R ⊆ R. To simplify presentation, we also deﬁne R1 := R and Rn := Rn−1 ◦ R for any relation R : S × S.
While d.wf. transition invariants are not in general well-founded, there is a
trivial subclass for which this is the case:
Deﬁnition 4 (Compositional Transition Invariant). A d.wf. transition invariant T is called compositional if it is also transitive, or equivalently, closed under composition with itself, i.e., when T ◦ T ⊆ T.5 A compositional transition invariant is of course well-founded, since it is an inductive transition invariant for itself . Using this observation and Theorem 1,
Corollary 1. A program P terminates if there exists a compositional transition invariant for P.
In Binary Reachability Analysis, the Model Checker needs to compute a counterexample to an intermediate termination argument, which is often diﬃcult. The counterexample begins with a stem, i.e., a path to the entry point of the loop. For many programs, the existence of a d.wf. transition invariant does not actually depend on the entry state of the loop. For example, termination of a trivial loop that increments a variable i to a given upper limit u does not actually depend on the initial value of i, nor does it depend on u. The assurance of progress towards u is enough to conclude termination.
The other purpose of the Model Checker in BRA is to check that a candidate transition invariant indeed includes R+ restricted to the reachable states. To this end, we note that the (non-reﬂexive) transitive closure of R is essentially an
unwinding of program loops:
∞ R+ = R ∪ (R ◦ R) ∪ (R ◦ R ◦ R) ∪... = Ri.
i=1 Instead of searching for a d.wf. transition invariant that is a superset of R+, we can therefore decompose the problem into a series of smaller ones. We consider a series of loop-free programs in which R is unwound k times, i.e., the program that contains the transitions in R1 ∪... ∪ Rk.
Observation 2. Let P = S, I, R and k ≥ 1. If there is a d.wf. Tk with k j j=1 R ⊆ Tk and Tk is also transitive, then Tk is a compositional transition invariant for P.
This suggests a trivial algorithm that attempts to construct d.wf. relations Ti for incrementally deep unwindings of P until it ﬁnally ﬁnds a transitive Tk, which We use the term compositional instead of transitive for transition invariants in order to comply with the terminology in the existing literature .
proves termination of P. However, this trivial algorithm need not terminate, even for simple inputs. This is due to the fact that Ti does not necessarily have to be diﬀerent from Ti−1, in which case the algorithm will never ﬁnd a compositional transition invariant.
We provide an alternative that does not suﬀer from this limitation and takes advantage of the fact that most terminating loops encountered in practice have transition invariants with few disjuncts. To present this algorithm, we require the following lemma, which enables us to exclude computations from the program
that we have already proven terminating in a previous iteration:
As an optimization, we may safely omit some of the Ti while searching for a
transitive Tk :
Lemma 2 (Optimization). Let T0,..., Tk be the sequence of d.wf. relations for application of Lemma 1. The claim of the lemma holds even if some of the T1,..., Tk−1 are not provided (empty).
Proof. We show that Q is a transition invariant for P. Let (x, x ) ∈ R+ ∩(R∗ (I)× R∗ (I)). As in the proof of Obs. 2, (x, x ) ∈ Rl for some l. The claim holds k trivially for l ≤ k as i=1 Ri ⊆ Q. For l k, note that (x, x ) ∈ (Rjk ◦ Rl−jk ) and 0 ≤ l − jk k for some j ≥ 1. Note that Rjk ⊆ Qj and Rl−jk ⊆ Q. Thus, (x, x ) ∈ (Qj ◦ Q) = Qj+1. As Q is transitive, Qj+1 ⊆ Q, and thus (x, x ) ∈ Q.
The proof of Lemma 1 still applies. As an example, our implemenation only uses those Ti where i is a power of two.
The procedure that we draw from Lemma 2 is Algorithm 1, and we call it Compositional Termination Analysis (CTA). This algorithm makes use of an external ranking procedure called rank, which generates a d.wf. ranking relation for a given set of transitions, or alternatively a set C ∈ S of states such that R∗ (C) contains inﬁnite computations. We say that rank is sound if it always returns either a d.wf. superset of its input or a non-empty set of states C, and we call it complete if it terminates on every input.
Algorithm 1 maintains a set X ⊆ S that is an over-approximation of the set of reachable states, i.e., R∗ (I) ⊆ X. It starts with X = S and at i = 1.
It iterates over i and generates d.wf. ranking relations Ti for the transitions in i j j=1 R \ T. As long as such relations are found, they are added to T. Once it ﬁnds a transitive T, the algorithm stops, as P terminates according to Lemma 2.
When ranking fails for some i, the algorithm checks whether there is a reachable state in C, in which case R∗ (C) contains a counterexample to termination and the algorithm consequently reports P as non-terminating. Otherwise, it removes C from X, which represents a reﬁnement of the current over-approximation of the set of reachable states.
Theorem 3. Assuming the sub-procedure rank is sound, Algorithm 1 is sound.
Proof. When the algorithm terminates with ‘terminating’ (line 10), the sequence of relations Ti constructed so far is suitable for application of Lemma 2, which proves termination. It is easy to see that the set R∗ (I) in Lemma 2 can be overapproximated to X. If the algorithm returns ‘non-terminating’ at line 8, it has found a set of reachable states from which inﬁnite computations exist, i.e., there is a concrete counterexample to termination.
Lines 12–14 ensure progress between iterations by excluding unreachable states (C) from the approximation X and adding the most recently found Ti in T. However, for non-terminating input programs, the algorithm may not terminate for two reasons: a) rank is not required to terminate, and b) there may be an inﬁnite sequence of iterations.
This is not the case for ﬁnite S if the input program is non-terminating, since sound and complete ranking procedures exist (e.g., [5, 2]) and progress towards the goal can thus be ensured: