Antoine Miné
email: mine@di.ens.fr

Static Analysis by Abstract Interpretation of Sequential and Multithreaded Programs

In the realm of embedded critical systems, it is crucial to guarantee the correctness of programs before they are deployed. Static analyzers can help by detecting at compile-time potentially erroneous program behaviors: they perform sound over-approximations to achieve an efficient analysis while not missing any potential behavior. We discuss the systematic design of such analyzers using abstract interpretation, a general theory of semantic approximation. After recalling the classic construction of static analyzers for sequential programs by abstraction of the concrete trace semantics, we introduce abstractions to derive threadmodular analyzers for multithreaded programs, borrowing ideas from rely/guarantee proof methods. Finally, we present two static analyzer tools, Astrée and AstréeA, that are used to check for run-time errors in large sequential and multithreaded embedded industrial avionic C applications.

Introduction

It is crucial to guarantee the correctness of programs before they are deployed, especially in the realm of embedded critical systems, where software cannot be corrected during missions and a single mistake can have dramatic consequences. Testing, the most widespread verification method employed in industry, is very efficient at catching errors, but it is costly and cannot, for efficiency reasons, test all executions. Hence, testing can miss errors. This is especially true for parallel and multithreaded programs: the huge number of possible thread interleavings causes a combinatorial explosion of executions, while some errors only appear in a tiny fraction of them (such as data-races). Formal methods, on the other hand, can provide rigorous guarantees that all the executions are correct.

We consider here static analyses, able to inspect program sources in order to find defects. We only consider semantic analyses, that are based on a mathematical notion of program behaviors, as opposed to syntax-based style checkers.

Unlike proof methods, which require the user to provide annotations, these analyses run on the original, unannotated source without human intervention. Full automation and efficiency imply that such analyses are approximated. We impose soundness: unlike testing, program behaviors are over-approximated so that, if an error is present, it will be detected. However, the analysis can report spurious errors. Sound static analyzers have been used for decades in applications, such as program optimization, where precision is not critical. Recent progress had lead to the design of tools able to check for simple but important safety properties (such as the absence of run-time error) with few or zero false alarms. We participated in the design of two of them [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF]: Astrée, an industrial-strength analyzer that checks for run-time errors in synchronous embedded C code, and AstréeA, its prototype extension targeting multithreaded embedded C applications.

These analyzers are based on abstract interpretation, which is a general theory of program semantics introduced by Cousot and Cousot in the late '70s [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Abstract interpretation stems from the observation that many semantics can be uniformly expressed as fixpoints of operators, after which seemingly unrelated semantics can be compared. It expresses formally the fact that some semantics are more abstract than (lose information with respect to) others as they compute approximations in less rich domains of properties. It provides tools to prove soundness: any property proved in an abstract semantic is still true in the concrete one. Finally, it provides tools to design and combine abstractions.

The aim of the article is to give a short overview of the theory underlying tools such as Astrée and AstréeA. Section 2 focuses on sequential programs and presents the classic construction of an effective analyzer by abstraction of the most concrete semantics of a program: its execution traces. Section 3 considers multithreaded programs and explains how, borrowing ideas from rely/guarantee proof methods [START_REF] Jones | Development Methods for Computer Programs including a Notion of Interference[END_REF], an efficient, thread-modular analysis can be constructed. Section 4 briefly presents the Astrée and AstréeA analyzers, and Sec. 5 concludes.

The modest contribution of this article is the formulation, in Sec. 3.4, of Jones' rely/guarantee method [START_REF] Jones | Development Methods for Computer Programs including a Notion of Interference[END_REF] in abstract interpretation form, as an abstraction of the execution traces of multithreaded programs by decomposition into intra-thread invariants and inter-thread interferences. This extends previous work in the 80's [START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF] that formalized earlier Owicki-Gries-Lamport methods [START_REF] Owicki | An axiomatic technique for parallel programs I[END_REF][START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF] as abstract interpretation. It also extends our recent previous work [START_REF] Miné | Static analysis of run-time errors in embedded real-time parallel C programs[END_REF], that only considered coarse abstract interferences, by exhibiting an intermediate layer of abstraction from which it can be recovered.

Abstractions for Sequential Programs

As a short introduction to abstract interpretation concepts, we review the formal construction of a static analyzer for sequential programs by abstraction of its trace semantics -see also [2, § II] for an extended introduction.

at (1):

i = 0 ∧ n = 0 at (2): i = 2 ∧ n = 0 at (3): 2 ≤ i ≤ max(2, n) at (4): 2 ≤ i ≤ n -1 ∧ n ≥ 3 at (5): 2 ≤ i ≤ n ∧ n ≥ 3 at (6): i = max(2, n) (a) (b)
Fig. 1. A simple sequential program (a), and invariant assertions (b).

Transition Systems

The semantics of a program is defined classically [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] in a very general way in small step operational form, as a transition system: (Σ, τ, I), where Σ is a set of states, I ⊆ Σ is the subset of initial states, and τ ⊆ Σ ×Σ is a transition relation. For sequential programs, the state set is defined as

Σ def = L × M,
where each state σ = ( , m) has a control part ∈ L denoting the current program point, and a memory part

m ∈ M def = V → V mapping program variables V ∈ V to values v ∈ V.
A transition models an atomic execution step, such as executing a machine-code instruction in a program. We denote by ( , m) → ( , m ) the fact that (( , m), ( , m )) ∈ τ , i.e, the program can reach the state ( , m ) from the state ( , m) after one execution step. The transition system derives mechanically from the program code itself, e.g., from the sequence of binary instructions or, more conveniently, by induction on the syntax tree of the source code. where and e denote respectively syntactic program points and expressions. The transition system τ [ P ] is derived by induction on the syntax of P as follows:

τ [ x := e ] def = { ( , m) → ( , m[x → v]) | m ∈ M, e m v } τ [ if e then P ] def = { ( , m) → ( , m) | m ∈ M, e m true } ∪ τ [ P ] ∪ { ( , m) → ( , m) | m ∈ M, e m false } τ [ while e do P ] def = { ( , m) → ( , m) | m ∈ M, e m true } ∪ τ [ P ] ∪ { ( , m) → ( , m) | m ∈ M, e m false } τ [ P ; P ] def = τ [ P ] ∪ τ [ P ]
where m[x → v] denotes the function mapping x to v and y = x to m(y), and e m v states that e can evaluate to the value v in the memory m.

Trace Semantics

We are not interested in the program itself, but in the properties of its executions. Formally, an execution trace is a finite sequence of states such that σ 0 ∈ I and ∀i, (σ i , σ i+1 ) ∈ τ . The semantics we want to observe, which is called a collecting semantics, is thus defined in our case as the set T ∈ P(Σ * ) of traces spawned by the program. It can be expressed [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF] as the least fixpoint of a continuous operator in the complete lattice of sets of traces:

σ 0 → σ 1 → • • • → σ n n i ... n i ... n i (a) (b) (c)
T = lfp F where F (X) def = I ∪ { σ 0 → • • • → σ i+1 | σ 0 → • • • → σ i ∈ X ∧ σ i → σ i+1 } (1)
i.e., T is the smallest set containing traces reduced to an initial state and closed under the extension of traces by an additional execution step. Note that we are observing partial execution traces; informally, we allow executions to be interrupted prematurely; formally, T is closed by prefix (it also includes the finite prefixes of non-terminating executions). This is sufficient if we are interested in safety properties, i.e., properties of the form "no bad state is ever encountered," which is the case here -more general trace semantics, able to also reason about liveness properties, are discussed for instance in [START_REF] Cousot | Constructive design of a hierarchy of semantics of a transition system by abstract interpretation[END_REF]. A classic result [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF] is that T can be restated as the limit of an iteration sequence: T = n∈N F n (∅). It becomes clear then that computing T is equivalent to testing the program on all possible executions (albeit with an unusual exhaustive breadth-first strategy) and that it is not adapted to the effective and efficient verification of programs: when the program has unbounded or infinite executions, T is infinite.

