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

Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs ⋆

Keywords: Parallel programs, static analysis, Abstract Interpretation, run-time errors

We present a static analysis by Abstract Interpretation to check for run-time errors in parallel C programs. Following our work on Astrée, we focus on embedded critical programs without recursion nor dynamic memory allocation, but extend the analysis to a static set of threads. Our method iterates a slightly modified non-parallel analysis over each thread in turn, until thread interferences stabilize. We prove the soundness of the method with respect to a sequential consistent semantics and a reasonable weakly consistent memory semantics. We then show how to take into account mutual exclusion and thread priorities through partitioning over the scheduler state. We present preliminary experimental results analyzing a real program with our prototype, Thésée, and demonstrate the scalability of our approach.

Introduction

Ensuring the safety of critical embedded software is important as a single "bug" can have catastrophic consequences. Previous work on the Astrée analyzer [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] demonstrated that static analysis by Abstract Interpretation could help, when specializing an analyzer to a class of programs (synchronous control/command avionics C software) and properties (run-time errors). In this paper, we describe ongoing work to achieve similar results for parallel embedded programs. We wish to match the current trend in critical embedded systems to switch from large numbers of single-program processors communicating through a common bus to single-processor multi-threaded applications communicating through a shared memory (for instance, in the context of Integrated Modular Avionics). We focus on detecting the same kinds of run-time errors as Astrée does (arithmetic and memory errors) and take data-races into account (as they may cause such errors), but we ignore other concurrency errors (such as dead-locks, live-locks, or priority inversions), which are orthogonal.

Our method is based on Abstract Interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], a general theory of the approximation of semantics, which allows designing static analyzers that are sound by construction, i.e., consider a superset of all program behaviors and thus cannot miss any bug, but can cause spurious alarms due to over-approximations. At its core, our method performs an analysis of each thread considering an abstraction of the effects of the other threads (called interferences). Each analysis generates a new set of interferences, and threads are re-analyzed until a fixpoint is reached. Thus, few modifications are required for a non-parallel analyzer to analyze parallel programs. Moreover, we show that few thread re-analyses are required in practice, resulting in a scalable analysis.

As we target embedded software, we can safely assume that there is no recursion nor dynamic allocation of memory, threads, or locks, which makes the analysis easier. In return, we handle two subtle points. Firstly, we consider a weakly consistent memory model: memory accesses not protected by mutual exclusion may cause behaviors that are not the result of any thread interleaving to appear, as they expose to concurrent threads compiler optimizations that are transparent on non-parallel programs. We handle this by proving that our semantics is invariant by some classes of program transformations. Secondly, we take into account the effect of a real-time scheduler that schedules the threads on a single processor according to strict, fixed priorities: only the unblocked thread of highest priority may run. This ensures some mutual exclusion properties that our target program exploits, and so should our analysis. This is achieved by partitioning with respect to an abstraction of the global scheduling state.

Our paper is organized as follows: Sec. 2 presents a classic non-parallel semantics, Sec. 3 considers threads in a shared memory, and Sec. 4 adds support for locks and priorities; Sec. 5 presents our prototype and experimental results, Sec. 6 discusses related work, and Sec. 7 concludes and envisions future work.

We alternate between two kinds of semantics: semantics based on control paths, that can model precisely thread interleavings, and semantics by structural induction on the syntax, that give rise to effective abstract interpreters. Figure 1 summarizes the semantics introduced in the paper, using ⊆ to denote the "is less abstract than" relation. Our analysis has already been mentioned, briefly and informally, in [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF]§ VI]. We offer here a formal, rigorous treatment.

Non-parallel Programs

This section recalls a classic static analysis by Abstract Interpretation of the runtime errors of non-parallel programs, as performed for instance by Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF]. The formalization introduced here will be extended later to parallel programs, and it will be apparent that an analyzer for parallel programs can be constructed by extending an analyzer for non-parallel programs with few changes.

Syntax

For the sake of exposition, we reason on a vastly simplified programming language. However, the results extend naturally to a realistic language, such as the non-parallel semantics parallel semantics subset of C excluding recursion and dynamic memory allocation. We assume a fixed, finite set V of variables and F of function names. A program has an entry-point entry ∈ F and associates to each function name f ∈ F a structured statement body(f ) ∈ stat in the following grammar:

P ( §2.2) ⊆ / / P ♯ ( §2.3) ✆ ( §2.4) = P I ( §3.2) ⊆ / / P ♯ I ( §3.
stat ::= X ← expr (assignment, X ∈ V) | if expr then stat (conditional) | while expr do stat (loop) | stat; stat (sequence) | f () (function call, f ∈ F) expr ::= X | [c 1 , c 2 ] | expr ⋄ ℓ expr where X ∈ V, c 1 , c 2 ∈ R ∪ { ±∞ }, ⋄ ∈ { +, -, ×, / }, ℓ ∈ L (1)
For the sake of simplicity, we do not handle local variables (all variables are visible at all program points) nor function arguments and returns. Due to the absence of recursion, these could be easily simulated by using a finite set of global variables. Our toy language is limited to a single data-type (real numbers in R) and numeric expressions. Constants are actually constant intervals [c 1 , c 2 ], which return a fresh value between c 1 and c 2 when evaluated. This allows modeling non-deterministic expressions and inputs from the environment. Each operator ⋄ ℓ is tagged with a syntactic location ℓ and we denote by L the finite set of all syntactic locations. The output of an analyzer will be the set of locations ℓ with errors (or rather, a superset of them, due to approximations).

Concrete Structured Semantics P

We present a concrete semantics, that is, the most precise mathematical expression of program semantics we consider. As it is undecidable, it will be abstracted in the next section to obtain a sound static analysis.

A program environment ρ ∈ E maps each variable to a value, i.e.,

E def = V → R.
The semantics E e of an expression e ∈ expr maps an environment to a set of values in P(R) (sets accounting for non-determinism) and a set of run-time error locations in P(L) (in our simple case, only for divisions by zero). It is defined by structural induction as follows:

∀e ∈ expr , E e : E → (P(R) × P(L))

E X ρ def = ({ ρ(X) }, ∅) E [c 1 , c 2 ] ρ def = ({ c ∈ R | c 1 ≤ c ≤ c 2 }, ∅) E e 1 ⋄ ℓ e 2 ρ def = let (V 1 , Ω 1 ) = E e 1 ρ in let (V 2 , Ω 2 ) = E e 2 ρ in ({ x 1 ⋄ x 2 | x 1 ∈ V 1 , x 2 ∈ V 2 , ⋄ = / ∨ x 2 = 0 }, Ω 1 ∪ Ω 2 ∪ { ℓ | ⋄ = / ∧ 0 ∈ V 2 }) where ⋄ ∈ { +, -, ×, / } (2)
We now consider the complete lattice D def = P(E)×P(L) with partial order ⊑ defined as the pairwise set inclusion (A, B)

⊑ (A ′ , B ′ ) def ⇐⇒ A ⊆ A ′ ∧B ⊆ B ′ .
We denote by ⊔ the associated join, i.e., pairwise set union. The structured semantics S s of a statement s is a morphism in D that, given a set of environments R and errors Ω before a statement s, returns the reachable environments after s as well as Ω enriched with the errors encountered during the execution of s:

∀s ∈ stat, S s : D → D S X ← e (R, Ω) def = (∅, Ω) ⊔ ρ∈R let (V, Ω ′ ) = E e ρ in ({ ρ[X → v] | v ∈ V }, Ω ′ ) S s 1 ; s 2 (R, Ω) def = (S s 2 • S s 1 )(R, Ω) S if e then s (R, Ω) def = (S s • S e = 0? )(R, Ω) ⊔ S e = 0? (R, Ω) S while e do s (R, Ω) def = S e = 0? (lfp λX. (R, Ω) ⊔ (S s • S e = 0? )X) S f () (R, Ω) def = S body(f ) (R, Ω) S e ⊲⊳ 0? (R, Ω) def = (∅, Ω) ⊔ ρ∈R let (V, Ω ′ ) = E e ρ in ({ ρ | ∃v ∈ V, v ⊲⊳ 0 }, Ω ′ ) with ⊲⊳ ∈ { =, = } (3)
where ρ[X → x] is the environment that maps X to x, and elements Y = X to ρ(Y ). Loops and conditionals use the synthetic "guard" statements e = 0? and e = 0? that filter their argument and keep only those environments that may evaluate, respectively, to null (i.e., false) or non-null (i.e., true) values. Guards and assignments are collectively called atomic statements. The semantics of loops uses a least fixpoint operator lfp to compute a loop invariant. We have the following property: Theorem 1. ∀s, S s is well defined and a strict, complete ⊔-morphism.

We can now define the concrete structured semantics of the program as follows:

P def = Ω, where (-, Ω) = S entry() (E 0 , ∅) (4)
where E 0 ⊆ E is a set of initial environments (e.g., E 0 def = { ρ 0 } where ∀X ∈ V, ρ 0 (X) = 0). Thus, we observe the set of run-time errors that can appear in executions starting at the beginning of entry in an initial environment. Note that, as ∀s, S s (∅, Ω) = (∅, Ω), we also observe errors occurring in executions that loop forever or halt before the end of entry.

Abstract Structured Semantics P ♯

The semantics P is not computable as it involves least fixpoints in an infiniteheight domain D. An effective analysis will instead compute an abstract semantics over-approximating the concrete one. This semantics is parametrized by an abstract domain of environments, i.e., a set E ♯ of computer-representable abstract elements, with a partial order ⊆ ♯ . Each abstract element represents a set of concrete environments through a monotonic concretization function γ E : E ♯ → P(E). In particular, there is an element

E ♯ 0 ∈ E ♯ representing ini- tial environments: γ E (E ♯ 0 ) ⊇ E 0 .
We also require a sound and effective abstract version of every concrete operator:

∪ ♯ E : (E ♯ × E ♯ ) → E ♯ with ∀A ♯ , B ♯ ∈ E ♯ , γ E (A ♯ ∪ ♯ E B ♯ ) ⊇ γ E (A ♯ ) ∪ γ E (B ♯
) and, for atomic statements s, i.e., s ∈ { X ← e, e = 0?, e = 0? }:

S s ♯ : (E ♯ × P(L)) → (E ♯ × P(L)) with ∀(R ♯ , Ω), (S s • γ)(R ♯ , Ω) ⊑ (γ • S s ♯ )(R ♯ , Ω) where γ(R ♯ , Ω) def = (γ E (R ♯ ), Ω)
i.e., the soundness condition requires an abstract operator to output supersets of the environments and error locations returned by the concrete one. Finally, when E ♯ has infinite strictly increasing chains, we require a widening operator ▽ E to ensure the convergence of abstract fixpoint computations in finite time:

▽ E : (E ♯ × E ♯ ) → E ♯ with ∀A ♯ , B ♯ ∈ E ♯ , γ E (A ♯ ▽ E B ♯ ) ⊇ γ E (A ♯ ) ∪ γ E (B ♯ ) and ∀(Y ♯ i ) i∈N , the sequence X ♯ 0 def = Y ♯ 0 , X ♯ i+1 def = X ♯ i ▽ E Y ♯ i+1
reaches a fixpoint X ♯ k = X ♯ k+1 for some k ∈ N. There exist many such abstract domains, for instance the interval domain [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], where an element of E ♯ associates an interval to each variable, or the octagon domain [START_REF] Miné | The octagon abstract domain[END_REF], where an element of E ♯ is a conjunction of constraints of the form

±X ± Y ≤ c with X, Y ∈ V, c ∈ R.
Given an abstract domain, we can provide an abstract semantics for nonatomic statements by induction, similarly to the concrete semantics (3), except that loops use the widening operator ▽ E :

S s 1 ; s 2 ♯ (R ♯ , Ω) def = (S s 2 ♯ • S s 1 ♯ )(R ♯ , Ω) S if e then s ♯ (R ♯ , Ω) def = (S s ♯ • S e = 0? ♯ )(R ♯ , Ω) ∪ ♯ S e = 0? ♯ (R ♯ , Ω) S while e do s ♯ (R ♯ , Ω) def = S e = 0? ♯ (lfp λX. X ▽ ((R ♯ , Ω) ∪ ♯ (S s ♯ • S e = 0? ♯ )X)) S f () ♯ (R ♯ , Ω) def = S body(f ) ♯ (R ♯ , Ω) (5) where (R ♯ 1 , Ω 1 ) ∪ ♯ (R ♯ 2 , Ω 2 ) def = (R ♯ 1 ∪ ♯ E R ♯ 2 , Ω 1 ∪ Ω 2 ) and (R ♯ 1 , Ω 1 ) ▽ (R ♯ 2 , Ω 2 ) def = (R ♯ 1 ▽ E R ♯ 2 , Ω 1 ∪ Ω 2 )
. The program semantics is, similarly to (4):

P ♯ def = Ω, where (-, Ω) = S entry() ♯ (E ♯ 0 , ∅) . (6)
The following theorem states the soundness of the abstract semantics: Theorem 2. P ⊆ P ♯ .

As our programs have no recursive procedures, the recursion in S • ♯ is bounded and we obtain an effective and sound static analysis. It is flow-sensitive and fully context-sensitive (behaving as if all function calls were inlined). It is relational whenever E ♯ is (e.g., with octagons [START_REF] Miné | The octagon abstract domain[END_REF]). Moreover, the number of abstract elements to keep in memory does not depend on the program size but on the maximum nesting of conditionals and loops: the analyzer is thus very memory friendly, which is critical to analyze large programs, as in Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF].

