Marius Bozga
email: bozga@imag.fr

Radu Iosif
email: iosif@imag.fr

Filip Konecny
email: ikonecny@fit.vutbr.cz

Filip Konečný

Deciding Conditional Termination

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

The termination problem asks whether every computation of a given program ends in a halting state. The universal termination asks whether a given program stops for every possible input configuration. Both problems are among the first ever to be shown undecidable, by A. Turing [START_REF] Turing | On computable numbers, with an application to the entscheidungsproblem[END_REF]. In many cases however, programs will terminate when started in certain configurations, and may 3 run forever, when started in other configurations. The problem of determining the set of configurations from which a program terminates on all paths is called conditional termination.

In program analysis, the presence of non-terminating runs has been traditionally considered faulty. However, more recently, with the advent of reactive systems, accidental termination can be an equally serious error. For instance, when designing a web server, a developer would like to make sure that the main program loop will not exit unless a stopping request has been issued. These facts lead us to considering the conditional non-termination problem, which is determining the set of initial configurations which guarantee that the program will not exit.

In this paper we focus on programs that handle integer variables, performing linear arithmetic tests and (possibly non-deterministic) updates. A first observation is that the set of configurations guaranteeing non-termination is the greatest fixpoint of the preimage of the program's transition relation 4 R. This set, called the weakest recurrent set, and denoted wrs(R) in our paper, can be defined in first-order arithmetic, provided that the closed form of the infinite sequence of relations {R i } i≥0 , obtained by composing the transition relation with itself 0, 1, 2, . . . times, can also be defined using first-order arithmetic. Moreover, if the fragment of arithmetic we use has quantifier elimination, the weakest recurrent set can be expressed in a quantifier-free decidable fragment of arithmetic. This also means that the problem wrs(R) ? = ∅ is decidable, yielding universal termination decidability proofs for free.

Contributions of this paper

The main novelty in this paper is of rather theoretical nature: we show that the non-termination preconditions for integer transition relations defined as either octagons or linear affine loops with finite monoid property are definable in quantifier-free Presburger arithmetic. Thus, the universal termination problem for such program loops is decidable. However, since quantifier elimination in Presburger arithmetic is a complex procedure, we have developed alternative ways of deriving the preconditions for non-termination, and in particular:

-for difference bounds, we reduce the problem of finding the weakest recurrent set to finding the maximal solution of a system of inequalities in the complete lattice of integers extended with ±∞, where the right-hand sides use addition and min operators. Efficient algorithms for finding such maximal solutions are based on policy iteration [START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF]. This encoding gives us a worst-case time complexity of O(n 2 • 2 n ) in the number of variables n, for the computation of the weakest recurrent set for difference bounds relations. -for octagonal relations (and implicitly for difference bounds relations, which are a subclass), we use a result from [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF], namely that the sequence {R i } i≥0 is, in some sense, periodic. We give here a simple quantifier elimination method, targeted for the class of formulae defining weakest recursive sets. The algorithm suggested here runs in worst-case time complexity of O(n 3 • 5 n ) in the number of variables n. Moreover, we investigate the existence of linear ranking functions, and prove that, for each well-founded octagonal relations, there exists an effectively computable witness relation i.e., a well-founded relation that has a linear ranking function. -for linear affine relations, weakest recurrent sets can be defined in Presburger arithmetic if we consider several restrictions concerning the transformation matrix. If the matrix A defining R has eigenvalues which are either zeros or roots of unity, all non-zero eigenvalues being of multiplicity one (these conditions are equivalent to the finite monoid property of [START_REF] Boigelot | Symbolic Methods for Exploring Infinite State Spaces[END_REF][START_REF] Finkel | How to compose presburger-accelerations: Applications to broadcast protocols[END_REF]), then wrs(R) is Presburger definable. Otherwise, if all non-zero eigenvalues of A are roots of unity, of multiplicities greater or equal to one, wrs(R) can be expressed using polynomial terms. In this case, we can systematically issue termination preconditions, which are of significant practical importance, as noted in [START_REF] Cook | Proving conditional termination[END_REF].

For space reasons, all proofs are deferred to the Appendix.

Practical applications Unfortunately, in practice, the cases in which the closed form of the sequence {R i } i≥0 is definable in a logic that has quantifier elimination, are fairly rare. All relations considered so far are conjunctive, meaning that they can represent only simple program loops of the form while(condition){body}, where the loop body contains no further conditional constructs. In order to deal with more complicated program loops, one can use the results from this paper in several ways:

-use the decision procedures as a back-end of a termination analyzer, in order to detect spurious non-termination counterexamples consisting of a finite prefix (stem) and a conjunctive loop body (lasso). The spurious counterexamples can be discarded by intersecting the program model with the complement of the weak deterministic Büchi automaton representing the counterexample, as in [START_REF] Iosif | Automata-based termination proofs[END_REF]. -abstract a disjunctive loop body R 1 ∨ . . . ∨ R n by a non-deterministic difference bounds or octagonal5 relation R # ⊇ R 1,...,n and compute the weakest recurrent set of the latter. The complement of this set is a set of configurations from which the original loop terminates. -attempt to compute a transition invariant i.e., an overapproximations of the transitive closure of the disjunctive loop body (R 1 ∨ . . . ∨ R n ) + (using e.g., the semialgorithmic unfolding technique described in [START_REF] Bozga | Transitive Closures Ultimately Periodic Relations[END_REF]) and overapproximate it by a disjunction R # 1 ∨ . . . ∨ R # m of difference bounds or octagonal relations. Then compute the weakest recurrent set of each relation in the latter disjunction. If wrs(R # 1 ) = . . . = wrs(R # m ) = ∅, the original loop terminates on any input, following the principle of transition invariants [START_REF] Podelski | Transition invariants[END_REF].

Related Work

The literature on program termination is vast. Most work focuses however on universal termination, such as the techniques for synthesizing linear ranking functions of Sohn and Van Gelder [START_REF] Sohn | Termination detection in logic programs using argument sizes[END_REF] or Podelski and Rybalchenko [START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF], and the more sophisticated method of Bradley, Manna and Sipma [START_REF] Bradley | Linear ranking with reachability[END_REF], which synthesizes lexicographic polynomial ranking functions, suitable when dealing with disjunctive loops. However, not every terminating program (loop) has a linear (polynomial) ranking function. In this paper we show that, for an entire class of non-deterministic linear relations, defined using octagons, termination is always witnessed by a computable octagonal relation that has a linear ranking function.

Another line of work considers the decidability of termination for simple (conjunctive) linear loops. Initially Tiwari [START_REF] Tiwari | Termination of linear programs[END_REF] shows decidability of termination for affine linear loops interpreted over reals, while Braverman [START_REF] Braverman | Termination of integer linear programs[END_REF] refines this result by showing decidability over rationals and over integers, for homogeneous relations of the form

C 1 x > 0 ∧ C 2 x ≥ 0 ∧ x ′ = Ax.
The non-homogeneous integer case seems to be much more difficult as it is closely related to the open Skolem's Problem [START_REF] Halava | Skolem's problem -on the border between decidability and undecidability[END_REF]: given a linear recurrence {u i } i≥0 , determine whether u i = 0 for some i ≥ 0.

Our work is concerned mostly with proofs of decidability: we show that the termination problem for a program loop becomes decidable if the closed form of the sequence of iterations of the loop can be defined in a decidable logic. As shown in [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF], for octagonal and linear affine relations with the finite monoid property, this closed form is Presburger definable, which now entails the decidability of the termination problem for these classes of relations.

The work which is closest to ours is probably that of Cook et al. [START_REF] Cook | Proving conditional termination[END_REF]. In this paper, the authors develop an algorithm for deriving termination preconditions, by first guessing a ranking function candidate (typically the linear term from the loop condition) and then inferring a supporting assertion, which guarantees that the candidate function decreases with each iteration. The step of finding a supporting assertion requires a fixpoint iteration, in order to find an invariant condition. Unlike our work, the authors of [START_REF] Cook | Proving conditional termination[END_REF] do not address issues related to completeness: the method is not guaranteed to find the weakest precondition for termination, even in cases when this set can be computed. On the other hand, it is applicable to a large range of programs, extracted from real-life software. To compare our method with theirs, we tried all examples available in [START_REF] Cook | Proving conditional termination[END_REF]. Since most of them are linear affine relations, we used our under-approximation method and have computed termination preconditions, which turn out to be slightly more general than the ones reported in [START_REF] Cook | Proving conditional termination[END_REF].

Preconditions for Non-termination

In the rest of this paper we denote by x = {x 1 , . . . , x n } the set of working variables, ranging over a domain of values denoted as D. A state is a valuation s : x → D, or equivalently, an n-tuple of values from D. An execution step is a relation R ⊆ D n × D n defined by an arithmetic formula R(x, x ′ ), where the set x ′ = {x ′ 1 , . . . , x ′ n } denotes the values of the variables after executing R once. If s and s ′ are valuations of the sets x and x ′ , we denote by R(s, s ′ ) the fact that (s, s ′ ) ∈ R. A relation R is said to be consistent if there exist states s, s ′ such that R(s, s ′ ).

Relational composition is defined as

R 1 • R 2 = {(s, s ′ ) ∈ D n × D n | ∃s ′′ ∈ D n . R 1 (s, s ′′ ) ∧ R 2 (s ′′ , s ′ )}. For any relation R ∈ D n × D n ,
we consider R 0 to be the identity relation, and we define

R i+1 = R i • R, for all i ≥ 0. The pre-image of a set S ⊆ D n via R is the set pre R (S) = {s ∈ D n | ∃s ′ ∈ S . R(s, s ′ )}. It is easy to check that pre i R (S) = pre R i (S)
, for any S ⊆ D n and for all i ≥ 0. For any i ≥ 0, we write R i for the formula defining the relation R i and R -i (⊤) for the formula defining the set pre R i (D n ).

Definition 1.

A relation R is said to be * -consistent if and only if, for any k > 0, there exists a sequence of states s 1 , . . . , s k , such that R(s i , s i+1 ), for all i = 1, . . . , k -1. R is said to be well-founded if and only if there is no infinite sequence of states {s i } i>0 , such that R(s i , s i+1 ), for all i > 0.

Notice that if a relation is not * -consistent, then it is also well-founded. However the dual is not true. For instance, the relation R = {(n, n -1) | n > 0} is both * -consistent and well-founded. Definition 2. A set S ⊆ D n is said to be a non-termination precondition for R if, for each state s ∈ S there exists an infinite sequence of states s 0 , s 1 , s 2 , . . . such that s = s 0 and R(s i , s i+1 ), for all i ≥ 0.

If S 0 , S 1 , . . . are all preconditions for non-termination for R, then the (possibly infinite) union i=0,1,... S i is a precondition for non-termination for R as well. The set wnt(R) = {S ∈ D n | S is a precondition for non-termination for R} is called the weakest non-termination precondition for R. A relation R is well-founded if and only if wnt(R) = ∅. A set S such that S ∩ wnt(R) = ∅ is called a termination precondition.