Example 2. The simple program in Fig. 1.a increments i in a loop, until it reaches a user-specified value n. Figure 2.a presents its trace semantics starting in the state set

I = { (1, [m → 0, i → 0]) }.
The program has infinite executions (e.g., if i is never incremented).

State Semantics

We observe that, in order to prove safety properties, it is not necessary to compute T exactly. It is sufficient to collect the set S ∈ P(Σ) of program states encountered, abstracting away any information available in T on the ordering of states. We use an abstraction function α state : P(Σ * ) → P(Σ):

S = α state (T ) where α state (X) def = { σ | ∃σ 0 → • • • → σ n ∈ X, i ∈ [0; n], σ = σ i } (2
) An important result is that, as T , S can be computed directly as a fixpoint:

S = lfp G where G(X) def = I ∪ { σ | ∃σ ∈ X, σ → σ }
or, equivalently, as an iteration sequence S = n∈N G n (∅), which naturally expresses that S is the set of states reachable from I after zero, one, or more transitions. The similarity in fixpoint characterisation of S and T is not a coincidence, but a general result of abstract interpretation (although, in most cases, the abstract fixpoint only over-approximates the concrete one: lfp G ⊇ α state (lfp F ), see [START_REF] Cousot | Constructive design of a hierarchy of semantics of a transition system by abstract interpretation[END_REF]). Dually, given a set of states S, one can construct the set of traces abstracted by S using a concretization function

γ state def = λS . { σ 0 → • • • → σ n | n ∈ N ∧ ∀i ∈ [0; n], σ i ∈ S }.
The pair (α state , γ state ) forms a Galois connection.1 A classic result [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] states that the best abstraction of F can be defined as α state • F • γ state , which in our case turns out to be exactly G. When the set of states is finite (e.g., when the memory is bounded), S can always be computed by iteration in finite time, even if T cannot. Obviously, S may be extremely large and require many iterations to stabilize, hence computing S exactly is not a practical solution; we will need further abstractions.

Program Proofs and Inductive Invariants

There is a deep connection [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] between the state semantics and the program logic of Floyd-Hoare [START_REF] Hoare | An axiomatic basis for computer programming[END_REF] used to prove partial correctness. If we interpret each logic assertion A at program point as the set of memory states A ⊆ M satisfying it, and note

M def = { ( , m) | m ∈ A }, then (A ) ∈L
is a valid (i.e., inductive) invariant assertion if and only if G(M ) ⊆ M . Moreover, the best inductive invariant assertion stems from lfp G, i.e., it is S. While, in proof methods, the inductive invariants must be devised by an oracle (the user), abstract interpretation opens the way to automatic invariant inference by providing a constructive view on invariants (through iteration) and allowing further abstractions.

Example 3. The optimal invariant assertions of the program in Fig. 1.a appear in Fig. 1.b, and Fig. 2.b presents graphically its state abstraction at point (3).

Memory Abstractions

In order gain in efficiency on bounded state spaces and handle unbounded ones, we need to abstract further. As many errors (such as overflows and divisions by zero) are caused by invalid arguments of operators, a natural idea is to observe only the set of values each variable can take at each program point. Instead of concrete state sets in P(Σ)

def = P(L×(V → V)), we manipulate abstract states in Σ C def = (L × V) → P(V).
The concrete and abstract domains are linked through the following Galois connection (so-called Cartesian Galois connection):

α cart (X) def = λ( , V ) . { v | ∃( , m) ∈ X, m(V ) = v } γ cart (X ) def = { ( , m) | ∀V, m(V ) ∈ X ( , V ) } (3)
Assuming that variables are integers or reals, a further abstraction consists in maintaining, for each variable, its bounds instead of all its possible values. We compose the connection (α cart , γ cart ) with (the element-wise lifting of) the following connection (α itv , γ itv ) between

P(R) and (R ∪ { -∞ }) × (R ∪ { + ∞ }): α itv (X) def = [min X; max X] γ itv ([a; b]) def = { x ∈ R | a ≤ x ≤ b } (4)
yielding the interval abstract domain [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF].

Another example of memory domain is the linear inequality domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] that abstracts sets of points in P(V → R) into convex, closed polyhedra. One abstracts P(Σ) L → P(V → V) by associating a polyhedron to each program point, which permits the inference of linear relations between variables. The polyhedra domain is thus a relational domain, unlike the domains deriving from the Cartesian abstraction (such as intervals). Following the same method that derived the state semantics from the trace one, we can derive an interval semantics from the state one: it is expressed as a fixpoint lfp G of an interval abstraction G of G. While it is possible to define an optimal G as α • G • γ -where (α, γ) combines (α itv , γ itv ) and (α cart , γ cart ) -this is a complex process when G is large, and it must be performed for each G, i.e., for each program. To construct a general analyzer, we use the fact that F , and so, G = α state • F • γ state , are built by combining operators for atomic language constructs, as in Ex. 1. It is thus possible to derive G as a combination of a small fixed set of abstract operators. More precisely, we only have to design abstraction versions of assignments, tests, and set union ∪. Generally, the combination of optimal operators is not optimal, and so, the resulting G is not optimal -e.g., (α

• G 1 • G 2 • γ)(X) ((α • G 1 • γ) • (α • G 2 • γ))(X).
Additionally, due to efficiency and practicality concerns, the base abstract operators may be chosen non-optimal to begin with. Achieving a sound analysis, i.e., γ(lfp G ) ⊇ lfp G, only requires sound abstracts operators, i.e., ∀X , (γ

• G )(X ) ⊇ (G • γ)(X ). The fact that G = α • G • γ,
and even the existence of an α function, while sometimes desirable, is by no mean requiredfor instance, the polyhedra domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] does not feature an abstraction function α as some sets, such as discs, have no best polyhedral abstraction.

Example 5. The interval abstraction x := y + z of a simple addition maps the interval environment

[x → [l x ; h x ]; y → [l y ; h y ]; z → [l z ; h z ]] at point to [x → [l y + l z ; h y + h z ]; y → [l y ; h y ]; z → [l z ; h z ]] at point , which is optimal.
Example 6. The optimal abstraction y := -z; x := y + z would map x to [0; 0]. However, the combination y := -z • x := y + z maps x to [l z -h z ; h z -l z ] instead, which is coarser when l z < h z .

Example 7. We can design a sound non-optimal fall-back abstraction for arbitrary assignments x := e by simply mapping x to [-∞; +∞].

