Damien Massé
email: damien.masse@univ-brest.fr

Policy Iteration-based Conditional Termination and Ranking Functions

, we proposed an approach for conditional termination analysis based on abstract fixpoint computation by policy iteration. This method is not based on ranking functions and does not directly provide a ranking relation, which makes the comparison with existing approaches difficult. In this paper we study the relationships between our approach and ranking functions and relations, focusing on extensions of linear ranking functions. We show that it can work on programs admitting a specific kind of segmented ranking functions, and that the results can be checked by the construction of a disjunctive ranking relation. Experimental results show the interest of this approach.

Introduction

Many approaches have been proposed to prove that a program terminates. Most techniques rely on the construction of ranking functions [START_REF] Cousot | Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming[END_REF][START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF] or ranking relations as transition invariants [START_REF] Podelski | Transition invariants[END_REF]. Ranking functions and relations, like invariants in safety analysis, offer a checkable result, not directly related to the technique used to construct them. Similarly, a conditional termination analysis [START_REF] Cook | Proving conditional termination[END_REF], i.e. an analysis which determines the set of terminating states, is expected to return not only the a set of terminating states, but an associated ranking function or relation.

In [START_REF] Massé | Proving termination by policy iteration[END_REF], we proposed to use policy iteration techniques in order to analyze conditional termination. Policy iteration (or strategy iteration) [START_REF] Costan | A policy iteration algorithm for computing fixed points in static analysis of programs[END_REF][START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF] has been developed as an alternative to the classical widening/narrowing techniques used for safety analysis by abstract interpretation on numerical programs. Applied on conditional termination, it can be used to compute, using linear optimization algorithms, an overapproximation of the (potentially) non-terminating states, hence proving the termination of the other states. However, it does not directly provide any ranking function or relation.

In this paper, we examine the relationships between our approach and ranking functions synthesis. We focus especially on disjunctive linear ranking relations and segmented linear ranking functions. We show the construction of a disjunctive ranking relation from the analysis, as well as the existence of a segmented linear ranking function. Reciprocally, we show that programs admitting some restricted form of segmented ranking function can be analyzed by policy iteration. We complete these results by a practical experiments on a prototype analyzer.

Notations

Let x = (x 1 , . . . , x n ) be a tuple of n variables. We denote any element of R x either by (x 1 = v 1 ; . . . ;

x n = v n ) or as a column vector v =    v 1 . . . v n    of R n .
When used as a matrix block, x represents the column vector

   x 1 . . .
x n   . Linear forms on R x are denoted either as a expression ( c 1 x 1 + . . . + c n x n ) or as a row vector (c 1 . . . c n ). Similarly, m × n-matrices M ∈ R m×n may be denoted as a m-tuple of linear forms on R x . Given a matrix M , we denote by M T its transpose.

3 Affine programs and semantics

Programs

For the sake of simplicity, we consider in this paper programs with only one program point. Hence, x being the set of (real) variables, a program is a pair (I, T) where I ⊆ R x is the set of initial states, and T ⊆ ℘ (R x × R x ) describes the transitions, each transition defining a relation between the values of the variables before and after the transition. Since we are interested in affine programs, I and T will be defined by linear constraints, that is:

1. I is a set of linear constraints on x 2. Each transition of T is described as a set of linear constraints on x, x where

x represents the variables after the transition.

In our framework, I can be used to compute an overapproximation of the reachable states. However, for simplicity we will assume that all states are reachable, and I will not be used.

Example 1. We consider the program

A of Fig 1. T = {t 1 , t 2 } is represented with: t 1 :     -1 0 0 0 0 -1 0 0 -1 -1 1 0 0 1 0 1         a b a b     ≤ ≤ = =     0 0 0 -1     Program A: 1: while a ≥ 0 do 2: a ← a + b 3: if b ≥ 0 then 4: b ← -b -1 5: else 6: b ← -b 7:
end if 8: end while Program B:

1: while x ≤ 100 do 2: if (*) then 3:

x ← -2x + 2 4: else 5:

x ← -3x -2 6: end if 7: end while Fig. 1. Two affine programs. a and b are integer variables, x is a real variable, and (*) is a non-deterministic choice.

t 2 :     -1 0 0 0 0 1 0 0 -1 -1 1 0 0 1 0 1         a b a b     ≤ ≤ = =     0 -1 0 0    
Note that we replace b < 0 by b ≤ -1 in the representation, since b is an integer variable. Our approach deals mainly with real variables, and using strict constraints (or floating-point computations) requires technical considerations which are outside the scope of this paper.

In the following, we will represent a transition as a pair (Q, q) where Q is a matrix and q is a vector such that the associated constraints are:

Q x x ≤ q
When the program has only one transition, the program is called a Linear Simple Loop (LSL). Termination of Linear Simple Loop is well known to be a decidable problem (at least for linear assignments) [START_REF] Tiwari | Termination of linear programs[END_REF]. However, deciding conditional termination of LSL is more complex [START_REF] Bozga | Deciding conditional termination[END_REF], and not always possible [START_REF] Dai | Non-termination sets of simple linear loops[END_REF].

Concrete semantics

To each program P is associated a transition relation τ ⊆ R x × R x . This relation can be used to construct a trace-based semantics to prove termination [START_REF] Cousot | An abstract interpretation framework for termination[END_REF]. However, we propose to use here a state based backward semantics: Proposition 1. The set S of states starting an infinite execution trace is equal to: S = gfp λY.pre(Y )

where pre ∈ ℘ (R x ) → ℘ (R x )
is the predecessor predicate transformer:

pre(Y ) = {v ∈ R x | ∃v ∈ Y, (v, v ) ∈ τ } = (Q,q)∈T {v ∈ R x | ∃v ∈ Y, Q v v ≤ q}
If Y is a polyhedron characterized with a set of linear constraints Ax ≤ c, pre(Y ) is a union of polyhedra, which can be computed using libraries like Apron [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]. However, even if pre(Y ) is computable, S is not computable, since the fixpoint computation may not terminate.

As seen in [START_REF] Cousot | An abstract interpretation framework for termination[END_REF], it is well-known that a ranking function can be defined from the iterates of the pre operator: Proposition 2. Let (S i ) i∈O be the iterates of gfp λY.pre(Y ) (i.e. S 0 = R x , S i+1 = pre(S i ) and, for all limit ordinal l, S l = ∩ i<l S i ). Then the function r defined on Σ \ S by:

∀x ∈ Σ \ S, r(x) = min{i ∈ O|r / ∈ S i } is a ranking function over Σ \ S: ∀x ∈ Σ \ S, ∀y ∈ Σ, x → y =⇒ (y / ∈ S ∧ r(y) < r(x))
However, computing (or approximating) S may not give the successive iterates.

Abstraction and abstract semantics

The template polyhedral abstraction [START_REF] Sankaranarayanan | Scalable analysis of linear systems using mathematical programming[END_REF] is a parametric sub-abstraction of the classical polyhedral abstraction, where the linear constraints used must belong to a template. In practice, the template is a matrix T ∈ R m×n . Each row of T represents a linear form of program variables. The matrix T defines an abstraction of ℘ (R n ), where an abstract element ρ is a element of T T = R m where R = R ∪ {-∞, +∞}.. The concretization function is defined as:

γ T (ρ) = {v ∈ R n | T v ≤ ρ} Note 1.
In the following, we may consider T as a matrix or as a set of m linear forms. For any ρ ∈ T T , we will denote by [ρ] f the component of ρ associated to f ∈ T .

In the context of this abstraction, the best abstract transformer pre = α T • pre • γ T is computable:

Lemma 1. With ρ ∈ T T , the component of pre (ρ) associated to f satisfies [pre (ρ)] f = max (Q,q)∈T [ (Q, q) ] f (ρ) with: -If {x|∃x , Q 0 T x x ≤ q ρ } = ∅, then [ (Q, q) ] f = -∞. -otherwise, [ (Q, q) ] f = min{λ(q T ρ T )|λ ≥ 0 ∧ Q T 0 T λ = f T 0 }
Hence pre (ρ) can be computed by solving m.|T| linear programs. However, the classical Kleene iterations (with widening and narrowing operators) can only be used to approximate the abstract semantics S = gfp pre with the following restrictions:

1. Using a dual widening operator can only be used to find an underapproximation of the abstract semantics [START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes[END_REF], which is not sound since our abstract semantics is an overapproximation of the concrete semantics 1 . 2. Using n steps of a narrowing operator would only find states terminating after at most n iterations.

Thus we need to use policy iteration to compute S .

Policy iteration

Policy or strategy iteration [START_REF] Costan | A policy iteration algorithm for computing fixed points in static analysis of programs[END_REF][START_REF] Gaubert | Static analysis by policy iteration on relational domains[END_REF][START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF] is a method to compute the least (or greatest) fixpoint of specific classes of monotonic operators. It can be seen as an adaptation of the classical Newton's method in the sense that the operator σ is approximated (w.r.t. a policy selection) by a policy σ 0 where the fixpoint of σ 0 is computable. A new policy is selected to approximate σ around the fixpoint of σ 0 , and the process iterates until a global fixpoint is reached.

The application of policy iteration to the computation of greatest fixpoints has been presented in [START_REF] Massé | Proving termination by policy iteration[END_REF]. Although this section extends slightly the framework by not restricting transitions to assignments, the results are similar.

Policy selection

Theorem 1. Given a transition t = (Q, q), [ t ] f is the minimum of two function ψ t and [φ t ] f where:

ψ t is monotonic and its image is in {-∞, +∞}; -[φ t ] f is the minimum of a finite number of affine expressions (with positive coefficients) on ρ.

Example 2. For t 1 in program A, and T = (-a, -a -b), we have:

ψ t1 (ρ) = +∞ [φ t1 ] -a (ρ) = -1 + ρ -a-b [φ t1 ] -a-b (ρ) = min(-1 + ρ -a-b , ρ -a )
Theorem 2. Let t be a transition, and ρ ∈ R m . The value of ψ t (ρ) and, if ψ t (ρ) = +∞, the affine expression for which φ t (ρ) is minimal can be computed by solving the following linear program:

max{f.x|∃x, x , Q 0 T x x ≤ q ρ } 1
The overapproximation being necessary to prove termination.

σ ← (+∞) Initial policy ρ ← (+∞) Initial fixpoint: while Φ(ρ) = ρ do Stop if fixpoint is reached for all f ∈ T do if [Φ(ρ)] f < [ρ] f then Change [σ] f only if it is not optimal for ρ [σ] f ← min-policy of [Φ] f such that [σ] f (ρ) = [Φ] f (ρ) end if end for ρ ← gfp ≤ρ σ
Compute the next fixpoint for the policy end while Fig. 2. Policy iteration algorithm for greatest fixpoint computation. This algorithm computes gfp Φ using min-policies: each policy component [σ] f is given by a choice between the min-terms of [Φ] f .

If this linear program is infeasible, then ψ t = -∞, otherwise, ψ t = +∞ and φ t f can be directly constructed from the optimal dual solution.

Given a current policy σ and its fixpoint ρ, the new policy σ is constructed as follows :

[σ ] f = max t∈T [σ t ] f where [σ t ] f = -∞ if ψ t (ρ 0 ) = -∞, and [σ t ] f is an affine expression of [φ t ] f (ρ 0 ) which is minimal for ρ 0 otherwise.
Proposition 3. The policy selection process constructs a new policy for which each component is the maximum of affine expressions. Example 3. For program A, if the current post-fixpoint is (ρ -a = 0, ρ -a-b = 0), the policy selection process gives:

[σ 1 ] -a (ρ) = max(ρ -a-b -1, ρ -a -1) [σ 1 ] -a-b (ρ) = max(ρ -a , ρ -a-b -1)
In the program, this policy expresses the fact that, if after an iteration the constraints -a ≤ u ≤ 0 and -a -b ≤ v ≤ 0 are satisfied, then before the iteration, the constraints -a ≤ max(u -1, v -1) and -a -b ≤ max(u, v -1) are satisfied.

In general, we will write the policy as a system of equations over the components of ρ, e.g.:

ρ -a = max(ρ -a-b -1, ρ -a -1) ρ -a-b = max(ρ -a , ρ -a-b -1)

Policy iteration result Theorem 3 ([23]

). Following the algorithm of policy iteration presented Fig. 2, the new fixpoint ρ l of each policy σ l is computable by solving two linear programs. Furthermore, the algorithm terminates and gives the abstract fixpoint S . Note 2. Although the algorithm of Fig. 2 starts with σ 0 = (+∞), we can adapt it to start from any post-fixpoint. Example 4. Figure 3 shows the results of the analyzes of programs A and B. The initial policy ((+∞)) is omitted. For both programs, Step 1 gives just the translation of the termination condition of the loop. Step 2 gives the equivalent of one more iteration. However, in Step 3, the relations between variables in the equation system enables to jump directly to the fixpoint. This jump is equivalent to ω iterations in the greatest fixpoint computation. Note that the analysis proves the termination of program A from every initial state. For program B, it proves that the programs terminates from x > 1.6 ∨ x < -1.2, which is the best result we can get with a polyhedral abstraction (x = 1.6 and x = -1.2 being both non-terminating states). However, it does not give the exact set of terminating states (e.g. one can check that this program terminates from any integer).

Step Policy Fixpoint

1 ρ-a = 0 -a ≤ 0 ρ -a-b = +∞ 2 ρ-a = max(0, ρ-a -1) -a ≤ 0 ρ -a-b = ρ-a -a -b ≤ 0 3 ρ-a = max(ρ -a-b -1, ∅ ρ-a -1) ρ -a-b = max(ρ-a, ρ -a-b -1)
Step Policy Fixpoint

1 ρx = 100 x ≤ 100 ρ-r = +∞ 2 ρx = 100 x ≤ 100 ρ-x = max((ρx -2)/2, -x ≤ 49 (ρx + 2)/3)) 3 ρx = max((ρ-x + 2)/2, x ≤ 1.6 (ρ-x -2)/3) ρ-x = max((ρx -2)/2, -x ≤ 1.2 (ρx + 2)/3)) (Prog. A) (Prog. B)

Relationships with ranking functions

The policy iteration process computes the exact abstract semantics of the program. Proposition 2 states that this fixpoint entails the existence of a ranking function based on the iterates of the fixpoint, but does not give the form of the ranking function (or relation). In order to compare this approach with other existing methods, we need to make this ranking function explicit, or at least precise the kind of ranking relations a program must satisfy to be successfully analyzable by policy iteration. Since we use linear templates, linear ranking functions and their derivatives (piecewise linear ranking functions and disjunctive linear ranking relations) are the most interesting candidates to compare with our approach.

Ranking functions and relations

Linear ranking function Linear ranking functions are commonly used to prove termination of simple programs. The ranking relation T (r) ⊆ S × S generated by a ranking function r is the well-founded relation defined as

T (r) = {(σ 1 , σ 2 ) | r(σ 2 ) ≺ r(σ 1 )}. If r is a ranking function for τ over S, then T (r) satisfies: τ ⊆ T (r) ∪ (Σ \ S) × Σ
We may use ordinals (O, <) as well-founded sets. However, since our approach deals with real values, we will denote by ≺ on a subset of R, any well-founded suborder of < on this subset.

Definition 2 (Linear ranking function).

A ranking function r on (O, ≺) is linear if O is a subset of R, ≺ is a sub-order of < on O, and r is linear.

Segmented linear ranking functions

The domain of segmented ranking functions is presented in [START_REF] Urban | The abstract domain of segmented ranking functions[END_REF] to infer termination properties on programs. Its analysis produces piecewise-segmented ranking functions to infer sufficient conditions on programs. The domain is parametrized by two numerical abstract domains for the partitioning of the environment and for the values of the function. The prototypes used intervals for the partitioning and affine forms for the functions, but it should be possible to use other linear constraints (maybe templates) for the partitioning (which should be costly). We propose to call this instantiation of the domain segmented linear ranking functions.

Definition 3 (Segmented linear ranking function). Let S ⊆ R m and τ a transition relation on R m , a ranking function r : S → O on S is segmented linear if it can be defined by a n-uplet (S 1 , r 1 ), . . . , (S n , r n ) where:

-{S i } 1≤i≤n is a partition of S, and each S i is a polyhedron; for all i, r i is defined on S i and r = r i on S i . all the r i are linear.

Disjunctive linear ranking relations An alternative to ranking functions are disjunctive ranking relations, defined as a finite union of ranking relations T = T 1 ∪ . . . ∪ T n . Although T may not be itself a ranking relation, a transition relation τ is well-founded if and only if its non-reflective transitive closure τ + is included in a disjunctive ranking relation (which is then called a transition invariant [START_REF] Podelski | Transition invariants[END_REF]). This approach is widely used to prove termination, using model-checking procedures to check the inclusion in transition invariants [START_REF] Kroening | Wintersteiger. Termination analysis with compositional transition invariants[END_REF][START_REF] Cook | Abstraction refinement for termination[END_REF]. Of course, disjunctive ranking functions can be used to prove conditional termination:

Lemma 2. Let P a program with a transition relation τ ⊆ Σ × Σ. Then P terminates from all states in S if and only if there exists a disjunctive ranking relation T = T 1 ∪ . . . ∪ T n such that:

τ + ⊆ T ∪ (Σ \ S) × Σ
In [START_REF] Yi | Termination proofs for linear simple loops[END_REF], Chen et al. proposed to infer disjunctive ranking relations for linear simple loops (LSLs), where each ranking relation T i is (by construction) based on a linear ranking function. More precisely, T i = T (r i ) such that there exists a polyhedral partition (P 1 , . . . , P k ) of R n where:

r i is linear over P 1 ; r i is constant over P 2 , . . ., P k and its values are always strictly lower than the elements of r i (P 1 ).

We will call these relations disjunctive linear ranking relations. Before considering the ranking functions induced by the policy iteration algorithm, we examine the relationships between disjunctive ranking relations and segmented ranking functions. Disjunctive linear ranking relations are strictly more powerful than segmented linear ranking functions: any segmented linear ranking function induces a disjunctive linear ranking relation, but the converse is not true. Theorem 4. Let τ ⊆ Σ × Σ and r a segmented linear ranking function for τ over S, defined by the n-uplet (S 1 , r 1 ), . . ., (S n , r n ). For all 1 ≤ i ≤ n, we define T i : S × S as:

T i = T (r i ) ∪ (S i × (S \ S i )) Then τ + ⊆ T 1 ∪ . . . ∪ T n ∪ (Σ \ S) × Σ.
Example 5. Program A admits a segmented linear ranking function r defined as:

r(a, b) =        0 if a < 0 1 if a ≥ 0 and a + b < 0 2a + 2 if a ≥ 0 and b ≥ 0 2(a + b) + 3 if a + b ≥ 0 and b < 0
The partition contains four sets. The disjunctive ranking relation allows any transition between two different sets, but only decreasing transitions (w.r.t. the local ranking function) inside one set. While not well-founded, it is the union of well-founded relations and includes the transition closure of τ .

The disjunctive ranking relation does not give any information about the relations between the elements of the partition, therefore it can prove the termination of programs which do not admit a segmented linear ranking function. x ← x + y 3:

if y ≥ 0 then 4:

y ← y -1 5:
end if 6: end while terminates and admits a disjunctive ranking relation defined by the ranking functions:

ρ 0 = x if y ≤ -1 and x ≥ 0 -1 if x < 0, or y > 0 ρ 1 = y if y > 0 0 if y ≤ 0
However, a segmented ranking function would need to be quadratic when y > 0.

Policy iteration and ranking relations

Our goal is to link the results of the policy iteration analysis with the existence of disjunctive ranking relations or segmented ranking functions. Since the policy iteration analysis gives an overapproximation of the non-terminating states, there exists a ranking function or relation on the complement, which should be related to the template used. 2 is given by ρ -x and 1.6 by ρ x . Therefore, it appears that the partial ranking functions are related to the negation of the template elements.

In general, we shall prove that if the policy iteration analysis shows that A is a set of terminating states:

1. A disjunctive linear ranking relation can be defined on A, of which the ranking relations are directly related to the template (Theorem 5). 2. We can also find on A a segmented linear ranking function r, with templaterelated restrictions of the domains of the subfunctions. To represent these restrictions, we shall describe r as a min-defined segmented ranking function, i.e. as a minimum of functions with overlapping domains (Definition 4). Furthermore, we prove the converse of this result, i.e. the existence of a segmented linear ranking function satisfying these restrictions on A implies that the policy iteration analysis can prove conditional termination on A (Theorem 6).

By Theorem 3, we know that the policy iteration process returns the exact abstract semantics of the program, defined as S = gfp α T • pre • γ T . The iterates of this fixpoint are elements of the template abstract domain. Hence we can expect a potential ranking relation to be closely related to the template linear forms. Theorem 5 formalizes this idea and shows that the programs directly admits a disjunctive linear ranking relation on the terminating part: Theorem 5. Let T be a template with m linear forms f 1 , . . . , f m over R x , and A an abstract element of T T . If gfp λX.(pre T (X)) = A , then there exists m ranking relations R 1 , R 2 , . . ., R m on R x \ γ T (A ) satisfying the conditions (C1) and (C2) defined as follows:

(C1) For all i, there exists a well-founded suborder ≺ i of < on R such that:

∀(v 1 , v 2 ) ∈ R n \ γ T (A ), (v 1 , v 2 ) ∈ R i ⇐⇒ -f i v 2 ≺ i -f i v 1 (C2) R 1 ∪ . . . ∪ R m is a disjunctive ranking relation for τ over R n \ γ T (A ): τ + ⊆ (R 1 ∪ . . . ∪ R m ) ∪ γ T (A ) × R n
Furthermore, with (pre T ) k denoting the k-th iterate of the operator pre T starting from R n , we can construct ≺ i as:

u ≺ i v ⇐⇒ ∃k ∈ O, u < -[(pre T ) k ] fi ≤ v
This theorem proposes well-founded orders ≺ i based on sets of iterates, which are not easy to use. We shall examine the problem of finding simpler orders in Sect. 5.3.

Example 8. We can prove the termination of program A with the template T = (-a, -a-b). The associated relations R 1 and R 2 can be defined on R 2 as follows:

((a, b), (a , b )) ∈ R 1 iff a ≺ a ((a, b), (a , b )) ∈ R 2 iff a + b ≺ a + b where u ≺ u ⇐⇒ a < 0 ≤ b ∨ 0 ≤ a + 1 ≤ b
We can see that R However, analyzing the program with the template T = (-x, -y) gives just the condition x ≥ 0 for potential non-termination, because the next iterate in the concrete domain gives the constraint x + y ≥ 0 which is not translated in the abstract domain.

Theorem 5 presents a disjunctive linear ranking relation of which the components are based on the policy iteration analysis. As we saw on Example 6, this does not prove the existence of a segmented linear ranking function. Two difficulties arise when we try to construct a segmented ranking function from the policy iteration analysis.

First, the domains of the subfunctions must partition the terminating states, whereas each well-founded order of Theorem 5 is defined on the whole domain. We circumvent the problem by including the possibility of overlapping domains. In this case, the value of the r is defined as the minimum of the values of the underlying functions.

Definition 4 (Min-defined segmented ranking functions). Let Σ be a set of states, S a subset of Σ and τ a transition relation on Σ, a ranking function r : S → O on S (where O ⊆ R) is min-defined segmented if it can be defined by a n-uplet (S 1 , r 1 ), . . . , (S n , r n ) where:

1. 1≤i≤n S i = S, 2. and ∀σ ∈ S, r(σ) = min σ∈Si r i (σ) (where min is the minimum with respect to the total order <).

Furthermore, r is min-defined segmented linear if all r i are linear.

Of course, any min-defined segmented ranking function can be transformed to a segmented ranking function by restricting the domain of the subfunctions. However, using them makes the following theorem much easier to present, as the domain of each subfunction becomes independent of the others subfunctions.

The second difficulty is the relationships between the values of different subfunctions. The easiest approach is to consider intermediate functions ϕ: Theorem 6. Let A ∈ T T . Then gfp λX.(pre T (X))

A if and only if there exists a min-defined segmented ranking function r = min i∈{1,...,m} r i : R n \ γ T (A ) → O such that for all i:

(C3) Dom(r i ) = {v ∈ R n | [A ] fi < f i v} (C4) ∀i, r i (v) = ϕ i (-f i v) where ϕ i is a monotonic function from ] -∞, -[A ] fi [ to O.
Proof (sketch). Let's consider the iterates (A k ) of pre T starting from (+∞). We define r i (v) as the maximal ordinal k such that

f i v ≤ [A k ] fi . One can easily check that this ordinal exists (if v ∈ Dom(r i )), that r i is monotonic w.r.t. -f i v,
and that r is a ranking function. Reciprocally, if a ranking function r satisfy (C3) and (C4), then we prove by transfinite induction that for all v ∈ γ T (A k ), r(v) ≥ k.

The limit case is a consequence of the co-continuity of γ T . For the successor case, let us suppose that there exists

v ∈ γ T (A k+1 ) = γ T • α T (pre(γ T (A k ))) such that r(v) < k + 1 (for example, r i (v) ≤ k). Then there exists v ∈ pre(γ T (A k )) such that f i v ≥ f i v, hence r i (v ) is defined by (C3) and r(v ) ≤ r i (v ) ≤ r i (v) ≤ k by (C4). Since v ∈ pre(γ T (A k )), there must be a successor v of v in γ T (A k )),
which by induction hypothesis must satisfy r(v ) ≥ k, which contradicts the fact that r is a ranking function.