Definition 3. A set S ⊆ D n is said to be recurrent for a relation R ∈ D n × D n if and only if S ⊆ pre R (S).
Proposition 1. Let S 0 , S 1 , . . . ∈ D n be a (possibly infinite) sequence of sets, all of which are recurrent for a relation R ∈ D n × D n . Then their union i=0,1,... S i is recurrent for R as well.

The set wrs(R) = {S ∈ D n | S is a recurrent set for R} is called the weakest recurrent set for R. By Proposition 1, wrs(R) is recurrent for R. Next we define the weakest recurrent set as the greatest fixpoint of the transition relation's pre-image.

Lemma 1. Given a relation R ∈ D n × D n , the weakest recurrent set for R is the greatest fixpoint of the function X → pre R (X).

As a consequence, we obtain wrs(R) = i>0 pre i R (D n ), by the Kleene Fixpoint Theorem. Since pre i R = pre R i , we have wrs(R) = i>0 pre R i (D n ). In other words, from any state in the weakest recurrent set for a relation, an iteration of any finite length of the given relation is possible. The following lemma shows that in fact, this is exactly the set of states from which an infinite iteration is also possible. Lemma 2. Given a relation R ∈ D n × D n , the weakest recurrent set for R equals its weakest precondition for non-termination.

The characterization of weakest recurrent sets as greatest fixpoints of the pre-image function suggests a method for computing such sets. In this section we show that, for certain classes of relations, these sets are definable in Presburger arithmetic, which gives a decision procedure for the well-foundedness problem for certain classes of relations, and consequently, for the termination problem for several classes of program loops.

Definition 4. Given a relation R ∈ D n ×D n defined by an arithmetic formula R(x, x ′ ), the closed form of R is a formula R (k) (x, x ′ ), with free variables x ∪ x ′ ∪ {k}, such that for every integer valuation i > 0 of k, R (i) (x, x ′ ) defines the relation R i . Example Consider for instance the relation R(x, x ′ ) ≡ x ≥ 0 ∧ x ′ = x -1. Then we have R (k) (x, x ′ ) ≡ x ≥ k -1 ∧ x ′ = x -k.
⊓ ⊔ Since, by Lemma 1, we have wrs(R) = gfp(pre R ) = i>0 pre R i (D n ), using the closed form of R, one can now define:

wrs(R) ≡ ∀k > 0 ∃x ′ . R (k) (x, x ′ ) (1)
Because Presburger arithmetic has quantifier elimination, wrs(R) can be defined in Presburger arithmetic 6 whenever R (k) can. In [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF] we show three classes of relations for which R (k) is Presburger definable: difference bounds, octagonal and finite-monoid affine relations (the formal definitions of these classes are given in the next section). For each of these classes of loops termination is decidable, by the above argument.

Example Consider again the relation R(x, x ′ ) ≡ x ≥ 0 ∧ x ′ = x -1 for which R (k) (x, x ′ ) ≡ x ≥ k -1 ∧ x ′ = x -k. Quantifier elimination yields wrs(R) ≡ ∀k > 0 ∃x ′ . x ≥ k -1 ∧ x ′ = x -k ≡ ∀k > 0 . x ≥ k -1 ≡ false. Hence the relation R is well-founded.
⊓ ⊔

Difference Bounds Relations

In this and the following sections, we assume that the variables x = {x 1 , . . . , x n } range over integers i.e., that D = Z.

Definition 5. A formula φ(x) is a difference bounds constraint if it is equivalent to a finite conjunction of atomic propositions of the form x i -x j ≤ a ij , for 1 ≤ i, j ≤ n, i = j, where a ij ∈ Z.
Given a difference bounds constraint φ, a difference bounds matrix

(DBM) repre- senting φ is a matrix m φ ∈ Z n×n ∞ such that (m φ ) ij = a ij , if x i -x j ≤ a ij
is an atomic proposition in φ, and ∞, otherwise. If φ is inconsistent (logically equivalent to false) we also say that m φ is inconsistent. The next definition gives a canonical form for consistent DBMs.

Definition 6. A consistent DBM m ∈ Z n×n ∞ is said to be closed if and only if m ii = 0 and m ij ≤ m ik + m kj , for all 1 ≤ i, j, k ≤ n.
Given a consistent DBM m, we denote by m * the (unique) closed DBM equivalent with it. It is well-known that, if m is consistent, then m * is unique, and can be computed from m in time O(n 3 ), by the classical Floyd-Warshall algorithm. The closure of DBM provides an efficient means to compare difference bounds constraints.

Proposition 2 ([17]

). Given two consistent difference bounds constraints ϕ(x) and ψ(x), the following conditions are equivalent:

-∀x . ϕ(x) → ψ(x) -(m * ϕ ) ij ≤ (m * ψ ) ij , for all 1 ≤ i, j ≤ n
In the following, let R be a relation defined by a difference bounds constraint. It is easy to show that, for any i ≥ 0, the relation R i is a difference bounds relation as wellin other words, difference bounds relations are closed under composition. Moreover, if S is a set defined by a difference bounds constraint, then the set pre R i (S) is defined by a difference bounds constraint as well. But since wrs(R) = i>0 pre R i (Z n ), it turns out that wrs(R) can be defined by a difference bounds constraint, since the class of difference bounds constraints is closed under (possibly infinite) intersections.

We are now ready to describe the procedure computing the weakest recurrent set for a difference bounds relation R. Since wrs(R) is a (possibly inconsistent) difference bounds constraint, we use the template µ(x, p) ≡ 1≤i =j≤n x ix j ≤ p ij , where p ij are parameters ranging over Z ±∞ (we clearly do not need to track the constraints of the form x ix i ≤ p ii ). Moreover, we assume that the template is closed (Definition 6), which can be encoded as a system of inequalities of the form:

p ij ≤ min p ik + p kj | k = i, k = j (2)
Next, we compute the (symbolic) difference bounds constraint corresponding to the set pre R (µ) ≡ ∃x ′ . R(x, x ′ ) ∧ µ(x ′ , p). This step requires computing the closure of the DBM corresponding to R ∧ µ, and elimination of the x ′ variables. The result is a closed symbolic DBM π, whose entries are min-terms consisting of sums of p ij and integer constants. Further, we encode the recurrence condition µ ⊆ pre R (µ), again as a system of inequalities (Proposition 2) of the form:

p ij ≤ π ij , i = j (3)
By conjoining the inequalities ( 2) and ( 3), we obtain a system of inequalities with variables p ij , whose right-hand sides are linear combinations of p ij with addition and min.

We are interested in the maximal solution of this system, which can be obtained using an efficient policy iteration algorithm [START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF] in the complete lattice of Z ±∞ with addition, min and max operators. This solution defines the weakest recurrent set for R, and consequently, the weakest precondition for non-termination of the R loop. Since wrs(R) is a difference bounds constraint, for any relation R definable by a difference bounds constraint, the maximal solution of the system is unique. It is to be noted that, if for some 1 ≤ i = j ≤ n we obtain p ij = -∞, then the weakest recurrent set is empty i.e., the relation R is well-founded, as shown by the following example.

Example Let us compute wrs(R) for R(x, x ′ ) ≡ z -x ≤ 0 ∧ x ′ = x -1 ∧ z ′ = z. The template used is µ(x, z) ≡ x -z ≤ p 1 ∧ z -x ≤ p 2 . We compute pre R (µ) ≡ x -z ≤ min(p 1 + 1, 1) ∧ z -x ≤ p 2 -1. The recurrence condition µ ⊆ pre R (µ)
is given by the following system: {p 1 ≤ min(p 1 + 1, 1), p 2 ≤ p 2 -1}, whose unique maximal solution is p 1 = 1, p 2 = -∞. This proves the well-foundedness of R. ⊓ ⊔

Lemma 3. Computing the weakest recurrent set of a difference bounds relation can be done in time

O(n 2 • 2 n ),
where n is the number of variables.

Octagonal Relations Definition 7. A formula φ(x) is an octagonal constraint if it is equivalent to a finite conjunction of terms of the form ±x

i ± x j ≤ a ij , where a ij ∈ Z and 1 ≤ i, j ≤ n.
We represent octagons as difference bounds constraints over the dual set of variables y = {y 1 , y 2 , . . . , y 2n }, with the convention that y 2i-1 stands for x i and y 2i for -x i , respectively. For example, the octagonal constraint

x 1 + x 2 = 3 is represented as y 1 - y 4 ≤ 3 ∧ y 2 -y 3 ≤ -3.
To handle the dual variables in the following, we define ī = i -1, if i is even, and

ī = i + 1 if i is odd. We say that a DBM m ∈ Z 2n×2n ∞ is coherent iff m ij = mj ī for all 1 ≤ i, j ≤ 2n.
The coherence property is needed because any atomic proposition x ix j ≤ a, in φ can be represented as both y 2i-1y 2j-1 ≤ a and y 2jy 2i ≤ a, 1 ≤ i, j ≤ n. We denote by φ the difference bounds formula φ[y 1 /x 1 , y 2 /x 1 , . . . , y 2n-1 /x n , y 2n /x n ] with free variables y. The following equivalence relates φ and φ :

φ(x) ⇔ (∃y 2 , y 4 , . . . , y 2n . φ ∧ n i=1 y 2i-1 + y 2i = 0)[x 1 /y 1 , . . . , x n /y 2n-1 ] (4)
Given a coherent DBM m representing φ, we say that m is octagonal-consistent if and only if φ is consistent. The following definition gives the canonical form of a DBM representing an octagonal-consistent constraint. Definition 8. An octagonal-consistent coherent DBM m ∈ Z 2n×2n is said to be tightly closed if and only if the following hold:

1. m ii = 0, ∀1 ≤ i ≤ 2n 3. m ij ≤ m ik + m kj , ∀1 ≤ i, j, k ≤ 2n 2. m iī is even, ∀1 ≤ i ≤ 2n 4. m ij ≤ ⌊ miī 2 ⌋ + ⌊ mj j 2 ⌋, ∀1 ≤ i, j ≤ 2n
Given an octagonal-consistent DBM m, we denote by m t the equivalent tightly closed DBM. The tight closure of an octagonal-consistent DBM m is unique and can be computed in time O(n 3 ) as m t i,j = min m * i,j ,

m * i, ī 2 + m * j,j
2 [START_REF] Bagnara | An improved tight closure algorithm for integer octagonal constraints[END_REF]. This generalizes to unbounded finite compositions of octagonal relations [START_REF] Bozga | Iterating octagons[END_REF]:

∀k ≥ 0 . (m t R k ) i,j = min (m * R k ) i,j , (m * R k ) i, ī 2 + (m * R k )j ,j 2 (5)
Notice that the above relates the entries of the tightly closed DBM representation of R k with the entries of the closed DBM representation of the relation defined by R k .

We are now ready to introduce a result [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF] that defines the "shape" of the closed form R (k) for an octagonal relation R. Intuitively, for each i ≥ 0, R i is an octagon, whose bounds evolve in a periodic way. The following definition gives the precise meaning of periodicity for relations that have a matrix representation.

Definition 9. An infinite sequence of matrices {M

k } ∞ k=1 ∈ Z m×m
∞ is said to be ultimately periodic if and only if:

∃b > 0 ∃c > 0 ∃Λ 0 , Λ 1 , . . . , Λ c-1 ∈ Z m×m ∞ . M b+(k+1)c+i = Λ i + M b+kc+i
for all k ≥ 0 and i = 0, 1, . . . , c -1. The smallest b, c for which the above holds are called prefix and period of the {M k } ∞ k=1 sequence, respectively. A result reported in [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF] is that the sequence {m t R i } i≥0 (5) of tightly closed matrices representing the sequence {R i } i≥0 of powers of an octagonal relation R is ultimately periodic, in the sense of the above definition. The constants b and c from Definition 9 will also be called the prefix and period of the octagonal relation R, throughout this section.

For a set v of variables, let

U (v) = {±v 1 ± v 2 | v 1 , v 2 ∈
v} denote the set of octagonal terms over v. As a first remark, by the periodicity of the sequence {m t R i } i≥0 , the closed form of the subsequence {R b+cℓ } ℓ≥0 (of {R i } i≥0 ) can be defined as:

R (ℓ) b,c ≡ u∈U(x∪x ′ ) u ≤ a u ℓ + d u (6)
for all ℓ ≥ 0, where a u and d u are entries (i, j) corresponding to the term u = y iy j in the octagonal DBMs Λ 0 and m t R b , respectively. This is the case, since the matrix sequence {m t R b+cℓ } ℓ≥0 is ultimately periodic i.e.,

m t R b+cℓ = m t R b + ℓΛ 0 , for all ℓ ≥ 0. Example Given an octagonal relation R ≡ x+y ≤ 5 ∧ x ′ = x+2 ∧ y ′ = y-1, we compute R (ℓ) b,c ≡ x+y ≤ -ℓ+5 ∧ x ′ -x = 2ℓ+2 ∧ y -y ′ = ℓ + 1 ∧ x+y ′ ≤ -2ℓ+4 ∧ x ′ +y ≤ ℓ+7 ∧ x ′ +y ′ ≤ 6
We have b = c = 1, and

R (k) ≡ R (k) b,c .
⊓ ⊔ Second, we notice that the greatest fixpoint of a monotonic 7 function can be computed by an infinite subsequence of the classical decreasing Kleene iteration. Concretely, we have that wrs

(R) = k>0 pre k R (Z n ) = ℓ≥0 pre b+cℓ R (Z n ).
The latter set can now be defined using the closed form of the subsequence (6) i.e., wrs(R)

≡ ∀ℓ ≥ 0 ∃x ′ . R (ℓ) b,c .
The proof of periodicity from [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF] relies on the fact that the DBM encoding of the closed form of R is tightly closed for any unfolding length k, see [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF]. Hence, the existential quantifier ∃x ′ can be eliminated by simply deleting all atomic propositions involving primed variables from [START_REF] Bozga | Transitive Closures Ultimately Periodic Relations[END_REF]. Further, we obtain:

wrs(R) ≡ ∀ℓ ≥ 0 u∈U(x) u ≤ a u ℓ + d u ≡ u∈U(x) u ≤ inf {a u ℓ + d u | ℓ ≥ 0}
where, for a set S ⊆ Z, inf S denotes the minimal element of S, if one exists, or -∞, otherwise. We have

inf {a u ℓ + d u | ℓ ≥ 0} = -∞ if a u < 0 d u otherwise
Hence wrs(R) is the empty set, if a u < 0 for some u ∈ U (x). Otherwise, we obtain wrs(R) ≡ u∈U(x) u ≤ d u . However, this is exactly the set defined by

R -b (⊤) ≡ ∃x ′ . R b (x, x ′ ) ≡ ∃x ′ . R (0)
b,c , by [START_REF] Bozga | Transitive Closures Ultimately Periodic Relations[END_REF]. The following complexity upper bound is a consequence of this fact. Example (continued) Following the decision procedure above, we obtain

wrs(R) ≡ ∀ℓ ≥ 0 ∃x ′ . R (ℓ) b,c ≡ ∀ℓ ≥ 0 . x+y ≤ -ℓ+5
Hence wrs(R) = ∅ i.e., R is well-founded.

⊓ ⊔

On the Existence of Linear Ranking Functions

A ranking function for a given relation R constitutes a proof of the fact that R is well-founded. We distinguish here two cases. If R is not * -consistent, then the wellfoundedness of R is witnessed simply by an integer constant i > 0 such that R i = ∅.

Otherwise, if R is * -consistent, we need a better argument for well-foundedness. In this section we show that, for any * -consistent well-founded octagonal relation R, the (strenghtened) relation defined by R -b (⊤) ∧ R is well-founded and has a linear ranking function, even when R alone does not have one. For space reasons, we do not give here all the details of the construction of such a function. However, the existence proof suffices, as one can use complete ranking function extraction tools (such as e.g. Rank-Finder [START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF]) in order to find them.

Definition 10. Given a relation R ⊆ Z n × Z n , a linear ranking function for R is a term f (x) = n i=1 a i x i such that
, for all states s, s ′ : x → Z:

1. f is decreasing: R(s, s ′ ) → f (s) > f (s ′ ) 2. f is bounded: R(s, s ′ ) → (f (s) > h ∧ f (s ′ ) > h), for some h ∈ Z.
The main result of this section is the following: It remains to prove that the witness relation defined by R -b (⊤) ∧ R has a linear ranking function, provided that it is well-founded. The proof is organized as follows. First we show that well-foundedness of an octagonal relation R is equivalent to the well-foundedness of its difference bounds representation R (Lemma 6). Second, we use a result from [START_REF] Bozga | Flat parametric counter automata[END_REF], that the constraints in the sequence of iterated difference bounds relations {R i } i≥0 can be represented by a finite-state weighted automaton, called the The above lemma reduces the problem of showing existence of a ranking function for an octagonal relation R(x, x ′ ) to showing existence of a ranking function for its difference bounds encoding R(y, y ′ ). Assume that f (y) is a ranking function for R. Then f [x i /y 2i-1 , -x i /y 2i ] n i=1 is a linear ranking function for R. Hence, in the rest of this section, we consider without loss of generality that R is a difference bounds relation.

Theorem 1. Let R ⊆ Z n × Z n be
zigzag

Zigzag Automata

For the later developments, we need to introduce the zigzag automaton corresponding to a difference bounds relation R. Intuitivelly, for any i > 0, the relation R i can be represented by a constraint graph which is the i-times repetition of the constraint graph of R. The constraints induced by R i can be represented as shortest paths in this graph, and can be recognized (in the classical automata-theoretic sense) by a weighted automaton A R . The structure of this automaton is needed to show the existence of a linear ranking function.

For a difference bounds relation R, we define the directed graph G R , whose set of vertices is the set x ∪ x ′ , and in which there is an edge from x i to x j labeled a ij if and only if the atomic proposition x ix j ≤ a ij occurs in R. Clearly, m R is the incidence matrix of G R . We define the concatenation of G R with itself as the disjoint union of two copies of G R , in which the x vertices of the second copy overlap with the x ′ vertices of the first copy. Then R m corresponds to the graph G m R , obtained by concatenating the graph of R to itself m > 0 times.

Example Let R ≡ x 3 -x ′ 2 ≤ 0 ∧ x 1 -x ′ 3 ≤ 0 ∧ x ′ 4 -x 4 ≤ 0 ∧ x ′ 3 -x 2 ≤ 0. Figure 1 (b) shows G R 8 , the 8-times unfolding of the graph G R representing R. ⊓ ⊔ x4 x3 x2 x1 x (0) x (1)
x (2) x (3) x (4) x (5) x (6) x (7) x (8) - Given a difference bounds relation R, the zigzag automaton A R recognizes all paths from x i to x j in G k R . Intuitively, a path π between x i and x j in G k R , is represented by a word w of length k, as follows: the w l symbol represents simultaneously all edges of π that involve only nodes from x (l) ∪ x (l+1) , for all 0 ≤ l < k. The alphabet of the zigzag automaton consists of subgraphs of G R , where the weight of a subgraph is the sum of the weights on its edges. The set of control states of the zigzag automaton is8 {l, r, lr, rl, ⊥} n . Clearly, the size of the zigzag automaton is at most 5 n . For a complete definition, the interested reader may consult [START_REF] Bozga | Flat parametric counter automata[END_REF].

Example Consider the relation R ≡ x 2 -x ′ 1 ≤ -1 ∧ x 3 -x ′ 2 ≤ 0 ∧ x 1 -x ′ 3 ≤ 0 ∧ x ′ 4 -x 4 ≤ 0 ∧ x ′ 3 -x 2 ≤ 0. An example of a run of A R recognizing a path of constraints in G 8 R is given in Figure 1 (b). The word accepted by π is a subgraph of G 8 R
shown in Figure 1 (a). The cycle π :

q 1 G1 --→ q 2 G2 --→ q 3 G3
--→ q 1 is taken several times in this run. The weights of the symbols on the run are w(G 1 ) = w(G 2 ) = w(G 4 ) = 0 and w(G 3 ) = -1. ⊓ ⊔ The following lemma proves the existence of a negative weight cycle in the zigzag automata corresponding to well-founded difference bounds relation. The intuition behind this fact is that the rates of the DBM sequence {m R i } i>0 are weights of optimal ratio (weight per length) cycles in the zigzag automaton. According to the previous section, if R is well-founded, there exists a negative rate for {m R i } i>0 , which implies the existence of a negative cycle in the zigzag automaton. Lemma 7. If R is a * -consistent well-founded difference bounds relation of prefix b ≥ 0, and A R is its corresponding zigzag automaton, then there exists a cycle π from a state q to itself, such that w(π) < 0 and there exists paths π i from an initial state to q, and π f from q to a final state, such that

|π i | + |π f | = b.
Next we prove the existence of a linear decreasing function, based on the existence of a negative weight cycle in the zigzag automaton. Lemma 8. If R is a * -consistent well-founded difference bounds relation of prefix b ≥ 0, then there exists a linear function f (x) such that, for all states s, s ′ :

x → Z we have R -b (⊤)(s) ∧ R(s, s ′ ) → f (s) > f (s ′ ).
Example We illustrate the construction of linear decreasing function on the relation

R ≡ x 2 -x ′ 1 ≤ -1 ∧ x 3 -x ′ 2 ≤ 0 ∧ x 1 -x ′ 3 ≤ 0 ∧ x ′ 4 -x 4 ≤ 0 ∧ x ′ 3 -x 2 ≤ 0 from the previous example. Summing the edges in π, we obtain x 2 -x ′ 1 + x 1 -x ′ 3 + x 3 -x ′ 2 + x ′ 4 -x 4 + x ′ 4 -x 4 + x ′ 4 -x 4 ≤ -1, which simplifies to x 1 + x 2 + x 3 - 3x 4 -(x ′ 1 + x ′ 2 + x ′ 3 -3x 4 ) ≤ -1. Letting f (x) = -(x 1 + x 2 + x 3 -3x 4 ), we have that f (x) > f (x ′ ).
⊓ ⊔ Last, we prove that the function f of Lemma 8 is bounded from below, concluding that it is indeed a ranking function. Since each run in the zigzag automaton recognizes a path from some x i to some x j , a run that repeats a cycle can be decomposed into a prefix, the cycle itself and a suffix. The path recognized may traverse the cycle several times, however each exit point from the cycle must match a subsequent entry point. These paths from the exit to the corresponding entries gives us the necessary lower bound. In fact, these paths appear already on graphs G R i for i ≥ b, where b is the prefix of R (Lemma 9). Hence the need for a strenghtened witness R -b (⊤) ∧ R, as R alone is not enough for proving boundedness of f . Lemma 9. Let R be a * -consistent octagonal relation with prefix b and period c. Then, for any 1 ≤ i, j ≤ 2n and k ≥ 1, we have