Concrete Path-Based Semantics ✆

We now propose an alternative concrete semantics based on control paths, which will come handy when considering parallel programs interleaving several threads. For non-parallel programs, its output is equal to that of the structured one.

A control path p is a finite sequence of atomic statements (i.e., X ← e, e = 0?, e = 0?). We denote by Π the set of all control paths. The set of paths π(s) ⊆ Π of a statement s is defined as follows:

π(X ← e) def = { X ← e } π(s 1 ; s 2 ) def = π(s 1 ); π(s 2 ) π(if e then s) def = ({ e = 0? }; π(s)) ∪ { e = 0? } π(while e do s) def = (lfp λX. { ǫ } ∪ (X; { e = 0? }; π(s))); { e = 0? } π(f ()) def = π(body(f )) (7)
where ǫ denotes then empty path, and ; denotes path concatenation (by analogy with statement sequencing s 1 ; s 2 ) and is naturally extended to sets of paths. When s contains a loop, π(s) is infinite, although many paths may be infeasible, i.e., have no corresponding execution (e.g., if all loops have a static bound).

Using the definitions from the structured semantics (3), we can define the semantics ✆ P of a set of paths P ⊆ Π as:

✆ P (R, Ω) def = { S s 1 ; . . . ; s n (R, Ω) | s 1 ; . . . ; s n ∈ P } (8
) which is similar to the standard meet over all paths solution1 of data-flow problems [18, § 2], but for concrete executions in the infinite-height lattice D. The meet over all paths and maximum fixpoint solutions of data-flow problems are equal for distributive frameworks; similarly, our structured and path-based concrete semantics (based on complete ⊔-morphisms) are equal:

Theorem 3. ∀s ∈ stat, ✆ π(s) = S s .

Parallel Programs in Shared Memory

In this section, we consider several threads that communicate through a shared memory, without any synchronization primitive. We also discuss memory consistency models and their effect on the semantics and static analysis.

A program has now a fixed, finite set T of threads. Each thread t ∈ T has an entry-point function entry t ∈ F. All the variables in V are shared and can be accessed by all threads.2

Concrete Interleaving Semantics P *

The simplest and most natural model of parallel program execution considers all possible interleavings of control paths from all threads. These correspond to sequentially consistent executions, as coined by Lamport [START_REF] Lamport | How to make a multiprocessor computer that correctly executes multiprocess programs[END_REF]. A parallel control path p is a finite sequence of pairs (s, t), where s is an atomic statement and t ∈ T . The semantics ✆ * P of a set of parallel control paths P is:

✆ * P (R, Ω) def = { S s 1 ; . . . ; s n (R, Ω) | (s 1 , -); . . . ; (s n , -) ∈ P } (9)
We denote by π * the set of all parallel control paths in the program:

π * def = { p | ∀t ∈ T , proj t (p) ∈ π(body(entry t )) } (10)
where proj t (p) projects p on a thread t by extracting the maximal path s 1 ; . . . ; s n such that (s 1 , t); . . . ; (s n , t) is a sub-path of p. The semantics P * of the parallel program is then:

P * def = Ω, where (-, Ω) = ✆ * π * (E 0 , ∅) . (11)

Concrete Interference Semantics P I

Because it reasons on infinite sets of paths, the interleaving concrete semantics is not easily amenable to flow-sensitive abstractions. We propose here a more abstract semantics that can be expressed by induction on the syntax and will lead to an effective static analysis after further abstraction.

We start by enriching the non-parallel semantics of Sec. 2.2 with a notion of interference. We call interference a triple (t, X, v) ∈ I, where

I def = T × V × R,
indicating that the thread t can set the variable X to the value v. The semantics of expressions is updated to take as extra arguments the current thread t and an interference set I ⊆ I. When fetching a variable X ∈ V, each interference on X from other threads is applied:

E I X (t, ρ, I) def = ({ ρ(X) } ∪ { v | (t ′ , X, v) ∈ I, t = t ′ }, ∅) (12)
while other functions are not changed with respect to (2), apart from propagating t and I recursively. As the interference is chosen non-deterministically, distinct occurrences of X in an expression may evaluate to different values. The semantics of statements is also enriched with interferences and is now a complete ⊔-morphism in the complete lattice D I def = P(E) × P(L) × P(I). The semantics of an assignment in a thread t both uses and enriches the interference set:

E0 : flag1 = flag2 = 0 flag1 ← 1; flag2 ← 1; if (flag2 = 0) if (flag1 = 0) critical section critical section (a) Mutual Exclusion Algorithm. E0 : x = y = 0 x ← x + 1; x ← x + 1; y ← x; (b) Parallel Incrementation.
S I X ← e, t (R, Ω, I) def = (∅, Ω, I) ⊔ ρ∈R ({ ρ[X → v] | v ∈ V }, Ω ′ , { (t, X, v) | v ∈ V })
where (V, Ω ′ ) = E I e (t, ρ, I) .

(

) 13
The other functions (not presented here) are easily derived: guards e ⊲⊳ 0? pass I to E I e and return I unchanged, while non-atomic statements are similar to (3), replacing S • with S I • . Moreover, using S I • in ( 8) defines a path-based semantics with interference ✆ I P, t . Theorem 3 naturally becomes:

Theorem 4. ∀t ∈ T , s ∈ stat, ✆ I π(s), t = S I s, t .
The semantics S I s, t still considers a statement s from a single thread t. To take into account multiple threads, we iterate the analysis of all threads until errors and interferences are stable:

P I def = Ω, where (Ω, -) def = lfp λ(Ω, I). t∈T let (-, Ω ′ , I ′ ) = S I entry t (), t (E 0 , Ω, I) in (Ω ′ , I ′ ) . ( 14
)
The interference semantics is sound with respect to the interleaving one (11):

Theorem 5. P * ⊆ P I .

However, it is generally not complete. Consider, for instance the program fragment in Fig. 2(a) inspired from Dekker's mutual exclusion algorithm. According to the interleaving semantics, both threads can never be in their critical section simultaneously. The interference semantics, however, allows thread 1 to read flag2 as either 0 (from E 0 ) or 1 (from interferences) at any program point, and likewise for thread 2 and flag1, and so, there is no mutual exclusion. In Fig. 2(b), two threads increment the same zero-initialized variable x. According to the interleaving semantics, either the value 1 or 2 is stored into y. However, in the interference semantics, the fixpoint builds a growing set of interferences, up to { (t, x, i) | t ∈ T , i ∈ N }, as each thread increments the possible values written by the other thread, resulting in any positive value being written into y.

Abstract Interference Semantics P ♯

I

The concrete interference semantics is defined by structural induction. It can thus be easily abstracted. We assume, as in Sec. 2.3, the existence of an abstract domain E ♯ abstracting sets of environments, with a concretization γ E and an element E ♯ 0 abstracting E 0 . Additionally, we assume the existence of an abstract domain N ♯ that abstracts sets of reals. It is equipped with a concretization γ N :

N ♯ → P(R), a least element ⊥ ♯ N such that γ N (⊥ ♯ N ) = ∅, an abstract join ∪ ♯
N and, if it has strictly increasing infinite chains, a widening ▽ N . Interferences are then abstracted using the domain

I ♯ def = (T × V) → N ♯ , with concretization γ I (I ♯ ) def = { (t, X, v) | v ∈ γ N (I ♯ (t, X)) },
(S I s, t • γ)(R ♯ , Ω, I ♯ ) ⊑ (γ • S I s, t ♯ )(R ♯ , Ω, I ♯ ) where γ(R ♯ , Ω, I ♯ ) def = (γ E (R ♯ ), Ω, γ I (I ♯
)), i.e., the abstract function overapproximates environment, error, and interference sets.

Classic abstract domains can be easily converted to the interference semantics. Consider, for instance, the case of an assignment (R ♯′ , Ω ′ , I ♯′ ) = S I X ← e, t ♯ (R ♯ , Ω, I ♯ ), when N ♯ is the interval domain [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] and E ♯ is an arbitrary domain. For each variable Y occurring in e, we compute its abstract interference:

Y ♯ def = ♯ N { I ♯ (t ′ , Y ) | t = t ′ }. If Y ♯ = ⊥ ♯ N , then Y is substi- tuted in e with the interval constant Y ♯ ∪ ♯ N itv Y (R ♯ ) (
where itv Y (R ♯ ) extracts the bounds of Y in the abstract environment R ♯ ) to get an expression e ′ . The result abstract environment and error set can now be computed using the native operators on

E ♯ as (R ♯′ , Ω ′ ) = S X ← e ′ ♯ (R ♯ , Ω). Finally, I ♯′ = I ♯ [(t, X) → itv X (R ♯′ ) ∪ ♯ N I ♯ (t, X)].
Note that I ♯ is not isomorphic to the interval domain [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]: the former abstracts V → P(R) and the later P(V → R). Sound abstractions for atomic statements then lift by induction on the syntax to sound abstractions for all statements, as in [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF]. Finally, an abstraction of the interference fixpoint [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] can be computed by iteration on abstract interferences, using a widening to ensure termination:

P ♯ I def = Ω, where (Ω, -) def = lfp λ(Ω, I ♯ ). ∀t ∈ T , let (-, Ω ′ t , I ♯ t ′ ) = S I entry t (), t ♯ (E ♯ 0 , Ω, I ♯ ) in ( t∈T Ω ′ t , I ♯ ▽ I ♯ I { I ♯ t ′ | t ∈ T }) . (15)
The following theorem states the soundness of the analysis: Theorem 6. P I ⊆ P ♯ I . The obtained analysis remains flow-sensitive and can be relational (provided that E ♯ is relational) within each thread, but abstracts interferences in a flowinsensitive and non-relational way. It is expressed as an outer iteration that completely re-analyzes each thread until the abstract interferences stabilize, and so, can be implemented easily on top of existing non-parallel analyzers. Compared to a non-parallel program analysis, the cost is multiplied by the number of outer iterations required to stabilize interferences. This number remained very low in our experiments (Sec. 5). More importantly, the overall cost is not related to the (combinatorial) number of interleavings, but rather to the amount of abstract interferences I ♯ , i.e., of actual communications between the threads. The speed of convergence can be controlled by adapting the widening ▽ N .

Weakly Consistent Memory Semantics P ′ *

The interleaving concrete semantics P * of Sec. 3.1, while simple, is not realistic. A first issue is that, as noted by Reynolds in [START_REF] Reynolds | Toward a grainless semantics for shared-variable concurrency[END_REF], such a semantics requires choosing a level of granularity, i.e., some basic set of operations that are assumed to be atomic. In our case, we assumed assignments and guards to be atomic. In contrast, an actual system may schedule a thread within an assignment and cause x to be 1 at the end of the program in Fig. 2(b) instead of the expected value, 2. A second issue, noted by Lamport in [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], is that the latency of loads and stores in a shared memory may break the sequential consistency in true multiprocessor systems: threads running on different processors may not agree on the value of a shared variable. E.g., in Fig. 2(a), each thread may acknowledge the change of value of a flag after it has tested the other one, causing both critical sections to be entered simultaneously. Moreover, Lamport noted in [START_REF] Lamport | How to make a multiprocessor computer that correctly executes multiprocess programs[END_REF] that reordering of independent loads and stores in one thread by the processor can also break sequential consistency (for instance performing the load from flag2 after the store to flag1 instead of before in the left thread of Fig. 2(a)). More recently, it has been observed [START_REF] Manson | The Java memory model[END_REF] that optimizations in modern compilers have the same ill-effect even on mono-processor systems: program transformations that are perfectly safe on a thread considered in isolation (for instance, reordering the assignment flag1 ← 1 and the test flag2 = 0) can cause non sequentially consistent behaviors to appear. In this section, we show that the interference semantics correctly handles these issues, by proving that it is invariant under a "reasonable" class of program transformations.

Acceptable program transformations of a thread are defined with respect to the path-based semantics ✆ of Sec. 2.4. A transformation of a thread t is acceptable if it gives rise to a set π ′ (t) ⊆ Π of control paths such that every path p ′ ∈ π ′ (t) can be obtained from a path p ∈ π(body(entry t )) by a sequence of elementary transformations from Def. 1 below, q q ′ indicating that the statement sequence q in a path can be replaced with q ′ . These transformations can only reduce the amount of errors and interferences, so that an analysis of the original program is sound with respect to the transformed one. In Def. 1, we say that X ∈ V is fresh if it does not occur in any thread; X ∈ V is local if it occurs in the current thread only; s[e ′ /e] is the statement s where some but not necessarily all occurrences of expression e may be changed into e ′ ; var(e) is the set of variables appearing in e; lval(s) is the set of variables modified by s; nonblock(e) hods if evaluating e cannot block the program: ∀ρ, E e ρ = (V, -) with V = ∅; e is deterministic if, moreover, |V | = 1; noerror(e) holds if evaluating e is always error-free: ∀ρ, E e ρ = (-, ∅).

Definition 1 (Elementary path transformations).

1. Redundant store elimination: X ← e 1 ; X ← e 2 X ← e 2 when X / ∈ var(e 2 ) and nonblock(e 1 ). 2. Identity store elimination X ← X ǫ.

Reordering of assignments:

X 1 ← e 1 ; X 2 ← e 2
X 2 ← e 2 ; X 1 ← e 1 when X 1 / ∈ var(e 2 ), X 2 / ∈ var(e 1 ), and nonblock(e 1 ). Store latency can be simulated using rules 8 and 3. Breaking a statement into several ones (i.e., reducing the granularity of atomicity) is possible with rules 7 and 8. Global optimizations, such as constant propagation and folding, can be achieved using rules 7 and 9, while rules 1-6 allow peephole optimizations. Additionally, thread transformations that respect the set of control paths (such as loop unrolling or function inlining) are acceptable.

Reordering of guards

Given the set of transformed paths π ′ (t), the interleaved executions π ′ * and the semantics P ′ * can be defined as in [START_REF] Delmas | Astrée: from research to industry[END_REF], [START_REF] Ferrara | Static analysis via abstract interpretation of the happens-before memory model[END_REF]:

π ′ * def = { p | ∀t ∈ T , proj t (p) ∈ π ′ (t) } P ′ * def = Ω, where (-, Ω) = ✆ * π ′ * (E 0 , ∅) . (16)
The following theorem extends Thm. 5 to transformed programs: Theorem 7. P ′ * ⊆ P I . However, it is not complete. The two semantics coincide, for instance, in the program of Fig. 2(a). However, in the case of Fig. 2(b), the interference semantics assumes that y can take any positive value, while the interleaving semantics after program transformation still only allows the values 1 and 2. Note also that Thm. 7 holds for our "reasonable" collection of program transformations, but may not hold when considering "unreasonable" ones. For instance, flag1 ← 1 should not be replaced (e.g., by a misguided prefetching optimizer) with flag1 ← 42; flag1 ← 1 in Fig. 2(a), as this would cause the value 42 to be possibly seen by the other thread. Our interference semantics disallows such "out-of-thinair" values to be introduced. This is consistent with other semantics, such as the Java one [START_REF] Manson | The Java memory model[END_REF][START_REF] Saraswat | A theory of memory models[END_REF]. Another example of invalid transformation is the reordering of assignments X 1 ← e 1 ; X 2 ← e 2 X 2 ← e 2 ; X 1 ← e 1 when e 1 may block the program (e.g., due to a division by 0) as the transformed program could expose errors in e 2 that cannot occur in the original program. Nevertheless, Def. 1 is not exhaustive and could be extended with some other "reasonable" transformations.

Parallel Programs With a Scheduler

The language and semantics of the preceding section are now extended to handle explicit synchronization primitives and a real-time scheduler.

Priorities and Synchronization Primitives

We denote by M a finite, fixed set of non-recursive mutual exclusion locks, socalled mutexes. The language (1) of Sec. 2.1 is enriched with primitives to control mutexes and scheduling as follows:

stat

::= lock(m) (mutex locking, m ∈ M) | unlock(m) (mutex unlocking, m ∈ M) | X ← islocked(m) (mutex testing, X ∈ V, m ∈ M) | yield (thread pause) (17)
These new statements are considered to be atomic and the set of paths of a program ( 7) is extended by stating π(s) def = { s } for them. We also assume that threads have fixed and distinct priorities. Thus, we denote threads in T simply by numbers from 1 to |T |, being understood that thread t has a strictly higher priority than thread t ′ when t > t ′ .

Our scheduling model is that of real-time processes, found in embedded systems (e.g, the ARINC 653 specification [2]) and as an extension to POSIX threads. Moreover, we consider that a single thread can execute at a given time (e.g., when all threads share a single processor). In this model, the unblocked thread with the highest priority always runs. All threads start unblocked but may block voluntarily by locking a mutex that is already locked or by yielding, which allows lower priority threads to run. Yielding denotes blocking for a nondeterministic amount of time, which is useful to model timers (as we abstract away actual time) or waiting for some external resource. A lower priority thread can be preempted when unlocking a mutex if a higher priority thread is waiting for this mutex. It can also be preempted at any point by a yielding higher priority thread that wakes up non-deterministically. Thus, we cannot assume that a blocked thread is necessarily waiting at a synchronization statement.

This scheduling model is precise enough to take into account fine mutual exclusion properties that would not hold if we considered arbitrary preemption or true parallel executions on concurrent processors (as found, e.g, in desktops). For instance, in Fig. 3, the high priority thread avoids a call to lock / unlock by testing with islocked whether the low priority thread acquired the lock and, if not, executes its critical section (modifying Y and Z) confident that the low priority thread cannot execute and enter its critical section before the high priority thread explicitly yields. Such reasoning is required to analyze precisely our target application (Sec. 5), and requires the real-time scheduler and single-processor hypotheses assumed in this section.

Concrete Scheduled Interleaving Semantics P H

We now refine the semantics of Sec. 3 to take scheduling into account, starting with the concrete interleaving semantics P * of Sec. 3.1. Interleavings that do not respect mutual exclusion or priorities are excluded, and thus, we observe fewer behaviors. This is materialized by the dotted ⊆ arrows between concrete semantics in Fig. 1 (no such property holds for abstract semantics as they are generally non-monotonic due to the use of widenings).

low priority high priority lock(m); X ← islocked(m); Y ← 1; if X = 0 then Z ← 1; Z ← 2; T ← Y -Z;
Y ← 2; unlock(m); yield; Fig. 3. Using priorities to ensure mutual exclusion.

We define a domain of scheduler states H that associates to each thread whether it is ready, yielding, or waiting for some mutex, as well as the set of mutexes it holds:

H def = (T → { ready, yield , wait(m) | m ∈ M })×(T → P(M)).
The domain of statements becomes: D H def = P(H × E) × P(L). The semantics of atomic statements is decomposed into three steps. Firstly, the function enabled t : D H → D H that keeps only the states where a given thread t can run:

enabled t (R, Ω) def = ({ ((b, l), ρ) ∈ R | b(t) = ready ∧ ∀t ′ > t, b(t ′ ) = ready }, Ω) .
Secondly, the semantic function S ′ H s, t for atomic statements s in thread t:

S ′ H yield, t (R, Ω) def = ({ ((b[t → yield ], l), ρ) | ((b, l), ρ) ∈ R }, Ω) S ′ H lock(m), t (R, Ω) def = ({ ((b[t → wait(m)], l), ρ) | ((b, l), ρ) ∈ R }, Ω) S ′ H unlock(m), t (R, Ω) def = ({ ((b, l[t → l(t) \ { m }]), ρ) | ((b, l), ρ) ∈ R }, Ω) S ′ H X ← islocked(m), t (R, Ω) def = ({ ((b, l), ρ[X → 0]) | ((b, l), ρ) ∈ R, ∀t ′ ∈ T , m / ∈ l(t ′ ) } ∪ { ((b, l), ρ[X → 1]) | ((b, l), ρ) ∈ R, ∃t ′ ∈ T , m ∈ l(t ′ ) }, Ω) S ′ H s, t (R, Ω) def = ({ ((b, l), ρ ′ ) | ((b, l), ρ) ∈ R, (R ′ , -) = S s ({ ρ }, Ω), ρ ′ ∈ R ′ }, Ω ′ )
where (-, Ω ′ ) = S s (R, Ω), for all other statements s, using (3). Thirdly, a scheduler step that wakes up yielding threads non-deterministically and gives each available mutex to the highest priority thread waiting for it:

sched(R, Ω) def = ({ ((b ′ , l ′ ), ρ) | ((b, l), ρ) ∈ R }, Ω), where ∀t, if b(t) = wait(m) ∧ ∀t ′ = t, m / ∈ l(t ′ ) ∧ ∀t ′ > t, b(t ′ ) = wait(m) then b ′ (t) = ready and l ′ (t) = l(t) ∪ { m } else l ′ (t) = l(t) and b ′ (t) = b(t) ∨ (b ′ (t) = ready ∧ b(t) = yield ) .
The semantics of an atomic statement s in a thread t combines all three steps:

S H s, t def = sched • S ′ H s, t • enabled t . ( 18
)
The semantics ✆ H P of a set P of interleaved paths and the semantics P H of the program are then defined, similarly to Sec. 3.1, ( 9)-( 11), as:

✆ H P (R, Ω) def = { (S H s n , t n • • • • • S H s 1 , t 1 )(R, Ω) | (s 1 , t 1 ); . . . ; (s n , t n ) ∈ P } P H def = Ω, where (-, Ω) = ✆ H π * ({h 0 } × E 0 , ∅) (19)
where h 0 def = (λt. ready, λt. ∅) denotes the initial scheduler state. As in Sec. 3.1, many control paths in π * are unfeasible, i.e., return an empty set of environments, some of which are now ruled-out by the enabled t function. Nevertheless, errors from a feasible prefix of an unfeasible path are still taken into account. This includes, in particular, any error that occurs before a deadlock.

W W lock(m) unlock(m) lock(m) unlock(m) R W R R W thread 2 thread 1 (a) Weakly consistent interferences. unlock(m) lock(m) unlock(m) lock(m) W W W R R W R thread 1 thread 2 (b) Well synchronized interferences.

Scheduled Weakly Consistent Memory Semantics P ′ H

In addition to restricting the interleaving of threads, synchronization primitives also have an effect when considering weakly consistent memory semantics: they enforce some form of sequential consistency at a coarse granularity level. More precisely, the compiler and processor handle synchronization statements specially, introducing the necessary flushes into memory and register reloads, and refraining from optimizing across them. We thus adapt the semantics P ′ * of Sec. 3.4 as follows. We consider a transformed thread as a set of paths π ′ (t) obtained from π(body(entry t )) using elementary path transformations from Def. 1, but no transformation should cross any synchronization primitive lock(m), unlock(m), yield or X ← islocked(m). Let π ′ * be defined as before as the interleaving of paths from all π ′ (t). The scheduled weakly consistent memory semantics is, based on [START_REF] Owicki | An axiomatic proof technique for parallel programs I[END_REF]:

P ′ H def = Ω, where (-, Ω) = ✆ H π ′ * ({h 0 } × E 0 , ∅) . (20)

Concrete Scheduled Interference Semantics P C

We now provide a structured version of the scheduled interleaving semantics P H . Similarly to Sec. 3.2, it is based on a notion of interferences, and it is not complete. To avoid considering interferences between parts of threads that are in mutual exclusion, interferences are partitioned with respect to a thread-local view of scheduler configurations. The finite set of configurations C is defined as:

C def = P(M) × P(M) × { weak , sync(m) | m ∈ M }
where the first subset of M denotes the mutexes locked by the thread while the second one denotes the mutexes held by no thread at all (as tested with islocked). The last component in C allows distinguishing between two kinds of interferences, which are depicted in Fig. 4: weakly consistent interferences (weak component in C) corresponding to read / write pairs not protected by mutual exclusion (Fig. 4.(a)), and well synchronized interferences (sync(m) component in C) where both the read and the write are protected by the same mutex m (Fig. 4.(b)). Weakly consistent interferences behave as in Sec. 3.2. For well synchronized accesses, only the last write before unlocking a mutex affects a read, and only until the variable read is overwritten while the mutex is held. The partitioned domain of interferences is then:

I def = T × C × V × R.
The semantics of a variable X read from an environment ρ ∈ E by a thread t is similar to ( 12), but we only apply the weakly consistent interferences from I ⊆ I that are not in mutual exclusion with a current configuration c ∈ C:

E C X (t, c, ρ, I) def = ({ ρ(X) } ∪ { v | (t ′ , c ′ , X, v) ∈ I, t = t ∧ excl (c, c ′ ) }, ∅) where excl ((l, u, s), (l ′ , u ′ , s ′ )) def ⇐⇒ l ∩ l ′ = u ∩ l ′ = u ′ ∩ l = ∅ ∧ s = s ′ . (21)
Other constructions are handled as in (2), where t, c, I are passed unused and unchanged. To handle precisely the islocked primitive in code similar to Fig. 3, it is necessary to represent some relationship between environments and scheduler states. Hence, environments are also partitioned with respect to C, although the third component of configurations is not used and always set to weak . The semantic domain of statements is now D C def = P(C × E) × P(L) × P(I), partially ordered by point-wise set inclusion. The semantics of assignments is similar to that of [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF], applied point-wise to each configuration:

S C X ← e, t (R, Ω, I) def = (∅, Ω, I) ⊔ (c,ρ)∈R ({ (c, ρ[X → v]) | v ∈ V }, Ω ′ , { (t, c, X, v) | v ∈ V })
where (V, Ω ′ ) = E C e (t, c, ρ, I) .

The semantics of synchronization primitives is as follows:

S C lock(m), t (R, Ω, I) def = ({ ((l ∪ { m }, ∅, s), ρ ′ ) | ((l, -, s), ρ) ∈ R, ρ ′ ∈ in(t, l, m, ρ, I) }, Ω, I ∪ { out(t, l, m ′ , ρ) | ((l, u, -), ρ) ∈ R, m ′ ∈ u }) S C unlock(m), t (R, Ω, I) def = ({ ((l \ { m }, u, s), ρ) | ((l, u, s), ρ) ∈ R }, Ω, I ∪ { out(t, l \ { m }, m, ρ) | ((l, -, -), ρ) ∈ R }) S C yield, t (R, Ω, I) def = ({ ((l, ∅, s), ρ) | ((l, -, s), ρ) ∈ R }, Ω, I ∪ { out(t, l, m ′ , ρ) | ((l, u, -), ρ) ∈ R, m ′ ∈ u }) (22) S C X ← islocked(m), t (R, Ω, I) def = ({ ((l, u ∪ m * t , s), ρ ′ [X → 0]) | ((l, u, s), ρ) ∈ R, ρ ′ ∈ in(t, l, m, ρ, I) } ∪ { ((l, u \ { m }, s), ρ[X → 1]) | ((l, u, s), ρ) ∈ R }, Ω, I ∪ { (t, c, X, v) | v ∈ { 0, 1 }, (c, -) ∈ R }) where m * t def = { m } if no thread t ′ > t can lock m, and ∅ otherwise in(t, l, m, ρ, I) def = { ρ ′ | ∀X ∈ V, ρ ′ (X) = ρ(X) ∨ (t ′ , (l ′ , ∅, sync(m)), X, ρ ′ (X)) ∈ I, t = t ′ , l ∩ l ′ = ∅ } out(t, l, m, ρ) def = { (t, (l, ∅, sync(m)), X, ρ(X)) | X ∈ V } .
The functions in(t, l, m, ρ, I) and out(t, l, m, ρ) respectively model entering and exiting a critical section protected by a mutex m in a thread t that also holds the mutexes in l: out collects a set of well synchronized interferences from an environment, while in applies them to an environment. Obviously, lock(m) uses in on m, while unlock uses out. Additionally, X ← islocked(m) creates two partitions: one where X = 1, and one where X = 0 and m is assumed to be unlocked, which is remembered in u. However, the assumption that m is unlocked only stands if the thread cannot be preempted at any point by a higher priority thread locking m, hence the side-condition on m * t -in practice, this condition is checked by remembering in the semantics which locks are issued by each thread; we do not present this for lack of space. Moreover, it stands only until the thread calls a blocking primitive (i.e., lock or yield), which gives the opportunity to a lower priority thread to lock m. Thus, blocking primitives use out to exit critical sections protected by all m ∈ u. Note that by replacing X ← islocked(m) with X ← [0, 1], we would obtain a less precise semantics, but which is also sound for true parallel or non real-time systems. We do not show the semantics of guards and non-atomic statements; they can be derived from (3) easily. The semantics P C of a program has the same fixpoint form as [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]: t∈T let (-, Ω ′ , I ′ ) = S C entry t (), t ({c 0 } × E 0 , Ω, I) in (Ω ′ , I ′ ) [START_REF] Steensgaard | Points-to analysis in almost linear time[END_REF] where the initial configuration is c 0 def = (∅, ∅, weak ) ∈ C. The semantics is sound with respect to that of Secs. 4.2-4.3: Theorem 8. P H ⊆ P C and P ′ H ⊆ P C . As in Sec. 3.4, this semantics is not complete. An additional loss of precision comes from the handling of well synchronized accesses. A main limitation is that such accesses are handled in a non-relational way, hence P C cannot represent relations enforced at the boundaries of critical sections but broken within, while P H can. For instance, in Fig. 3, we cannot prove that Y = Z holds outside critical sections, but only that Y, Z ∈ [START_REF] Adve | Shared memory consistency models: A tutorial[END_REF]2]. This shows in particular that even programs without data-races have behaviors in P C outside the sequentially consistent ones. Yet, we can prove that T = 0, i.e., the assignment to T is free from interference. Our implementation is actually a little smarter than [START_REF] Saraswat | A theory of memory models[END_REF] and uses a modified out that does not consider interferences for variables not modified while m is held. Finally, our implementation can also report data-races by simply inspecting the set of interferences during each assignment.

P C def = Ω,

Abstract Scheduled Interference Semantics P ♯

C

The interference semantics with scheduler P C can be abstracted similarly to P I . As in Sec. 3.3, we assume the existence of two abstract domains E ♯ and N ♯ abstracting respectively P(E) and P(R). We lift these domains by partitioning under C: D ♯ C def = (C → E ♯ ) × P(L) × I ♯ , where abstract interferences are in

I ♯ def = (T × C × V) → N ♯ . The concretization is: γ(R ♯ , Ω, I ♯ ) def = ({ (c, ρ) | ρ ∈ γ E (R ♯ (c)) }, Ω, { (t, c, X, v) | v ∈ γ N (I ♯ (t, c, X)) }).
Sound abstract transfer functions can be derived easily from those in E ♯ and N ♯ . For instance, the assignment is similar to that of Sec. 3.3, except that it is applied point-wise to each R ♯ (c) and it only considers the abstract interferences from the configurations not in mutual exclusion with c. Synchronisation primitives are implemented mostly by joining partitions (using ∪ ♯ E ) and copying non-relational information between E ♯ and N ♯ (for in and out). Transfer functions for non-atomic statements are derived as in [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF]. Finally, the abstract analysis P ♯ C computes a fixpoint over the interferences identical to [START_REF] Lamport | How to make a multiprocessor computer that correctly executes multiprocess programs[END_REF]. The resulting analysis is sound:

Theorem 9. P C ⊆ P ♯ C .
Due to partitioning, P ♯ C is less efficient than P ♯ I . However, partitioned environments are mostly empty: Sec. 5 shows that, in practice, at most program points, R ♯ (c) = ⊥ ♯ E except for a few of configurations. Partitioned interferences are less sparse because, being flow-insensitive, they accumulate information for configurations reachable from any program point. However, this is not problematic: as interferences are non-relational, a large number of partitions can be manipulated efficiently. Thanks to partitioning, the precision of P ♯ C is much better than P ♯ I in the presence of locks and priorities. For instance, P ♯ C can discover that T = 0 in Fig. 3, while the analysis of Sec. 3.3 would only discover that T ∈ [-1, 1] due to spurious interferences from the high priority thread.

Experimental Results

The abstract analysis of Sec. 4.5 has been implemented in Thésée, our prototype analyzer. It analyzes C without recursion nor dynamic memory allocation. It is sound, and checks for integer and float arithmetic overflows, divisions by zero, invalid array and pointer accesses, and assertion failures. It also reports data-races, but ignores other parallel-related hazards. In particular, it does not check for dead-locks nor unbounded priority inversions. In fact, they cannot occur in our target application as all locks have a timeout. Thésée is based on Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], a static analyzer for synchronous embedded C software, which was successfully applied to prove the absence of run-time errors in large critical control/command software from Airbus [START_REF] Delmas | Astrée: from research to industry[END_REF]. Thésée benefited directly from Astrée's numerous abstract domains and iteration strategies targeting embedded C code. The adaptation to the analysis of parallel programs, including the addition of the interference fixpoint iterator and the scheduler partitioning domain, required adding approximately 6 KLines of code to the 100 KLines analyzer, and did not require any structural change.