We now know how to define systematically a sound abstract operator G which can be efficiently computed. Nevertheless, the computation of lfp G by naive iteration may not converge fast enough (or at all). Hence, abstract domains are generally equipped with a convergence acceleration binary operator , called widening and introduced in [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Widenings extrapolate between two successive iterates and ensure that any sequence X i+1 def = X i G (X i ) converges in finite time, possibly towards a coarse abstraction of the actual fixpoint.

Example 8. The classic interval widening [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] sets unstable bounds to infinity:

[l 1 ; h 1 ] [l 2 ; h 2 ] def = -∞ if l 2 < l 1 l 1 otherwise ; +∞ if h 2 > h 1 h 1 otherwise (5)
When analyzing Fig. 1, the iterations with widening at (3) give the following intervals for i: i 0 = [2; 2] and i 1 = [2; 2] [2; 3] = [2; +∞], which is stable.

To balance the accumulation of imprecision caused by widenings and combining separately abstracted operators, it is often necessary to reason on an abstract domain strictly more expressive than the properties we want to prove -e.g., the polyhedra domain may be necessary to infer variable bounds that the interval domain cannot infer, although it can represent them, such as x = 0 in Ex. 6.

Further Considerations

We end this introduction with some pointers to additional material. Firstly, there exists a large library of abstract domains, in particular numeric ones, and associated operators with various precision versus cost trade-offs - [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF] describes a few of them. An actual analyzer will use a combination, such as a reduced product, of many domains [START_REF] Cousot | Combination of abstractions in the Astrée static analyzer[END_REF]. Secondly, we have assumed for simplicity that the set of variables V is finite, but abstract domains able to handle an unbounded memory exist; this is necessary when dynamic memory allocation is used. They often combine abstractions of the memory shape and of the contents of numeric fields, as in [START_REF] Venet | Nonuniform alias analysis of recursive data structures and arrays[END_REF]. Likewise, an efficient handling of procedures requires abstracting the control state L (which can be large, or even unbounded in the case of recursivity). Call-string methods [START_REF] Sharir | Two approaches to interprocedural data flow analysis[END_REF] are an instance of such abstractions. Finally, alternate iteration techniques exist [START_REF] Bourdoncle | Efficient chaotic iteration strategies with widenings[END_REF], as well as methods to decompose the global fixpoint into several local ones to achieve a modular analysis [START_REF] Cousot | Compositional separate modular static analysis of programs by abstract interpretation[END_REF].

We now consider multithreaded programs in a shared memory. We show how, starting from a classic concrete semantics based on interleaved executions [START_REF] Cousot | Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles[END_REF] and applying abstract interpretation, we can construct an effective thread-modular static analysis which is similar to rely/guarantee proof methods [START_REF] Jones | Development Methods for Computer Programs including a Notion of Interference[END_REF].

Labelled Transition Systems

We assume a finite set T of threads. Each thread t ∈ T has its own control space L t and transition relation τ t ⊆ Σ t ×Σ t , where Σ t def = L t ×M. The state space and transitions for the whole program are derived from those of individual threads as follows. Program states live in Σ def = ( t∈T { t } → L t )×M, i.e., each thread has its own control point, but the memory is shared. The semantics of the program is defined as a labelled transition system (Σ, τ, I), where the transition relation

τ ⊆ Σ × T × Σ is defined as: 2 (( ¯ , m), t, ( ¯ , m )) ∈ τ if (( ¯ [t], m), ( ¯ [t], m)) ∈ τ t and ∀t = t, ¯ [t ] = ¯ [t ]
. It states that an execution step of the program is an execution step of some thread and updates only that thread's control location. We denote such a step as ( ¯ , m) t → ( ¯ , m ). Labels t ∈ T are used to explicitly remember which thread caused each transition.

Interleaved Trace Semantics

As for sequential programs, we consider finite prefixes of executions and ignore liveness properties -in the context of parallel programs, liveness properties are related to fairness conditions, which is a very complex issue not discussed here; see [START_REF] Cousot | Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles[END_REF] for a complete treatment. The trace semantics T is defined as in (1):

T = lfp F where F (X) def = I ∪ { σ 0 t0 → • • • ti → σ i+1 | σ 0 t0 → • • • ti-1 → σ i ∈ X ∧ σ i ti → σ i+1 } (6)
which thus corresponds to executions consisting of arbitrary interleavings of transitions from any threads. Given the similarity with the sequential trace semantics, a natural idea to analyze a parallel program is to forget about labels and apply the state and memory abstractions (Secs. 2.3, 2.5). The problem with this method is the huge number of control states to consider: t∈T |L t | instead of |L|. Moreover, τ is much larger that t∈T τ t as a single transition in τ t is repeated for each possible control state of other threads t =t L t . As a consequence, constructing an abstraction G of F from abstractions of atomic instructions requires a combination of many more such functions than for sequential programs. This makes even coarse Cartesian interval abstractions impracticable.

(1) while true do (5) while true do at (1),( 2),( 4): x ≤ y (2) if x < y then (6) if y < 10 then at (3):

x < y (3)

x := x + 1;

(7) y := y + 1; at (5),( 6),( 8): y ≤ 10 (4) done; (1) while true do (5) while true do at (1),( 2),( 4): x ∈ { -2, 0 } (2)

x := x + 1;

x := x -2; at (3):

x ∈ { -1, 1 } (3) x := x -1; (7)
x := x + 2; at (5),( 6),( 8): x ∈ { 0, 1 } (4) done;

(8) done; at (7):

x ∈ { -2, -1 } (a) (b)
Fig. 4. A program requiring flow-sensitivity (a), and its invariant assertions (b).

Rely/Guarantee

Proof methods for parallel programs, such as Owicki-Gries-Lamport [START_REF] Owicki | An axiomatic technique for parallel programs I[END_REF][START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF] and rely/guarantee [START_REF] Jones | Development Methods for Computer Programs including a Notion of Interference[END_REF] solve this issue by attaching invariants to thread control points in t∈T L t instead of combinations of thread points in t∈T L t . The price to pay is a refined notion of invariance: the properties attached to a thread t must also be proved stable by the effect of the other threads t = t. In rely/guarantee methods, this effect is explicitly provided as extra annotations in t that are assumed to hold (relied on) when checking the invariants for t and proved correct (guaranteed) when checking the other threads t = t. It then becomes possible to check each thread in a modular way, i.e., without looking at the code of the other threads, relying on the annotations instead.

Example 9. Figure 3 presents a program with two threads: the first one increments x up to y and the second one increments y up to 10. For conciseness, we exemplify the rely/guarantee conditions at a single program point. Consider the problem of proving that x < y holds at (3), just after the test. We need to prove that the assertion is stable by the action of the second thread. It is sufficient to rely on the fact that the second thread does not modify x and only increments y. This property is, in turn, guaranteed by analyzing the second thread, relying only on the fact that the first thread does not modify y.

Interference Semantics

We now rephrase the idea of rely/guarantee methods as an abstract interpretation of the interleaved trace semantics T (6). We decompose the trace semantics using two complementary abstractions: an abstraction into thread-local invariants (which is inspired from the formalization in [START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF] of Owicki-Gries-Lamport methods [START_REF] Owicki | An axiomatic technique for parallel programs I[END_REF][START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF] as an abstract interpretation) and an abstraction into interthread interferences (which is new). Firstly, the local invariant S[t] of a thread t is defined by projecting, with the bijection π t , the reachable states α state (T ) (2) on t's control state L t :

S[t] def = (Π t • α state )(T ) where Π t (X) def = { π t (x) | x ∈ X } and π t ( ¯ , m) def = ( ¯ [t], m[∀t = t, p t → ¯ [t ]]) (7)
We keep the control state ¯ [t ] of other threads t = t encoded as extra variables p t in the memory (called auxiliary variables in Owicki-Gries [START_REF] Owicki | An axiomatic technique for parallel programs I[END_REF]). It is possible to remove these variables and keep only t's control information to get:

α ctrl t ( S[t]) where α ctrl t (X) def = { ( , m) | ∃ ¯ , π t ( ¯ , m) ∈ X ∧ ¯ [t] = } (8)
but α ctrl t is known to be an incomplete abstraction: some invariance properties on S[t] cannot be proved using α ctrl t ( S[t]) only (see Ex. 12). Secondly, the interference Ā[t] of a thread t is defined as the possible actions it has on other threads, as observed in the interleaved trace semantics T :

Ā[t] def = { (σ i , σ i+1 ) | ∃σ 0 t0 → • • • tn-1 → σ n ∈ T, t i = t } (9)
Interferences are actually subsets of the transition relation restricted to those transitions appearing in actual traces starting in I. We can then express S[t] in fixpoint form as a function of Ā and the transitions caused by thread t:

S[t] = lfp G t ( Ā)
where

G t ( Ȳ )(X) def = Π t (I) ∪ { π t (σ ) | ∃π t (σ) ∈ X, σ t → σ ∨ ∃t = t, (σ, σ ) ∈ Ȳ [t ] } (10)
i.e., to reach a new program state from a known one, we either execute a step from thread t (in t →) or a step from another thread (in Ā[t ]). Moreover, we can express directly Ā as a function of S:

Ā[t] = B( S)[t] where B( Ȳ )[t] def = { (σ, σ ) | π t (σ) ∈ Ȳ [t] ∧ σ t → σ } (11)
which expresses that Ā[t] corresponds to the transitions in τ t starting from a reachable state. This yields the following nested fixpoint characterisation of S:

S = lfp H where H( X)[t] def = lfp G t ( B( X)) (12)
which can be computed in iterative form as:

S = ¯ n∈N Hn ( ∅) while H( X)[t] = n∈N (G t ( B( X))) n (∅)
. The benefit of this characterization is that the computation of H( X)[t] only depends on its argument X and the transition relation of the thread t, not on the transition relations of the other threads: the inner fixpoint is thus similar to the analysis of a sequential process. However, as analyzing a thread in a given set of interferences B( X) gathers a new, larger set of interferences B( H( X)), the analysis must be performed again with this enriched set until it becomes stable. This is the role of the outer fixpoint.

Memory and Interference Abstractions

Our interference semantic S is very concrete (the state semantics α state (T ) can be recovered fully from it), and too large to be computed directly. An effective and efficient analyzer can be designed by applying abstractions independently to local invariants and to interferences, while keeping the nested fixpoint form of [START_REF] Feret | Static analysis of digital filters[END_REF]. Firstly, any memory abstraction, such as intervals (4) or polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], can be applied directly to each local invariant S[t]. As the number of variables is often a critical parameter in the efficiency of abstract domains, a faster but coarser analysis can be achieved by removing the auxiliary variables from S[t] with α ctrl t (8) prior to memory abstraction. Secondly, we abstract interferences Ā[t]. For instance, it is possible to forget the control state of all threads using a flow-insensitive abstraction α flow :