(m R -k (⊤) ) i,j < ∞ → (m R -b (⊤) ) i,j < ∞.
Lemma 10. If R is a * -consistent well-founded difference bounds relation of prefix b, and f (x) is the linear decreasing function from Lemma 8, there exists an integer h such that, for all states s, s

′ : x → Z, (R b (⊤)(s) ∧ R(s, s ′ )) → (f (s) ≥ h ∧ f (s ′ ) ≥ h).
Example (continued) We will continue the previous example and illustrate the boundedness of f = -(x 1 + x 2 + x 3 -3x 4 ) (see Figure 1b). Since there is a path from x

(6) 2 to x (6) 4 in G 3 G 4 (and hence in G 2 R ), then R 2 → (x 2 -x 4 ≤ -1)
, and by Lemma 9, we obtain R b → (x 2x 4 ≤ -1). Similarly, since there is a path x

(5) 3 ; x (5) 4 in G 2 G 3 G 4 (and hence in G 3 R ), we obtain R b → (x 3 -x 4 ≤ -1).
Similarly, since there is a path

x (4) 1 ; x (4) 4 in G 1 G 2 G 3 G 4 (and hence in G 4 R ), we obtain R b → (x 3 -x 4 ≤ -1
). Summing up these inequalities, we obtain that f (x) = -(

x 1 + x 2 + x 3 -3x 4 ) ≥ 3 and, thus R -b (⊤) ∧ R → (f ≥ 3).
As an experiment, we have tried the RANKFINDER [START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF] tool (complete for linear ranking functions), which failed to discover a ranking function on this example. This comes with no surprise, since no linear decreasing function that is bounded after the first iteration exists.

⊓ ⊔

Linear Affine Relations

Let x = x 1 , . . . , x n ⊤ be a column vector of variables ranging over integers. A linear affine relation is a relation of the form R(x, x ′ ) ≡ Cx ≥ d ∧ x ′ = Ax + b, where A ∈ Z n×n , C ∈ Z p×n are matrices, and b ∈ Z n , d ∈ Z p are column vectors of integer constants. Notice that we consider linear affine relations to be deterministic, unlike the difference bounds and octagonal relations considered in the previous. In the following, it is convenient to work with the equivalent homogeneous form:

R(x, x ′ ) ≡ C h x h ≥ 0 ∧ x ′ h = A h x h A h = A b 0 1 C h = C -d x h = x x n+1 (7)
The closed form of a linear affine relation is defined by the following formula:

R (k) (x, x ′ ) ≡ ∃x n+1 , x ′ n+1 .x ′ h = A k h x h ∧∀0 ≤ ℓ < k.CA ℓ h x ≥ 0 ∧ x n+1 = 1 (8)
Intuitively, the first conjunct defines the (unique) outcome of iterating the relation x ′ = Ax + b for k steps, while the second (universally quantified) conjunct ensures that the condition (Cx ≥ d) has been always satisfied all along the way. The definition of the weakest recursive set of a linear affine relation is (after the elimination of the trailing existential quantifier):

wrs(R)(x) ≡ ∃x n+1 ∀k > 0 . C h A k h x ≥ 0 ∧ x n+1 = 1 (9)
The main difficulty with the form (9) comes from the fact that the powers of a matrix A cannot usually be defined in a known decidable theory of arithmetic. In the following, we discuss the case of A having the finite monoid property [START_REF] Boigelot | Symbolic Methods for Exploring Infinite State Spaces[END_REF][START_REF] Weber | On finitely generated monoids of matrices with entries in n[END_REF], which leads to wrs(R) being Presburger definable. Further, we relax the finite monoid condition and describe a method for generating sufficient termination conditions, i.e. sets S ∈ Z n such that S ∩ wrs(R) = ∅. Some basic notions of linear algebra are needed in the following. If A ∈ Z n×n is a square matrix, and v ∈ Z n is a column vector of integer constants, then any complex number λ ∈ C such that Av = λv, for some complex vector vC n , is called an eigenvalue of A. The vector v in this case is called an eigenvector of A. It is known that the eigenvalues of A are the roots of the characteristic polynomial det(A -λI n ) = 0, which is an effectively computable univariate polynomial in λ. A complex number r is said to be a root of the unity if r d = 1 for some integer d > 0.

In the previous work of Weber and Seidl [START_REF] Weber | On finitely generated monoids of matrices with entries in n[END_REF], Boigelot [START_REF] Boigelot | Symbolic Methods for Exploring Infinite State Spaces[END_REF], and Finkel and Leroux [START_REF] Finkel | How to compose presburger-accelerations: Applications to broadcast protocols[END_REF], a restriction of linear affine relations has been introduced, with the goal of defining the closed form of relations in Presburger arithmetic. A matrix A ∈ Z n×n is said to have the finite monoid property if and only if its set of powers {A i | i ≥ 0} is finite. A linear affine relation has the finite monoid property if and only if the matrix A defining the update has the finite monoid property.

Lemma 11 ([12, 2]). A matrix A ∈ Z n×n has the finite monoid property iff:

1. all eigenvalues of A are either zero or roots of the unity, and 2. all non-zero eigenvalues are of multiplicity one.

Both conditions are decidable.

In the following, we drop the second requirement of Lemma 11, and consider only linear relations, such that all non-zero eigenvalues of A are roots of the unity. In this case, R (k) cannot be defined in Presburger arithmetic any longer, thus we renounce defining wrs(R) precisely, and content ourselves with the discovery of sufficient conditions for termination. Basically given a linear affine relation R, we aim at finding a disjunction φ(x) of linear constraints on x, such that φ ∧ wrs(R) is inconsistent, without explicitly computing wrs(R).

Lemma 12. Given a square matrix A ∈ Z n×n , whose non-zero eigenvalues are all roots of the unity. Then (A m ) i,j ∈ Q[m], for all 1 ≤ i, j ≤ n, are effectively computable polynomials with rational coefficients.

We turn now back to the problem of defining wrs(R) for linear affine relations R of the form [START_REF] Braverman | Termination of integer linear programs[END_REF]. First notice that, if all non-zero eigenvalues of A are roots of the unity, then the same holds for A h [START_REF] Bozga | Flat parametric counter automata[END_REF]. By Lemma 12, one can find rational polynomials p i,j (k) defining (A k h ) i,j , for all 1 ≤ i, j ≤ n. The condition (9) resumes to a conjunction of the form:

wrs(R)(x) ≡ n i=1 ∀k > 0 . P i (k, x) ≥ 0 (10)
where each

P i = a i,d (x) • k d + . . . + a i,1 (x) • k + a i,0 (x) is a polynomial in k whose coefficients are the linear combinations a i,d ∈ Q[x].
We are looking after a sufficient condition for termination, which is, in this case, any set of valuations of x that would invalidate [START_REF] Cook | Proving conditional termination[END_REF]. The following proposition gives sufficient invalidating clauses for each conjunct above. By taking the disjunction of all these clauses we obtain a sufficient termination condition for R.

Lemma 13. Given a polynomial P (k, x) = a d (x) • k d + . . . + a 1 (x) • k + a 0 (x), there exists n > 0 such that P (n, x) < 0 if, for some i = 0, 1, . . . , d, we have a d-i (x) < 0 and a d (x) = a d-1 (x) = . . . = a d-i+1 (x) = 0.

Example Consider the following program [START_REF] Cook | Proving conditional termination[END_REF], and its linear transformation matrix A.

while (x ≥ 0) 3 , hence the only eigenvalue is 1, with multiplicity 3. Then we compute A k (see above), and

x ′ = x + y y ′ = y + z A =   1 1 0 0 1 1 0 0 1   A k =   1 k k(k-1) 2 0 1 k 0 0 1   The characteristic polynomial of A is det(A -λI 3 ) = (1 -λ)
x ′ = x + k • y + k(k-1)
2 z gives the value of x after k iterations of the loop. Hence the (precise) non-termination condition is:

∀k > 0 . z 2 • k 2 + (y -z 2 ) • k + x ≥ 0 The sufficient condition for termination is: (z < 0) ∨ (z = 0 ∧ y < 0) ∨ (z = 0 ∧ y = 0 ∧ x < 0) ⊓ ⊔
We can generalize this method further to the case where all eigenvalues of A are of the form q • r, with q ∈ R and r ∈ C being a root of the unity. The main reason for not using this condition from the beginning is that we are, to this point, unaware of its decidability status. With this condition instead, it is sufficient to consider only the eigenvalues with the maximal absolute value, and the polynomials obtained as sums of the polynomial coefficients of these eigenvalues (see Corollary 2 in Appendix 5). The result of Lemma 12 and the sufficient condition of Lemma 13 carry over when using these polynomials instead.

Experimental Evaluation

We have validated the methods described in this paper by automatically verifying termination of all the octagonal running examples, and of several integer programs synthesized from (i) programs with lists [START_REF] Bouajjani | Programs with lists are counter automata[END_REF] and (ii) VHDL models [START_REF] Smrcka | Verifying parametrised hardware designs via counter automata[END_REF]. We have first computed automatically their precise transition invariant T by adapting the method for reachability analysis for counter automata, described in [START_REF] Bozga | Transitive Closures Ultimately Periodic Relations[END_REF], and implemented in the FLATA tool [13]. Then we automatically proved that T is contained in a disjunction of octagonal relations, which are found to be well-founded by the procedure described in Section 4.

We first verified termination of the LISTCOUNTER and LISTREVERSAL programs, which were obtained using a translation scheme from [START_REF] Bouajjani | Programs with lists are counter automata[END_REF], which generates an integer program from a program manipulating dynamically allocated single-selector linked lists. Using the same technique, we also verified the COUNTER and SYNLIFO programs, obtained by translating VHDL designs of hardware counter and synchronous LIFO [START_REF] Smrcka | Verifying parametrised hardware designs via counter automata[END_REF]. These models have infinite runs for any input values, which is to be expected, as they encode the behavior of synchronous reactive circuits.

Second, we compared (Table 1) our method for termination of linear affine loops with the examples given in [START_REF] Cook | Proving conditional termination[END_REF], and found the same termination preconditions as they do, with one exception, in which we can prove universal termination in integer input values (row 3 of Table 1). The last example from [START_REF] Cook | Proving conditional termination[END_REF] is the Euclidean Greatest Common Divisor algorithm, for which we infer automatically the correct termination preconditions using a disjunctively well-founded octagonal abstraction of the transition invariant.

PROGRAM

COOK ET. AL [START_REF] Cook | Proving conditional termination[END_REF] LINEAR AFFINE LOOPS if (lvar ≥ 0) while (lvar < 2 30 ) lvar = lvar < < 1;