Our target parallel application is another large program from Airbus consisting of 1.6 MLines of C code and 15 threads. It runs under an ARINC 653 realtime OS [2]. The code is quite complex as it mixes string formatting, list sorting, network protocols (e.g., TFTP), and automatically generated synchronous logic. The program was completed with a 2 500 line hand-written model of the ARINC 653 OS implementing the various API calls, in C enriched with analyzer-specific intrinsics (mutex lock, unlock, etc.).

The analysis currently takes 14h on our 2.66 GHz 64-bit intel server using one core. An important result is that only four iterations are required to stabilize abstract interferences. Moreover, there are a maximum of 52 partitions for abstract interferences and 4 partitions for abstract environments, so that the analysis fits in 32 GB of memory. The analysis generates around 7600 alarms. This high number is understandable: Thésée is naturally tuned for avionic control/command software as it inherits abstract domains E ♯ , N ♯ from Astrée, but the analyzed program is not limited to control/command processing. We started adapting these domains and can already report some improvements compared to earlier experimental results (50h and 12000 alarms [4, § VI]), using the same iterator and scheduler partitioning. However, independently from the choice of abstract domains E ♯ , N ♯ , a better treatment of well synchronized interferences will surely be required to achieve zero false alarms. Following the design-byrefinement of Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], we have focused on the analysis of a single (albeit large and complex) real-life software and started refining the analyzer to lower the number of alarms.

Related Work

There are far too many works on the semantics and analysis of parallel programs to provide a fair survey and comparison here. Instead, we focus on a few works that, we hope, provide a fruitful comparison with ours.

The idea of attaching to each thread location a local invariant and to handle proofs of parallel programs as that of sequential programs with interferences dates back to the Hoare-style proof method of Owicki and Gries [START_REF] Owicki | An axiomatic proof technique for parallel programs I[END_REF] and Lamport [START_REF] Lamport | Proving the correctness of multiprocess programs[END_REF] and has been well studied since (see [START_REF] De Roever | Concurrency Verification: Introduction to Compositional and Noncompositional Methods[END_REF] for a modern account and a partial survey). It has been studied from an Abstract Interpretation point of view in [START_REF] Cousot | Invariance proof methods and analysis techniques for parallel programs[END_REF] and applied to static analysis. Two examples are the analysis of C with POSIX threads by Carré and Hymans [START_REF] Carré | From single-thread to multithreaded: An efficient static analysis algorithm[END_REF] and that of Java with its weak memory model by Ferrara [START_REF] Ferrara | Static analysis via abstract interpretation of the happens-before memory model[END_REF]. Unlike those, we do not handle thread creation, but we do take into account scheduler properties. Fully flow-insensitive analyses, e.g. Steensgaard's popular points-to analysis [START_REF] Steensgaard | Points-to analysis in almost linear time[END_REF], naturally handle parallel programs. Unfortunately, the level of accuracy required to prove safety properties demands the use of (at least partially) flow-sensitive and relational methods, which we do.

Model-checking also has a long history of verifying parallel systems, including recently weak memory models [START_REF] Atig | On the verification problem for weak memory models[END_REF]. Partial order reduction methods [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF] are used to limit the number of interleavings to consider, with no impact on completeness. In contrast, we abstract the problem sufficiently so that no interleaving need to be considered at all, at the cost of completeness. Unlike context-bounded approaches [START_REF] Qadeer | Context-bounded model checking of concurrent software[END_REF], our method considers all executions until completion.

Weakly consistent memory models have been studied mostly for hardware [START_REF] Adve | Shared memory consistency models: A tutorial[END_REF]. Pugh pioneered its use in programming language semantics, culminating with the Java memory model [START_REF] Manson | The Java memory model[END_REF]. It is described in terms of implicit conditions on interleaved execution traces and is quite complex. We chose instead a generative approach based on control path transformations matching closely optimization models, similarly to the work of Saraswat et al. [START_REF] Saraswat | A theory of memory models[END_REF]. Our focus is on models that are realistic and can be abstracted into interference semantics suitable for efficient static analysis.

Conclusion

We presented a static analysis to detect all run-time errors in embedded C software with several threads communicating through a shared memory with weak consistency and scheduled according to strict priorities. Our method is based on a notion of interferences and partitioning with respect to a scheduler state. It can be implemented on top of analyzers for sequential programs, leveraging a growing library of abstract domains. Promising early experimental results on real code demonstrate the scalability of the approach.

A broad avenue for future work is to bridge the gap between the interleaving semantics and its incomplete abstraction in terms of interferences. Abstracting well synchronized accesses in a non-relational way is a severe limitation that we wish to suppress. We also wish to add support for other synchronization primitives, such as condition variables and atomic variables, and exploit more properties of real-time schedulers. A more precise analysis may require the use of history-sensitive abstractions, an avenue we wish to explore. Moreover, more precise or more general interference semantics could be designed by adjusting the notion of weak memory consistency. Finally, we wish, in future work, to analyze errors specifically related to parallelism, such as dead-locks, live-locks, and priority inversions, including quantitative time-related properties (e.g., bounded priority inversions).

Fig. 1 .

 1 Fig. 1. Semantics defined in this paper.

Fig. 2 .

 2 Fig. 2. Incompleteness examples for the interference semantics.

  and ∪ ♯ I and ▽ I defined point-wise. Abstract semantic functions now have the form: S I • ♯ : D ♯ I → D ♯ I with D ♯ I def = E ♯ × P(L) × I ♯ , and the soundness condition becomes:

Fig. 4 .

 4 Fig. 4. Weakly consistent versus well synchronized scheduled interferences.

  where (Ω, -) def = lfp λ(Ω, I).

  : e 1 ⊲⊳ 0?; e 2 ⊲⊳ 0? e 2 ⊲⊳ 0?; e 1 ⊲⊳ 0? when noerror(e 2 ). 5. Reorder guard before assignment: X 1 ← e 1 ; e 2 ⊲⊳ 0? e 2 ⊲⊳ 0?; X 1 ← e 1 when X 1 / ∈ var(e 2 ) and either nonblock(e 1 ) or noerror(e 2 ). 6. Reorder assignment before guard: e 1 ⊲⊳ 0?; X 2 ← e 2 X 2 ← e 2 ; e 1 ⊲⊳ 0? when X 2 / ∈ var(e 1 ), X 2 is local, and noerror(e 2 ). Sub-expression elimination: s 1 ; . . . ; s n X ← e; s 1 [X/e]; . . . ; s n [X/e] when X is fresh, ∀i, var(e) ∩ lval(s i ) = ∅, and noerror(e). 9. Expression simplification: s s[e ′ /e] when ∀ρ, I, E I e (t, ρ, I) ⊒ E I e ′ (t, ρ, I).

	7. Assignment propagation: X ← e; s	X ← e; s[e/X]
	when X / ∈ var(e), var(e) are local, and e is deterministic.
	8.

The lattices used in data-flow analysis and abstract interpretation are dual: the former uses a meet to join paths while we employ a join.

As the set of threads is finite, thread-local variables, such as function locals and parameters, could be handled by duplicating the functions and renaming the variables.

⋆ This work is supported by the INRIA project "Abstraction" common to CNRS and ENS in France.


Emna Salhi
email: emna.salhi@irisa.fr

Samer Lahoud
email: samer.lahoud@irisa.fr

Bernard Cousin
email: bernard.cousin@irisa.fr

Heuristics for Joint Optimization of Monitor Location and Network Anomaly Detection

To reduce monitoring cost, the number of monitors that are to be deployed has to be minimized and the overhead of monitoring flows on the underlying network has to be reduced. In a recent work, we demonstrated, using ILP formulations, that there is a trade-off between these two minimization objectives. However, we have shown that the trade-off could be efficiently balanced by optimizing monitor location and anomaly detection costs jointly. The problem is NP-complete, hence ILPs could not deliver solutions for large networks. In this paper, we address the scalability issues. We propose two greedy algorithms that optimize monitor location cost and anomaly detection cost jointly. The first algorithm is based on an exhaustive heuristic that explores all paths that are candidate to be monitored, in order to select a subset of paths that reduces the total monitoring cost. On the opposite, the second algorithm is based on a selective heuristic that avoids exploring all the candidate paths to further improve scalability. The main challenge of this heuristic is to not degrade the solution quality. The two algorithms have been evaluated through extensive simulations on networks of hundred of billions of paths. The comparison of the solutions delivered by the two algorithms to each other and to the solutions delivered by the ILP demonstrates that the selective algorithm provides near-optimal solutions, while achieving a desirable scalability with respect to the network size and significant reduction of the computation time.

I. INTRODUCTION