α flow (X) def = { (m, m ) | ∃ ¯ , ¯ , (( ¯ , m), ( ¯ , m )) ∈ X }
Intuitively, this means that, when analyzing a thread t, we consider that any instruction from any thread t = t may be executed at any point of thread t. Then, by noting that P((V → V)×(V → V)) P(({ 1, 2 }×V) → V), we can see a set of pairs of maps on V as a set of maps on { 1, 2 } × V, with twice as many variables; hence, we can apply any memory abstraction to α flow (X). Another solution consists in abstracting the relation α flow (X) with its image, using the following abstraction α img , before applying a memory abstraction:

α img (X) def = { m | ∃m, (m, m ) ∈ X }
which is coarser but more efficient as it avoids doubling the number of variables. By combining α flow , α img , and α cart (3), we abstract thread interferences in a non-relational and flow-insensitive way, as the set of values each thread can store into each variable during the thread execution. Further abstractions, such as intervals α itv (4), can be applied. This yields an efficient analysis: the abstract interference is simply a global map from T × V to intervals, and we can build an abstraction H ( X )[t] of H( X)[t] by combining abstractions for each instruction of thread t (as Ex. 5 but slight modified to take interferences into account). Example 11. We analyze Fig. 3 using intervals, by applying α ctrl t , α cart , and α itv to local invariants, and α flow , α img , α cart , and α itv to interferences. We find that, at (3), x ∈ [0; 9]. The information that x < y is lost. The second thread produces the abstract interferences [x → ∅, y → [0; 10]], i.e., we infer that it cannot modify x and can only put values from [0; 10] into y. We lose the information that y can only increase.

Example 12. Consider the program in Fig. 4. When analyzing the first thread, we note that, at (2), x can be 0 or -2, depending on whether the second thread is at [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF] or [START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF]. Moreover, to prove that x stays in { -2, 0 } at (2), it is necessary to infer that the interference from the second thread can only increment x when it is at [START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF], and decrement it when it is at [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF]. A flow-insensitive abstraction using α ctrl t and α flow would instead infer that x can be incremented arbitrarily and decremented arbitrarily. It would not allow us to prove that x is bounded.

Further Considerations

A practical consequence of ( 12) is that a thread-modular static analyzer can be designed by slightly modifying a sequential analyzer: all we need to do is keep track of (abstract) interferences as well as reachable states, and add an external fixpoint iteration to re-analyze each thread until the inferred interferences stabilize. As for memory abstractions, there are many choices in how to abstract interferences, with various cost versus precision trade-offs and various levels of expressiveness. Although we presented only flow-insensitive non-relational abstract interferences, we can envision abstractions keeping (at least partially) flow and relational information. This is in contrast to our earlier formalization [START_REF] Miné | Static analysis of run-time errors in embedded real-time parallel C programs[END_REF] which only allowed flow-insensitive non-relational interferences, and can now be seen a special case of the framework presented here. In the presence of mutual exclusion primitives and scheduling policies that restrict the interleaving of threads (such as thread priorities), a model of the scheduler can be incorporated into the semantics to refine the notion of interference. For instance [START_REF] Miné | Static analysis of run-time errors in embedded real-time parallel C programs[END_REF] handles locks by partitioning flow-insensitive, non-relational abstract interferences with respect to the set of locks each thread holds. Another remark is that the interleaved trace semantics (6) is not realistic in the context of modern multicore architectures and compilers; non-coherent caches and optimizations can expose extra behaviors. However, we proved in [START_REF] Miné | Static analysis of run-time errors in embedded real-time parallel C programs[END_REF] that, provided that a flow-insensitive abstraction of interferences is used, the abstract semantics is sound even in the presence of weakly consistent memory models, so that the results of the static analysis can still be trusted in realistic settings. Finally, we did not discuss the case of an unbounded number of threads, which requires further abstraction.

Applications

We now briefly describe two static analysis tools that were designed at the École normale supérieure using abstract interpretation principles.

Astrée

Astrée is a static analyzer that checks for run-time errors in synchronous (hence sequential) embedded critical C programs. It covers the full C language, including pointers and floats, but excluding dynamic memory allocation and recursivity (forbidden in the realm of critical software). It checks for arithmetic overflows, and invalid arithmetic and memory operations. It is sound, and so, never misses any existing error. Due to over-approximations, it can signal false alarms. Although Astrée can analyze many kinds of codes, it is specialized to control-command avionic software, on which it aims at efficiency and certification, i.e., zero false alarm. It was able to prove quickly (2h to 53h) the absence of run-time error in large (100 K to 1M lines) industrial avionic codes. This result could be achieved using a specialization process: starting from a fast and coarse analyzer based on intervals, we added manually more powerful abstract domains as they were needed. Some were borrowed from the large library of existing abstractions, and others were developed specifically for the avionic application domain (such as an abstraction of digital filters [START_REF] Feret | Static analysis of digital filters[END_REF]). Astrée is a mature tool: it is industrialized and made commercially available by AbsInt [START_REF] Absint | Angewandte Informatik. Astrée run-time error analyzer[END_REF]. More details can be found in [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF].

AstréeA

AstréeA aims at checking for run-time errors in multithreaded embedded critical C programs. It is based on the Astrée code-base and inherits all of its abstractions. Additionally, it implements the interference fixpoint analysis described in Sec. 3. Interferences are abstracted in a flow-insensitive and non-relational way, which was sufficient to give encouraging experimental results. On our target application, a 1.6 Mlines industrial avionic software with 15 threads, AstréeA reports around 1 300 alarms in 50h. More details can be found in [START_REF] Miné | Static analysis of run-time errors in embedded real-time parallel C programs[END_REF][START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF]. AstréeA is a research prototype in development; we are currently improving it with more powerful memory and interference abstractions.

Conclusion