lvar > 0 ∨ lvar < 0 ∨ lvar ≥ 2 30 lvar (k) =2 k •lvar (0) ¬(lvar=0)∨lvar≥2 30 while (x ≤ N) if (*) { x=2*x+y; y=y+1; } else x ++; x > N ∨ x + y ≥ 0 x (k) ≥2 k •(x (0) +y (0) +1)-k-y (0) -1 y (k) ≤y (0) +k x>N∨x+y≥0 while (x ≥ N) x = -2*x + 10; x > 5 ∨ x + y ≥ 0 x (k) =(-2) k •(x (0) -10 3 )+ 10 3 x = 10 3 ⇐⇒ true //@ requires n > 200 x = 0; while (1) if (x < n) { x=x+y; if (x ≥ 200) break; } y > 0 x (k) =x (0) +k•y (0)
y>0 Table 1. Termination preconditions for several program fragments from [START_REF] Cook | Proving conditional termination[END_REF]. The even rows of column 3 represent the closed form of the transition relation, while the rows give the termination preconditions.

Conclusions

We have presented several methods for deciding conditional termination of several classes of program loops manipulating integer variables. The universal termination problem has been found to be decidable for octagonal relations and linear affine loops with the finite monoid property. In other cases of linear affine loops, we give sufficient termination conditions. We have implemented our method in the FLATA tool [13] and performed a number of preliminary experiments.

A Proofs from Section 2

Proof of Proposition 1 For each i we have S i ⊆ pre R (S i ) ⊆ pre R ( j=0,1,... S j ). The last inclusion is by the monotonicity of pre R . Hence j=0,1,... S j ⊆ pre R ( j=0,1,... S j ).

⊓ ⊔

Proof of Lemma 1 By the Knaster-Tarski Fixpoint Theorem, gfp(pre

R ) = {S | S ⊆ pre R (S)} = wrs(R). ⊓ ⊔
Proof of Lemma 2 "wrs(R) ⊆ wnt(R)" Let s 0 ∈ wrs(R) be a state. Then there exists s 1 ∈ wrs(R) such that R(s 0 , s 1 ). Applying this argument infinitely many times, one can construct an infinite sequence s 0 , s 1 , s 2 , . . . such that R(s i , s i+1 ), for all i ≥ 0. Hence s 0 ∈ wnt(R).

"wnt(R) ⊆ wrs(R)" Let s 0 ∈ wnt(R). Then there exists an infinite sequence s 0 , s 1 , s 2 , . . . such that R(s i , s i+1 ) for all i ≥ 0. Then, for all i ≥ 0,

s 0 ∈ pre i R (s i ) ⊆ pre i R (D n ), by monotonicity of pre R . Hence s 0 ∈ i≥0 pre i R (D n ) = gfp(pre R ). By Lemma 1, s 0 ∈ wrs(R).
⊓ ⊔

B Proofs from Section 3

Proof of Lemma 3 The algorithm of Gawlitza and Seidl [START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF] runs in time at most O(n • |S|), where n is the number of variables in the system, and |S| denotes the size of the system i.e., the sum of the expression sizes of the right-hand sides. In our case, the min-terms in the first system (2) are of size at most O(n), while in the second system (3), we have min-terms of size at most O(2 n ). Since the number of variables in both systems is n 2 , the result follows.

-if inf{ an 2 } ∞ n=0 = -∞ then inf{a n } ∞ n=0 = -∞ -if inf{a n + n b } ∞ n=0 = -∞ then inf{a n } ∞ n=0 = -∞ or inf{b n } ∞ n=0 = -∞ -if inf{min(a n , b n )} ∞ n=0 = -∞ then inf{a n } ∞ n=0 = -∞ or inf{b n } ∞ n=0 = -∞ Proof. By contraposition. Suppose that inf S 1 = -∞ and inf S 2 = -∞. Then, ∃k 1 ≥ 1 . ∀l 1 ≥ k 1 . a k1 = a l1 and ∃k 2 ≥ 1 . ∀l 2 ≥ k 2 . b k2 = b l2 . Let k = max{k 1 , k 2 }. Then clearly, ∀l ≥ k . a k 2 = a l 2 ∧ a k + b k = a l + b l ∧ min{a k , b k } = min{a l , b l }. Hence inf S t = -∞, inf S p = -∞, and inf S m = -∞. ⊓ ⊔
Proof of Lemma 6 Let b and c be the prefix and period of R. In Section 4 we proved that a * -consistent octagon R is well-founded if and only if the closed form of the sequence {R b+cℓ } ℓ≥0 contains an atomic proposition of the form u ≤ a u ℓ + d u , where u ∈ U (x) is an octagonal term, and a u < 0. We will show that the same holds if we use the closed form of the sequence {R b+cℓ } ℓ≥0 instead. Notice that for any k ≥ 0, the difference bounds encoding of R -k (⊤) is the projection of m t R k on the entries corresponding to unprimed variables i.e., (m t R k ) ↓y . By the monotonicity of pre R , the sequence {(m t R k ) ↓y } k≥0 is decreasing. Since the elements of the sequence are defined by [START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF], we can apply Proposition 3 and observe that if for some

1 ≤ i, j ≤ 2n, inf{(m t R k ) i,j } k≥0 = -∞, then also inf{(m * R k ) i2,j2 } k≥0 = -∞
for some (i 2 , j 2 ) ∈ {(i, j), (i, ī), ( j, j)}. Hence R is well-founded iff there exists a negative coefficient a u in the closed form of {R b+cℓ } ℓ≥0 iff R db is well founded. For the sake of completeness, we present key results of [START_REF] Schutter | On the ultimate behavior of the sequence of consecutive powers of a matrix in the max-plus algebra[END_REF]. Let G = (V, E, ν : E → Z) be a weighted digraph and M G the associated incidence matrix. Let G(V ′ ), V ′ ⊆ V be a subgraph induced by V ′ . We say that G(V ′ ) is strongly connected if for any two

different vertices v 1 , v 2 ∈ V ′ , v 1 = v 2 there exists a path from v 1 to v 2 . G(V ′ ) is a strongly connected component of G if there is no V ′ ⊂ V ′′ ⊆ V such that G(V ′′ ) is strongly connected. Given a path π : v 0 c1 -→ v 1 c2 -→ v 2 . . . v p-1 cp -→ v p , the length of π is |π| = p, the weight of π is w(π) = p i=1 c i , average weight of π is w(π) |π| .
A cycle is a path where v 0 = v p . A cycle of a strongly connected graph G is critical if it has maximum average weight among all cycles of G.

A cycle of a strongly connected graph G is critical if it has minimum average weight and cyclicity of G is the greatest common divisor of lengths of critical cycles in G. [START_REF] Schutter | On the ultimate behavior of the sequence of consecutive powers of a matrix in the max-plus algebra[END_REF]) Let G be a strongly connected digraph, c its cyclicity and λ the minimum average weight of critical cycles in G. Then, M G is ultimately geometric with period c and rate Λ, where Λ i,j = cλ for all i, j. [START_REF] Schutter | On the ultimate behavior of the sequence of consecutive powers of a matrix in the max-plus algebra[END_REF]) Let G be a digraph and let {c 1 , . . . , c m } and {λ 1 , . . . , λ m } be cyclicities and minimum average weights of critical cycles of strongly connected components of G. Then, M G is ultimately periodic with period c = lcm(c 1 , . . . , c m ) and rates {Λ ′ 0 , . . . , Λ ′ c-1 }, where (Λ ′ k ) i,j ∈ {cλ 1 , . . . , cλ m } for all 0 ≤ k < c and for all i, j.