Example 10. Example 5 gives a segmented ranking r function for program A, which can also be min-defined:

r(a, b) = min(r -a (a, b), r -a-b (a, b))
with r -a (resp. r -a-b ) depending only on a (resp. a + b):

r -a (a, b) = 0 if a < 0 2a + 2 if a ≥ 0 r -a-b (a, b) = 1 if a + b < 0 2(a + b) + 3 if a + b ≥ 0
Theorem 6 shows the form of a potential ranking function for the set of terminating states found by the policy iteration algorithm. Also, it gives a completeness result by describing the programs analyzable with a specific template as any program admitting a min-defined segmented ranking function satisfying these conditions. Since linear ranking functions satisfy them, we can deduce that programs admitting linear ranking functions can be proved to terminate by policy iteration (with an appropriate template):

Corollary 1. If a program admits a linear ranking function r, then a policy iteration analysis with a template T including -r can prove its termination.

Conditional termination with a linear ranking function, however, is more complicated since condition (C3) make strong assumptions on the domain of the ranking function.

Example 11. The program 1: while x ≥ 0 do 2:

x ← x + y 3: end while admits x as a linear ranking function when y < -1. However, an analysis with the template (-x, -y) cannot give any result of the form A = (x >= 0, y >= -1) because the domain of the ranking function associated to x should be all the states satisfying x < 0. More generally, while the set of non-terminating states is (x >= 0, y >= 0), we can prove that no template can give this result.

On the other hand, with an initial constraint of the form y ≤ -< 0, the analysis proves the termination of the program.

On the well-founded relations

Theorem 5 proposes well-founded relations ≺ i defined from (infinite) sets of iterates of the abstract computation. However, relations found in the literature are generally defined directly. For example, a common order used in linear ranking functions is ≺ (with > 0) defined as:

a ≺ b ⇐⇒ a + ≤ b
Such an order is useful because checking a ≺ b is easier, and because it shows the evolution of the states towards termination.

In this section we study the possibility of constructing theses kinds of orders (not based on infinite sets) from the analysis. Our first step is consider the sequence of policies. This sequence constructs a finite and decreasing chain of p + 1 fixpoints ρ 0 = (+∞), . . . , ρ p . Projecting this chain to the i-th component gives a decreasing sequence ρ i 0 = +∞, . . . , ρ i p . As a result, any couple (a, b) where a < -ρ i k ≤ b can be included in ≺ i . Hence we can construct ≺ i as:

≺ i = ≺ i,1 ∪ ≺ i,2 ∪ . . . ∪ ≺ i,p ∪ ] -∞, -ρ i 1 [ × [-ρ i 1 , +∞[ ∪ . . . ∪ ] -∞, -ρ i p [×[-ρ i p , +∞[ (1)
where each ≺ i,k is associated to the k-th policy and only defined on [-ρ i k-1 , -ρ i k [. Example 12. With program B, we need two well-founded orders ≺ x and ≺ -x on R. Since the successive fixpoints (for the linear form x) gives x ≤ 100 and x ≤ 1.6 (cf. Fig. 3), we may construct ≺ x as:

a ≺ x b ⇔ a < -1.6 ≤ b or a < -100 ≤ b or (a, b) ∈ [-100, -1.6[ ∧ a ≺ x,3 b or (a, b) ∈] -∞, -100[ ∧ a ≺ x,1 b
where ≺ x,1 (resp. ≺ x,3 ) is a well-founded suborder of < on ] -∞, -100[ (resp. [-100, -1.6[).

Finding an order for each policy is difficult. Let's restrict ourselves to the case of a LSL. The policy is described as a system of affine equations, and the next fixpoint as the limit of a sequence (ν k ) of the form:

ν 0 = ρ j ν k+1 = Aν k + B
where A is a nonnegative matrix. Then we have ν k-1 -ν k = A k (ν 0 -ν 1 ) (where ν 0 -ν 1 is also nonnegative). Using [20, Sect. 9.3], we get the following proposition: Proposition 4. Let P be a LSL, and ρ 0 , . . . , ρ p the sequence constructed by policy iteration on P , ρ i k-1 and ρ i k the i-th component of ρ k-1 and ρ k . Then there exists a well-founded order ≺ i,k for equation (1) and a integer d > 0 such that:

-if ρ k = -∞, ∃ > 0, (≺ i,k ) d ⊆≺ where a ≺ b ⇔ a + ≤ b -otherwise: ∃h > 1, (≺ i,k ) d ⊆≺ h,-ρ i k where a ≺ h,-ρ i k b ⇔ (-ρ i k -a) ≥ h(-ρ i k -b) In this proposition, (≺ i,k ) d =≺ i,k • . . . •≺ i,k is the d-th power of ≺ i,k . Note that ≺ or ≺ h,-ρ i k are well-founded orders on [-ρ i k-1 , -ρ i k [, which implies that ≺ i,k is a well-founded order.
This proposition does not directly give ≺ i,k , but it shows that decreasing sequences decreases (at least) on average linearly when ρ k = -∞ and geometrically (from the upper bound) when ρ k is finite. Although this results is not proven on the general case, we expect the progressions to be similar in most cases.

Example 13. Continuing the previous example, we consider ≺ x,1 on ]-∞, -100[ and ≺ x,3 on [-100, -1.6[. The first policy (associated to ≺ x,1 ) returns the next fixpoint after one iteration. Hence we can just define ≺ x,1 = ∅.

The third policy (associated to ≺ x,3 ) converges with a geometric rate. The order ≺ x,3 can be defined as:

u ≺ x,3 u ⇐⇒ (-1.6 -u) ≥ 4(-1.6 -u )
Concretely, this results shows that from an initial value x > 1.6, the value of x (when x > 0) diverges from 1.6 at a geometric rate.

Experiments

Template selection

A prototype analyzer implementing the policy iteration algorithm was developed, using VPL2 to handle exact polyhedral and linear programming operations. Since our analysis use the template polyhedral domain, selecting a correct template was an issue. However, overapproximating the greatest fixpoint enables a progressive refinement of the template: any fixpoint computed with a template can be used as a starting post-fixpoint with another template. Based on this idea, the following heuristics was implemented:

1. first, a few backwards steps in the general polyhedral domain is computed; 2. then the actual linear constraints are used as a basis for the template and the abstract fixpoint is computed for this template; 3. the process can be iterated from the new post-fixpoint, alternating between backward direct iterations and policy iterations. Since every intermediate result is a safe approximation, we can stop anytime, or if the fixpoint is reached.

This heuristics can be compared to existing techniques for invariant analyses which uses partial traces to specialize the abstract domain [START_REF] Amato | Deriving numerical abstract domains via principal component analysis[END_REF][START_REF] Seladji | Fixpoint computation in the polyhedra abstract domain using convex and numerical analysis tools[END_REF]. In the worst case, the analysis gives the same result as a classical narrowing, returning an approximation of the states which do not terminate after n loop iterations. In the best case, it gives the abstract greatest fixpoint in the (general) polyhedral domain, which may not be the exact set of non-terminating states.

Example 14. In the terminating program (from [START_REF] Cook | Ramsey vs. lexicographic termination proving[END_REF]):

1: while x = 0 do 2:

if x > 0 then 3:

x ← x -1 4:

else 5:

x ← x + 1 6:

end if 7: end while the decreasing iterations in the polyhedral domain stabilizes immediately at ] -∞, +∞[. The problem can be solved by using several program points (or, similarly, state partitioning) to separate the cases x > 0 and x < 0. LSL test suite First, we used the LSL test suite proposed by Chen et al. [START_REF] Yi | Termination proofs for linear simple loops[END_REF]. This suite has 38 LSL loops, of which 12 are non-terminating, 7 are terminating with linear ranking functions, and 19 are terminating with non-linear ranking functions. Our prototype analyzed the whole test suite in 0.5 second. The results are summarized on Table 1. Terminating LSLs with a linear ranking function are all proved to terminate (although our heuristics does not guarantee this).

Results

Terminating LSLs without a linear ranking function are proved to terminate most of the time, yet our analyzer failed in 6 cases whereas Chen et al.'s algorithm, which is specifically designed to prove termination on LSLs, failed only twice. Interpreting the results of non-terminating LSLs is harder since this test suite was not designed for conditional termination analysis. For 2 LSLs, our approach managed to find the exact set of terminating states, something which was not possible with only narrowings. For 3 LSLs, the greatest fixpoint is directly reached by a few iterations in the polyhedral domain. Finally, for the other programs, the PI techniques does not refine the decreasing iteration sequence. These results show that our approach is quite fast and can find complex termination properties, but not as efficient as a technique specifically designed for linear simple loops.

Other programs To our knowledge, no test suite exists for termination analysis (or conditional termination) on general programs. Hence we tested some examples given on previous works. The analyzes were fast and sometimes successful. However, several cases failed to give interesting results. We identified two main causes.

1. The iterates in the polyhedral domain stabilize after a few iterations, as in Example 14. This problem is directly related to the use of polyhedral abstractions. 2. Termination (or interesting conditional termination) requires the use of lexicographic ordering [START_REF] Cook | Ramsey vs. lexicographic termination proving[END_REF]. Our approach seems to be more suited to prove termination when the ranking relations are interlinked than when they form a lexicographic order. This is especially interesting as other approaches (limited to termination analysis) are specifically designed for lexicographic ordering [START_REF] Cook | Ramsey vs. lexicographic termination proving[END_REF][START_REF] Alias | Multidimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF]. Hence our approach can be used in complement to those.

For both problems, partitioning the set of states should improve the results.

Conclusion

This paper has described how policy iteration can be used to find conditional termination properties. The analysis is fast and the result can be precise, although it relies heavily on the abstract domain used. To improve the analysis, we plan to investigate the application of dynamic trace partitioning [START_REF] Rival | The trace partitioning abstract domain[END_REF] for conditional termination. Another possibility would be to extend the policy iteration framework to other abstract domains such as the generalized template domain [START_REF] Colón | Generalizing the template polyhedral domain[END_REF] or quadratic templates [START_REF] Adjé | Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis[END_REF].

Fig. 3 .

 3 Fig. 3. Results of the policy iteration process on program A with the template T = (-a, -a -b) and program B with the template T = (-x, x).

Definition 1 (

 1 Ranking function). If Σ is a set of states, S a subset of Σ, and τ ⊆ Σ × Σ a transition relation, a ranking function over S is defined by an ordered set (O, ≺) and a function r : S → O such that ≺ is a well-founded order and: ∀σ ∈ S, σ τ → σ ⇒ σ ∈ S and r(σ ) ≺ r(σ) If τ represents the transition relation induced by a program P , the existence of a ranking function over S shows that the program terminates from any state in S.

Example 6 .

 6 The program 1: while x ≥ 0 do 2:

Example 7 .

 7 For program B, the policy iteration analysis (with T = (x, -x)) proves that the program terminates from x > 1.6 or x < -1.2. A ranking function r should be defined on ] -∞, -1.2[ ∪ ]1.6, +∞[. Since |x| increases at each iteration, r should be increasing on ] -∞, -1.2[ (with lim x→-1.2 r(x) = ω) and decreasing on ]1.6, +∞[ (with lim x→1.6 r(x) = ω). Hence, on ] -∞, -1.2[, x is a ranking function, whereas -x is a ranking function on ]1.6, +∞[. Note that the value -1.

1 and R 2 Example 9 .

 29 are generated by the functions a and a + b. Example 9 shows that the converse of Theorem 5 does not hold: The program seen in Example 6 admits a disjunctive ranking relation T (ρ 0 ) ∪ T (ρ 1 ) with ρ 0 = x and ρ 1 = y with the well-founded order ≺ defined as a ≺ b ⇔ a < 0 ≤ b ∨ a + 1 ≤ b.

Table 1 .

 1 Experiment results

		LSL test suite[5]
	Programs		Results
	Terminating : 26	Linear r.f.: 7 Non-linear r.f.: 19	Termination proved: 7 Termination proved: 13
	38 LSLs		Exact semantics with PI: 2
	Non-terminating : 12	Exact semantics with narrowing: 3
			No improvement: 7

http://verasco.imag.fr/wiki/VPL

Acknowledgements. The author thanks D. Monniaux, L. Gonnord and S. Putot as well as the anonymous referees for their comments and suggestions.


Rémy Léone

Jérémie Leguay

Paolo Medagliani

Claude Chaudet
email: claude.chaudet@telecom-paristech.fr

MakeSense: Managing Reproducible WSNs Experiments

Keywords: experiment automation, Wireless Sensors networks, experiments reproducibility, COOJA, CONTIKI

Wireless Sensor Networks (WSN) users often use simulation campaigns before real deployment to evaluate performance and to finetune application and network parameters. This process requires repeating the same experiments under similar conditions and to collect, parse and present data efficiently. This paper introduces MakeSense: a tool that automates this workflow and that allows reproducing simulations easily by defining the whole experiment and post-processing steps in a single JSON configuration file, easy to share and to modify. MakeSense also provides interfaces to interact with a running simulation, allowing to send external stimuli and to collect data in real time. MakeSense currently runs over the COOJA simulator, but has been built to be easily adapted to other architectures, including real testbeds.

Introduction

Evaluating applications and protocols through simulation always follow the same workflow from the simulation parameters definition to the creation of graphs that represent performance under different conditions. Yet, no generic tool really provides a way to automate the whole process and people often rely on ad-hoc scripts. Some tools such as NEPI [START_REF] Lacage | NEPI: using independent simulators, emulators, and testbeds for easy experimentation[END_REF] focus on the interaction between testbeds, but do not address wireless sensor network platforms and hence, their architecture may be too complex for constrained devices.

In this paper, we introduce MakeSense, a tool that automates large-scale WSN experiments and facilitates adaptation and reproducibility. MakeSense relies on a single JSON configuration file described in section 2 from scenario definition to graphs generation. Sharing this lightweight file with the specific source code is sufficient to let others reproduce an experiment, improving the results trustworthiness [START_REF] Aruliah | Best practices for scientific computing[END_REF]. MakeSense runs today over the COOJA simulator, but is designed to be generic and to be adapted to real testbeds too. We then describe its workflow and functionalities, including online interaction with simulation and describe a demonstration in section 3.

[...] " interference_range " : 5 0 . 0 , "makefile_template" : " s i m p l e _ m a k e f i l e " , "mote_types" : { " h e l l o " : { " color " : " b l u e " , " description " : " Router " , "firmware_address" : [ " nodes " , " h e l l o " , " h e l l o -world . sky " ] , "rpl_instance_id" : 30 } } , "motes" : [ { "mote_id" : 1 , "mote_type" : " h e l l o " , " s e t t i n g s " : { "lambda" : 1 } , "socket_port" : 6 0 0 0 1 , "x" : 1 0 , "y" : 0 } , 2 MakeSense Core Functionalities

JSON Configuration file

All simulation parameters such as random seeds, transmission range are defined in a single JavaScript Object Notation configuration file. An excerpt of such a configuration file is presented on Listing 1.1. The file starts by the definition of some general parameters, such as the wireless interference range and specifies a template for the Makefile that will serve during the building process. It then defines one or several mote types (e.g. routers, end nodes, ...), the firmware they will use and gives them an RPL instance ID. In the motes section, it instantiates the different nodes with respect to the templates and specifies individual parameters such as their coordinates, their ID (address) and the UDP port on which they will be reachable during the simulation. As this configuration file specifies all relevant parameters for a simulation, it is easy to use templates and scripting to run large experimental campaigns.

A script can generate a series of such files, referring to the same or to different source codes, run experiments and store the JSON files as scenario descriptors, as they are lightweight.

Workflow

MakeSense workflow, represented schematically on Figure 1, is composed of 6 steps that can be called independently, thanks to their loose coupling, or run in sequence using the run_all shortcut. make creates the whole environment necessary for the experiment execution. It compiles the source code and creates the configuration files required by the simulation tool from templates. deploy uploads the simulation files from a local repository to a remote location to run several simulations in parallel. This step can easily be adapted to upload firmwares to a real testbed. run_exp launches the simulation series. MakeSense can launch concurrently, several functions that will fetch the simulation output through the nodes' serial or network interfaces. Each node has its own independent log file. analyze parses trace files, e.g. PCAP files or text logs file, by applying a set of filters to produce CSV files that contain only the desired information. Filters are easy to specify and MakeSense includes a set of basic filters. plot produces graphs using the CSV files produced by the analyze step and the info in the settings files to select relevant data. report gathers all the results into a single HTML report file.

Multiple control channels

The simulation runs from its beginning to its end without user interaction, or can be run in real-time mode, allowing real-time interaction with traffic generators such as real applications, other simulators, or a user using an interactive command line and visualizing performance evolution through the COOJA scripting engine, as illustrated on Fig. 2. This feature allows to let the WSN run as if it were a real network and to measure its reaction to external, controlled, stimuli.

Demonstation

The COOJA implementation of MakeSense uses the Python programming language and other libraries such as fabric, jinja2 and matplotlib. As a demonstration, we use COOJA [START_REF] Eriksson | COOJA/MSPSim: interoperability testing for wireless sensor networks[END_REF] in real time mode to simulate a network of 10 nodes connected using an RPL tree. The first node is a border router that connects all the remaining nodes that are CoAP servers, to the hosting operating system. We send traffic to the different sensor nodes from the shell and from the script engine contained inside the simulator. This traffic is composed of CoAP and PING requests. As specified in the configuration file, MakeSense generates without user interaction various graphs. For example, Fig. 3 represents the theoretical connectivity graph, extracted from the sole configuration file using circular transmission range. Fig. 4 is a representation of the real RPL tree, generated by querying nodes for RPL information on their serial interface, without perturbing the network traffic. Fig. 5 is a classical per-protocol throughput graph, showing the use of per-protocols filters and Fig. 6 represents delay of Ping requests issued from the hosting operating system, that shows the interaction with the outside world.

Conclusion

This paper describes and shows an example use of MakeSense, a framework for automating series of simulation in order to make them reproducible and reusable. The current implementation is tailored for the Cooja simualtor, and we are working on its adaptation to real testbeds. The MakeSense Python implementation for Cooja is available at: http://github.com/sieben/makesense.

  figures

Figure6.

  Figure3. Connectivity graph


Vincent Legout
email: vincent.legout@cea.fr

Mathieu Jan
email: mathieu.jan@cea.fr

Laurent Pautet
email: laurent.pautet@telecom-paristech.fr

An off-line multiprocessor real-time scheduling algorithm to reduce static energy consumption

Energy consumption of highly reliable real-time embedded systems is a significant concern. Static energy consumption tends to become more important than dynamic energy consumption. This paper aims to propose a new off-line scheduling algorithm to put as much as possible processors in lowpower states instead of idling. In these states, energy consumption is reduced, enhancing the battery life-time of mission critical systems. However, no instruction can be executed and a transition delay is required to come back to the active state. Activating deeper low-power states requires to produce larger idle periods. As the processor usage is constant for a given task set, this objective implies reducing the number of idle periods. Our proposal is to modelize the processors idle time as an additional task. Then we formalize the problem as a linear equation system with the objective of reducing the number of preemptions (or executions) of this additional task. Simulations show that our algorithm is more energy efficient than existing algorithms.

I. INTRODUCTION

Embedded systems tend to have a limited power supply usually provided by batteries. Therefore minimizing the power consumption is an important concern to increase the autonomy of the embedded electronics. For example, power consumption is a major concern in the design of Unmanned Aerial Vehicles, which must also perform real-time processing. Fulfilling both constraints in a reliable way is still challenging. In such realtime systems, many devices can consume power. This work concentrates on the consumption of processors.

The energy consumption can be divided into two categories: dynamic consumption and static consumption, the former being caused by the activity of the processor while the later (mainly due to leakage currents) cannot change when the processor is active, no matter the activity. Note that thermal considerations on energy consumption are out of the scope of this work. Solutions to save energy exist at both hardware and software level. DPM (Dynamic Power Management) and DVFS (Dynamic Voltage and Frequency Scaling) are the two main software solutions. DPM aims to reduce the static consumption by putting system components in low-power states where energy consumption is reduced but no instruction can be executed. A transition delay is required to get the system back to the active state. DVFS deals with dynamic consumption and tries to execute tasks at lower frequencies (and therefore lower supply voltage).

Dynamic consumption used to be more important than static consumption. Therefore, most of the research works were dedicated to design approaches based on DVFS. Existing algorithms rarely try to reduce the static consumption. They mainly use DPM only when DVFS is no longer efficient (e.g. [START_REF] Jejurikar | Leakage aware dynamic voltage scaling for real-time embedded systems[END_REF], [START_REF] Chen | Leakage-aware energy-efficient scheduling of real-time tasks in multiprocessor systems[END_REF]). However, static consumption becomes more important than dynamic consumption, one reason being the higher density of chips or the smaller supply voltage [START_REF] Sueur | Dynamic voltage and frequency scaling: The laws of diminishing returns[END_REF]. We compared the DPM solution introduced in this paper and a DVFS solution using a specific processor. The results showed that DPM can already be more efficient than DVFS, especially when the number of available frequencies is limited. The efficient use of DPM is therefore becoming an important issue, in particular in real-time embedded systems. However, only few publications address the management of static consumption on multiprocessor systems. And the existing solutions are not efficient enough, they produce shorter idle periods than possible.

This paper explores the problem of maximizing the use of low-power states on symmetric multiprocessor embedded real-time systems in order to save energy when scheduling tasks. On hard real-time systems, deadlines must be respected, thus low-power states should be used with care in order for processors to be ready when the system needs them. Transition delays required to come back from a low-power state to the running state must be taken into account.

The contribution of this paper is to propose an off-line scheduling algorithm that reduces static consumption. While guaranteeing the schedulability of the task set, the objective of the algorithm is to increase the duration of the idle periods by merging them when possible. The processor usage being constant for a given task set, the time processors are expected to be idle remains identical whatever the scheduler used. Therefore the objective can also be expressed as the minimization of the number of idle periods. Contrary to current algorithms, it does not use priority assignment to schedule tasks. It formalizes the problem using linear programming such that the constraint (satisfying deadlines) and the objective (generating larger idle periods) of the scheduling algorithm can be met.

The remainder of this paper is as follows. Section II describes the main solutions found in the literature, then section III defines the processor and task models used in this paper while section IV details our algorithm. Sections V presents the experimental results and section VI concludes.

II. RELATED WORK

One of the first approaches to use DPM on hard real-time systems was proposed by Lee et al. [START_REF] Lee | Scheduling techniques for reducing leakage power in hard real-time systems[END_REF] for tasks with dynamic or static priority on a uniprocessor system. Their goal was to extend the duration of the idle periods of the processor. When the processor is idle, it delays task executions even when tasks are ready and start executing tasks just in time to prevent a deadline miss. Jejurikar et al. [START_REF] Jejurikar | Leakage aware dynamic voltage scaling for real-time embedded systems[END_REF] and Chen and Kuo [START_REF] Chen | Procrastination for leakage-aware ratemonotonic scheduling on a dynamic voltage scaling processor[END_REF] improved the solution by increasing the duration of the procrastination period (i.e. the time spent delaying a task execution). Zhu et al. [START_REF] Zhu | Dvsleak: combining leakage reduction and voltage scaling in feedback edf scheduling[END_REF] proposed another improvement when tasks do not use all their worst case execution time.

However, these last three solutions all use DPM on top on DVFS. Indeed, their main common objective is to decrease the dynamic consumption which is modelized as a function of the running frequency such as P dyn ≈ f α (with α between 2 and 3) ( [START_REF] Yao | A scheduling model for reduced cpu energy[END_REF], [START_REF] Aydin | Dynamic and aggressive scheduling techniques for power-aware real-time systems[END_REF], [START_REF] Chen | Energy-efficient scheduling for real-time systems on dynamic voltage scaling (dvs) platforms[END_REF]). Thus P dyn being a convex and increasing function of the processor frequency, there is a critical frequency f crit such that running at a frequency lower than f crit is not efficient compared to DPM. Therefore many algorithms using both DPM and DVFS, like [START_REF] Jejurikar | Leakage aware dynamic voltage scaling for real-time embedded systems[END_REF] or [START_REF] Chen | Procrastination for leakage-aware ratemonotonic scheduling on a dynamic voltage scaling processor[END_REF], only use DPM when DVFS schedules tasks at f < f crit .

On multiprocessor systems, when energy consumption is not a concern, no optimal scheduling algorithm exists for partitioned scheduling (i.e. where tasks are bounded to a specific processor) and only few exist for global scheduling (i.e. where migration is allowed). These optimal global algorithms are mainly based on fair scheduling like PFair [START_REF] Baruah | Proportionate progress: a notion of fairness in resource allocation[END_REF]. However, partitioned scheduling is more widespread than global scheduling because it is equivalent to uniprocessor scheduling when tasks have been assigned to processors.

Energy-aware scheduling algorithms mainly use partitioned scheduling. For periodic task systems, Chen et al. [START_REF] Chen | Leakage-aware energy-efficient scheduling of real-time tasks in multiprocessor systems[END_REF] first partition tasks and then use power-aware uniprocessor scheduling algorithms to decrease both static and dynamic consumptions. Seo et al. [START_REF] Seo | Energy efficient scheduling of real-time tasks on multicore processors[END_REF] and Haung et al. [START_REF] Huang | Leakage-aware reallocation for periodic real-time tasks on multicore processors[END_REF] also use partitioned scheduling. Their algorithms first partition tasks off-line, then allow task migration on-line. Indeed, tasks can finish earlier than expected and the idea is to migrate them to create larger idle periods. However, these algorithms are on-line and they do not have a global overview of the duration of all idle periods on one hyper-period.

Bhatti et al. [START_REF] Bhatti | Controlling energy profile of rt multiprocessor systems by anticipating workload at runtime[END_REF] used global scheduling with DPM. The goal of their algorithm, AsDPM, is to use as few processors as possible, letting the others asleep. When one task or more are ready to be scheduled, AsDPM always keeps one processor busy and activates the other ones only when required. However, the algorithm is not optimal and can activate more processors than needed because it cannot anticipate all future job executions.

All these algorithms use DVFS or DPM and base their scheduling decisions on task priority assignment. It activates the higher priority task as soon as it becomes ready. This approach can be suitable for DVFS but it prevents the creation of large idle periods and thus an effective use of DPM. Among the other approaches that does not use priority assignment, one was proposed by Lemerre et al. [START_REF] Lemerre | Equivalence between schedule representations: Theory and applications[END_REF]. They use linear programming to compute off-line a valid schedule. The advantage of this approach is to be able to add scheduling objectives in the linear equation system. For example Megel et al. [START_REF] Megel | Minimizing task preemptions and migrations in multiprocessor optimal real-time schedules[END_REF] used it with the objective of decreasing the number of preemptions for optimal multiprocessor global scheduling.

III. MODEL

This section introduces the notations used in the remainder of this paper.

A. Processors

The system has m identical processors (with m > 1). Global scheduling is adopted, i.e. tasks and jobs can migrate from one processor to another. We make the optimistic assumption that task preemptions and migrations have no effect on energy consumption. This assumption shall be relaxed in future works.

To use DPM, we assume processors have at least one lowpower state. In a low-power state, a processor cannot execute any instruction and its energy consumption is reduced. When the system decides to wake up a processor, the processor takes a certain amount of time to come back to the nominal state and it cannot execute any instruction while waking up. We assume that the consumption used while waking up is equal to the consumption in the nominal state.

When the system has to choose a low-power state, it must be aware of the duration of the idle interval which must be greater than the transition delay required to wake up. In the literature the minimal length of an idle period to use a lowpower is called the Break-Even time (BET).

B. Tasks

We consider a set Γ of n independent, preemptible and periodic tasks. Each task τ releases jobs periodically every period T and has a worst case execution time C. Tasks have implicit deadlines, i.e. deadlines are equal to periods. The task set hyper-period is named H and is the least common multiple of all periods of tasks in Γ. Task utilization u is the ratio C T and the task set global utilization is the sum of all utilizations: U = n-1 i=0 u i . The job set J Γ contains all jobs of Γ scheduled during the hyper-period H.

The situation where global utilization is equal to the number of processors is trivial, all processors are always active. More generally, a task set with U ∈ N is schedulable such as U processors are always active while the others are always sleeping, therefore generating no transition delay. Thus we assume global utilization U is such as:

m -1 < U < m (1)
And if mx -1 < U < mx, set m = mx and let the x last processors always asleep (x ∈ N * , x < m).

We adopt the representation from [START_REF] Lemerre | Equivalence between schedule representations: Theory and applications[END_REF] and [START_REF] Megel | Minimizing task preemptions and migrations in multiprocessor optimal real-time schedules[END_REF] where the hyper-period is divided in intervals, an interval being delimited The weight of a job on an interval is defined as the fraction of processor required to execute job j on interval k. J k is the subset of J Γ that contains all active jobs in interval k. E j is the set of intervals on which job j can run. It must contain at least one interval. The example task set in figure 1 has two tasks and four jobs (jobs 1 to 3 from τ 1 and job 4 from τ 2 ).

In this example, E 4 is {1, 2, 3} and J 1 is {1, 4}.

Verifying the schedulability of the task set can be expressed as a linear problem from which the weights of all jobs on every interval can be obtained using a linear solver. For the task set to be schedulable, the following equations must hold [START_REF] Lemerre | Equivalence between schedule representations: Theory and applications[END_REF]:

∀k, j∈J k w j,k ≤ m (2) ∀k, ∀j, 0 ≤ w j,k ≤ 1 (3) ∀j, k∈Ej w j,k × |I k | = j.c (4)
Where j.c is the worst case execution time of job j. The first inequality means that the utilization on an interval cannot exceed the number of processors. The second inequality forbids the duration of a job on an interval to be negative or to exceed the length of the interval. And the third equation guarantees that all jobs are completely executed.

Solving the linear program given by equations ( 2), ( 3) and (4) gives the weight of all jobs on every interval thus a complete and valid schedule. This schedule however does not optimize the energy consumption. Our goal is to add constraints and objectives to generate large idle periods to put the processor in low-power states. This is the contribution of this work in the next section.

IV. ALGORITHM

This section introduces the detailed algorithm used to obtain the weights of jobs in a hyper-period such that it generates large idle periods. The name of the algorithm is LPDPM, as in Linear Programming DPM.

A. Motivation

We assume that processors can switch to a low-power state on every idle period (i.e. BET = 0) and that tasks always use their worst case execution time. Thus, regardless of the scheduler used, the processors utilization is constant over a Fig. 2. Global-EDF schedule hyper-period. Thus to evaluate the DPM power efficiency of a scheduling algorithm, the number of idle periods generated can be used, the less the better as: 1) the number of wake up transitions from a low-power state (and therefore of the associated penalties) is reduced and 2) the duration of idle periods increases allowing the use of deeper low-power states. Depending on the length of the idle period, the most efficient low-power state fulfilling the transition delay can be selected.

Figure 2 pictures the schedule on a two processors system of a task set composed of three tasks (with WCET and period of (3,8), (6, 10) and (4,16)) with Global-EDF. This example demonstrates that classical schedulers like Global-EDF are not suitable for DPM. They generate more idle periods than necessary.

B. Approach

During a hyper-period, one or more idle periods are generated and one or more processors switch to a low-power state. The objective is to have as few idle periods as possible. To address this problem, we choose to modelize the idle time with an additional task τ ′ . τ ′ is a periodic task with a period equals to H and a utilization equals to m -U . τ ′ thus only has one job in a hyper-period. Note that this operation is feasible only because m -1 < U < m as the utilization of τ ′ must be less than 1. The new task set has a global utilization of m and is therefore schedulable.

Getting as few idle periods as possible is now equivalent to decreasing the number of preemptions of τ ′ inside the hyper-period. This objective should now be added to the linear equation system.

However, it should be noted that τ ′ does not represent the actual idle time when tasks are executed. Indeed, tasks usually do not use all their worst case execution time. Thus, at run-time, processors can be idle while not executing τ ′ and multiple processors can be idle simultaneously. Modelizing the expected idle time with τ ′ is just a way to help generating a schedule with guaranteed idle periods in the worst case scenario.

C. Objectives

As stated in the last section, the hyper-period is divided into multiple intervals. An interval in which the weight of τ ′ is 1 is called an idle interval. And an interval in which the weight of τ ′ is 0 is called a busy interval.

In order to generate as few preemptions as possible, an interval should be either an idle or a busy interval and similar intervals (busy or idle) should be consecutive. Say differently, the weight of τ ′ on every interval should be either 1 or 0, and similar intervals where the weight of τ ′ is identical should be consecutive. Intervals where the weight of τ ′ is strictly between 0 and 1 are the less attractive because they include a preemption. To simplify, the weight of τ ′ on interval k is written w k . The objectives can be summarized as:

• w k should be either 1 or 0 • Intervals where w k = 1 should be consecutive • Intervals where w k = 0 should be consecutive However, it may be unavoidable to generate non-busy/idle intervals, that is where the weight of τ ′ would be neither 1 nor 0.

D. Formalization

Objectives should now be written as linear equations in order to use them in our linear equation system. As defined in the last paragraph, the first objective is to obtain as many intervals as possible where the weight of τ ′ is one, that is idle intervals. In terms of linear programming, expressing this constraint requires adding a new variable to express the nonavailable floor function. Let f k be a binary variable such that:

f k = 1 if w k = 1 0 else (5)
This equation can be linearized as:

w k + f k ≥ 1 (6)
Such that minimizing f k forces w k to be equal to 1. The objective is therefore to minimize the sum of all f k in order to obtain a maximum number of idle intervals, that is with w k equal to 1.

The second objective is to obtain periods where w k is zero, that is busy intervals. Like f k , let e k be a binary variable such that:

w k -e k ≤ 0 (7)
And having for objective to minimize the sum of all e k will increase the number of busy intervals.

The next goal is to make idle or busy intervals consecutive. Let f c k and ec k be two binary variables such that:

f c k = 1 if f k = 1 and f k+1 = 0 0 else ( 8
)
ec k = 1 if e k = 1 and e k+1 = 0 0 else (9)
Those two equations can be modelized as:

         f k -f k+1 -f c k ≤ 0 -f k + f c k ≤ 0 f k+1 + f c k ≤ 1 -f c k ≤ 0 (10)
         e k -e k+1 -ec k ≤ 0 -e k + ec k ≤ 0 e k+1 + ec k ≤ 1 -ec k ≤ 0 (11)
Minimizing the sum of all f c k and the sum of all ec k is then going to make idle or busy intervals consecutives. Therefore, the final objective is (subject to equation ( 2), ( 3), ( 4), ( 6), ( 7), ( 10) and ( 11)):

Minimize k f k + e k + f c k + ec k (12)

E. Scheduling inside an interval

Resolving the linear system gives a weight for each task on every interval such that the number of idle periods is minimized. It outputs a solution that satisfies the linear system which however may not be the optimal solution. To schedule tasks inside intervals, EDZL [START_REF] Wei | Current results on edzl scheduling for multiprocessor real-time systems[END_REF] or IZL [START_REF] Megel | Minimizing task preemptions and migrations in multiprocessor optimal real-time schedules[END_REF] can be used.

Unfortunately, as explained previously, the solver can generate intervals where the weight of τ ′ is neither 1 nor 0 (nonidle/busy intervals). Those intervals where 0 < w k < 1 are the only intervals where the on-line scheduler should be careful not to generate additional idle periods if possible. In particular, an additional idle period should be merged with a previous idle period to save transition delays. To solve this problem, we choose to schedule τ ′ at the beginning or at the end of the interval to stick the execution of τ ′ in the current interval to the one in the previous or next interval.

Moreover, to share the load between processors, the processor executing τ ′ can be changed when τ ′ is preempted. It does not increase the number of idle periods and could be an interesting way, in a future work, to handle thermal impact of our solution on the energy consumption.

Figure 3 pictures the schedule of the task set from subsection IV-B with LPDPM. Where Global-EDF was generating 9 short idle periods, LPDPM creates 2 much larger idle periods.

V. EVALUATION

In order to compare our solution with existing algorithms, we conducted a simulation-based experimental study using the energy information of the STM32L boards, which are based on the ARM Cortex-M3 processor [START_REF]STM32L151xx and STM32L152xx advanced ARMbased 32-bit MCUs[END_REF]. It has four low-power states described in table I. Using a simulator, we generated random task sets and scheduled them on two hyper-periods with several schedulers. This simulation was conducted with 4 processors and each task set has 10 tasks. Task utilizations are computed randomly between 0.01 and 0.99 with a uniform distribution using the well-known UUniFast algorithm from Bini et Buttazzo [START_REF] Bini | Biasing effects in schedulability measures[END_REF]. The period of each task is also chosen randomly between 10 and 100. 2000 task sets were generated for each global utilization. Then, each task set was scheduled by the following schedulers: RUN [START_REF] Regnier | Run: Optimal multiprocessor real-time scheduling via reduction to uniprocessor[END_REF], U-EDF [START_REF] Nelissen | Reducing preemptions and migrations in real-time multiprocessor scheduling algorithms by releasing the fairness[END_REF] and LPDPM. RUN and U-EDF are two optimal multiprocessor scheduling algorithms aiming to reduce the number of preemptions and migrations. The implementation of LPDPM uses IBM ILOG CPLEX to solve the linear problem. We limited the solving time to 60 seconds and we rejected the task set when a solution was not found. The mean number of idle periods is plotted on figure 4 for each global utilization. Figure 5 gives the repartition of the idle periods lengths for each scheduler. Those figures illustrate the fact that LPDPM generates less and larger idle periods. For example, all idle periods created by the other algorithms have a length less then 120 while LPDPM can generate idle periods with a length up to 240. Note that the ordinate is plotted on a logarithmic scale in figure 5. Figure 6 gives the relative consumption of other schedulers, the consumption of LPDPM being always one. The consumption is computed based on the values from table I. LPDPM is always more energy efficient and the difference is of course reduced when the global utilization increases.

Finally, figure 7 pictures the number of preemptions for each scheduler. Even if RUN and U-EDF are two algorithms specifically designed to reduce the number of preemptions, LPDPM behaves as well as U-EDF and only less than 1.5 worse than RUN. This makes LPDPM viable. Improving the linear problem to decrease the number of preemptions of the regular tasks is left for future works.

VI. CONCLUSION

In this paper we introduced LPDPM, an off-line poweraware scheduling algorithm for multiprocessor real-time systems. It focuses only on static energy consumption. The algorithm tries to increase the duration of the idle periods such that deeper low-power states can be activated. It introduces an additional task accounting for the time where processors are expected to be idle. It then decreases the number of preemptions of this task.

Contrary to other DVFS or DPM algorithms, LPDPM uses an off-line approach. Another difference is that LPDPM does not consist in mapping task to priorities in order to schedule the system. It assigns weights to tasks on intervals where each interval is delimited by two task releases. Linear programming is used to get all the weights. With this approach, constraints and objectives can be formally expressed. The constraint is to meet deadlines. The objective is to decrease the number of preemptions of the idle task. Simulations show that LPDPM significantly decreases the number of idle periods and is therefore more energy efficient than existing algorithms. The of LPDPM is to minimize the number of idle periods. And then, based on the length of the idle period, a low-power state can be selected. Thus the linear equation system does not depend on the processors used. However, the assumption that minimizing the number of idle periods is always more energy efficient can be false with some processors. Therefore, we plan to relax this assumption in future works.

At run-time, if the actual execution time of tasks is lower than their WCET, the duration of idle periods increases. It could potentially allow the use of deeper low-power states. Therefore, an on-line algorithm should be able to use the unused computation time to increase the length of existing idle periods, following the same idea as Seo et al. [START_REF] Seo | Energy efficient scheduling of real-time tasks on multicore processors[END_REF]. At present, LPDPM only works for periodic tasks with implicit deadlines. We plan to extend our approach to schedule sporadic tasks with constrained deadlines.

Energy consumption depends on the temperature. Using LPDPM, the idle processor used for each new idle period can be changed to share the load and decrease the temperature of processors. But future works should modelize thermal impacts on energy consumption such that LPDPM could generate thermal-aware schedules.

Fig. 1 .w 2 , 2 * |I 2 | w 3 , 3 * |I 3 | 4 8 w 4 , 1 *

 122233841 Fig. 1. An example of 2 tasks with periods of 4 and 12 respectively

Fig. 3 .

 3 Fig. 3. LPDPM schedule

Fig. 4 .

 4 Fig. 4. Mean number of idle periods

Fig. 5 .Fig. 6 .

 56 Fig. 5. Distribution of idle periods lengths

Fig. 7 .

 7 Fig. 7. Mean number of preemptions

ACKNOWLEDGEMENT

The authors would like to thank Vincent David for his remarks in the early stages of this work.