Christophe Alias

Alain Darte

Paul Feautrier

Laure Gonnord

Clément Quinson

Program Termination and Worst Time Complexity with Multi-Dimensional Affine Ranking Functions

Keywords: static analysis, termination proof, multidimensional affine ranking functions, worst-case time complexity estimation analyse statique, preuve de terminaison, génération de fonctions de terminaison multidimensionnelles affines, estimation de la complexité au pire

A standard method for proving the termination of a flowchart program is to exhibit a ranking function, i.e., a function from the program states to a well-founded set, which strictly decreases at each program step. Our main contribution is to give an efficient algorithm for the automatic generation of multi-dimensional affine nonnegative ranking functions, a restricted class of ranking functions that can be handled with linear programming techniques. Our algorithm is based on the combination of the generation of invariants (a technique from abstract interpretation) and on an adaptation of multi-dimensional affine scheduling (a technique from automatic parallelization). We also prove the completeness of our technique with respect to its input and the class of rankings we consider. Finally, as a byproduct, by computing the cardinal of the range of the ranking function, we obtain an upper bound for the computational complexity of the source program, which does not depend on restrictions on the shape of loops or on program structure. This estimate is a polynomial, which means that we can handle programs with more than linear complexity. The method is tested on a large collection of test cases from the literature. We also point out future improvements to handler larger programs.

Introduction and motivation

The problem of proving program correctness has been with us since the early days of Computer Science. In a seminal paper [START_REF] Floyd | Assigning meaning to programs[END_REF], R. W. Floyd proposed what has become one of the standard approaches: affix assertions to each program point and prove that they are consequences of the assertions of its predecessors in the program control graph. The assertions at the entry point of the program are its preconditions, the assertions at loop entry points are invariants, while the assertions at its exit point must entail correctness, according to some set of requirements. Constructing the required set of assertions is a tedious and error-prone task. In the case of a loop-free program, it is possible to mechanically build all the assertions, either going forward from the preconditions, or backward from the requirements. However, there exist while loop programs whose invariants are recursively enumerable but not recursive [START_REF] Blass | Inadequacy of computable loop invariants[END_REF]. Since the formalisms we dare use for describing sets in compilers -finite and co-finite sets, regular and context-free languages, polyhedra, Presburger arithmetics -all deals with recursive sets, this means that in some cases, the invariants must be approximated, mostly using techniques from abstract interpretation [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF].