Theorem 2. (Theorem 2.4 in

Theorem 3. (Corollary of Theorem 3.3 in

Corollary 1. For all v 1 , v 2 ∈ V s.t. (Λ 0 ) v1,v2 = ∞ there exists a critical cycle π : v ; v of length p and paths π i : v 1 ; v and π f : v ; v 2 s.t. |π i | + |π f | = b s.t. ∀k ≥ 0 . (M b+pk G ) v1,v2 = w(π i ) + kw(π) + w(π f )
Notice that zigzag automaton can be viewed as a digraph and hence Theorems 2 and 3 apply to them. This means that difference bounds relations are ultimately periodic. Let b, c, Λ 0 , . . . , Λ c-1 be the prefix, period, and rates of R. Then, b + 2, c, Λ 0 , . . . , Λ c-1 are the prefix, period, and rates of M R , the incidence matrix of a zigzag automaton A R . Moreover, the closed form of

{R b+cℓ } ℓ≥0 is R (l) b,c ≡ i =j x i -x j ≤ 0 ) Ii,j ,Fi,j ℓ + (M R b ) i,j (11)
or, equivalently

R (l) b,c ≡ i =j x i -x j ≤ (Λ 0 ) Ii,j ,Fi,j ℓ + (M b+2 R ) Ii,j ,Fi,j (12)
Proof of Lemma 7 By the decision procedure in Section 4, if R is * -consistent and well-founded, then the closed form ϕ (l) r of {R b+cℓ } ℓ≥0 contains an atomic formula x ix j ≤ aℓ + d where a, d ∈ Z, a < 0. By the Equation ( 11), a = (Λ 0 ) Ii,j ,Fi,j . By Theorems 2 and 3, (Λ 0 ) Ii,j ,Fi,j is a c-multiple of the average weight of some critical cycle in some SCC of A R . One of these cycles is π of length p from Corollary 1 (since b + 2 in this lemma corresponds to b in Corollary 1, due to special initial and final transitions in A R ). a < 0 implies (Λ 0 ) Ii,j ,Fi,j < 0, which in turn implies w(π) = p c (Λ 0 ) Ii,j ,Fi,j < 0. Other properties stated in this lemma follow from Corollary 1 for special case k = 1.

⊓ ⊔

Proof of Lemma 8 By Lemma 7, there is a negative critical cycle π of length p in the zigzag automaton:

q 1 G1 --→ q 2 . . . q p Gp --→ q 1 . Let G j = (x ∪ x ′ , E j ) for all 1 ≤ j ≤ p.
Consider the following sum of all constraints represented by edges appearing in the zigzag cycle (note that the sum of weights of these edges equals w(π)):

1≤j≤p   (xi-→x ′ j )∈Ej (x i -x ′ j ) + (x ′ i -→xj)∈Ej (x ′ i -x j )   ≤ w(π) (13)
The left-hand side of (13) can be written equivalently as

1≤j≤p    1≤i≤n, (qj )i=r (x i -x ′ i ) + 1≤i≤n, (qj )i=l (-x i +x ′ i ) + 1≤i≤n, (qj )i=lr (-x i +x i ) + 1≤i≤n, (qj )i=rl (-x ′ i +x ′ i )    (14)
and thus, after simplifications (-x i +x i = 0, -x ′ i +x ′ i = 0), (13) can be written equivalently as

1≤j≤p    1≤i≤n, (qj )i=r (x i -x ′ i ) + 1≤i≤n, (qj )i=l (-x i + x ′ i )    ≤ w(π) (15)
Let f denote the negated sum of all unprimed terms in ( 14) and f ′ denote the negated sum of all primed terms in [START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF]. Then, clearly f ′ = -f [x ′ /x]. Thus, (15) can be written as

f ′ -f ≤ w(π) (16)
Notice that since w(π) < 0, we establish that f ′f < 0 hence f is strictly decreasing.

Since, for all states s, s

′ we have R(s, s ′ ) → f (s) > f ′ (s), we have that R -b (⊤)(s) ∧ R(s, s ′ ) → f (s) > f ′ (s). ⊓ ⊔ Proof of Lemma 9 (Case 1 ≤ k ≤ b) By monotonicity of pre R , (m R -k (⊤) ) i,j ≥ (m R -b (⊤) ) i,j . Thus if (m R -k (⊤) ) i,j = ∞, then clearly (m R -b (⊤) ) i,j < ∞. (Case k > b) Let p = ⌈ k-b c ⌉, and k ′ = b + pc. Note that R k ′ = R (ℓ) b,c [p/ℓ]. Since k ′ ≥ k, by the same argument as for case (1 ≤ k ≤ b), (m R -k ′ (⊤) ) i,j < ∞. Since R (ℓ)
b,c is closed, y iy j ≤ aℓ + d, where a, d ∈ Z, is one of its conjuncts. Since R --→ q 2 . . . q p Gp --→ q 1 be the negative cycle used to construct f , and π f be the suffix from Lemma 8. By construction of the zigzag automaton, for any 1 ≤ j ≤ p, |{i | (q j ) i = r}| = |{i | (q j ) i = l}|

It follows from [START_REF] Halava | Skolem's problem -on the border between decidability and undecidability[END_REF] that each (q j ) i = r contributes to f with a term -x i and that each (q j ) i = l contributes to f with a term +x i and that each (q j ) i ∈ {r, l} doesn't contribute at all. We now demonstrate that for each 1 ≤ j ≤ p, there exists a bijective matching β j : {i | (q j ) i = r} → {i | (q j ) i = l} such that for any 1 ≤ i 1 ≤ n s.t. β j (i 1 ) = i 2 , the difference x i2x i1 is bounded in R -b (⊤) ∧ R, formally R -b (⊤) ∧ R → (x i2 -x i1 ≥ h) for some h ∈ Z. Let j ∈ {1, . . . , p}. By construction of the zigzag automaton, the concatenated graph G j G j+1 . . . G p π f connects each (q j ) i1 s.t. (q j ) i1 = r with a unique (q j ) i2 s.t. (q j ) i2 = l. This induces the required bijection β j . Since G j G j+1 . . . G p π f is a sub-

graph of G p+|π f | R
, it follows that there is a path

x (0) i1 ; x (0) i2 in G p+|π f | R
, in other words, R p+|π f | → x i1x i2 ≤ h for some h ∈ Z. By Lemma 9, R b → x i1x i2 ≤ h ′ for some h ′ ∈ Z too.

Clearly, R -b (⊤) ∧ R → x i1x i2 ≤ h ′ too. Since x i1x i2 ≤ h ′ if and only if x i2x i1 ≥ -h ′ , we obtain the required property. xA m+d = a d-1 A m+d-1 + . . . + a 1 A m+1 + a 0 A m f i,j (m + d) = a d-1 f i,j (m + d -1) + . . . + a 1 f i,j (m + 1) + a 0 f i,j (m) By Theorem 4, we have that (A m ) i,j = p 1,i,j (m)λ m 1 + . . . + p s,i,j (m)λ m s for some polynomials p 1,i,j , . . . , p s,i,j ∈ C[m] of degrees less than the multiplicities of λ 1 , . . . , λ s , respectively. ⊓ ⊔

Proof of Lemma 12

Assume from now on that all non-zero eigenvalues λ 1 , . . . , λ s of A are such that λ d1 1 = . . . = λ ds s = 1, for some integers d 1 , . . . , d s > 0. The method given in [START_REF] Boigelot | Symbolic Methods for Exploring Infinite State Spaces[END_REF] for testing the finite monoid condition for A gives also bounds for d 1 , . . . , d s . Then we have λ L 1 = . . . λ L s = 1, where L = lcm(d 1 , . . . , d s ). As d 1 , . . . , d s are effectively bounded, so is L. By Corollary 2, we have that, if m is a multiple of L, then (A m ) i,j = p i,j (m) for some effectively computable polynomial p i,j ∈ C[m] i.e., for m multiple of L, A m is polynomially definable. But since p i,j (m) assumes real values in an infinity of points m = kL, k > 0, the it must be that its coefficients are all real numbers, i.e. p i,j ∈ R[m]. Moreover, these coefficients are the solutions of the integer system:    p i,j (L) = (A L ) i,j . . . p i,j ((d + 1)L) = (A (d+1)L ) i,j

Lemma 4 .

 4 Computing the weakest recurrent set of an octagonal relation can be done in time O(b • n 3 ), where b is its prefix and n is the number of variables. Alternatively, this problem has O(n 3 • 5 n ) worst-case time complexity.

Lemma 5 .

 5 a * -consistent and well-founded octagonal relation, with prefix b ≥ 0. Then, the relation defined by R -b (⊤) ∧ R is well founded and has a linear ranking function.The first part of the theorem is proved by the following lemma: Let R ⊆ Z n ×Z n be a relation, and m > 0 be an integer. Then wrs(R) = ∅ if and only if wrs(R m ) = ∅, where R m is the relation defined by R -m (⊤) ∧ R.

Lemma 6 .

 6 automaton in the sequel. If the relation defined by R is well-founded, then this weighted automaton must have a cycle of negative weight. The structure of this cycle, representing several of the constraints in R, is used to show the existence of the linear ranking function for the witness relation R -b (⊤) ∧ R. Let R ⊆ Z n ×Z n be an octagonal relation and R db be the difference bounds relation defined by R. Then R is well-founded if and only if R db is well-founded.

Fig. 1 .

 1 Fig. 1. (a) Unfolding of GR. Here x (i) = {x (i) | x ∈ x}. (b) A run of the zigzag automaton over a path in G R 8 .

4 Proof of Lemma 4 Proposition 3 .

 443 Let b and c be the prefix and period of R, respectively. If Λ 0 has at least one negative entry, then wrs(R) = ∅. Otherwise, wrs(R) ≡ R -b (⊤), and we can compute it by composing R with itself b times. Each composition requires a quantifier elimination which takes at most O(n 3 ). Since there are exactly b quantifier eliminations, we have the result. For the second part, b + c is the length of a path in the zigzag automaton A R , with no repeated states. Hence b + c is bounded by the number of states in the zigzag automaton A R , which is at most 5 n . Also, computing Λ 0 of R requires iterating R up to b + c.⊓ ⊔Proof of Lemma 5 "⇒" By the fact that R ← R -m (⊤) ∧ R and the monotonicity of wrs. "⇐" We prove the dual. Assume that wrs(R) = ∅ i.e., there exists an infinite sequence s 1 , s 2 , . . . such that R(s i , s i+1 ), for all i > 0. Then all s i belong to the set defined by R -m (⊤), hence s 1 , s 2 , . . . is an infinite sequence for the relation defined by R -m (⊤) ∧ R as well. ⊓ ⊔ Let {a n } ∞ n=0 and {b n } ∞ n=0 be sequences. Then the following hold:

⊓ ⊔ Definition 11 .

 11 The sequence {g k } ∞ k=0 is ultimately geometric if there exist b ∈ N 0 , c ∈ N, and λ ∈ Q ∞ such that ∀k ≥ 0, ∀s ∈ {0, . . . , c-1} . g b+s+(k+1)c = λ + g b+s+kc Definition 12. The sequence {g k } ∞ k=0 is ultimately periodic if there exist b ∈ N 0 , c ∈ N, and λ 0 , . . . , λ c-1 ∈ Q ∞ such that ∀k ≥ 0, ∀s ∈ {0, . . . , c-1} . g b+s+(k+1)c = λ s + g b+s+kc

  is closed, (m R -b (⊤) ) i,j = d = ∞. ⊓ ⊔Proof of Lemma 10 Let f be a linear decreasing function from Lemma 8. Let π : q 1 G1

D Proofs from Section 5 Definition 13 .Corollary 2 .

 5132 Now since f = 1≤j≤p 1≤i1,i2≤n βj (i1)=i2 (x i2x i1 ) and since we proved that each of the differencesx i2x i1 in the sum is bounded in R -b (⊤) ∧ R, it follows that f is bounded in R -b (⊤) ∧ R too, formally R -b (⊤) ∧ R → (f ≥ h) for some h ∈ Z. ⊓ ⊔ A function f : N → C issaid to be a C-finite recurrence if and only if:f (m + d) = a d-1 f (m + d -1) + . . . + a 1 f (m + 1) + a 0 f (n), ∀m ≥ 0 for some d ∈ N and a 0 , a 1 , . . . , a d-1 ∈ C, with a d-1 = 0. The polynomial x da d-1 x d-1 -. . . a 1 xa 0 is called the characteristic polynomial of f .A C-finite recurrence always admits a closed form.Theorem 4 ([11]). The closed form of a C-finite recurrence is:f (m) = p 1 (m)λ m 1 + . . . + p s (m)λ m swhere λ 1 , . . . , λ s ∈ C are non-zero distinct roots of the characteristic polynomial of f , and p 1 , . . . , p s ∈ C[m] are polynomials of degree less than the multiplicities of λ 1 , . . . , λ s , respectively.Next, we define the closed form for the sequence of powers of A. Given a square matrix A ∈ Z n×n , we have:(A m ) i,j = p 1,i,j (m)λ m 1 + . . . + p s,i,j(m)λ ms where λ 1 , . . . , λ s ∈ C are non-zero distinct eigenvalues of A, and p 1,i,j , . . . , p s,i,j ∈ C[m] are polynomials of degree less than the multiplicities of λ 1 , . . . , λ s , respectively. Proof. If det(A-xI n ) = x d -a d-1 x d-1 -. . .-a 1 x-a 0 is the characteristic polynomial of A, then we have A da d-1 A d-1 -. . .a 1 Aa 0 = 0 by the Cayley-Hamilton Theorem. If we define f i,j (m) = (A m ) i,j , then we have

  Clearly, since A ∈ Z n×n , A p ∈ Z n×n , for any p ≥ 0.Hence p i,j ∈ Q[m]. ⊓ ⊔ Proof of Lemma 13 Assuming the condition a d-i (x) < 0 and a d (x) = a d-1 (x) = . . . = a d-i+1 (x) = 0, for some 0 ≤ i ≤ d, we have P (k, x) = a d-i (x) • k d + . . . + a 1 (x) • k + a 0 (x).Since the dominant coefficient a d-i (x) is negative, the polynomial will assume only negative values, from some point on. ⊓ ⊔

This definition is the dual of the reachability set, needed for checking safety properties: the reachability set is the least fixpoint of the post-image of the transition relation.

The linear affine relations considered in this paper are deterministic, which makes them unsuitable for abstraction.

Or, for that matter, in any theory that has quantifier elimination.

In our case, pre k 1 R (Z n ) ⊇ pre k 2 R (Z n ), for k1 ≤ k2.

The intuition behind the names {l, r, lr, rl, ⊥} of components of control states is that they capture the direction of incoming and outgoing edges (l for left, r for right).

⋆ This work was supported by the French national project ANR-09-SEGI-016 VERIDYC, by the Czech Science Foundation (projects P103/10/0306 and 102/09/H042), the Czech Ministry of Education (projects COST OC10009 and MSM 0021630528), the Barrande project MEB021023, and the EU/Czech IT4Innovations Centre of Excellence CZ.1.05/1.1.00/02.0070. initial configuration non-terminating.


Ananda Basu

Saddek Bensalem

Marius Bozga

Julien Mottin

Francois Pacull

Athanasios Poulakidas

Aggelis Aggelis

System Level Modeling, Analysis and Code Generation: Object Recognition Case Study 1

One of the most important challenges in complex embedded systems design is developing methods and tools for modeling and analyzing the behavior of application software running on multi-processor platforms.

We propose a tool-supported flow for systematic and compositional construction of mixed software/hardware system models. These models are intended to represent, in an operational way, the set of timed executions of parallel application software statically mapped on a multiprocessor platform. As such, system models will be used for performance analysis using simulation-based techniques as well as for code generation on specific platforms. The construction of the system model proceeds in two steps. In the first step, an abstract system model is obtained by composition and specific transformations of (1) the (untimed) model of the application software, (2) the model of the platform and (3) the mapping between them. In the second step, the abstract system model is refined into concrete system model, by including specific timing constraints for execution of the application software, according to chosen mapping on the platform. We illustrate the system model construction method and its use for performance analysis and code generation on an object recognition application provided by Hellenic Airspace Industry. This case study is build upon the HMAX models algorithm [RP99] and is looking at significant speedup factors. This paper reports results obtained on different system model configurations and used to determine the optimal implementation strategy in accordance to hardware resources.

Introduction

Performance of embedded application software strongly depends on features of the underlying hardware platform. Getting the maximum throughput out of many-core platforms demands application software to be designed taking parallelism into account from scratch. This is needed to catch up with the fast growth of computing capacity due to the foreseeable exponential increase of physical parallelism. But programming, testing and verifying parallel software with currently existing tools is notoriously hard, even for experts.

The aim of the SMECY project is to develop new programming technologies and design flows enabling the exploitation of many (100s) core platforms. This paper illustrates one of the design flows developed in SMECY, as depicted in Figure 1. This flow is rigorous, automated and allows fine-grain analysis of final hardware/software system dynamics. It is rigorous because it is based on formal models described in BIP [START_REF] Basu | Modeling Heterogeneous Real-time Components in BIP[END_REF], with precise semantics that can be analyzed by using formal techniques. A system model in BIP is derived by progressively integrating constraints induced on application software by the underlying hardware platform. The system construction method has been introduced in [BB+11a]. The application software and the abstract model of the platform are initially defined using DOL [START_REF] Thiele | Mapping Applications to Tiled Multiprocessor Embedded Systems[END_REF]. In contrast to ad-hoc modeling approaches, the system model is obtained, in a compositional and incremental manner, from BIP models of the application software and respectively, the hardware architecture, by application of (automated) source-tosource transformations that are proven correct-by-construction. The system model describes the behavior of the mixed hardware/software system and can be simulated and formally verified using the BIP toolset. Moreover, it can be used as a basis for automatic code generation for the target platform. We experiment the design flow above on the parallel software model derived from a sequential version of the HMAX models algorithm [START_REF] Riesenhuber | Hierarchical Models of Object Recognition in Cortex[END_REF] developed at Hellenic Airspace Industries. We target implementations on the P2012 platform [START_REF] Stmicroeletronics | Platform 2012: A Many-core Programmable Accelerator for Ultra-Efficient Embedded Computing in Nanometer Technology[END_REF]. P2012 is a high performance, embedded multicore platform currently developed by STMicroelectronics. Although the hardware is not yet physically available, P2012 is supported by compilation and virtual simulation tools. Using the system model and the associated performance analysis tools, we are able to obtain, in a fully automatic way, fine-grained performance results for various implementations. Such results provide helpful insights to a software developer both for the selection of the right parallel decomposition and its optimal mapping on the given platform.

Building faithful system models is mandatory for performance evaluation. Simulation-based methods use adhoc executable system models such as [START_REF] Kienhuis | An Approach for Quantitative Analysis of Application-Specific Dataflow Architectures[END_REF] or tools based on SystemC [START_REF] Moussa | Exploring SW Performance using SoC Transaction-Level Modeling[END_REF]. The latter provide cycleaccurate results, but in general, they have long simulation time as a major drawback. As such, these tools are not adequate for thorough exploration of hardware architecture dynamics neither for estimating effects on real-life software execution. Alternatives include trace-based co-simulation methods as used in Spade [START_REF] Lieverse | System Level Design with SPADE: an M-JPEG case study[END_REF] or Sesame [START_REF] Erbas | A Framework for System-Level Modeling and Simulation of Embedded Systems Architectures[END_REF]. Additionally, there exist much faster techniques that work on abstract system models e.g., Real Time Calculus [START_REF] Thiele | Real-time Calculus for Scheduling Hard Real-Time Systems[END_REF] and SymTA/S [H05]. They use formal analytical models representing a system as a network of nodes exchanging streams. The dynamics of the execution platform can be usually oversimplified and characterized by execution times. Nonetheless, these techniques allow usually estimation of pessimistic worst-case quantities (delays, buffer sizes, etc) and moreover, they require an abstract model of the application software. Building such abstract models requires a significant modeling effort and, if done manually, the construction can be error-prone and lead to inaccurate models. Similar limitations exist in performance analysis techniques based on Timed-Automata [START_REF] Abdeddaim | Scheduling with Timed Automata[END_REF][START_REF] Salah | Compositional Timing Analysis[END_REF]. These can be used for modeling and solving scheduling problems. An approach combining simulation and analytic models is presented in [KBPT06], where simulation results can be propagated to analytic models and vice versa through adequate interfaces.

The paper is organized as follows. Section 2 introduces the HMAX models algorithm. Section 3 introduces the target platform, that is, the P2012 many-core developed by STMicroelectronics. Section 4 introduces the modeling formalisms used and the system model construction method. The implementation and experimental results obtained on the HMAX mapped on P2012 platform are presented in sections 5 and 6. Section 7 concludes and provides ongoing and future work directions.

HMAX Algorithm

HMAX is a powerful computational model of object recognition [START_REF] Riesenhuber | Hierarchical Models of Object Recognition in Cortex[END_REF] which attempts to model the rapid object recognition of human brain. Hierarchical approaches to generic object recognition have become increasingly popular over the years [SWP05, ML08], they indeed have been shown to consistently outperform flat single-template (holistic) object recognition systems on a variety of object recognition task. Recognition typically involves the computation of a set of target features at one step, and their combination in the next step. A combination of target features at one step is called a layer, and can be modeled by a 3D array of units which collectively represent the activity of set of features (F) at a given location in a 2D input grid.

HMAX starts with an image layer of gray scale pixels (a single feature layer) and successively computes higher layers, alternating "S" and "C" layers: Simple ("S") layers apply local filters that compute higher-order features by combining different types of units in the previous layer. Complex ("C") layers increase invariance by pooling units of the same type in the previous layer over limited ranges. At the same time, the number of units is reduced by subsampling.

In our case study experiment, we only considered the two first layers of the HMAX model algorithm. In a preprocessing phase, the input raw image is converted to gray scale input (only one input feature: intensity at pixel level) and the image is then sub-sampled at several resolutions. For the S1 layer, a battery of three filters is applied to the sub-sampled images (three features) and finally for C1 layer we take the spatial max of computed filters across two successive scales.

In this application model, parallelism can be exploited at several levels. First at the layer level, independent features can be computed simultaneously. Second, at the pixel level, the atomic computation of contribution to a feature may be distributed among computing resources. In the scope of this paper, we will consider parallelism at the layer level.

P2012 Platform

Platform 2012 (P2012) [START_REF] Stmicroeletronics | Platform 2012: A Many-core Programmable Accelerator for Ultra-Efficient Embedded Computing in Nanometer Technology[END_REF] is an area and power efficient many-core computing fabric, jointly developed by STMicroelectronics and CEA. The P2012 computing fabric is highly modular, as it is based on multiple clusters implemented with independent power and clock domains, enabling aggressive fine-grained power, reliability and variability management. Clusters are connected via a high-performance fully-asynchronous network-on-chip (NoC), which provides scalable bandwidth, power efficiency and robust communication across different power and clock domains. Each cluster features up to 16 tightly-coupled processors sharing multibanked level-1 instruction and data memories, a multi-channel advanced DMA engine, and specialized hardware for synchronization and scheduling acceleration. P2012 achieve extreme area and energy efficiency by aggressive exploitation of domain-specific acceleration at the processor and cluster level. In the scope of this case study, each processor has been specialized with modular extensions dedicated to floating-point unit computation. Other extension such as vector units or other special-purpose instructions may also be chosen at design-time. A P2012 cluster (Figure 4) aggregates a multi-core computing engine, called Encore and a cluster controller.

The Encore cluster includes a number of processing elements (PEs) varying from 1 to 16. Each PE is built with a highly configurable an extensible processor called STxP70-v4. It is a cost effective and customizable 32-bit RISC core supported by comprehensive state-of-art toolset. The Encore 16 PEs do not have private data caches or memories, therefore avoiding memory coherency overhead. Instead, the PEs can directly access a L1-shared program cache (P$) and a L1-shared tightly coupled data memory (TCDM). Each core therefore has two 64 bitports to the shared memories, a read-only instruction port and a read/write data port. The P$ cache is a 256 KB, 64-bank, direct mapped cache memory while the TCDM is a 256-KB, 32-bank memory. The P$ and the TCDM have been architected with a banking factor of 4 and 2, respectively. The P$ and the TCDM can therefore support a throughput of one instruction fetch and one data access per PE on each clock cycle. Encore provides runtime acceleration by the means of the Hardware Synchronizer (HWS). Various synchronization primitives such as semaphores, mutexes, barriers, joins, etc. can be implemented using accelerated support of the HWS.

The cluster controller (CC) consists of a cluster processor subsystem, a DMA subsystem, a CC interconnect and several interfaces: one to the Encore 16 PEs and one to the asynchronous NoC. The cluster processor is designed around a STxP70-V4 dual-issue core without extension and with 16-KB P$ and 16-KB of local memory.

The Platform 2012 Development Kit provides support for several platform programming models (PPM).

Standards-based programming models are based on industry standards that can be implemented effectively on P2012. The supported standards are OpenMP and OpenCL. Another supported PPM is called Native Programming Layer (NPL). NPL is an API which closely coupled the platform capabilities. It allows the highest level of control on application to resource mapping at the expense of abstraction and platform independence.

The P2012 SDK also features platform models for the execution and the simulation of applications running on the P2012 platform. For the scope of this paper, we used a mono-cluster simulator of the fabric and an Encore engine featuring 16 PEs. We targeted the NPL for fine-tuned control of the deployment of the application on the platform, and to achieve better performances.

System Level Modeling

We briefly recall hereafter the construction of a mixed software/hardware system model introduced in [BB+11a]. The flow of the construction is illustrated in Figure 1. The method takes as inputs representations of the application software, the hardware platform and the mapping. These inputs are provided using the concrete formalism available in the DOL framework [START_REF] Thiele | Mapping Applications to Tiled Multiprocessor Embedded Systems[END_REF]. The output is the system model in BIP framework [START_REF] Basu | Modeling Heterogeneous Real-time Components in BIP[END_REF]. The construction breaks down into several well identified translation and model transformation phases operating on DOL and BIP models.

DOL (Distributed Operation Layer) [TBHH07]

) is a framework devoted to the specification and analysis of mixed hardware systems. DOL provides languages for the representation of particular classes of applications software, multi-processor architectures and their mappings. In DOL, application software is defined using a variant of Kahn process network model. It consists of a set of deterministic, sequential processes (in C) communicating asynchronously through FIFO channels. The hardware architecture is described as interconnections of computational and communication resources such as processors, buses and memories. The mapping associates application software components to resources of the hardware architecture, that is, processes to processors and FIFO channels to memories. For the scope of this paper, we target a simplified, preliminary version of the P2012 platform. This version consists of a mono-cluster version of the P2012 fabric and an Encore engine featuring 16 PEs. Figure 6 presents the abstract model of this platform in DOL. Behavior is defined as automata or Petri nets extended with data and functions described in C/C++. The description of coordination between components is layered. The first layer describes the interactions between components. The second layer describes dynamic priorities between interactions and is used to express scheduling policies. BIP has clean operational semantics that describe the behavior of a composite component as the composition of the behaviors of its atomic components. This allows a direct relation between the underlying semantic model (transition systems) and its implementation. The BIP toolset [BIPa, BIPb] includes a rich set of tools for modeling, execution, analysis (both static and on-the-fly) and transformations of BIP models. It provides a dedicated programming language for describing BIP models. The front-end tools allow editing and parsing of BIP programs, followed by code generation (in C/C++). The code can be used either for execution or for performance analysis using backend simulation tools.