One of the highly desired features in network monitoring is to minimize the cost of deploying and maintaining monitoring devices, and reduce communications between the monitoring devices and the Network Operations Center (NOC); while preventing monitoring flows from interfering with real traffic flows. These features could be achieved by minimizing the number of monitors that are to be deployed (e.g. [START_REF] Kumar | Efficient Beacon Placement for Network Tomography[END_REF], [START_REF] Chen | Tomography-based Overlay Network Monitoring[END_REF]), minimizing the number of monitored paths (e.g. [START_REF] Naidu | Detecting Anomalies Using End-to-End Path Measurements[END_REF], [START_REF] Argawal | Diagnosing link-level anomalies using passive probes[END_REF], and avoiding redundant measurements (e.g. [START_REF] Barford | Network Performance Anomaly Detection and Localization[END_REF], [START_REF] Zhao | Towards Efficient Large-Scale VPN Monitoring and Diagnosis under Operational Constraints[END_REF]); respectively. However, we argue that there is an interplay between these objectives. Indeed, reducing the number of monitoring devices and the number of monitoring flows results in monitoring long paths that are quite likely to overlap, which increases redundant measurements. Our previous work [START_REF] Salhi | Joint Optimization of Monitor Location and Network Anomaly Detection[END_REF] illustrated this conflictual aspect through ILP formulations. We proposed a monitoring cost model that includes a monitor location cost and an anomaly detection cost. Simulation results demonstrated that a joint optimization of the two costs reduces efficiently their trade-off. However, the problem is NP-complete, and hence, solutions can not be found for large networks using ILPs. Typically, to overcome scalability issues, the set of candidate paths that are to be monitored is restrained to a small subset. Unfortunately, none of the related works investigated the impact of this restriction on the quality of the monitoring solution neither did they specify how to choose the set of candidate paths. In this paper, we further investigate these issues. Acknowledging the efficiency of the joint optimization model to balance the trade-off between the multiple minimization objectives [START_REF] Salhi | Joint Optimization of Monitor Location and Network Anomaly Detection[END_REF], we keep on considering this technique to devise novel greedy algorithms. The aim is to come up with large-scale heuristics that apply for large networks and achieve good quality solutions. The first algorithm that we call exhaustive greedy algorithm starts by selecting a pair of monitor locations that maximizes the number of covered links; and then it explores all paths between the selected monitors, in order to choose a set of paths that maximizes the number of links it can cover and minimizes redundant measurements. Additional monitors and paths are selected iteratively in order to reduce the number of overlaps among paths that are to be monitored, thereby reducing the cost of the solution. The second algorithm that we call selective greedy algorithm is based on a heuristic that minimizes drastically the number of explored paths. The underlying idea is to choose a set of non-overlapping paths that maximizes link coverage, and then select additional paths and potentially additional monitors to cover the remaining links. The paths of this set should be long enough to increase the number of covered links. However, we do not require them to be the longest paths of the network. This relaxation avoids exploring all paths between selected monitors. We perform an in depth-first order exploration of the network to find long enough paths between the considered monitors quickly. This would reduce the computation time and improve the scalability of the algorithm. However, this heuristic should not worsen the quality of the solution. To investigate this issue, we compare this algorithm to the exhaustive algorithm and to the ILP through extensive simulations. Results demonstrate that the selective algorithm provides solutions quite close to the exact solutions. Furthermore, it outperforms the exhaustive algorithm and the ILP in terms of computation time and scalability.

II. PROBLEM FORMULATION

The main notations used in the paper are reported in TABLE I. The network topology is represented as a undirected graph G = (N, E) comprising a set of nodes N connected by links in E. Let P be the set of network paths. Unless mentioned, the set of monitor locations, i.e. candidate locations where to deploy monitors, is the set of network nodes N ; and the set of paths that are candidate to be monitored is the set of network paths P . Let Cl l be the cost of monitoring link l and Cm n the cost of monitoring node n. The link monitoring cost expresses the cost of injecting monitoring flows throughout the link. It should be proportional to the load of the link, in order to balance fairly the monitoring load over all the network links. The monitor location cost expresses the effective cost of deploying hardware and software monitoring devices on the selected location. This cost should include also the distance of the location to the NOC, in order to reduce the communications between the monitors and the NOC. The cost of monitoring a path equals the sum of its individual link monitoring costs. The total monitoring cost is expressed as follows:

Total Monitoring Cost = ∑ l∈E,p∈P Cl l δ lp Z p + ∑ n∈N Cm n Y n (1)
The above cost is the cost of locating monitoring devices and detecting link-level network anomalies. We note that, in this work, we are not interested in the localization of anomalies. We adopt a two-phase monitoring approach that decouples the localization task from the detection task. Acknowledging the claim that network anomalies are rare events [START_REF] Naidu | Detecting Anomalies Using End-to-End Path Measurements[END_REF], the efficiency of this two-phase approach lies in the minimization of network usage when the network performs normally, i.e. during the detection phase. In this work, we are interested in selecting a set of monitor locations and and a set of paths to be monitored that can cover all the network links. The challenge is to reduce jointly the number of monitors to be deployed and the load of monitoring flows on the underlying network. We come up with two greedy algorithms that address this problem. The aim is to find largescale heuristics that achieve low-cost solutions and reduce the computation time. The two algorithms will be compared to each other, and to the exact solution of the problem formulated in [START_REF] Salhi | Joint Optimization of Monitor Location and Network Anomaly Detection[END_REF], in order the assess their efficiency.

III. HEURISTICS

In this section, we describe two greedy algorithms inspired from the monitoring cost model introduced in [START_REF] Salhi | Joint Optimization of Monitor Location and Network Anomaly Detection[END_REF]. The aim of the algorithms is to optimize jointly the cost of monitor location and the cost of network anomaly detection. The first algorithm is based on an exhaustive heuristic that explores all the network paths; whereas the second algorithm is based on selective heuristics that address scalability issues by reducing the number of explored paths. The challenge is to improve scalability without negatively impacting the solution quality. The length of path p in number of links nbOverlaps(p)

The number of overlaps of p with paths in SP and T P nbCL

The number of links covered by paths in SP nbT CL

The number of links temporary covered by paths in T P nbOverlaps

The number of overlaps among paths in SP and T P Cm n

The cost of deploying a monitor on node n Cl l

The cost of monitoring link l Z p A binary variable that indicates wether path p is selected to be monitored Y n

A binary variable that indicates wether node n is selected as a monitor location δ lp A binary parameter that indicates wether link l belongs to path p

A. Exhaustive Greedy Algorithm

Algorithm 1 describes the exhaustive algorithm. The aim of the algorithm is to select a set of monitor locations and a set of paths to be monitored that cover all the network links in a way that minimizes the number of monitors and reduces overlaps among monitored paths. This algorithm is a two-step nested algorithm. -First step: It selects a monitor location. This is done by adding the end-node of a path that has its other end-node selected as monitor location, and maximizes the term # newly covered links -# of links already covered. We can also take into consideration the distance of monitors to the NOC in order to privilege the nearest monitors, thereby reducing the communication cost.

-Second step: it greedily selects paths to be monitored between the monitor added at the first step and monitors previously selected. At each iteration, a path that maximizes the term # newly covered links -# of links already covered is selected. The second step ends when all the network links are covered or when there are no more paths that can cover links that are not yet covered. These two nested steps are re-iterated greedily until adding a new monitor does not improve the best solution obtained over the previous iterations. We expect that this algorithm performs well for small and sparse networks, because it explores all monitor locations and all paths between the new monitor and the previously selected monitors in order to select the best items. This leads to select few paths and monitors that achieve a full link coverage, and reduces redundant measurements. However, for the same reasons, the algorithm is not expected to scale for large and highly meshed networks where the number of paths between a pair of nodes increases drastically. An obvious heuristical improvement of this algorithm would be to relax the first step by randomly choosing a monitor location. This would avoid exploring all paths having one of their end-nodes selected as monitor, however, we still have to explore all paths between the newly added monitor and the previously added monitors in order to choose a path that achieves a good balance between the number of links it covers and the number of redundant measurements it yields. Let n be the end node of p that is not in SM 23:

CP ← {all paths having one of their end nodes n and the other one in SM }\{p} 24:

Add n to SM 25:

Go to step 6 26: else 27:

END OF THE ALGORITHM 28: end if

B. Selective Greedy Algorithm

As mentioned above, the main challenge we are facing is scalability concerns with respect to the number of candidate paths. Our purpose is to come up with new heuristics that reduce the number of explored paths without worsening the of the solution. We propose a two-stage greedy algorithm. The first stage selects two monitor locations and then selects a set of non-overlapping paths that maximize link coverage. The second stage selects additional paths and monitors in order to cover the remaining links. For the first stage, we provide a heuristic that avoids exploring all paths between the selected monitors. For the second stage, we provide a heuristic that minimizes jointly the number of monitors and redundant measurements, thereby reducing the total monitoring cost. end while 35: end for Stage 1: it selects a set of disjoint paths between a pair of monitors. The aim is to cover as much links as possibile without generating overlaps among selected paths. This problem can be viewed as a maximum set packing problem [START_REF] Feige | Interactive proofs and the hardness of approximating cliques[END_REF]. The maximum set packing problem is the problem of selecting the maximum number of pairwise disjoint sets among the input sets. This problem was shown to be NP-complete [START_REF] Feige | Interactive proofs and the hardness of approximating cliques[END_REF]. In our case, the set of paths between the considered monitors maps to the input sets and the elements are the network links. This formal complexity proof of the problem justifies our proposal of an approximative heuristic. The key idea is to select iteratively a path having its end nodes selected as monitors, remove links that are covered by the selected path from the network graph, and then re-iterate. The selected paths must cover the maximum number of links.

Algorithm 2 Selective Greedy Algorithm

A good heuristic would be to select, at each iteration, the longest path. However, such a heuristic requires exploring all paths between the considered monitors, and subsequently yields serious scalability issues. Alternatively, our heuristic selects at each iteration a "good path". By "good path" we mean a path that is not necessarily the longest path, but it is a long path which computation do not require exploring a large number of network paths. An efficient solution is to explore the network graph in an in depth-first order between the considered monitors. The first stage ends no more paths can be constructed between the considered monitors.

Stage 2: by the end of the first stage we get two deployed monitors, a set of disjoint paths to be monitored and a set of uncovered links. This stage aims at covering these uncovered links by selecting more paths and potentially deploying more monitors in a way that reduces jointly the number of monitors and redundant measurements. The algorithm proceeds by computing the longest path composed of only uncovered links, say p ul . For the two end nodes of the computed path, it proceeds as follows. If the end-node is not already selected as monitor then it computes a path segment, say p, from this node to one of the selected monitors, that minimizes the term: length(p) -# links of p that are uncovered. The idea is to choose a path segment that maximizes the number of uncovered links and minimizes the number of redundant measurements. Now if the cost of redundant measurements generated by p dominates the cost of deploying a monitor at the end-node, then a monitor will be deployed at the end-node and p will be dropped, otherwise p will be concatenated to p ul . Links covered by p ul are removed from the set of uncovered links, and the process is re-iterated until the set of uncovered links is empty.

IV. PERFORMANCE EVALUATION

In this section, we describe first the methodology of our evaluation, then we show and analyze our results.

A. Evaluation Methodology

Extensive simulations on random topologies generated using the topology generator BRITE (AS level, Waxman model) [9] was conducted on a PC equipped with a 2,992.47 MHz Intel(R) Core(TM)2 Duo processor and 3.9 GB of RAM. A summary of the characteristics of the topologies considered in our evaluation is depicted in TABLE II. All results are the mean over 20 simulations. The aim of the evaluation is to investigate the efficiency of our heuristics. Namely, we 1) implemented the two proposed algorithms and compared the solutions they delivered in order to verify their scalability with respect to the network size, and the impact of the selective heuristics on the quality of the solutions; 2) compared the solutions delivered by the algorithms to the exact solutions delivered by the path-based ILP [START_REF] Salhi | Joint Optimization of Monitor Location and Network Anomaly Detection[END_REF], in order to investigate the gap of the greedy solutions to the optimal; and also 3) relaxed the path-based ILP formulation to a linear program, solved the LP, performed a random rounding of the LP results and then took the results as an input for the exhaustive greedy algorithm. The LP results constitutes a good starting point for the greedy algorithm and reduces the number of candidate paths and candidate monitors, that is why we consider the use of the LP results in combination with the greedy algorithm. In our evaluation, we considered a centralized active monitoring infrastructure, where the NOC have a global view of the network topology. The cost of deploying monitors was set equal to the cost of monitoring links, i.e. Cl l = Cm n = 1 ∀l, n.