At the same time, it was soon realized that this method proves only partial correctness, i.e., that the program gives the correct result if and when it terminates. To prove termination, one needs a variant or ranking function (a W-function in Floyd's terminology), i.e., a function from the states of the program to some well-founded set, which strictly decreases at each program step. Here again, it would be nice to have an algorithm for building ranking functions, but this is not possible in all cases since it would give a solution to the undecidable halting problem. However, this does not preclude the existence of partial solutions, which, e.g., handle only programs (or approximated models) of a restricted shape, or look for rankings in a restricted class of functions. Our main goal is to provide such an algorithm, which applies to arbitrary programs but considers only the set of multi-dimensional nonnegative affine functions under lexicographic ordering, as defined formally in Section 2.

The construction of a ranking function can sometimes be linked to the evaluation of the worst case execution time (WCET) of the source program. Obviously, if a program does not terminate, its WCET is infinite. If the program terminates and a ranking function exists, then, under some hypotheses, it can give some information on the WCET. For example, if the ranking function has co-domain N (one-dimensional function), its value at program start is an upper bound on the number of steps before termination since it decreases at least by one at each program step. (The situation is more complicated in the case of multi-dimensional ranking functions, i.e., if the co-domain is N d .) In other words, if accurate, the ranking function can give the order of magnitude of the WCET, or time complexity [START_REF] Gulvani | SPEED: Precise and efficient static estimation of program computational complexity[END_REF] of the program but not its exact value. This estimate is static and "high-level" in the sense that it just counts the program steps. Estimating the WCET is much more difficult [START_REF] Wilhelm | The determination of worst-case execution times-overview of the methods and survey of tools[END_REF].

The rest of the paper is organized as follows. We first describe integer interpreted automata, a standard model for abstracting the control part of arbitrary non-recursive programs. We then define ranking functions and prove a few general results. Section 3 is the main part of the paper; we present a new method for constructing multidimensional affine ranking functions and to infer the computational complexity of the source program. We prove the relative completeness of the method, which means that if there exists a ranking function for the set of invariants we have found, then our algorithm finds one. In Section 4, we report on our implementation through a large set of benchmarks from the literature. We next describe other approaches to the termination problem and conclude, pointing to some unsolved problems and outlining future work.

Definitions and elementary properties 2.1 Notations

Hereafter, matrices are written with capital letters (as A) and column vectors with a top arrow (as x). The components of a vector x of dimension d are denoted by x[i], 0 ≤ i < d. Thus, the i-th component of x is x[i -1]. Sets are represented with calligraphic letters such as W, K, etc.

Integer interpreted automata

In the tradition of most previous work on program termination and static program analysis, we do not start from the program itself but from an abstraction: the associated integer interpreted automaton. This is similar to the flowcharts which were used a long time ago to express programs (see, e.g., Manna's book [START_REF] Manna | Mathematical Theory of Computing[END_REF]) until the advent of structured programming. However, when one looks at real-life programs, many deviations from the strict structured model can occur, including premature loop termination, exceptions, and even the occasional goto. Starting from a flowchart allows us to not depend of the details of the syntax and semantics of the source language, which can be dealt with by an appropriate preprocessor.

A program is represented by a general relational (integer) interpreted automaton (K, n, k init , T ) defined by:

• a finite set K of control points;

• n integer variables represented by a vector x of size n; • an initial control point k init ∈ K; • a finite set T of 4-tuples (k, g, a, k ′ ), called transitions, where k ∈ K (resp. k ′ ∈ K) is the source (resp. target) control point, g : Z n → B = {true, f alse} is a guard (function from variable valuations to Booleans), and a : Z n → P(Z n ) is an action that assigns to each variable valuation x a subset a( x) of Z n .

Semantics

The set of states is K × Z n . A trace from (k 0 , x 0 ) to (k, x) is a sequence (k 0 , x 0 ), (k 1 , x 1 ), . . . , (k p , x p ) such that k p = k, x p = x and for each i, 0 ≤ i < p, there exists in T a transition (k i , g i , a i , k i+1 ) such that g i ( x i ) = true and x i+1 ∈ a i ( x i ). Given an initial valuation v, a state (k, x) is reachable from v iff (if and only if) there exists a trace from

(k init , v) to (k, x). A state (k, x) is reachable if there exists v ∈ Z n such that (k, x) is reachable from v.
The set of reachable states is denoted by R. Note that there can be two forms of non-determinism in the "execution" of an interpreted automaton. First, if a( x) is not a singleton, a transition can lead to several distinct variable valuations (a( x) = Z is a way to assign to x a random value). Second, if there exist (k, x) ∈ R and two transitions (k, g 1 , a 1 , k 1 ) and (k, g 2 , a 2 , k 2 ) such that g 1 ( x) and g 2 ( x) are both true, then two different states after (k, x) are possible.

In this paper, we consider affine interpreted automata, a subclass of integer interpreted automata with affine guarded transitions. In this case, the guard is a conjunction of affine tests and the set of pairs ( x, x ′ ) where x ′ ∈ a( x) is described by a polyhedron.

Definition 1 (General affine guarded transition)

A transition t = (k, g, a, k ′ ) is
• g( x) is true iff G x + g ≥ 0 (component-wise)
where g is an integer vector and G an integer matrix with n columns and as many rows as the size of g;

• x ′ ∈ a( x) iff A x + A ′ x ′ + a ≥ 0 (component-wise)
where a is an integer vector and A and A ′ are integer matrices with n columns and as many rows as the size of a. We write a = (A, A ′ , a).

The algorithms and theory we develop in the next sections can handle general affine interpreted automata. However, in terms of implementation, the tool we rely on for the computation of invariants (see Section 3.1) is, so far, limited to the case where actions define functions but with unspecified components: in other words, for each x, a( x) is a singleton { x ′ } where each component of x ′ is either expressed as an affine function of the components of x, or unspecified (i.e., it can take any value in Z), which we denote by the symbol "?". This will be sufficient to handle general (extended) affine relations, as we will see in Section 3.1. In this case, we identify a( x) with the element x ′ ∈ (Z ∪ {?}) n it contains, and we say that a( x) is an affine function of x.

An example of such an automaton is given in Figure 1. The control points are labelled for convenience, and transitions are represented with arrows indexed by g a (g is omitted when g = true).

Example 1

The C code below is an abstraction of a real C code computing the greatest common divisor (gcd) of two polynomials. // expr is an expression, A is an array, // r is a constant positive integer parameter. da = 2r; db = 2r;a while (da >= r) { cond = ( da >= db || A[expr] == 0 ); if (!cond) { tmp = db; db = da; da = tmp -1; } else da = da -1; } This simplified code is itself abstracted by the automaton of Figure 1, where init is the initial control point and loop corresponds to the while loop. The fact that the condition A[expr]==0 cannot be statically evaluated introduces some non-determinism in the automaton. To enter the then part of the test, the condition da < db must be true (transition t 3 ) while the else part can always be traversed (transition t 2 ) as long as the termination test of the while loop is false (additional condition da >= r for both transitions). Definition 2 (Bounded non-determinism) An affine interpreted automaton has bounded non-determinism if there exists B ∈ N, such that, for each state (k, x), the number of states (k ′ , x ′ ) that can be obtained after one transition from state (k, x) is at most B.

Invariants

The guard g in a transition t = (k, g, a, k ′ ) gives a necessary condition on variables x to traverse the transition t and to apply its corresponding action a. To get the exact valuations x of variables for which the action a can be performed, one needs to take into account the initial valuations and the successive conditions that led to the control point k. We denote by R k the set of possible valuations x of variables when the control is in k:

R k = { x ∈ Z n | (k, x) ∈ R}.
Then, there exists a trace containing the transition (k, g, a, k ′ ) iff x ∈ R k and g( x) is true. Note that R k does not depend on any initial valuation. More precisely, it is the union, for all initial valuations v, of the set of vectors x such that (k, x) is reachable from v.

In practice, it is difficult to determine the set R k exactly but it is possible to give over-approximations, thanks to the notion of invariants. An invariant on a control point k is a formula φ k that is true for all reachable states (k, x):

x ∈ R k ⇒ φ k ( x) is true.
An invariant is affine if it is the conjunction of a finite number of affine conditions on program variables. The set R k is then over-approximated by the integer points within a polyhedron P k . Some analyzes exist that can compute such a polyhedral approximation. We briefly present in Section 3.1 the technique and software tool we use in our implementation for deriving such affine invariants.

Example 1 (Cont'd)

For the automaton of Figure 1, the vector x is equal to (r, da, db). The most precise affine invariants are:

• for the control point init :

N * × Z 2 . • for loop : {(r, da, db) | 0 ≤ r -1 ≤ da ≤ 2r, r ≤ db ≤ 2r}.

Termination and ranking functions

Invariants can only prove partial correctness of a program. The standard technique for proving termination is to consider ranking functions and well-founded sets, as we now recall.

A well-founded set W is a set with a (total or partial) order (we write a ≺ b if a b and a b) such that there is no infinite descending chain, i.e., an infinite sequence (x i ) i∈N such that x i ∈ W and x i+1 ≺ x i for all i ∈ N.

Definition 3 (Ranking function)

A ranking function is a function ρ : K × Z n → W, from the automaton states to a well-founded set (W, ), whose values decrease at each transition t = (k, g, a, k ′ ):

x ∈ R k ∧ g( x) = true ∧ x ′ ∈ a( x) ⇒ ρ(k ′ , x ′ ) ≺ ρ(k, x) (1)
Definition 4 (1D and kD ranking function) A ranking function ρ is one dimensional if its co-domain is

(N ≤). It is multi-dimensional of dimension k (or k-dimensional) if its co-domain is (N k ≤ lex )
, where ≤ lex is the standard lexicographic order on integer vectors.

INRIA

Obviously, the existence of a ranking function implies program termination for any valuation v at the initial control point k init . The next lemma shows that this existence is also a necessary condition.

Lemma 1 An integer interpreted automaton terminates for any initial valuation if and only if it has a ranking function. Furthermore, if it terminates and has bounded nondeterminism, there is a one-dimensional ranking function, i.e., with co-domain (N, ≤).

Proof If an integer interpreted automaton has a ranking function ρ with co-domain (W, ), but does not terminate for some initial valuation v, then there is an infinite trace (k n , x n ) n∈N from (k init , v). As ρ is a ranking function, the sequence ρ(k n , x n ) is an infinite descending chain in the well-founded set (W, ), impossible.

Conversely, if an integer interpreted automaton terminates for any initial valuation, consider the set W = K × Z n of all its states and define the relation ≺ as follows: if (k, x) ∈ R and (k, g, a, k ′ ) is a transition such that g( x) is true, then define (k ′ , x ′ ) ≺ (k, x) for all x ′ ∈ a( x). Then, extend the relation ≺ to its transitive closure ≺ + . Note that (k 1 , x) ≺ + (k 2 , y) iff there is a trace from (k 1 , x) to (k 2 , y) (this is true because the guards depend only on the current state and not on the traces that lead to it). Finally, consider the relation + defined by x + y iff x ≺ + y or x = y. There is no infinite trace starting from a reachable state (k, x), thus in particular no circuit, hence + is a partial order and it has no infinite descending chain. The identity function on (W, + ) is thus a ranking function.

Finally, suppose that the interpreted automaton terminates and has bounded nondeterminism (see Definition 2). Then, there is a one-dimensional ranking function, i.e., from K × Z n into (N, ≤). Indeed, consider a reachable state (k, x). The previouslydefined relation ≺, when restricting to states reachable from (k, x), i.e., those smaller than (k, x) for ≺ + , corresponds to a DAG rooted at (k, x). This DAG has no infinite path since the automaton terminates. Furthermore, if its paths were of unbounded length, the DAG would be of infinite size, and, by König's lemma, this would contradict the bounded determinism hypothesis. Hence, we may define ρ(k, x) as the maximum length of a path starting from state (k, x). By construction, ρ is a one-dimensional ranking function.

Remark 1

We point out that there is a strong similarity between Lemma 1 and the existence of a free schedule for a computable system of uniform recurrence equations (SURE) defined by Karp,Miller,and Winograd [28,[START_REF] Darte | Scheduling and Automatic Parallelization[END_REF]. For a SURE, a computation (k, x), defined for x ∈ D k , depends on a bounded number of other computations (k i , x i ), 1 ≤ i < p k , where x i = xd i and d i is an integer vector. If x i D i , (k i , x i ) is available as an input, otherwise it has to be computed first. If this "unrolling" of computations terminates, (k, x) can be computed. A schedule σ assigns a "date" (a nonnegative integer) to each (k, x) such that σ(k, x) ≥ σ(k i , x i ) + 1 if (k, x) depends on (k i , x i ). The free schedule is the fastest one if each computation is assumed to take one unit of time. In a SURE and even in a SARE (system of affine recurrence equations for which x i = a i ( x) where a i is an affine function), each state (k, x) depends on a bounded number of other states (k i , a( x)), 1 ≤ i < p k . Therefore, as in Lemma 1, the free schedule exists for a computable SURE or SARE. In other words, SUREs and SAREs are modeled by a structure similar to an affine interpreted automaton. The main difference is in the interpretation, in terms of computations. In systems of recurrence equations, computations actually take place in the opposite order of transition traversals. Furthermore, all traces from a given state are followed. In an interpreted automaton, only some transitions from a given state are performed ("non-determinism"), depending on the guards, and for each transition, only one x ′ ∈ a( x) is considered. But, in terms of properties and algorithms to build them, free schedule and ranking function are very similar.

Remark 2

The (countable) well-founded set W can be embedded in a countable ordinal (following set theory terminology). Each ordinal corresponds to a total order that can be fairly complicated to express or compute in practice. In general, algorithms for termination (or similarly for scheduling SUREs) look for special sets W and ranking functions of a certain class. For example, in [START_REF] Lee | Ranking functions for size-change termination[END_REF], Lee studies ranking functions for a particular approximation of recursive programs, those with the so-called SCT property (size-change termination). According to this study, for SCT programs, it is sufficient to consider "minimums and maximums over lexicographic tuples", i.e., simple functions into the ordinal ω d = (N d , d ), where d stands for the lexicographic order for vectors of size d.

Affine ranking functions

In this paper, in the context of affine interpreted automata, we restrict ourselves to functions ρ(k, x), affine for the second parameter (i.e., when k is fixed), and with co-domain (N d , d ). Characterizing the smallest class of ranking functions (as well as "smallest" ordinal) needed for affine interpreted automata is, to our knowledge, an open problem. However, our algorithm is complete in the sense that it always finds an affine ranking if one exists. Furthermore, the dimension d is determined by the algorithm, and not a priori, and it is the smallest possible.

Note that Floyd [START_REF] Manna | Mathematical Theory of Computing[END_REF] uses a condition weaker than Condition (1): let H be a subset of K such that any cycle of the automaton contains at least one control point in H. Then to prove termination, it is enough to exhibit a function into a well-founded set, which decreases on all paths from one point in H to another. That a ranking satisfying Condition (1) can also serve in this context is obvious. Furthermore, since both techniques are equivalent to termination, the existence of a function ρ decreasing on paths implies the existence of a ranking function ρ ′ , as defined in Section 2.3, i.e., decreasing on transitions. However, both techniques differ when restricting to particular wellfounded sets or class of functions. The next lemma gives a more precise view of the difference between these two proof mechanisms for the simplest case of an interpreted automaton where all actions a( x) define affine functions.

Given the set H, for each transition t = (k, g, a, k ′ ), we define R t,H as follows:

x ∈ R t,H iff x ∈ R k
and there is a trace, starting with the transition t, from (k, x) to (h, y) for some h ∈ H. To prove termination, it is sufficient to check that a ranking function decreases for transition t only for x ∈ R t,H because if x R t,H , any trace starting from (k, x) through the transition t visits a finite number of control points (otherwise it would go through a cycle of the automaton, thus through some h ∈ H).

Lemma 2 Consider an integer interpreted automaton such that all actions a( x) define a function. Suppose there is an affine function

ρ into (N d , d )
, decreasing on all paths between two control points in H. Then, there is a piecewise affine function ρ ′ into (N d+1 , d+1 ), decreasing on all transitions t for all states (k, x) such that x ∈ R t,H .

Proof Since each cycle of the automaton contains a point in H, removing all outgoing edges for vertices in H leads to a DAG G. Given k ∈ K, let h(k) be the height of k, i.e., the length of the longest path, in G, starting from k (if k has no successor, h(k) = 0). The function ρ is defined only for elements in H. The ranking ρ ′ that we build has an

INRIA extra dimension. For k ∈ H and x ∈ R k , we set ρ ′ (k, x) = ρ(k, x) 0 . We extend ρ ′ for all k ∈ K \ H,

by induction on increasing values of h(k).

To make the notations simpler, we denote by ρ(k, x) the first

d dimensions of ρ ′ (k, x), even for k H. Assume ρ ′ is defined for all k ′ such that h(k ′ ) < n. Consider k such that h(k) = n and x ∈ R k . Let t i = (k, g i , a i , k i ), i ∈ [1.
.p], be the transitions such that x ∈ R t i ,H . (If there is no such transition for x, there is nothing to do.) We let:

ρ ′ (k, x) = max d { ρ(k i , a i ( x)) | i ∈ [1..p] } n + 1 .
Thanks to this inductive construction, ρ ′ is decreasing for each transition t = (k, g, a, k ′ ), k H, and

x ∈ R t,H . It remains to consider all transitions t = (k, g, a, k ′ ) such that k ∈ H. Let x ∈ R t,H . By definition of R t,H and construction of ρ ′ , there is h ∈ H such that ρ(k ′ , a( x)) = ρ(h, A( x))
where A is the composition of all actions a along the path to h. The property of ρ on paths implies

ρ(k ′ , a( x)) = ρ(h, A( x)) ≺ d ρ(k, x), thus ρ ′ (k ′ , a( x)) ≺ d+1 ρ ′ (k, x) as desired.
With this construction, if ρ is affine, then ρ ′ is piecewise affine due to the use of the maximum function for defining ρ ′ . The previous lemma shows that there is an interaction between the class of functions we consider and the way we prove termination, either with a (global) ranking function, decreasing for each transition, or with a function decreasing on paths, as Floyd proposes. Also, constraining the ranking function to decrease even for x R t,H is an over-approximation. We will come back to this later.

Generating affine ranking functions for affine interpreted automata

Generating invariants

In this paper, we chose to generate invariants through the use of linear relation analysis [START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF]. We first recall the main characteristics of this method. We first make a restriction on the form of the actions we consider: we restrict to what we call extended affine functions.

Definition 5 (Extended affine function)

An extended affine function a : Z n → (Z ∪ {?}) n assigns to the vector x an extended unique vector x ′ where for all i,

0 ≤ i < n, x ′ [i] ∈ Z ∪ {?}. The i-th component of x ′ is

defined either as an affine function of the components of x or is non deterministic (i.e., it can take any value in Z).

As in Definition 1, the guards g of transitions are polyhedral guards of form G x + g ≥ 0 and actions are extended affine functions. These transitions are called extended guarded affine transitions.

Collecting semantics:

As R k is the set of possible variable valuations when the control is in k, we get, for each k ∈ K:

R k ≡ if k = k init then Z n else (k ′ ,g,a,k)∈T a(R k ′ ∩ g) where R k ′ ∩ g stands for { x ∈ R k ′ | g( x) = true} and a(R k ′ ∩ g) stands for {a( x) | x ∈ R k ′ ∧ g( x) = true}.
The initial invariant can be refined if some information is provided at program start as for Example 1 for the condition r ≥ 1.

Iterative computations

The linear relation analysis consists in attaching to each control point k a polyhedron P k , which is an over-approximation of R k (thus, x ∈ P k is an invariant), as follows:

P k ≡ if k = k init then ⊤ else (k ′ ,g,a,k)∈T a(P k ′ ⊓ g)
where:

• ⊤ denotes the polyhedron representing R n ,

• ⊔ and ⊓ denote respectively the convex union (convex hull) and the intersection of polyhedra,

• a(P k ) = {a( x) | x ∈ P k } is computed by first applying the affine part of a to P k , and then eliminating the "undefined variables" (whose value is specified by the symbol ?). Efficient polyhedral libraries exist for computing these operations, such as Polylib1 , PPL 2 , and the polyhedra part of APRON 3 . We are then left with a system of fixpoint equations (with m = #K):

∀k ∈ K, P k = F k (P 1 , . . . , P k , . . . , P m )
whose least solution exists (by Tarski's theorem) and can be computed by iteration from P k = ⊥ = ∅, ∀k. Of course, this computation will raise the problem of convergence. This problem is solved thanks to the widening operator ∇. The general definition of a widening operator [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] ensures the convergence of the sequence

∀k ∈ K, P k = F ∇ k (P 1 , . . . , P k , . . . , P m )
The functions F ∇ k are defined with a subset K ∇ ⊆ K of "cutting nodes" such that each loop in the program contains at least one control point in K ∇ (this is similar to the set H used in the previous section for Floyd's termination proof method). Then

F ∇ k =        P k ∇F k (P 1 , . . . , P k , . . . , P m ) if k ∈ K ∇ F k (P 1 , . . . , P k , . . . , P m ) otherwise
Finally, the limit, obtained after a finite number of steps, is an over-approximation of the least solution of the initial system. In linear relation analysis, the set of widening nodes K ∇ is usually defined as the set of entry nodes of the strongly connected components of the graph. We also use the standard widening on polyhedra, as defined in [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] and [START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF], which roughly consists in keeping for P 1 ∇P 2 only the constraints of P 1 also satisfied by P 2 .

Aspic tool

To compute invariants, we chose to use the tool A 4 , which provides an implementation of abstract acceleration [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF]. Compared to the standard widening approach, this method computes the exact reachability set for "accelerable" loops, which locally avoids the use of widening and globally increase precision. A takes as input an affine counter automaton and generates an affine invariant for each control point.

Example 1 (Cont'd)

With the initial condition r ≥ 1 and loop exit to end with guard r > da, A produces the following invariants:

• P init = {1 ≤ r};

• P loop = {da ≤ 2r, db ≤ 2r, 1 ≤ r, r ≤ db, r -1 ≤ da}; • P end = {da < r, db ≤ 2r, 1 ≤ r, r ≤ db, r -1 ≤ da}.
We extended A with a -ranking option, which initializes each variable to an unknown value at the initial control point. The discovered invariants are then parameterized by these initial values.

General affine relations

The use of A does not restrict the fragment of programs we are able to deal with since we can encode a general affine transition (see Definition 1) into a combination of two extended affine transitions (see Definition 5).

Lemma 3 A general affine transition (as defined in Definition 1) can be encoded by the sequence of two extended affine transitions.

Proof Let t = (k, g, a, k ′ ) be a general affine transition. Let z be a vector of n fresh variables, and k new a new control point. Then, the transition t is equivalent to the combination of t 1 and t 2 , where:

• t 1 = (k, g, a 1 , k new ) with a 1 ( z) = (?) n • t 2 = (k new , g 2 , a 2 , k ′ ) where g 2 ( x, z) is true iff z ∈ a( x) (affine guard) and a 2 ( x) = z (projection).
In other words, an affine relation that does not define a function is encoded in the guard of a transition. Let us illustrate this construction. The following transition:

k k ′ 3 2x ′ + 7x 19 2y 42
is equivalent to the following couple of transitions:

k k new k ′ z :=?
x ′ := z 2y 42 3 2z + 7x 19

Computing affine ranking functions

This section presents an algorithm to construct multi-dimensional affine ranking functions, i.e., ranking functions ρ : K × Z → N d , affine for the second parameter. The integer d is the dimension of the ranking. For the sake of clarity, we first explain in Section 3.2.1 the particular case d = 1, i.e., how to get a one-dimensional affine ranking function. The method is then generalized in Section 3.2.2 to compute an affine ranking function of dimension d > 1.

Note: as we use linear programming (but not integer linear programming), we may end up with functions with rational components. Then, we can always multiply such a function by a suitable integer to get a ranking function with integer values. Thus, in the rest of the paper, we will not insist on this subtlety any longer.

One-dimensional affine ranking functions

As explained in Section 3.1, in practice, the exact sets R k are not necessarily available. They are over-approximated by invariants P k , with R k ⊆ P k , which are, in our case, described by polyhedra. The conditions that a ranking function must satisfy are then related to these invariants and not to the exact sets of reachable states.

A one-dimensional ranking function ρ has co-domain N, i.e., it assigns a nonnegative integer to each relevant state:

x ∈ P k ⇒ ρ(k, x) ≥ 0 (2)
Consider Inequality [START_REF] Anderson | Affine-based size-change termination[END_REF], which specifies that the ranking decreases on transitions. Let Q t be the polyhedron described by the constraints of a transition t = (k, g, a, k ′ ), i.e., x ∈ P k , g( x) is true, and x ′ ∈ a( x). For an affine interpreted automaton, Q t is directly built from matrices A, A ′ , and G, and vectors a and g (see Definition 1 in Section 2.2). Inequality (1) becomes:

y = ( x, x ′ ) ∈ Q t ⇒ ρ(k, x) -ρ(k ′ , x ′ ) ≥ 1 (3)
More general cases can be handled the same way if the set of pairs ( x, x ′ ) is overapproximated by a polyhedron. Now, it remains to translate Inequalities (2) and (3) into a linear system and to get a ranking function by means of a linear solver. Classically, we use the affine form of Farkas lemma [START_REF] Schrijver | Theory of linear and integer programming[END_REF] to linearize the constraints: Lemma 4 (Farkas lemma, affine form) An affine form φ :

R n → R with φ( x) = c. x + c 0 is nonnegative everywhere in a non-empty polyhedron { x | A x + a ≥ 0} iff: ∃ λ ∈ (R + ) n , λ 0 ∈ R + such that φ( x) ≡ λ.(A x + a) + λ 0
The notation ≡ is a formal equality, which means that x can be eliminated and coefficients identified. In other words:

∃ λ ∈ (R + ) n , λ 0 ∈ R + such that c = λ.
A and c 0 = λ. a + λ 0 For all x, φ( x) is thus expressed as the dot product of x and a nonnegative combination of the normals of the facets of P, plus a nonnegative constant. We can now apply the affine form of Farkas lemma to Inequalities (2) and (3). Write P k x + p k ≥ 0 the constraints that define P k . For Inequality (2), we get:

∃ λ k ∈ (R + ) n , λ 0 k ∈ R + such that ρ(k, x) ≡ λ k .(P k x + p k ) + λ 0 k (4)
Similarly, let us write

Q t = { y = ( x, x ′ ) | Q t y + q t ≥ 0}. We call ∆ t (ρ, x, x ′ ) = ρ(k, x) - ρ(k ′ , x ′ ) the delay of transition t. Inequality (3) states that ∆ t (ρ, x, x ′ ) ≥ 1, which means: ∃ µ t ∈ (R + ) n , µ 0 t ∈ R + s.t. ∆ t (ρ, x, x ′ ) -1 ≡ µ t .(Q t y + q t ) + µ 0 t ( 5
)
A substitution of (4) in ( 5) and an identification on each dimension of y leads to a linear system S t with nonnegative unknowns

λ k , λ 0 k (from ρ(k, x)), λ k ′ , λ 0 k ′ (from ρ(k ′ , x ′
)), µ t , and µ 0 t . Finally, concatenating all S t for all transitions t ∈ T gives a linear system S, with nonnegative unknowns ( λ k , λ 0 k ) k∈K and ( µ t , µ 0 t ) t∈T , that characterizes all onedimensional affine ranking functions for the automaton.

INRIA

Example 1 (Cont'd)

As explained before, A provides the following invariants (the initial values are denoted by r 0 , da 0 , db 0 ):

• P init = {1 ≤ r 0 = r, db = db 0 , da = da 0 } • P loop = {da ≤ 2r, db ≤ 2r, r ≤ db, r -1 ≤ da, 1 ≤ r = r 0 } • P end = {da < r, db ≤ 2r, r ≤ db, r -1 ≤ da, 1 ≤ r = r 0 }
For readability in the following systems, for i ≥ 1 and k ∈ K, we write λ i k instead of λ k [i -1], same for µ. Also x stands for the vector (da, da 0 , db, db 0 , r, r 0 ). The subsystem ( 4) is obtained by applying Farkas lemma to P init , P loop , and P end (here, with no simplification):

(4i) ρ(init, x) = λ 0 init + λ 1 init (r -1) + λ 2 init (r 0 -1) + λ 3 init (r 0 -r) + λ 4 init (r -r 0 ) + λ 5 init (db 0 - db) + λ 6 init (db -db 0 ) + λ 7 init (da 0 -da) + λ 8 init (da -da 0 ) with λ i init ≥ 0 for all i ∈ [0..8]; (4ii) ρ(loop, x) = λ 0 loop + λ 1 loop (2r -da) + λ 2 loop (2r -db) + λ 3 loop (r -1) + λ 4 loop (db -r) + λ 5
loop (dar -1) + λ 6 loop (r 0r) + λ 7 loop (rr 0 ) with λ i loop ≥ 0 for all i ∈ [0..7]; (4iii) and a similar formula for the control point end.

To get the subsystem (5), we first compute Q t (here in logical form):

• Q t 1 = x ∈ P init ∧ da ′ = 2r ∧ db ′ = 2r ∧ r ′ = r; • Q t 2 = x ∈ P loop ∧ r ≤ da ∧ da ′ = da -1 ∧ db ′ = db ∧ r ′ = r; • Q t 2 = x ∈ P loop ∧ r ≤ da < db ∧ da ′ = db -1 ∧ db ′ = da ∧ r ′ = r.
And, finally, we obtain:

(5i) ρ(init, x) -ρ(loop, x ′ ) -1 = µ 0 t 1 + µ 1 t 1 (r 0 -1) + µ 2 t 1 (r -r 0 ) + µ 3 t 1 (r 0 -r) + . . . + µ 7 t 1 (da ′ -2r) + µ 8 t 1 (2r -da ′ ) + µ 9 t 1 (db ′ -2r) + µ 10 t 1 (2r -db ′ ) + . . . with µ i t 1 ≥ 0 for all i;
(5ii) and similar expressions for transitions t 2 and t 3 .

In (5i), we replace the expressions involving ρ by the values obtained in (4i) and (4ii). We do the same in the other expressions coming from [START_REF] Bouajjani | Minimal state graph generation[END_REF]. We obtain a conjunction of conditions involving the different λ k and µ k . The solver finally produces:

• ρ(init, x) = 2r 0 + 3; • ρ(loop, x) = 2 + da + db -2r; • ρ(end, x) = 0.
which means that the loop terminates in at most 2r 0 + 3 steps (including at most 2r 0 + 1 iterations of the while loop). The quantity i = 2 + da + db -2r, which is automatically extracted, can be viewed as a kind of counter for the while loop.

Solving the system S gives a termination test that will work providing the invariants are accurate enough. Note however that, since ρ is, so far, affine and one-dimensional, there is no hope, with this method, to be able to determine the termination of an automaton whose worst time complexity (WTC), i.e., maximal trace length, is more than linear in the input variables. The extension in the next section can determine the termination of some programs with a non-linear (but still polynomial) time complexity.

Multi-dimensional affine ranking functions

Using multi-dimensional affine ranking functions, i.e., affine ranking functions with codomain (N d , d ) for some integer d, extends the set of programs whose termination can be determined. Indeed, some terminating programs with polynomial time complexity (of degree ≤ d) can now be handled, while no one-dimensional affine ranking function exists for them. Furthermore, when it exists, a polynomial WTC can be derived from the ranking, with a simpler method than by manipulating directly polynomials of degree d.

For a d-dimensional ranking function ρ, the decreasing constraint expressed by Inequality (1) becomes:

( x, x ′ ) ∈ Q t ⇒ ∆ t (ρ, x, x ′ ) ≻ d 0 (6)
which means that ∆ t (ρ, x, x ′ ) 0 and its first nonzero component is positive. Unlike for a one-dimensional ranking function where we look for a function ρ such that ρ(k, x) -ρ(k ′ , x ′ ) ≥ 1, here we consider each dimension σ = ρ[i] of ρ with the relaxed constraint:

(

x, x ′ ) ∈ Q t ⇒ σ(k, x) -σ(k ′ , x ′ ) ≥ ε t (7)
with 0 ≤ ε t ≤ 1. As we did in Section 3.2.1, we obtain a linear system S t ( λ k , λ 0 k , λ k ′ , λ 0 k ′ , µ t , µ 0 t , ε t ) for each transition, this time with the additional unknown ε t . Then, considering all transitions, we get a global system S. For a solution σ of S, we say that a transition t is satisfied if ε t = 1, otherwise, it is respected.

To build a multi-dimensional ranking ρ, we use a greedy algorithm, similar to the scheduling algorithm of [START_REF] Feautrier | Some efficient solutions to the affine scheduling problem, part II, multi-dimensional time[END_REF], that builds the different dimensions of ρ, one after the other, from dimension 0 to dimension d -1, respecting unsatisfied transitions until all are satisfied for some dimension. Furthermore, for each dimension, we try to satisfy as many transitions as possible by maximizing the number of ε t equal to 1. This boils down to solving the following optimization:

m = max          t∈T ε t | t=(k,g,a,k ′ )∈T S t ( λ k , λ 0 k , λ k ′ , λ 0 k ′ , µ t , µ 0 t , ε t )          (8)
It is easy to see that any solution leading to some ε t > 0 can be multiplied by a suitable positive constant to a solution with ε t = 1. Thus, for any optimal solution of (8), a transition t satisfies either ε t = 0 or ε t = 1. Similarly, one can build an integer optimal solution from any rational optimal solution. The variables ( λ k ) k∈K define an affine function that we use as the first dimension of ρ. By construction, ρ[0] satisfies (3) for every transition t such that ε t = 1. Other transitions are simply respected (ε t = 0). We process them in the subsequent dimensions. For that, we build a new system S, obtained by concatenating the different S t , but only for the transitions t with ε t = 0, and we iterate the process. This way, we define ρ [START_REF] Anderson | Affine-based size-change termination[END_REF], ρ [START_REF] Amir | A complexity tradeoff in ranking-function termination proofs[END_REF], and so on. When none of the remaining transitions can be satisfied, i.e., when the maximum m is 0, the algorithm stops and no multi-dimensional ranking function is found. Otherwise, as the number of transitions is finite, all of them are eventually satisfied, after a finite number of steps, by some dimension of ρ. In this case, the algorithm outputs, for each k ∈ K, an affine function ρ(k, .) : Z n → N d k , where d k is the number of successive systems, involving the control point k, that were solved. We can complete each ρ(k, .) with arbitrary additional dimensions so that they all have co-domain N d , with d = max k d k . This defines an affine ranking function ρ of dimension d.

Example 2 Consider the automaton of Figure 2 with the context N ≥ 0 in control point k 0 . Aspic finds the following invariants:

• P k 0 = {0 ≤ N = N 0 , j = j 0 , i = i 0 }; • P k 1 = {0 ≤ N = N 0 , 0 ≤ i ≤ N}; • P k 2 = {0 ≤ N = N 0 , 1 ≤ i ≤ N, 0 ≤ j ≤ N}.
Solving the system while maximizing

ε t 1 + ε t 2 + ε t 3 + ε t 4 leads to ε t 1 = ε t 2 = ε t 4 = 1 and ε t 3 = 0. The corresponding function (first dimension of the ranking) is ρ(k 0 , x)[0] = INRIA k 0 k 1 i := N k 2 j > 0 j := N j = 0 t 1 t 2 i > 0 t 4 t 3 j -- i -- Figure 2: Automaton with a multi-dimensional ranking 2N + 1, ρ(k 1 , x)[0] = 2i, ρ(k 2 , x)[0] = 2i -1.
We keep the transition t 3 for the next dimension, and we get ε

t 3 = 1 with ρ(k 2 , x)[1] = j. The complete ranking function is thus ρ(k 0 , x) = 2N + 1, ρ(k 1 , x) = 2i, ρ(k 2 , x) = (2i -1, j).
Note that, for k 0 and k 1 , the ranking is only one-dimensional. It can be extended arbitrarily, for example as ρ(k 0 , x) = (2N + 1, 0) and ρ(k 1 , x) = (2i, 0), if a globally 2D ranking function is desired.

Completeness

Since non-terminating programs exist, there is no hope of proving that a ranking function always exists. Moreover, there are terminating affine interpreted automata with no multi-dimensional affine ranking. Thus, all we can prove is that, if a multi-dimensional affine ranking exists, our algorithm finds one. This section gives such a completeness result. Also, as the sets R k are over-approximated by invariants P k , completeness has to be understood with respect to these invariants. We first need a few definitions and lemmas.

We say that a lexicographically positive vector x is of level i if its i-th component is its first nonzero component: x[ j -1] = 0 if j < i and x[i -1] > 0. Without loss of generality, we assume that all d-dimensional ranking functions we consider are such that d equals ℓ, the maximal level of all ∆ t (ρ, x, x ′ ). Indeed, all dimensions ρ[i] for i ≥ ℓ are useless to decrease on transitions. We can also define the sum of two multidimensional ranking functions of dimensions d 1 and d 2 , even if d 1 d 2 , as stated by the next lemma.

Lemma 5 Let ρ 1 and ρ 2 be two multi-dimensional ranking functions of dimensions d 1 and d 2 . One can define a ranking ρ of dimension d

≤ min (d 1 , d 2 ) such that ρ[i] = ρ 1 [i] + ρ 2 [i], for all i < d.
Proof Assume, without loss of generality, d 1 ≤ d 2 . We can first extend ρ 1 by d 2d 1 null dimensions and compute ρ 1 + ρ 2 . Since delays are linear in the ranking functions and since the sum of two lexicopositive vectors is lexicopositive, ρ 1 + ρ 2 is a ranking function. Note that if u 1 and u 2 are both lexicopositive with levels l 1 and l 2 , then the level of u 1 + u 2 is min(l 1 , l 2 ). Thus, the maximal level d of all ∆ t (ρ, x, x ′ ) is at most min(d 1 , d 2 ). It follows that all dimensions of ρ 1 + ρ 2 beyond d ≤ d 1 are useless and can be removed.

A consequence of Lemma 5 related to our greedy algorithm is that, if a transition t 1 (resp. t 2 ) is satisfied by the first dimension of a ranking ρ 1 (resp. ρ 2 ), then the first dimension of ρ 1 + ρ 2 satisfies both transitions. Thus, there is no trade-off to make when deciding which transitions to satisfy at the dimension being considered.

Lemma 6 If ρ is a d-dimensional ranking function and T a lower triangular d × d matrix, with positive diagonal, then T ρ, defined by

(T ρ)( x) = T (ρ( x)), is a ranking function. Proof We have ∆ t (T ρ, x, x ′ ) = T ∆ t (ρ, x, x ′ ). Let ℓ be the level of ∆ t (ρ, x, x ′ ). For i < ℓ -1, ∆ t (T ρ, x, x ′ )[i] = ∆ t (ρ, x, x ′ )[i] = 0. For i = ℓ -1, ∆ t (T ρ, x, x ′ )[i] = T i,i × ∆ t (ρ, x, x ′ )[i] > 0. Thus ∆ t (T ρ, x, x ′
) is lexicographically positive and its level is ℓ. The remaining components are irrelevant. Lemma 6 will be used to show that if a transition is only partially satisfied (i.e., ε t = 0 but there are some x and x ′ such that ∆ t (ρ[0], x, x ′ ) ≥ 1), then we can still keep considering these satisfied pairs ( x, x ′ ) for further dimensions. This will not prevent the algorithm to find an affine ranking if one exists.

We now need a technical lemma, which generalizes the affine form of Farkas lemma to lexicographic order. Under its hypotheses, Lemma 7 states that we can always replace an affine function of dimension d by a linear combination of its dimensions (thus a function of dimension 1) and get the same "satisfied" vectors.

Lemma 7 Let P = { x | A x + a ≥ 0} be a polyhedron and δ a d-dimensional affine function such that, ∀ x ∈ P, δ( x) d 0 and not all δ( x), x ∈ P, have level < d. Then, there is α such that, ∀ x ∈ P, α.δ( x) ≥ 0 and α.δ( x) 0 if δ( x) 0. More precisely, there is a matrix Λ whose rows are lexicographically nonnegative and such that any α is suitable, provided that α

[d -1] > 0, Λ α ≥ 0 and (Λ α)[i] = 0 only if the corresponding row of Λ is 0.
Proof Let P i be the set of x ∈ P such that δ( x) has level > i. By definition, P 0 = P and

P i+1 = P i ∩ { x | δ[i]( x) = 0}. Since not all δ( x) have level < d, P i ∅ for all i < d.
For all x ∈ P 0 , δ[0]( x) ≥ 0. Since P 0 ∅, by Farkas lemma, δ[0]( x) ≡ λ 0 .(A x + a) + r 0 with λ 0 ≥ 0 and r 0 ≥ 0. If d > 1, δ[0]( x 0 ) = 0 thus r 0 = 0. Furthermore, if x ∈ P 0 , δ[0]( x) = 0 iff (A x + a)[i] = 0 for each i such that λ 0 [i] > 0:

P 1 = { x | A x + a ≥ 0; (A x + a)[i] = 0 if λ 0 [i] > 0}
where some inequalities that define P 0 are now equalities. The same study can now be done for P 1 if d > 2. The only difference is that, because of the equalities (called saturated inequalities), Farkas lemma leads to δ [START_REF] Anderson | Affine-based size-change termination[END_REF]

( x) ≡ λ 1 .(A x + a) with λ 1 [i] ≥ 0 if λ 0 [i] = 0 (standard inequality), otherwise λ 1 [i] can be of any sign if λ 0 [0] > 0 (saturated inequality). Then, for x ∈ P 1 , δ[1]( x) = 0 iff (A x + a)[i] = 0 for each i such that λ 0 [i] = 0 and λ 1 [i] > 0.
Finally, by induction, we get the following properties, for all 0 < j < d:

• P j = P j-1 ∩ { x | (A x + a)[i] = 0 if λ j-1 [i] > 0}, i.e., P j = P ∩ { x | (A x + a)[i] = 0 if ∃k<j s. t. λ k [i] > 0}; • δ[ j]( x) ≡ λ j .(A x + a) + r j ; • r j = 0 if j < d -1, r d-1 ≥ 0; • λ j [i] ≥ 0 if λ k [i] = 0 for all k < j.
The last property can be interpreted as follows. If Λ is the matrix whose columns are the vectors λ, then each row of Λ is lexicographically nonnegative. Thus, there exists α such that Λ α ≥ 0 (component-wise) and (Λ α)[i] = 0 only if the corresponding row INRIA of Λ is equal to 0. For that, we just need to define the components of α successively, from the last one to the first one. Indeed, a row i of Λ of level j + 1, thus with Λ i, j > 0 and Λ i,k = 0 for k < j, corresponds to a constraint k≤ j Λ i,k α[k] > 0, i.e., it gives a lower bound on α[ j], once all α[k], for k > j, have been fixed:

α[ j] > - k> j λ k [i] α[k] λ j [i]
We can also choose α such that α

[d -1] > 0. Now, for such α, α.δ( x) = (Λ α).(A x + a) + α[d -1]r d-1
, thus α.δ( x) ≥ 0 for all x ∈ P. It remains to show that α.δ( x) 0 if δ( x) 0. Let ℓ be the level of δ( x). If ℓ < d, x ∈ P ℓ-1 and x P ℓ . Thus δ[ℓ -1]( x) > 0 and there is i such that λ ℓ-1 [i] > 0 and (A x + a)[i] > 0. Thus, Λ i,ℓ-1 > 0, then α[i] > 0, and finally α.δ( x) > 0. If ℓ = d, the situation is the same except that it is possible that λ ℓ-1 .(A x + a) = 0. But, in this case, we must have r d-1 > 0 and again α.δ( x) > 0.

Note that our algorithm, described in Section 3.2.2, looks for a function that always fully satisfies at least one transition, otherwise it stops. Lemma 8 shows that this strategy is not a restriction, at least for the first dimension.

Lemma 8 If an affine interpreted automaton has an affine ranking function ρ, then there is an affine ranking function ρ ′ , of same dimension, whose first dimension fully satisfies at least one transition

, i.e., ∃ t ∈ T such that ∀( x, x ′ ) ∈ Q t , ∆(ρ ′ [0], x, x ′ ) ≥ 1.
Proof The trick is to use Lemma 7 to replace the first dimension of ρ by a linear combination of the first ℓ min dimensions that, all together, satisfy all constraints of at least one transition. ℓ min is defined as follows. For each transition t, each ∆ t (ρ, x, x ′ ) is a lexicographically positive vector. Let ℓ t be the maximal level of all ∆ t (ρ, x, x ′ ) for ( x, x ′ ) ∈ Q t . Then ℓ min is the minimum of all ℓ t .

For each transition t = (k, g, a, k ′ ), let δ t be the affine function of dimension ℓ min defined, for all y = ( x, x ′ ), by the first ℓ min components of ρ(k, x) -ρ(k ′ , x ′ ): δ t satisfies the hypotheses of Lemma 7 for Q t . Let Λ be the matrix formed by all rows of the matrices Λ t associated to the different δ t . Its rows are all lexicographically nonnegative, thus again, we can select α such that, for all t ∈ T and for all y ∈ Q t , α.δ t ( y) ≥ 0 and α.δ t ( y) 0 if δ t ( y) 0.

We now come back to ρ. We extend α, with 0s, to get a vector with same dimension as ρ. Then α.ρ is a linear combination of the first ℓ min dimensions of ρ. By construction, if t ∈ T and ( x, x ′ ) ∈ Q t , ∆( α.ρ, x, x ′ ) ≥ 0 and ∆( α.ρ, x, x ′ ) > 0 if the level of ∆(ρ, x, x ′ ) is ≤ d. Thus, replacing ρ[0] by α.ρ defines a ranking ρ ′ whose first dimension fully satisfied all transitions t such that ℓ t = ℓ min .

Note: so far, we did not enforce ( α.ρ)(k, x) ≥ 0 for all x ∈ P k . We can handle this additional constraint thanks to Lemma 7 again. We can also simply impose directly α ≥ 0 (component-wise). We can now use all lemmas to prove the algorithm completeness.

Theorem 1 If an affine interpreted automaton, with associated invariants, has an affine ranking function, then the algorithm of Section 3.2.2 finds one and its dimension is minimal.

Proof Consider an affine ranking function ρ of dimension d. According to Lemma 8, there is an affine ranking function ρ ′ of dimension d that fully satisfies at least one transition. Thus, the algorithm of Section 3.2.2 succeeds to generate a one-dimensional function σ, which maximizes the number of fully satisfied transitions. In particular, σ fully satisfies all transitions fully satisfied by ρ ′ , otherwise, as showed for Lemma 5, the function ρ ′ [0] + σ fully satisfies more transitions than σ, a contradiction. Thus, if we replace ρ ′ [0] by σ, we get a new ranking ρ ′′ of dimension d. Now, there is a subtlety. For computing the next dimension of the ranking function with the algorithm of Section 3.2.2, we could consider only the pairs ( x, x ′ ) ∈ Q t such that ∆ t (σ[0], x, x ′ ) = 0. Nevertheless, to make the algorithm simpler, we keep the whole Q t as soon as the transition t is not fully satisfied. We need to show that this strategy does not weaken the algorithm. We use again Lemma 7, considering this time only the transitions t not fully satisfied by ρ ′′ [0] = σ. Again, for these transitions, the hypotheses of Lemma 7 are fulfilled if we consider the two first dimensions of ∆ t (ρ ′′ , x, x ′ ). As we did for Lemma 8, there is a (one-dimensional) linear combination δ of ρ ′′ [0] and ρ ′′ [START_REF] Anderson | Affine-based size-change termination[END_REF] such that ∆(δ, x, x ′ ) ≥ 0 and ∆(δ, x, x ′ ) > 0 if ∆(ρ ′′ , x, x ′ ) has level ≤ 2. Finally, if we replace the second dimension of ρ ′′ by δ, Lemma 6 shows that we get a new ranking function ρ ′′′ of dimension d. Furthermore, by construction of δ, the last d -1 dimensions of ρ ′′′ satisfy all transitions not fully satisfied by its first dimension, i.e., by σ, the first dimension generated by the algorithm of Section 3.2.2.

We can now iterate the process similarly until all transitions are satisfied, which shows that the algorithm of Section 3.2.2 generates a ranking of dimension at most d. This is true for any d, dimension of an affine ranking function, thus the ranking function generated by the algorithm of Section 3.2.2 has minimal dimension.

To summarize the proof, we start from an affine ranking of dimension d. We show that there is an affine ranking of dimension d that fully satisfies at least one transition. This proves that our algorithm does not stop and generates a one-dimensional function σ. Then, we show that there is an affine function of dimension d first dimension is σ. Finally, we show that there is an affine function of dimension d, whose first dimension is σ, and such that the d -1 last dimensions satisfy all transitions not fully satisfied by σ. Iterating the process, this shows our algorithm terminates and generates an affine ranking of dimension ≤ d, for any possible dimension d.

Remark 3

The proof of Theorem 1 is similar to the proof given in [START_REF] Vivien | On the optimality of Feautrier's scheduling algorithm[END_REF] of the optimality of the multi-dimensional scheduling algorithm of Feautrier [START_REF] Feautrier | Some efficient solutions to the affine scheduling problem, part II, multi-dimensional time[END_REF]. The main difference is that we handle the general case of transitions where a( x) is a set not just a singleton, i.e., we do not assume that the actions are functions. Also, as far as we could check, the initialization of the induction in Theorem 1, i.e., the fact that the algorithm fully satisfies at least one transition if a multi-dimensional affine function exists, seems to be missing in [START_REF] Vivien | On the optimality of Feautrier's scheduling algorithm[END_REF]. In our proof, this property is given by Lemma 8.

Scalability

The size of the system (8) is roughly proportional to the number of transitions in the automaton. This may be too much for the underlying linear solver. However, the situation can be improved along the lines of [START_REF] Feautrier | Scalable and structured scheduling[END_REF]. Notice first that each transition has its own set of Farkas multipliers, the µ t of (5). These multipliers can be eliminated one transition at a time, thus leaving only the λ k as unknowns. Furthermore, the unknowns in the constraint system for a transition pertain only to the source and sink of the transition. Hence, the grand constraint system (8) is a block representation of the connexion graph of the automaton: each system (5) generates a block of rows in which only the columns corresponding to the unknowns for the source and sink of transition t INRIA are nonzero. These unknowns can be successively eliminated using various heuristics (e.g., eliminate first the unknowns for a state of minimum degree), leaving only a system of constraints on the ε t , which is then solved for the maximum σ. The different λ are then recovered by a process of back substitution, and there is no need to compute the µ t .

In these algorithms, elimination (or projection) turned out to be best achieved by a combination of Gaussian elimination, controlled Fourier-Motzkin elimination, and Chernikova algorithm.

Worst-case time complexity

As shown in the survey by Wilhelm et al. [START_REF] Wilhelm | The determination of worst-case execution times-overview of the methods and survey of tools[END_REF], the computation of a worst-case execution time (WCET) is a highly complex affair, as it has to take into account the program, its data, and the processor on which it is run. Handling all these complexities is beyond the scope of our paper. Our aim is to evaluate an abstract WCET, as would be observed on a processor with a perfectly additive timing model, executing one automaton transition in unit time. We call this quantity the worst time complexity of the program (WTC). Such an estimate can be useful, for example as a template with unknown coefficients, to be fitted to actual measurements by a process of regression. It is also standard in high-level synthesis to need an upper-bound on the number of loop iterations ( loops as well as  loops), to enable scheduling optimization at higher level. We thus define the WTC as an upper bound on the number of transitions executed, given an initial value of the counter variables.

With this definition, one could over-approximate WTC by the total number of reachable states, i.e., WTC ≤ k #R k or even more conservative WTC ≤ k #P k as R k is itself over-approximated by P k . In addition to the fact that this is a very rough over-approximation, this technique can even lead to an infinite WTC, even for a terminating automaton, if some P k is unbounded. Rather, we use the ranking function itself to select the useful bounded constraints. Indeed, consider a trace (k 0 , x 0 ), (k 1 , x 1 ), . . . , (k p , x p ) in the execution of the automaton. Since by definition of a ranking function, ρ(k i+1 , x i+1 ) ≺ ρ(k i , x i ), and since ≺ is a strict order, it follows by transitivity that all ρ(k i , x i ) are distinct in W. Hence, the length of the trace is bounded by the cardinal of the co-domain of ρ:

WTC ≤ # k ρ(k, P k ) ≤ k #ρ(k, P k ) (9)
The first inequality is more accurate but harder to compute as it involves a union of sets. Counting integer points means considering Z-polyhedra, i.e., intersections of an integer lattice (e.g., Z n ) and a polyhedron (e.g., P k ). As x → ρ(k, x) is affine, the number of integer points in ρ(k, P k ) can be over-approximated as the cardinal of some Z-polyhedron (e.g., using Smith form) or computed exactly as the number of points in the image of a Z-polyhedron by an affine function. Such problems have been deeply studied in the context of high performance computing, using various techniques related to Ehrhart polynomials [START_REF] Clauss | Counting solutions to linear and nonlinear constraints through Ehrhart polynomials: Applications to analyze and transform scientific programs[END_REF][START_REF] Clauss | Handling memory cache policy with integer points counting[END_REF][START_REF] Verdoolaege | Experiences with enumeration of integer projections of parametric polytopes[END_REF][START_REF] Verdoolaege | Counting integer points in parametric polytopes using Barvinok's rational functions[END_REF]. To deal with unions, it is also possible to use tools that generate loops from polyhedra, such as Cloog 5 , which implements a modified version of [START_REF] Quilleré | Generation of efficient nested loops from polyhedra[END_REF]. Then, counting points directly in loops is also an option as done in [START_REF] Lokuciejewski | A fast and precise static loop analysis based on abstract interpretation, program slicing, and polytope models[END_REF].

We point out that, in the present version, the WTC is computed according to the rightmost expression in [START_REF] Chawdhary | Ranking abstractions[END_REF]. Implementing a more precise version, with unions, is left for future work.

Example 2 (Cont'd) In this very simple, fully-deterministic, example, the two inequalities of (9) lead to the same upper bound WTC ≤ 1 + (N 0 + 1) + N 0 (N 0 + 1) = 1 + (N 0 + 1) 2 .

Experimental results

We have built a tool suite that converts a C program into an integer interpreted automaton, constructs its invariants, tests its termination and, if successful, computes an upper bound for its WTC.

Implementation The first tool, c2fsm is just an exercise in parsing and control graph construction. The main difficulties come from the complexity of C syntax and semantics, and mainly from the convention that an assignment can occur at any depth in an expression. Our guidelines have been to consider only assignments to integer variables, and to give a variable the bottom value unless it is assigned an affine form in other integer variables. The fact that C has no Booleans is both a simplification and a hindrance, as it forbids the use of some of the techniques that were developed for synchronous languages compilation [START_REF] Bouajjani | Minimal state graph generation[END_REF]. The result of this analysis is presented as a system of states and transitions in the input format of A which is responsible for the computation of invariants. The reader is referred to [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] or [START_REF] Danthony-Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF] for a full description of A.

The ranking algorithm and the worst time complexity are implemented in a tool called R. The minor premise of Farkas lemma (the fact that the polyhedron is non-empty) and the system 8 are solved with the PIP tool (Parametric Integer Programming), now wrapped in the Piplib library 6 . The Ehrhart polynomials part of the Polylib library is then used for computing time complexities.

Preliminary results

This tool chain has been tested on a large set of benchmarks from the literature. Most of the examples were collected in [START_REF] Chawdhary | Ranking abstractions[END_REF] from many other papers dealing with termination analysis. They can be found at the following web address: http://www.dcs.qmul.ac.uk/~aziem/esop/.

Furthermore, the source code for all the examples (including ours) are given in the appendix, following the order of the results. The results are summarized in Table 1. The test cases we developed for checking our algorithm are marked by ♣. first two columns give information about the test cases. The third column gives statistics about the (generated) interpreted automaton, in the following way: number of relevant variables, number of control points, number of transitions. The fourth column gives either the dimension of the ranking function if the algorithm succeeds, or DK ("don't know") if it fails to prove termination. The timing measurements (last column) have been done on a 2 GHz Pentium with 1 GByte of memory running Debian 2.6. These measures include the invariants computation time from the A file, the computation of the ranking function, and the evaluation of the WTC.

Name

Comments

In most cases, we were able to prove termination, even for nondeterministic examples like random2d in Table 1. Nested loops are correctly handled, and we find multi-dimensional rankings for them. The case of recursion is often handled by making assumptions about (the values of) the variables after a recursive call (for instance we assume that the result of ackermann is always positive). We were also able to prove the termination of some sortings algorithms like bubblesort and insertsort. The ranking we discover for bubblesort may seem of the wrong dimension, but the additional dimensions have constant values and the order of magnitude of the WTC is still O(size 2 ) as expected. For the nestedLoop example, which has a very complicated iteration domain, most of the time (16s) is spent in computing the WTC. However, we are for the moment unable to prove the termination of mergesort due to scalability reasons. Note also that we did not try yet to eliminate redundant variables or constraints in the different algorithms. We therefore manipulate polyhedra of higher dimensions than needed. In addition, since the termination of concurrent programs depends on a fairness hypothesis, we were unable to solve some of the examples of [START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF]. We found the precision of our algorithm to be strongly dependent on the quality of the invariants, and also the quality of the affine approximation of some (non affine) affectations in the C programs. Moreover, in many cases we had to add some preconditions on the values of initial variables. It seems that most of these preconditions were not mentioned in the literature. However, some of them can be precomputed with a forward-backward analysis, like in [START_REF] Cousot | Proving program invariance and termination by parametric abstraction, Lagrangian relaxation, and semidefinite programming[END_REF].

Related work

Using ranking functions to prove correctness was first proposed in [START_REF] Floyd | Assigning meaning to programs[END_REF]. Early approaches were semi-automatic: one had to guess ranking functions, and then prove their correctness using some form of Hoare logic. Attempts to automate this process followed [START_REF] Colón | Synthesis of linear ranking functions[END_REF][START_REF] Colón | Practical methods for proving program termination[END_REF][START_REF] Bradley | Linear ranking with reachability[END_REF]. It was then realized that one-dimensional rankings were not powerful enough, and propositions to build multi-dimensional [START_REF] Bradley | The polyranking principle[END_REF] or polynomial rankings [START_REF] Cousot | Proving program invariance and termination by parametric abstraction, Lagrangian relaxation, and semidefinite programming[END_REF] followed. We believe that our method (which was suggested by our previous work on scheduling [START_REF] Feautrier | Some efficient solutions to the affine scheduling problem, part II, multi-dimensional time[END_REF]), is a satisfactory solution to this problem.

However, the applicability of our method to large programs is still to be ascertained. In [START_REF] Manna | Termination of programs represented as interpreted In Spring Joint Computer Conference[END_REF], Manna suggested to select a subset of the states of the automaton (cutpoints) in such a way that each cycle in the graph crosses at least one cut point. Termination follows if one can find a ranking function, defined only on the cut points, and which decreases on each path from a cut point to another cut point. It is easy to extend such a function to all states (see Lemma 2) but the resulting global ranking will use the max operator, and may therefore be just piecewise affine rather than affine. It is clear that this method is a way of reducing the program automaton by removing states and merging transition by relation composition. This can be done before the computation of invariants, or after application of Farkas lemma, as suggested in Section 3.4. Assessing the relative merits of these two approaches is left for future work.

A large body of research followed the introduction of the size change termination (SCT) principle in [START_REF] Chin | The size-change principle for program termination[END_REF]. The difference in the two approaches are mainly in semantics: the automaton represents a call graph instead of a control graph, and the variables may be summary information about data structures, like the length of a list or the size of a tree. More importantly, the relations between input and output variables of a transition are restricted to one of the two forms x ′ < y and x ′ ≤ y. An attempt to lift this INRIA restriction can be found in [START_REF] Anderson | Affine-based size-change termination[END_REF]. In [START_REF] Amir | A complexity tradeoff in ranking-function termination proofs[END_REF], it is shown that termination of an SCT system can be proved using an exponential number of very simple local ranking functions, or with a global ranking function involving an exponential number of subterms. This is in contrast to a very simple consequence of Theorem 1, that the dimension of our ranking function is no larger than the number of transitions (and even no larger than the number of variables with some stronger hypotheses [START_REF] Darte | Scheduling and Automatic Parallelization[END_REF]). The explanation is probably that the two sets of programs for which our algorithm succeeds and for which the SCT formalism succeeds are almost disjoint.

Another trend of research has been started in [START_REF] Podelski | Transition invariants[END_REF] and pursued in [START_REF] Chawdhary | Ranking abstractions[END_REF]. Here, one uses several (local) ranking relations, all of them well founded, the intuition being that each relation proves termination of a part of the program. A consistency condition is necessary: the transitive closure of the transition relation of the program must be included in the union of all local ranking relations. The problem is how to find the local rankings, and how to prove the consistency condition. It may be that we can help at least for the first problem: apply our algorithm to cleverly chosen subsets of the automaton states, as for example strongly connected components or loops.

Conclusion

Contributions

The main contribution of this paper is the design of an algorithm for the construction of multi-dimensional ranking functions, which, in contrast to to the combinatorial algorithm of [START_REF] Bradley | The polyranking principle[END_REF], is greedy but nevertheless complete (with respect to the invariants found and the class of ranking functions considered) and optimal in the dimension of the ranking function. The algorithm makes no assumption whatever on the shape of the source program, and can handle, with proper preprocessing (i.e., after the program is approximated to fit into the affine interpreted automaton model), multiple loops of arbitrary nesting patterns, premature termination and goto's, nondeterministic choices and values, exceptions, and Boolean guards of arbitrary structure. Note also that, in case of failure, our algorithm can also exhibit an execution trace which may not terminate, but all the details are not worked up yet.

The computation of the worst time complexity (WTC) is delegated to a very comprehensive stand-alone algorithm. This means that no arbitrary restrictions about the shape of loops and tests are necessary. We can directly rely on existing methods and tools for counting integer points within Z-polyhedra and images of Z-polyhedra by affine functions. More generally, our work establishes a strong link with computation models, theoretical results, and tools, developed by the automatic parallelization and high-performance computing community, and which seem to be not so used (or partly re-discovered) in the context of program termination. We believe that this connection can lead to further fruitful developments to face other problems faced by both communities.

Future work

There is nevertheless room for many improvements. The preprocessor we use for converting a program into an interpreted automaton is somewhat brute force: any construct that is not affine in integer variables is replaced by the bottom value, which is absorbing (⊥ ⊕ x = ⊥ for most operators), and which prints as true in a guard and as a ques-tion mark in an action. This can be improved by noticing that some operations, like modulo and integer division, can be linearized by the introduction of fresh variables, or that a bottom value may be constrained: for instance, a square is always non-negative. Also, variables with a finite domain, like Booleans and enums, can be used to refine the states. This may cost a large increase in the size of the automaton but has the direct benefit of extending the class of ranking functions considered, as these do not need to be affine anymore for such "unrolled" variables. Making sure that domains of integer variables are "fat" (to use the terminology of [START_REF] Darte | Linear scheduling is nearly optimal[END_REF]) increases the chance that an affine ranking exists and improves the quality of WTC produced.

There is always room for improving an invariant constructor like A. One may for instance improve the acceleration algorithms and loops treatment, or use additional abstract interpretation frameworks, like the congruences and lattices of [START_REF] Granger | Static analysis of linear congruence equalities among variables of a program[END_REF]. Also, to prove program termination, it may be interesting to try to combine the construction of the invariants and of the ranking functions to increase the accuracy of the method, thanks to a better control on how widening is performed when computing invariants.

Last but not least, the power of the ranking algorithm can be increased in many ways. For instance, experiments have shown that imposing that ranking functions are nonnegative everywhere (see Inequality 2) is too strong a constraint in many cases. It is enough to impose it at a set of cut points. If the automaton graph becomes acyclic when these cut points are removed, then termination is still guaranteed, notwithstanding the relaxed nonnegativity constraint.

Research on the SCT paradigm has shown that ranking functions of a more complex shape, like piecewise affine functions, are necessary in some cases. In our framework, this means splitting the invariant of some state(s) by an affine constraint. How to choose the states to split and the splitting predicate is left for future research.

There remains the question of interprocedural termination. If there is no recursive call, one may resort to inlining, but this will raise again the question of scalability. One may want to combine the SCT approach with the present one: if there is no infinite path in the call graph, and no infinite path in each function control graph, then termination is guaranteed. However, in many cases, the caller and the callee may interact in complex ways, especially in the presence of side effects, and this will greatly complicate a termination test.

A point we have not investigated is the termination of distributed programs. Our algorithm fails when termination depends on a fairness hypothesis.

1 t 1 t 2 t 3 Figure 1 :

 1131 Figure 1: Affine interpreted automaton

2 . 2 2 . 3 6 3affine ranking functions for affine interpreted automata 9 3 . 1 3 . 2

 222363132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Integer interpreted automata . . . . . . . . . . . . . . . . . . . . . . 4 Termination and ranking functions . . . . . . . . . . . . . . . . . . . Generating Generating invariants . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Computing affine ranking functions . . . . . . . . . . . . . . . . . . 11 3.2.1 One-dimensional affine ranking functions . . . . . . . . . . . 12 3.2.2 Multi-dimensional affine ranking functions . . . . . . . . . . 13 3.3 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.4 Scalability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.5 Worst-case time complexity . . . . . . . . . . . . . . . . . . . . . . . 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 6.2 Future work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

Table 1 :

 1 Experimental results

		Ref	Variables Control points Transitions dim ρ Time (s)
	easy1	[9]	3	4	5	1	0.05
	easy2	[9]	3	3	3	1	0.05
	ackermann	[3]	2	7	7	1	0.07
	terminate	[12]	3	1	1	1	0.05
	gcd	[6]	2	5	1	1	0.07
	rsd	♣	3	3	4	1	0.06
	nd-loop	♣	2	5	5	1	0.05
	wcet2	♣	2	3	5	1	0.11
	relation1	♣	2	4	4	1	0.06
	ndecr	♣	2	4	4	1	0.05
	cousot11	[16]	3	4	5	1	0.07
	cousot16	[16]	2	3	4	1	0.05
	random2d	[9]	5	10	21	1	2.70
	random1d	[9]	3	4	6	2	0.08
	wise	♣	2	6	10	2	0.20
	wcet0	♣	3	6	8	2	0.05
	wcet1	♣	3	6	8	2	0.20
	decr	♣	2	4	5	2	0.06
	exmini	♣	4	3	6	2	0.08
	aaron2	[9]	3	6	10	2	0.13
	while2	1	3	3	4	2	0.06
	cousot9	[16]	3	4	5	2	0.08
	perfect	[8]	4	7	10	2	0.23
	loops	[34]	3	4	5	2	0.07
	insertsort	♣	3	6	7	2	0.07
	bubblesort	[9]	4	10	17	3	0.38
	ax	♣	4	3	6	3	0.07
	nestedLoop	[26]	6	12	17	3	18
	determinant	[8]	4	6	7	4	0.15
	maccarthy91 [13]	4	6	7	DK	0.15

RR n°7037

http://icps.u-strasbg.fr/polylib/

http://www.cs.unipr.it/ppl/

http://apron.cri.ensmp.fr/library/

http://laure.gonnord.org/pro/aspic/aspic.htmlINRIA

http://www.cloog.org RR n°7037

piplib.org INRIA

A Source code of kernels

This section provides the source code of the kernels used for the experimental results. We also recall the execution times given in table 1. The timings were obtained on a 2GHz Pentium with 1GByte of memory running on a Debian 2.6. easy1 (0.05s) int x,y,z; x = 0; y = 100; while (x < 40) { if (z==0) x = x + 1; else x = x + 2; } easy2 (0.05s) int x,y,z; x = 12; y = 0; while (z > 0)