As an example, Figure 7 The system model embodies the hardware constraints into the software model according to the mapping. The construction of the system model in BIP is obtained by a sequence of translations and transformations of the DOL representations, as follows: 1. automatic translation of the application software in DOL into a BIP model. The translation is structural: processes and FIFO channels in DOL are translated into atomic components in BIP, connections in DOL are translated into connectors in BIP. 2. automatic translation of the hardware architecture model in DOL into a BIP model. The translation is also structural: hardware resources (processor, memory, bus, etc) are translated into BIP components, hardware interconnections are translated into connectors in BIP. 3. construction of an initial, abstract system model using source-to-source transformation of the previous two models and composition according to the mapping. 4. refinement of the previous system model by including specific timing information about the execution of the software on the platform.

All the transformations above preserve functional properties of the application software model. Moreover, the system model includes specific timing constraints for execution of the application software on the hardware platform. These constraints are obtained by cross compiling the application model into executable code for the target and measuring the execution time of the elementary blocks of code (e.g., BIP transitions). The timing information is integrated in the system model through the source-to-source transformation done in last refinement step (number 4 in the list above).

For experiments, we restrict ourselves to the S1 layer of the HMAX models algorithm. The process network in DOL consists of 14 processes and 24 FIFO channels. This DOL model is about 700 lines of XML (defining the process network structure) and 1500 lines of C (defining the process behavior). The software model in BIP is constructed automatically from the DOL model. It consists of 38 atomic components interconnected using 48 connectors. The BIP software model is about 2000 lines of BIP code. The system model obtained by deploying the S1 layer on a single P2012 cluster consists of 125 atomic components interconnected using about 1500 connectors. The total BIP description totalizes about 13000 lines of BIP code. This description is compiled into about 50000 lines of C++ code, used for simulation and performance analysis, as explained below.