We have provided in this article a short glimpse of abstract interpretation theory and its application to the systematic construction of static analyzers for sequential and parallel programs. Two key reasons make abstract interpretation-based constructions attractive. Firstly, its ability to relate in a formal way the output of a static analyzer all the way down to the precise dynamic behavior of the input program (its execution traces), both in terms of soundness proof and information loss. Secondly, the ability to decompose the design of an analyzer as the combination of independent, reusable abstractions, which allows the modular implementation of analyzers (e.g., abstract domains designed for Astrée could be reused in AstréeA). Future work includes the design of new abstractions to improve the AstréeA analyzer prototype and reduce the number of alarms on selected embedded multithreaded C programs. In particular, the derivation of thread-modular abstract semantics for parallel programs through the use of concrete interferences we introduced here opens the way to the design of flowsensitive and relational interference abstractions, which was not possible in the earlier framework underlying AstréeA.

Example 1 .

 1 Consider the simple programming language syntax: P ::= x := e | if e then P | while e do P | P ; P

Fig. 2 .

 2 Fig. 2. Semantics of the program in Fig. 1 at various levels of abstractions: (a) traces, and (b) reachable states and (c) intervals at program point (3).

Example 4 .

 4

Figure 2 .

 2 c presents the interval abstraction of the program in Fig.1.a at point (3). The relational information that i ≤ n when n ≥ 2 is lost.

Fig. 3 .

 3 Fig. 3. A simple multithreaded program (a), and its invariant assertions (b).

Example 10 .

 10 The interval abstractionx := y + 1 in the environment [x → [l x ; h x ]; y → [l y ; h y ]] at and the global interference map [x → [l x ; h x ]; y → [l y ; h y ]]gives, at , the interval x → [min(l x , l x + min(l y , l y ) + 1); max(h x , h x + max(h y , h y ) + 1)].

I.e., ∀X ∈ P(Σ * ), ∀Y ∈ P(Σ), α state (X) ⊆ Y ⇐⇒ X ⊆ γ state (Y ).

The x notations indicates that x is a finite vector. x[i] is its value at index i. We also use vector functions f . The i-th component of y's image f (y) is denoted f (y)[i]. Finally, ∅, ∪, and ⊆ denote respectively ∅, ∪, ⊆ extended element-wise to vectors.

Acknowledgments. We thank the anonymous referees on a earlier version of [16] for pointing out the link between the analysis performed by AstréeA and rely/guarantee methods, which was not apparent to us before. We also thank Patrick Cousot for urging us to provide a sequence of explicit abstraction functions detailing precisely which information is lost at each step of our construction, instead of providing a monolithic soundness proof as we did in [16].

This work was partially supported by the INRIA project "Abstraction" common to CNRS and ENS in France, and by the project ANR-11-INSE-014 from the French Agence nationale de la recherche.

(1) i := 2;

(2) n := input int();

(3) while i < n do (4) if input bool() then i := i + 1; (5) done; (6) assert i >= 2;

A Proofs

All the results from Sect. 2 are very classic, so, we do not prove them here (see for instance [START_REF] Cousot | Constructive design of a hierarchy of semantics of a transition system by abstract interpretation[END_REF]). Instead, we focus on the new results presented in Sect. 3: the nested fixpoint characterization of the reachable states of a parallel program using interferences.

A.1 Proof of [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF] The proof that the operator F in [START_REF] Cousot | Constructive versions of Tarski's fixed point theorems[END_REF] indeed has a least fixpoint, T , is analogous to that of F in [START_REF] Absint | Angewandte Informatik. Astrée run-time error analyzer[END_REF]. As F is a continuous morphism in the complete partial order of trace sets ordered by inclusion, i.e., F ( i X i ) = i F (X i ), we can apply Kleene's fixpoint theorem [START_REF] Cousot | Constructive design of a hierarchy of semantics of a transition system by abstract interpretation[END_REF], which states that lfp F exists and is exactly equal to n∈N F n (∅).

We now repeat this classic proof for the sake of completeness. Let us note X def = n∈N F n (∅). We first prove that X is indeed a fixpoint of F , then that it is smaller than any other fixpoint. Indeed,

, as the continuity of F implies its monotonicity, hence F n+1 (∅) ⊆ Y as Y = F (Y ). Thus, by recurrence, ∀n, F n (∅) ⊆ Y , which implies that X ⊆ Y . Hence, X is the least fixpoint of F .

A.2 Proof of [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] By definition [START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF], S[t] def = Π t (α state (T )) and T = lfp F with F (X)

We first prove by recurrence on n that Π t (α state (F n (∅))) = G n (∅). Intuitively, G n (∅) corresponds to the states, projected on thread t, that can be reached from I after at most n execution steps. When n = 0, Π t (α state (F 0 (∅))) = G 0 (∅) = ∅. Assume that the property holds for some n and let us prove that it holds for n + 1. As π t is one-to-one, we can reason on G n+1 (∅) and the states σ such that π t (σ) ∈ G n+1 (∅), so, let us consider such a σ. Then, either (a) σ ∈ I, or σ can be reached from some σ such that π t (σ ) ∈ G n (∅) and either (b)

Moreover, by recurrence hypothesis, σ ∈ α state (F n (∅)), i.e., there exists a trace in T with at most n transitions and ending in σ . This means that, if a transition

also exists in a trace of length at most n + 1 in T (the set of traces is "closed by fusion" [START_REF] Cousot | Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles[END_REF]). Hence, case (c) is equivalent to the existence of t = t and a trace

Thus, the disjunction of (a), (b), and (c) is equivalent to the existence of a trace in F n+1 (∅) containing σ, which is equivalent to σ ∈ α state (F n+1 (∅)). This ends the proof by recurrence.

We now use the characterization of fixpoints by iteration: we proved in the proof of ( 6) that T = n∈N F n (∅). Kleene's theorem implies likewise that lfp G = n∈N G n (∅). By continuity of Π t and α state , we get that

A.3 Proof of (11)

We now prove that Ā

→ σ n , which ends the proof.

A.4 Proof of (12)

We now prove that S = lfp H, where H( X)[t] def = lfp G t ( B( X)), and give the iterative form of lfp H.

Firstly, we prove that S is a fixpoint of H. Indeed, for any t, [START_REF] Cousot | Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles[END_REF], which equals S[t] by [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF].

Secondly, we prove that lfp H can be expressed in iterative form. To do so, we prove that H is continuous. Kleene's fixpoint theorem applied to the continuous function G t gives the following characterization of H: H( X)[t] = n∈N (G t ( B( X))) n (∅). To simplify notations, we define, for each t and n, the function Īn ( X)[t] def = (G t ( B( X))) n (∅). Then, we have H( X) = ¯ n∈N Īn ( X). We note that each Īn is continuous. Hence, we have:

, which proves the continuity of H. We can thus apply Keene's fixpoint theorem to H itself to get lfp H in iterative form: lfp H = n∈N Hn ( ∅). Finally, we prove that S ⊆lfp H. To do this, we prove by recurrence on n that, if σ n is reachable after n steps, i.e., if there exists some trace σ 0 t0

As σ 0 ∈ I, we indeed have π t (σ 0 ) ∈ Π t (I). Assume that the property is true at rank n and consider a trace σ 0


C Albea
email: calbea@laas.fr

Diego Puschini

Suzanne Lesecq

Yeter Akgul

Advanced coupled voltage-frequency control for power efficient DVFS management

Keywords: Dynamic voltage frequency scaling, control, power aware system, system stability

Power management is a hot-topic in complex System-on-Chip (SoC) designs. In the context of advanced technologies, Dynamic Voltage-Frequency Scaling (DVFS) techniques are widely proposed to improve efficiency. Nowadays, these mechanisms are composed of independent actuators controlling the applied voltage and clock frequency. A predefined sequence has to be used to switch from one state to another in order to avoid timing faults but increasing the energy cost. The timing of the sequence depends on the dynamic response of actuators. In this work, an external controller is designed in order to couple both actuators to manage the voltage and frequency transient periods, increasing power efficiency. The proposed controller has been implemented to couple a Vdd-hopping mechanism with a Frequency-Lock Loop circuit.

Introduction