We refer to the exhaustive greedy algorithm as GA-1.1, to the exhaustive greedy algorithm with random selection of monitors as GA-1.2, to the selective greedy algorithm as GA-2, and to the path-based ILP formulation as ILP. We denote by LP-assisted greedy algorithm the exhaustive greedy algorithm applied on the results of the LP.

B. Simulation Results

TABLE III depicts the CPU computation time versus the network topology for the five approaches. Results show that the ILP formulation does not deliver a solution for topologies with 10 nodes and 31 links, and larger due to memory concerns; whereas GA-1.1 and the LP-assisted greedy algorithm suffer memory concerns for networks with 12 nodes and 41 links, and larger. This is because these approaches handle a large set of candidate paths, and hence do not scale for meshed networks. Note that the computation time of the LP-assisted greedy algorithm increases exponentially. TABLE III shows that the resolution of GA-1.1 takes less than 4 seconds of CPU time for these topologies. This means that the resolution of the LP takes quite a long time for average networks and shows serious scalability concerns for large networks. However, in a future work, we will focus on this issue, and propose an efficient solution to resolve the linear relaxations of the ILP formulations proposed in [START_REF] Salhi | Joint Optimization of Monitor Location and Network Anomaly Detection[END_REF].

Further, we note that the random selection of monitors improves slightly the scalability of the exhaustive algorithm. Indeed, we got a solution for topologies (12, 41) in about 10 seconds. However, as discussed previously, this improvement does not hold for highly meshed networks. As expected, the selective greedy algorithm succeeds to overcome the memory insufficiency problem, and delivers solutions for all the considered topologies in quite a short time, e.g. 177 seconds for the largest networks. Now, we investigate the quality of the solutions. For this purpose, we compute the total monitoring cost as given in [START_REF] Salhi | Joint Optimization of Monitor Location and Network Anomaly Detection[END_REF]. Simulation results for the five approaches and the 8 considered topologies are depicted in TABLE IV. This metric illustrates the cost gap between the different approaches and shed light on the impact of the selective heuristics on the quality of the solution. Surprisingly, the selective algorithm performs better than the exhaustive algorithm and the LP-assisted greedy algorithm, although it does not explore all the network paths. This is because, the selective algorithm starts by covering the maximum number of paths using only 2 monitors and without generating redundant measurements, and then, it balances the load between monitors and links while covering the remaining links. Furthermore, for small networks, the gap between the exact solutions of the ILP and the solutions of the selective algorithm is negligible. Lacking of results for large networks for the four first approaches to be compared to the solutions of the selective algorithm, we plotted in Fig. 1 the percentage of network usage for this algorithm in order to validate its efficiency for large networks. The percentage of network usage is computed as follows: ) * 100 Fig. 1 shows that the percentage of network usage decreases when the network size increases. This could be explained by the fact that when the number of paths increases, we get more candidate paths, which increase the possibility to reduce the number of overlaps among monitored paths using few monitors. We note that the percentage of network usage increases slightly for TOP(30, 120) and then it remains constant for TOP(50, 250), although the number of links and the number of paths have doubled. This demonstrates that the selective algorithm scales well with respect to the network size, and specifically the number of network paths. V. CONCLUSION

In this paper, we proposed novel greedy algorithms for joint optimization of monitor location and network anomaly detection. Our main goal was to come up with large-scale heuristics that reduce the overall monitoring cost. We evaluated our algorithms on networks with hundred of billions of paths. Results show that the selective algorithm outperforms the exact approach, i.e. the ILP, and the exhaustive algorithm in terms of scalability and computation time. Furthermore, it provides near-optimal solutions for small networks, and tends to decrease the percentage of network usage when the network size gets larger. Our ongoing work is on extending our monitoring cost model and our heuristics to multi-domain networks.

Fig. 1 .

 1 Fig. 1. Resource Usage for GA-2

  Algorithm 1 Exhaustive Greedy Algorithm 1: p ← the longest path of the network 2: Add the end nodes of p to SM 3: CP ← {all paths between nodes in SM }\{p} 4: Add p to SP 5: nbCL ← length(p) 6: Select a path p in CP ∪ BP that maximizes length(p) -CP ← CP \ {p} 16: if (not all links are covered OR the solution can be improved) then

		nbOverlaps(p)
	7: if ( nbOverlaps(p) == 0 ) then
	8:	Add p to SP
	9:	nbCL += length(p)
	10: else
	11:	Add p to T P
	12:	nbT CL += length(p) -nbOverlaps(p)
	13:	nbOverlaps += nbOverlaps(p)
	14: end if
	15: 17:	BP ← T P
	21:	update SP, TP, nbOverlaps, nbCL and nbTCL (Steps
		7-14)
	22:

18:

Resert T P , nbT CL and nbOverlaps 19: CP ← {all paths having one and only one of their end nodes in SM } 20: Select a path p in CP that maximizes length(p) -nbOverlaps(p)

1 :

 1 for all (n1, n2) ∈ N 2 do

	2:	Reset SM , SP , nbOverlaps, L
	3:	Add n1 and n2 to SM
	4:	CP ← {all paths between n1 and n2}\{paths between
		n1 and n2 crossing links in L}
	5:	while ( CP ! = ∅ ) do
	6:	Select a "good path" p in CP
	7:	Add p to SP
	8:	L ← L\{links of p}
	9:	update CP (step ?)
	10:	end while
	11:	while ( L ! = ∅ ) do
	12:	let p = {i..k..j} be the longest path composed of
		links in L
	13:	if ( i / ∈ SM ) then
	14:
	16:	p 1 ← N U LL
	17:	Add i to SM
	18:	else
	19:
	21:	end if
	22:	end if
	23:	if ( j / ∈ SM ) then
	24:
	26:	p 2 ← N U LL
	27:	Add j to SM
	28:	else
	29:
	31:	end if
	32:	end if
	33:	Add concatenate(p 1 , p, p 2 ) to SP
	34:

compute a path p 1 between i and a node in SM that minimizes length(p 1 ) -

#links of p 1 in L 15: if ( (#links of p 1 in L) * C l > C m ) then nbOverlaps + = #links of p 1 in L 20: L ← L\{links of p 1 }

compute a path p 2 between j and a node in SM that minimizes length(p 2 ) -#links of p 2 in L 25: if ( #links of p 2 in L * C l > C m ) then nbOverlaps + = #links of p 2 in L 30: L ← L\{links of p 2 }

This work has been supported by Alcatel-Lucent Labs France, under the grant n. 09CT310-01