Performance Analysis on the System Model

The system model captures, besides the pure functionality of the application software, all the non-functional constraints induced on it by the target platform. The system model can therefore be used to analyze nonfunctional properties such as contention for buses and memory accesses, transfer latencies, contention for processors, etc. In the proposed design flow, these properties are evaluated by simulation of the system model extended with observers. Observers are regular BIP components that sense the state of the system model and collect pertinent information with respect to the properties of interest i.e., the delay for particular data transfers, the blocking time on buses, etc. Actually, we provide a collection of predefined observers allowing to monitor and record specific information for most common non-functional properties.

Simulation is performed by using the native BIP simulation tool [BIPa]. The BIP system model extended with observers is used to produce simulation code that runs on top of the BIP engine, that is, the middleware for execution/simulation of BIP models. The outcome of the simulation with the BIP engine is twofold. First, the information recorded by observers can be used as such to gain insight about the properties of interest. Second, with some caution3 , the same information can be used to build much simpler, abstract stochastic models. These models can be further used to compute probabilistic guarantees on properties by using statistical-model checking. This two-phase approach combining simulation and statistical model-checking has been successfully experimented in a different context [BB+10]. Moreover, it is fully scalable and allows (at least partially) overcoming the drawbacks related to simulation-based approaches, that is, the long simulation times and the lack of confidence in the results obtained.

For example, in our application, the execution time of 2D-Gabor filters on P2012 PEs ranges from 220 10 6 to 0,68 10 6 cycles, depending on the size of the input image (ranging from 100x100 to 15x15 pixels). By using these values in the system model, the total execution time of the S1 layer is estimated as 225 10 6 cycles. This overall execution time is negatively impacted by the long access time (i.e., about 100 cycles) to the L3 memory (where all FIFOs are mapped) as well as by the bus contention. A slightly better result is obtained if the FIFOs are all mapped into the TCDM memory. In this case, the memory access time is about 1 cycle and there is no more contention. The total execution time reduces to about 220 10 6 cycles. However, such a mapping is not feasible due to memory size constraints, that is, FIFOs cannot fit all simultaneously within the TCDM memory.

Implementation and experiments on P2012

We are developing an infrastructure for generating code from the BIP system models. We seek for portability and therefore, the generated code targets a particular runtime that can be eventually deployed and run on different platforms, including P2012.

The runtime provides generic API for thread management, memory allocation, communication and synchronization. The generated code is not bound to any particular platform and consists of the functional code and the glue code. The functional code implements the application tasks, that is, processes in the original DOL/BIP models. For each task, a C file is generated that contains the description of the data and a thread routine describing the behavior. The behavior is a sequential program consisting of computation statements and communication calls, that is, invocation of particular API provided by the runtime. The glue code implements the main routine that handles the allocation of threads to cores and the allocation of data to memories. Threads are created and allocated to processors according to the mapping description. Moreover, data allocation consists of allocation of the thread stacks and allocation of FIFO queues for communication. All these operations are realized by using the API provided by the runtime.

As shown in Figure 1, the generated code is finally compiled by the native platform compiler. The code is linked with the runtime, hardware dependent library, to produce the binary executable(s) for execution on the platform. For our experiments, we have used the Native Programming Layer (NPL), a common runtime implemented for both P2012 and MPARM platforms [START_REF] Benini | MPARM: Exploring the Multiprocessor SoC Design Space with SystemC[END_REF]MPS]. The generated code has been run on virtual platforms available in the P2012 SDK 2011.1, namely GEPOP -the P2012 POSIX-based simulator -and the P2012 TLM simulator.

Conclusions

We illustrate a rigorous design flow for development of application on manycore platforms. We consider one of the most challenging case studies provided in the SMECY project, namely the implementation of the HMAX models algorithm for object recognition on P2012, a highly modular, embedded manycore platform developed by STMicroelectronics. Given the application software, an abstract model of the target platform and a mapping, our design flow allows (1) to derive a faithful system model for performance analysis and (2) to produce implementations. The flow is fully automated and mainly supported by the BIP toolset.

This work is being extended in several directions. First of all, we are refining the input DOL model of the HMAX in order to exhibit more fine-grain parallelism, i.e., within 2D-Gabor and Max filters. This refinement seems to be mandatory to increase overall runtime performances. Second, we plan to evaluate and target implementations on the latest P2012 SDK available, which features multi-cluster support as well as optimized runtimes. Third, regarding the design flow, we are working on extensions to richer hardware models, which include for example DMA controllers, bus bridges and/or NoC communication. Moreover, we plan to include and evaluate statistical model checking for system models consisting of multiple software applications running in parallel, following the method described in [START_REF] Basu | Statistical Abstraction and Model-Checking of Large Heterogeneous Systems[END_REF].

Figure 1 :

 1 Figure 1 : The BIP/DOL Design Flow in SMECY

Figure 2 :

 2 Figure 2 : HMax Layers Computation

Figure 3 :

 3 Figure 3 : P2012 Fabric Template Figure 4 : P2012 Cluster P2012 is based on a modular infrastructure as depicted in Figure 3. Fabric-level communication is based on an asynchronous NoC organized in a 2D mesh structure. The routers of this NoC are implemented in a Quasi-Delay-Insensitive (QDI) asynchronous (clock-less) logic. They provide a natural Globally Asynchronous Locally Synchronous (GALS) scheme isolating the clusters logically and electrically. The number of clusters is a parameter of the fabric. A configuration up to 32 clusters is supporter in the current implementation. One important characteristic of the fabric is that all local storage at the cluster level is visible in a global memory map, which also includes memory-mapped peripherals. In this non-uniform memory architecture (NUMA), remote memories (off-cluster or off-fabric) are expensive to access. For this reason, DMA engines are available for hardware-accelerated global memory transfers. At the fabric level, a configurable number of I/O channels, implemented via multiple DMAs, can be used for connecting the fabric to the rest of the SoC. Finally, a fabric controller serves as the control interface between the SoC and the fabric.

Figure 5

 5 Figure 5 presents the process network model constructed from the S1 layer of the HMAX models algorithm. It contains processes Splitter, GFilter1 … GFilter12, MaxFilter1 … MaxFilter11 and Joiner. The Splitter builds the 12 scales of the input image and dispatches them to Filters. Each GFilter1 … GFilter12 implements a 2D-Gabor filter with different orientation. Their results are then sent, feature by feature, to MaxFilters. Each MaxFilter convolves outputs produced by two adjacent GFilters. The results are finally gathered by the Joiner.

Figure 5 :Figure 6 :

 56 Figure 5 : KPN model of the HMAX S1-C1 layers in DOL

  presents the model of a 2D-Gabor filter as an atomic component in BIP. This component consists of 6 control locations (START, S1,... S4, DETACH) and two ports, DOL_read and DOL_write. NDPF_state, size and address are local data (variables) of the component. The variables address and size are associated with the ports. The transitions are either internal transitions (internal_step) where local computation and updates are made, or port interactions, where the component exchanges data and synchronizes with the other BIP components.

Figure 7 :

 7 Figure 7 : BIP Model of a 2D-Gabor Filter

This work has been supported by the ARTEMIS JU Project SMECY, grant no. ARTEMIS-2009-1-100230.

Contact author: Marius Bozga, VERIMAG -Centre Equation, 2 Avenue de Vignate,

Gieres France, email: Marius.Bozga@imag.fr

in order to learn a probability law, the values must be representative and independent