The growing demand for more autonomy of mobile equipments at the same time that general purpose microprocessors hitting the power wall, increases the necessity to research technique for rising power-efficiency of computing. Actually, power consumption is a limiting factor in Very-Large-Scale Integration (VLSI), especially for mobile applications. Dynamic Voltage and Frequency Scaling (DVFS) [START_REF] Choudhary | Hardware based frequency/voltage control of voltage frequency island systems[END_REF] has proven to be highly effective to reduce the power consumption of the chip while meeting the performance requirements [START_REF] Horowitz | Low-power digital design[END_REF]. The key idea behind local DVFS is to control the supply voltage and the frequency of a circuit at runtime to minimize the power consumption while satisfying the computation/throughput constraints [START_REF] Choi | Fine-grained dynamic voltage and frequency scaling for precise energy and performance tradeoff based on the ratio of off-chip access to on-chip computation times[END_REF]. The DVFS technique mainly rely on two actuators. These drivers need to be dynamically controlled in order to reduce the power consumption while maintaining the required performance. More precisely, the control policy must be carefully designed in order to achieve high power efficiency at low area cost. The voltage driver fixes the supply voltage of the circuit. It can be a classical buck converter [START_REF] Liu | A dynamic buck converter with ultra fast response and low voltage ripples designed for DVS systems[END_REF] or a Vdd-hopping converter [START_REF] Albea | Robust saturated control for low-power circuits[END_REF][START_REF] Miermont | A power supply selector for energy-and area-efficient local dynamic voltage scaling[END_REF]. On the other side, the frequency actuator is a clock generator classically based on a Phase-Locked Loop (PLL) or a Frequency-Locked Loop (FLL).

On traditional synchronous CMOS circuits, the applied clock frequency should be chosen considering the supply voltage. For a given voltage a high frequency produces timing faults [START_REF] Zhai | The limit of dynamic voltage scaling and insomniac dynamic voltage scaling[END_REF], i.e. the clock cycle provides not enough time for logic cells to drive the output signals. On the contrary, a low frequency for a given voltage will result on poor calculation performance for a high energy consumption. For these reasons, the actuators management policy should ensure a predefined sequence to change from one voltage-frequency state to another. For instance, for an increasing frequency step the management policy should firstly increase the supply voltage, and once the output is stabilized, the frequency can be increased. The timing of this sequence depends on the dynamic response of actuators.

A consequence of technology scaling in advanced CMOS technologies is the in-die and die-to-die process variability. From a practical viewpoint, it is becoming increasingly difficult to manufacture integrated circuits with tight parametric values [START_REF] Miermont | A power supply selector for energy-and area-efficient local dynamic voltage scaling[END_REF]. In addition, circuit parameter are more sensible to temperature and voltage variations. Therefore, in order to obtain optimal performance, the clock frequency must be controlled according to Process, Voltage and Temperature (PVT) variations. Recently, control techniques have been applied to develop DVFS drivers. For instance, in [START_REF] Albea | Robust saturated control for low-power circuits[END_REF][START_REF] Bui | A generic method for embedded measurement and compensation of process and temperature variations in SOCs[END_REF], the closed-loop control of the voltage actuator is dealt with; and in [START_REF] Albea | Optimal and robust control for a small-area fll[END_REF], a robust control for a Frequency Lock-Loop (FLL) is presented.

In these previous works, the internal control of every driver has been independently treated. However, in order to improve DVFS efficiency, every PVT variation should impact the sequence timing of the management of drivers. This work deals with a joint control of voltage and frequency drivers, increasing power efficiency and avoiding timing faults. The proposed joint control allows to manage devices with different dynamics, allowing to simultaneously apply voltage and frequency set-point steps and providing global stability.

The rest of this paper is organized as follows: in Section 2, the problem statement is established. Architecture and internal control of each actuator are presented in Section 3. Next, Section 4 is consecrated to the joint control technique. Some simulations are presented in Section 5. The paper ends with conclusions and future work.

Notation. For a given x ∈ R,

sat M m (x)    M if x > M x if m ≤ x ≤ M m if x < m ∆x x k -x k-1 is the value of x in two consecutive sampling time. Finally, L 2 is the space of {x k } with the norm: x k 2 2 ∞ k=0 x T k x k < ∞, i.e.
, it is bounded energy.

Problem statement

DVFS circuitry applies voltage v c and frequency f to the functional synchronous circuit. Depending on the integration technology, each possible supply voltage allows a maximum clock frequency without timing faults. Moreover, a very high voltage produces permanent circuit damages. In the voltage-frequency plane and in the context of this work, these constraints are approximated by a forbidden area as shown in Fig. 1a. In order to improve efficiency, the DVFS mechanism changes the applied voltage and frequency values in a sequential way in order to avoid the circuit to get into the forbidden area. For instance, for changing from a set-point (V 1 , F 1 ) to another one (V 2 , F 2 ), where V 1 < V 2 and F 1 < F 2 , firstly voltage is changed while frequency is remained constant, and latter frequency is changed while voltage is constant, and vice-versa [START_REF] Beigné | An innovative local adaptive voltage scaling architecture for on-chip variability compensation[END_REF]. The problem statement considers to jointly control the voltage and frequency drivers in order to follow an optimal transition from (V 1 , F 1 ) to (V 2 , F 2 ) as represented in Fig. 1b, instead of using a sequential management as in Fig. 1a. This new strategy improves the system efficiency and matches the different dynamics of driver while guaranteeing global system stability.

Actuator architecture and control

As mentioned before, in this work the DVFS is implemented by Vdd-Hopping and FLL drivers. Each circuit is independently controlled by an internal control law. The very lengthy algebraic calculations required to derive the results presented here are omitted due to lack of space; they may be found in [START_REF] Albea | Robust saturated control for low-power circuits[END_REF][START_REF] Albea | Optimal and robust control for a small-area fll[END_REF].

FLL

The main blocks of the FLL are modeled through design considerations and accurate simulations. These blocks are a Digitally-Controlled Oscillator (DCO) that provides a clock, a sensor (i.e. a counter) to measure the clock frequency, a comparator that compares the output clock frequency with the target one, and a digital controller. In Fig. 2, a sketch of the FLL is shown.

Digitally-Controlled Oscillator. The DCO was firstly designed considering technological parameters for the delay cells. Then, based on accurate low-level simulations (Spice level), a linear DCO model has been approximated. It has been assumed that this model evolves over the time with PVT variations [START_REF] Albea | Optimal and robust control for a small-area fll[END_REF]. The simplified DCO model is:

f k = b + K DCO u f k + B w ν f k (1)
where f, f k ∈ R 1 are the analog and digital frequency output respectively, u f k ∈ N is coded over 8 bits between 0 and 255 and it is a digital representation of a

Controller DCO Sensor e k-1 u fk f (t) f r f k-1 K s f k K DCO K + - z -1 K s Figure 2: FLL architecture.
clock frequency. T sf is the sampling period, b is the DC-offset, K DCO is a gain. ν f is a bounded energy signal to take into account any possible disturbance, and B w is a constant that defines the disturbance magnitude. In order to take into account the PVT variation effects, it is assumed that parameters K DCO , b and B w can change in a certain interval.

Sensor. The digital sensor counts the number of generated clock peaks during a sampling period of time. This sensor introduces a delay of one sampling period that is represented in the feedback loop model:

M k K s f k-1 Control. Define e k K s (f r -f k )
, where f r is the reference signal and K s is a positive constant that represents the sensor gain. Then, the error equation is:

e k = -b -K DCO u f k -B w ν f k + K s f r (2)
In order to limit the FLL area cost and taking into account the control objectives, a simple digital integral controller is defined:

u f k = u f k-1 + K(K s f r -M k ) = u k-1 + K f e k-1 (3)
where K f is a controller parameter to be tuned ensuring:

• closed-loop stability;

• robustness against PVT variations;

• suited performance (no overshoot, no static error, short transient period);

• low area overhead and

• exogenous disturbance rejection.

In [START_REF] Albea | Optimal and robust control for a small-area fll[END_REF], a method for obtaining an optimal and robust H ∞ control has been presented, which accomplishes all requirements given above.

Vdd-Hopping

In [START_REF] Miermont | A power supply selector for energy-and area-efficient local dynamic voltage scaling[END_REF] a discrete circuit that handles two-voltage levels with a Vdd-Hopping technique accomplishing a DVS architecture was presented in order to reduce power consumption. The Vdd-Hopping circuit is composed of: a high voltage supply, V h ; a low voltage supply, V l ; a set of PMOS transistors connected in parallel between V h and the core voltage, v c , and a PMOS transistor connecting V l to v c when the low voltage level is the steady-state. The set of parallel PMOS transistors allows evolving the output voltage from a low voltage level to a high voltage level (rising transient period) and from a high voltage level to a low voltage level (falling transient period). The steady-state must correspond to a high voltage level or a low voltage level. For simplicity, the low voltage supply, V l , as well as the PMOS transistor connecting it to v c are disregarded for control design purposes. The main objective is to ensure that v c achieves the two voltage levels by switching the PMOS transistors. Fig. 3 represents this circuit. In this architecture, at least, one transistor must always be switched on.

M1 R1

Mn-1 Rn-1 The voltage loop equation yields to the relationship:

Mn Rn V h IMPEDANCE Il(vc) I leak C R L M2 R2 CONTROL u vk v c
V h -v c R u vk = v c R L + I leak + C dv c dt (4)
where R u k R0 u vk , u k being the number of transistors switched on, thus, u vk ∈ U = {1, 2, ..N } and it is the control variable.

The system load (fed circuit) is represented as an impedance which depends on the applied clock frequency f and on v c [START_REF] Miermont | A power supply selector for energy-and area-efficient local dynamic voltage scaling[END_REF]. It is composed of a current supply, I leak , a capacitance, C, and a dynamic resistance, R L (f, v c ), representing the dynamic and short-circuit consumption. I leak is assumed constant. In this work, the load model presented in [START_REF] Miermont | A power supply selector for energy-and area-efficient local dynamic voltage scaling[END_REF] is employed.

Consider k v rv ck where v r is the voltage reference and v ck is the sampling core voltage. Now, from Eq. ( 4), the approximated discrete-time voltage error equation is:

k+1 = (1 -Tsβ) k + Ts v b(vr -V h )u vk + Ts(βvr + δ -bu vk k ) + νv k (5)
where ν v k is an additional exogenous disturbance from v r and it is

L 2 , β 1 R L C > 0, δ I leak C > 0 and b 1 R0C > 0.
T sv must be less or equal to the smaller 1 f . The approximated time-discretization ( 5) is performed by using the forward Euler method, by assuming that the sampling time is small enough to the system evolution.

The proposed controller for this system is based on a linear controller [START_REF] Albea | Control and stability analysis for the Vdd-hopping mechanism[END_REF]:

uv k = sat N 1 {u vk-1-h 1 + round (K1∆ k-h 1 -h 2 + K2 k-h 1 -h 2 1 )} ( 6
)
where h 1 and h 2 are sampling-period delays and h h 1 + h 2 . K 1 and K 2 are controller parameters and they must be tuned in such a way that the following properties are ensured:

• closed-loop stability;

• robustness regarding PVT variations and delays;

• suited performance (no current peaks, no static error, short transient period);

• low area overhead and

• exogenous disturbance rejection.

In [START_REF] Albea | Robust saturated control for low-power circuits[END_REF], a state-space representation was given by ( 5) and a mechanism has been presented in order to compute K 1 and K 2 for achieving optimal and robust control, which accomplish almost all requirements given above. Only, the rejection of exogenous disturbance was not considered. An easy extension of this method is performed here for taking into account this last requirement.

Theorem 2 presented in [START_REF] Albea | Robust saturated control for low-power circuits[END_REF] is extended in order to consider any disturbance input. Assume, there exists a minimum disturbance attenuation, γ * ≥ 0, such that, for all γ ≥ γ * the L 2 gain between the disturbance vector ν v k and the output vector z k is less or equal to γ. i.e.

z k 2 2 -γ 2 ν v k 2 2 < 0, ∀ν v k ∈ L 2 for φ l = 0, -h ≤ l ≤ 0. (7)
Assumption 1 There exists a Lyapunov function V k , with condition V k+1 -V k < 0 and a γ, such that,

V k+1 -V k + z T k+1 z k+1 -γ 2 (ν T k ν k ) ≤ ζ T Γζ < 0. ( 8
)
where

ζ [ k k -k-1 ψ k ν k ]
T is an augmented state vector and Γ ∈ R 4×4 is a symmetric matrix.

Theorem 1 Consider system (5) and control law (6) with h 1 , h 2 ≥ 0 ∈ N known constant delays and K, G ∈ R 1×2 . If there exist T, Y, B ∈ R 2×1 and

Q 1 ∈ R 2 with K v = T Q -1 1 , G = Y Q -1 1 , A, Q, R, R, P1 , S > 0 ∈ R 2 for j = 1, ..., 64 and c, µ, γ > 0 such that: min K µ P1 > 0 (9) Γ(j) < 0 j = 1, ...., 64, (10)
  P1 -µ 0 0 * S -µ 0 * * R -µ   < 0, (11)
Λ > 0 [START_REF] Miermont | A power supply selector for energy-and area-efficient local dynamic voltage scaling[END_REF] being Γ(j) defined in Eq. ( 13), found at the top of next page, are satisfied. Then, in the vertices j, the equilibrium is asymptotically stable as well as the current peaks are limited in the entire polytope.

Γ(j)           Γ(j) 1 Γ(j) 2 -Ξ(j) T + S Q 1 Ξ(j) Ξ(j) Q 1 * P1 -2Q 1 + h R 0 0 0 0 Q 1 * * -R -S 0 0 0 0 * * * -Q -1 0 0 0 * * * * -R -1 0 0 * * * * * -R -1 0 * * * * * * -γ 2 I           , (13)
where Ξ(j) (α

(j) k T + (1 -α (j) k )Y ), Γ(j) 1 Q 1 A (j) T + A (j) Q 1 -2Q 1 + Ξ(j) T + Ξ(j) , Γ(j) 2 P1 + Q 1 A (j) T -2Q 1 + Ξ(j) T Proof 1
The proof is an extension of the proof presented in [START_REF] Albea | Robust saturated control for low-power circuits[END_REF] for Theorem 2, taking into account the functional cost [START_REF] Bui | A generic method for embedded measurement and compensation of process and temperature variations in SOCs[END_REF].

The implementation of the controller described of equation ( 6) requires a low area overhead. The saturation function is due to the control signal constraint mentioned before. The control objective is to achieve a reference signal. An control structure for the Vdd-Hopping circuit that manages current peaks is patent pending [START_REF] Albea | Dispositif de commande numérique pour un tableau de transistors pmos en parallele[END_REF].

Joint control

As explained before, the main deal in this work is to jointly control the evolution of the frequency output of the FLL and the evolution of the voltage output of the Vdd-Hopping in order to reduce the power consumption. The solution presented here is shown in Fig. 4. This mechanism is composed of:

1) Vdd-Hopping + Control 2) FLL + Control 4) P ower-aware control 3) Scaling Mechanism v c f f r v r w v w f 5) Voltage limiter 6) Frequency limiter M U X v c , f
1. Voltage actuator. This circuit is a stable Vdd-Hopping circuit, Eq. ( 4), with its internal control law, Eq. ( 6), and a sampling time T v s .

2. Frequency actuator. In this block, there is a stable FLL, Eq. ( 1), with its internal control law, Eq. ( 3), and a sampling time T f s .

3. Scaling mechanism. This mechanism allows to compensate the different dynamics of the two actuators. Note that each actuator presents a different sampling period. In this block the faster dynamic is under-sampled.

4.

Power-aware control. It generates perturbations that are added to the corresponding references, in such a way that both references evolve following a given trajectory that induces an increase of power efficiency.

5. Voltage limiter. This block ensures that the system voltage will not reach the forbidden area.

Frequency limiter. This block, similar to block 5), ensures that the applied frequency will not reach the forbidden area.

Joint control

The joint power-aware control (block 4) is defined as:

w v w f v c k -f k -F0 M f k -(F 0 + M v c k ) = 1 -1 -1 1 k e k Ks ,
where F 0 and M are parameters that define the optimal trajectory of the variable states in order to improve power efficiency. This optimal path is defined by

f k = F 0 + M v c k . Remind e k = K s (f r -f k ) and k = v r -v ck .
Let rewrite in a compact way:

w k = -Lx k (14)
where

w k [w v k w f k ] T , x k [ e k
Ks k ] T , L ∈ R 2×2 is semidefinite positive matrix, thus, it is not inversible. w k is added to the reference, as shown in Fig. 4.

Remark 1 L is a connection matrix, whose terms define the optimal trajectory that the state must follow in order to achieve the consensus.

Assumption 2 Consider a closed loop system under the form

x k+1 = (A + B K) x k , (15)
with x k = [ e k Ks k k-1 ] T ∈ R 1×3 and A+B K = diag{a+b K f , A+B K v } ∈ R 3×3 where a + b K f is a FLL closed loop and A + B K v is a Vdd-Hopping closed loop.
This system is stable and robust as well as it does not present overshoots.

Theorem 2 There exists a system (15), whose input is perturbed by (14). Consider a definite positive matrix P ∈ R 3×3 associated to the stability of system (15), such that,

-( L + P) (A T + K T B T -LT K T B T )( L + P) * -( L + P) < 0 ( 16
)
where L ∈ R 3×3 is an augmented vector from L ∈ R 2×2 , in order to be agree with the dimension of x k . Then, Lx k converges to zero and the system is globally asymptotically stable.

Proof 2 The global system is

x k+1 = (A + B K -B K L) x k . ( 17
)
Take as Lyapunov function:

U k = x T k L x k + x T k P x k ≥ 0,
in order to make that L x k converges to zero at the same time that x k converges to zero. Note that L is semidefinite positive.

U k+1 -U k = ( x T k+1 ( L + P) x k+1 -x T k ( L + P) x k ) = x T k A T + (I 3 -LT ) K T B T )( L + P) (A + B K(I 3 -L) -( L + P) x k < 0
Applying Schur complement and pre-and post-multiplying matrix by [I 3 ( L + P)] LMI (16) is achieved.

Remark 2

The global system composed of:

• discrete models of the FLL (1) and Vdd-Hopping circuit (4), with their corresponding controllers (3), [START_REF] Beigné | An innovative local adaptive voltage scaling architecture for on-chip variability compensation[END_REF], that, among others, reject disturbance and

• the joint control mechanism is globally asymptotically stable from Theorem 2.

Voltage and frequency limiter

The voltage and frequency references with their corresponding perturbations are saturated in the limiter blocks 5) and 6) as follows:

sat V h f -F 0 M (v r + w v k ) (18) sat F0+M vc fmin (f r + w f k ) ( 19
)
Remark 3 The internal control of the FLL (3) ensures that there is no overshoot. Likewise, the Vdd-hopping is an approximate first-order system (see Property 1 in [START_REF] Albea | Advanced control design for voltage scaling converters[END_REF]). Consequently, there is no overshoot in the voltage and frequency outputs.

Corollary 1 From limiters (18)-( 19) and Remark 3 timing faults are avoided, i.e., the state does not go to the forbidden area.

Simulations

The proposed joint control has been evaluated in the Matlab environment. For this test-case, the FLL are reported from [START_REF] Albea | Optimal and robust control for a small-area fll[END_REF]. The sampling period is 60ns and the control gain is K = 0.392. Likewise, for the Vdd-Hopping system is taken from [START_REF] Albea | Robust saturated control for low-power circuits[END_REF] with a sampling period of 2ns. The control gains are Figure 5 shows the evolution of both voltage and frequency when the joint control is implemented for rising and falling steps. For the same scenario, Fig. 6 shows the w v and w f evolution when system is rising from (V 1 , F 1 ) to (V 2 , F 2 ) and dropping from (V 2 , F 2 ) to (V 1 , F 1 ). The changing commands have been applied at 2µs for the rising step and at 10µs for the dropping step. Note that the rising and dropping evolutions are not symmetrical due to the limiters (Eq. ( 18)-( 19)) that avoid timing faults and the non-linear nature of voltage driver. In Fig. 7 the voltage-frequency evolution in the VF plane is shown. Note that, as indeed, the DVFS circuit does not cross the reference trajectory, which also limits the forbidden area.

K 1 = -1.24, K 2 = 0.22. (V 1 , F 1 ) = (0.8V, 50LSB) and (V 2 , F 2 ) = (1.11V, 200LSB
Finally, the power consumption has been analyzed for a rising step, comparing the joint control with an equivalent non-coupled system. A safe sequence has been established for the non-coupled system, applying firstly a rising voltage step at 2µs and then a rising frequency step at 5µs. Total transition period corresponding to the trajectory from (V 2 , F 2 ) to (V 1 , F 1 ) represented in Fig. 1a, is estimated to 7µs. Figure 8 shows the normalized power comparison for this period. The energy gain for this interval has been estimated to 40.5%.

Conclusions

In this work, a joint controller has been designed to jointly manage voltage and clock frequency in DVFS mechanism. It has been implemented to control a Vdd-Hopping driver and a FLL clock generator. The internal controller of each driver was studied in [START_REF] Albea | Robust saturated control for low-power circuits[END_REF][START_REF] Albea | Optimal and robust control for a small-area fll[END_REF]. Among other characteristics, these independent closedloop systems reject perturbations and provide outputs without signal overshoots.

From these properties, it has been designed an external joint controller, in such a way that the complete system is globally stable. Finally, a limiter was introduced in each reference in order to guarantee that there is no timing faults. This joint controller has been validated through Matlab simulations. It has been shown, that the power consumption can be reduced by 40.5% in the evaluated testcase. As future work, a attraction region induced by limiters ( 18)-( 19) will be estimated. Likewise, it is expected to validate these results in Spice.

  With joint control.

Figure 1 :

 1 Figure 1: Evolution of v c and f .

Figure 3 :

 3 Figure 3: Vdd-hopping architecture.

Figure 4 :

 4 Figure 4: DVFS system with joint control.

Figure 5 :

 5 Figure 5: Evolution of voltage-frequency with joint control.

Figure 6 :

 6 Figure 6: Evolution of voltage and frequency perturbations.

Figure 7 :

 7 Figure 7: Evolution of voltage and frequency.

Figure 8 :

 8 Figure 8: Power comparison for coupled and non-coupled systems.

  ). For the joint control M = 485 and F 0 = -335.

								(A)
		1.15
												Vout
		1.1										Vref
												Vref + WV
		1.05
	Voltage (V)	0.9 0.95 1
		0.85
		0.8
		0.75	0	0.2	0.4	0.6	0.8	1	1.2	1.4	1.6	1.8	2
								Time (s)				x 10 -5
								(B)
		250
												Fout
												Fref
		200										Fref + WF
	Frequency (LSB)	100 150
		50
		0	0	0.2	0.4	0.6	0.8	1	1.2	1.4	1.6	1.8	2
								Time (s)				x 10 -5

Acknowledgment

This work has received partial funding from the EU FP7 PRO3D project under grant agreement no. 278776 and from EU Artemis JU Pollux project under grant agreement no. 100205.