Thomas Mari

Thao Dang

Gregor Gössler

Explaining Safety Violations in Real-Time Systems

Keywords: causal explanations, real-time, safety Explications causales, temps réel, sûreté

We tackle the problem of explaining faults in real-time systems. Intuitively, an explanation of the violation of a safety property by an execution is a concise excerpt of the faulty execution that retains only the elements that were relevant for entailing the violation, thus exhibiting how causes accumulate over time and propagate to entail the effect. Fault explanation therefore goes beyond the well-known concepts of fault diagnosis and localization. We provide a formal definition of causal explanations on dense-time models, based on the wellstudied formalisms of timed automata and zone-based abstractions. Our approach is able to account for limited observability of the faulty execution. We propose a symbolic formalization to effectively construct such explanations, which we have implemented in a prototype tool. We illustrate our approach on several examples.

Introduction

Embedded real-time systems have been part of our daily lives for several decades now, and the number of such devices is growing exponentially. There is a rich body of work on software engineering, formal verification, and certification of such systems. However, when looking at the headlines about failures and casualties caused by embedded systems, one may wonder whether we have learned to fully master their growing complexity.

As a complementary approach, accountability aims at constructing systems in such a way that the responsibilities for a failure can be identified and explained post mortem [START_REF] Küsters | Accountability: definition and relationship to verifiability[END_REF]. Intuitively, an explanation is a concise excerpt of the observed execution that retains only the elements that were relevant for entailing the violation. However, formalizing this objective is far from obvious, and different communities have tackled the problem under different angles.

A first challenge consists in conveying the "right" amount of information, e.g., in order to help a human expert in quickly understanding the causes of the violation, or to automatically react to the failure by swapping a component or changing parameters. In this work we are interested in causal explanations that allow us to track the chains from cause to effect while eliminating irrelevant events from the explanation.

A second challenge is to devise explanations that satisfy the requirements of embedded systems. First, embedded real-time systems usually have an infinite state space, requiring reasoning on an appropriate abstraction. Nevertheless, research on reasoning about causation on abstractions is only in its infancy [START_REF] Beckers | Approximate causal abstractions[END_REF][START_REF] Gössler | Causality analysis and fault ascription in component-based systems[END_REF]. Second, explanations for embedded systems have to cope with the limited observability of state and events, which is again an issue that is hardly addressed in existing work on causation.

The work presented in this paper is part of an ongoing effort to construct explainable embedded real-time systems. We investigate how to construct, from a system model, a safety property, and an execution log that violates the property, a concise explanation of how the log brought about the violation of the property.

This paper makes the following contributions. We provide a formal definition of causal explanations on dense-time models, based on the well-studied formalism of timed automata. We propose a symbolic approach to effectively construct explanations. We illustrate our approach on several examples and a case study.

Related Work

Causal explanations. Our construction of choice explanations is based on effective choice explanations for discrete-event systems [START_REF] Gössler | Towards Causal Explanations of Property Violations in Discrete Event Systems[END_REF]. The latter are, in turn, inspired by [START_REF] Jin | Fate and free will in error traces[END_REF], which leverages game theory to explain counterexample traces from model-checking by exhibiting the portions of the trace in which the system could have avoided the violation of an expected property no matter how the environment behaves.

Several authors have proposed a construction of explanations for the satisfaction of a property P by an execution trace based on sub-sequences of the trace that are sufficient to entail P , such as explanatory diagnoses [START_REF] Mcllraith | Explanatory diagnosis: Conjecturing actions to explain observations[END_REF] and causal compression [START_REF] Danos | Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models[END_REF]. However, in contrast to our approach, subsequence explanations do not convey any information about the outcome produced by alternative branches in a non-deterministic system.

Static program slicing [START_REF] Weiser | Program slicing[END_REF] determines a part ("slice") of a program that influences a set of variables at a given point. Dynamic slicing [START_REF] Korel | Dynamic program slicing[END_REF] computes a slice for a given computation, yielding a smaller slice. In contrast to slicing, our approach accounts for counterfactual runs that have not been taken in the actual execution.

Fault diagnosis, localization, and repair. Counterfactual causation has been studied in many disciplines as a precise assessment of individual causes that contribute to bring about an effect, see e.g. the influential definition of actual causality in [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF]. Some form of counterfactual reasoning has been used by many authors to diagnose, localize, and repair faults. We only cite some representative examples here. As these approaches exhibit individual causes rather than chains from cause to effect, they are less apt to explain how contributory causes accumulate over time and propagate to entail an effect. The seminal work of [START_REF] Reiter | A theory of diagnosis from first principles[END_REF] proposes a framework of model-based fault diagnosis that defines a diagnosis as a minimal sets of components whose faults make the observations consistent with the system model. The use of a distance metric is explored in [START_REF] Groce | Error explanation with distance metrics[END_REF] to localize, based on an error trace, a possible fault as the difference between the error trace and a closest correct trace. Similarly, Delta debugging [START_REF] Zeller | Why Programs Fail[END_REF] starts from a failing and a passing input and finds a pair of a failing and a passing input with minimal distance. A variant of actual causality is used in [START_REF] Beer | Explaining counterexamples using causality[END_REF] to over-approximate the set of causes for the first violation of an LTL formula by a trace. The goal of program repair is, given a program that violates an expected property P , to construct a syntactically close program that satisfies P , see e.g. [START_REF] Von Essen | Program repair without regret[END_REF] for the repair of reactive programs. Closer to our setting, [START_REF] Kölbl | Clock bound repair for timed systems[END_REF] uses MaxSMT to repair clock bounds in a network of timed automata so as to ensure an expected property.

In contrast to the pieces of related work cited above that are based on some form of model to compare the actual execution with counterfactual traces, many recent techniques summarized under the umbrella term of explainable AI lack a model and hence, the possibility of counterfactual reasoning [START_REF] Pearl | Theoretical impediments to machine learning with seven sparks from the causal revolution[END_REF].

Preliminaries

Let C be a set of clock variables that take values in R + . A C-valuation is a function C → R + . Let 0 denote the C-valuation assigning 0 to all clocks. An atomic constraint on C is an inequality c ∼ k or c -c ∼ k where c, c ∈ C, ∼ ∈ {≤, <, ≥, >} and k ∈ N. We say that a C-valuation v satisfies an atomic constraint c ∼ k

(or c-c ∼ k) if v(c) ∼ k (or v(c)-v(c ) ∼ k). A C-constraint
is a finite conjunction of all atomic constraints on C. Let C denote the set of C-constraints. By abuse of notation, we use a C-constraint interchangably with the sets of C-valuations that satisfy it.

Definition 1 (Timed Automaton). A timed automaton (TA) A is a tuple A = Σ, L, L 0 , C, F, I, E where • Σ is a finite set of events;

• L is a finite set of locations;

• L 0 ⊆ L is the set of initial locations; • C is a set of clock variables;
• F ⊆ L is a set of accepting locations;

• I : L → C specifies for each location an invariant;

• E ⊆ L × C × Σ × 2 C × L is a set of edges of the form e = , g, σ, X,
where and are respectively source and target locations; σ is an event; g is the guard of e; and X is a set of clocks to be reset when the edge is traversed.

To account for the fact that some events are not observable, the set Σ of events is partitioned into two subsets of observable and unobservable events.

We formalize the semantics of timed automata using labeled transition systems, or LTS. An LTS is a tuple Σ, V, E, V 0 , V F where Σ is the alphabet, V is a set of nodes, E ⊆ V × Σ × V is the set of labeled transitions, and V 0 ⊆ V and V F ⊆ V are the sets of initial and accepting nodes, respectively. For ν ∈ V let ν • = {ν ∈ V | ∃σ ∈ Σ : (ν, σ, ν ) ∈ E} be the postset of ν. In the following we use the terms LTS and graph interchangeably.

Definition 2 (Semantic LTS). The semantic LTS of a timed automaton A = Σ, L, L 0 , C, F, I, E is the LTS sem(A) = Σ , V, E, V 0 , V F where • Σ = Σ ∪ R + is the set of labels; • V = {( , v) | ∈ L ∧ v ∈ I( )}, i.
e. the states of A are the pairs ( , v) where v ∈ I( ) is a clock valuation that satisfies the invariant of the location ;

• V 0 = {( , v) ∈ V | ∈ L 0 ∧ v = 0};
• V F = V (indeed the accepting states do not matter);

• the set of transitions are of two types, discrete and time transitions:

E = (( , v), σ, ( , v )) | ∃g, X : , g, σ, X, ∈ E ∧ v = v[X := 0] ∧ v ∈ I( ) ∪ ( , v), δ, ( , v ) | δ > 0 ∧ v = v + δ ∧ v ∈ I( )
The states ( , v ) and ( , v ) are respectively called e-successor δ-successor of ( , v).

As usual we write ( , v)

• - → ( , v ) for ( , v), •, ( , v ) ∈ E.
By abuse of notation we omit the curly braces in {ν 0 } when there is a single initial state. Note that since δ is a real number, a time transition ( , v) δ -→ ( , v ) can be split into an arbitrary number k of time transitions, that is, ( , v)

δ1 -→ ( , v 1 ) δ2 -→ ( , v 2 ) . . . δ k -→ ( , v k ) such that δ = δ 1 + δ 2 + . . . + δ k .
Definition 3 (Runs and Traces). Let G = Σ, V, E, V 0 , V F be an LTS.

• A run of G starting from ν 1 ∈ V is a (finite or infinite) sequence of states and transitions:

ρ = ν 1 e1 -→ ν 2 e2
-→ . . .. We denote by Υ(G) the set of all runs of G. A state ν is reachable if there is a run from an initial state to ν.

• Given a run ρ ∈ Υ(G), the sequence of labels in ρ is called trace. We denote by Ψ(G) the set of all traces of G.

Definition 4 (Timed Log). A timed log is a one-clock, deterministic and acyclic TA. In addition, all the events of the automaton are observable.

An example of timed log is a timed automaton roughly depicted as follows:

l 0 x=t0,a,∅ -----→ l 1 x=t1,b,∅ -----→ l 2 x=t2,a,∅
-----→ l 3 , with l 3 as an accepting location and l 0 an initial location. The edge from the location l 0 to the location l 1 has the guard x = t 0 ; its event is a; and its set of clocks to be reset is empty.

As mentioned in the introduction, we are interested in explaining why a system, modeled as a timed automaton A, violates a safety property. To this end, we define a safety property observer as a timed automaton with one sink state, to model the property violation of a timed log. In addition, this observer is required to be receptive with respect to all observable events of A, as defined in the following. An LTS Σ, V, E, V 0 , V F is receptive over Σ 1 ⊆ Σ if at every reachable state ν, all events in Σ 1 are enabled, that is, ∀σ ∈ Σ 1 ∃ν : ν σ -→ ν . Given a timed log L and a safety property observer P, we say that L violates the safety property at hand if each run of L is a run of P that reaches the sink state.

The sets of states and transitions of a timed automaton are infinite, and therefore, as in verification, finite abstractions can be used to construct explanations. In this work, we use timeabstracting bisimulations to abstract away the quantitative information about time lapses in the execution of a timed automaton. This leads to finite discrete abstractions of the original timed automata from which we can compute choice-based explanations [START_REF] Gössler | Towards Causal Explanations of Property Violations in Discrete Event Systems[END_REF]. The following definition is adapted from [START_REF] Tripakis | Analysis of timed systems using time-abstracting bisimulations[END_REF] so as to distingluish events, and accepting vs. non-accepting states.

Definition 5 (Strong bisimulations). A binary relation ∼ on an LTS

G = Σ, V, E, V 0 , V F is a
strong bisimulation if for any pair of nodes p and q of G such that p ∼ q, the following conditions hold:

• ∀σ ∈ Σ ∀p ∈ V : p σ -→ p =⇒ ∃q : q σ -→ q ∧ p ∼ q ;
• the above condition also holds when p and q are swapped;

• p ∈ V F ⇐⇒ q ∈ V F .
When G is the semantic LTS of a TA, the relation ∼ is a strong time-abstracting bisimulation (STAB) if for any pair of nodes p = 1 , v 1 and q = 2 , v 2 of G such that p ∼ q, the following conditions hold:

• 1 = 2 ; • ∀σ ∈ Σ \ R + ∀p ∈ V : p σ -→ p =⇒ ∃q : q σ -→ q ∧ p ∼ q ; • ∀δ > 0 ∀p ∈ V : p δ -→ p =⇒ ∃δ > 0 ∃q : q δ -→ q ∧ p ∼ q ;
• the above conditions also hold when p and q are swapped;

• p ∈ V F ⇐⇒ q ∈ V F .
We use STAB, implemented in Minim [START_REF] Tripakis | Analysis of timed systems using time-abstracting bisimulations[END_REF], to construct a finite symbolic abstraction of TA. We then reduce the latter with respect to strong bisimulation so as to merge bisimilar states involving different locations.

Explanations

Our goal is to explain, for a TA A modelling a system, an observer P of a safety property, and a timed log L of observable events of A that violates P, how the violation came to happen. More precisely, in this work, we focus on non-deterministic choices in the execution that entailed the failure, where different choices would have helped to avoid it. Prominent of such failures are "concurrency bugs" that only occur in certain interleavings of threads, and deadline misses due to bad scheduling decisions in real-time systems.

To construct such explanations for real-time systems, we lift the effective choice explanations formalized in [START_REF] Gössler | Towards Causal Explanations of Property Violations in Discrete Event Systems[END_REF] to timed automata. The main steps of our construction, as shown in Figure 1, are the following.

1. Construct a timed log observer L c from L that tracks, for any run ρ of L c , whether the observable behavior of ρ produces L. 2. Compose A, P, and L c to form a timed automaton A||P||L c , where is the standard parallel composition of timed automata, see e.g. [START_REF] Yovine | KRONOS: A verification tool for real-time systems[END_REF].

Inria model A observer P log L A||P||L c observer L c abstraction [A||P||L c ] subgraph G i levels of choice ξ explanation E i
3. Construct a discrete abstraction [A||P||L c ] of the continuous-time semantics of A||P||L c , using a time-abstracting bisimulation.

4. Compute the levels of choice on [A||P||L c ] that, intuitively, represent, for each equivalence class q ∈ [A||P||L c ], the number of bad choices ξ(q) left before violating P.

Extract, from [A||P||L c

], a sequence of subgraphs G i representing the traces that will be condensed to an explanation of length i.

6. Abstract away, from each G i , all transitions that do not decrease ξ, in order to obtain the explanation E i that retains only those (discrete or timed) transitions that contributed to the failure.

We will now discuss each of these steps.

Log observer.

Given an alphabet Σ and a timed log L over the observable alphabet Σ obs ⊆ Σ, we construct a log observer that accepts all runs over Σ and enters an accepting sink state whenever an observed behavior is inconsistent with the log.

Definition 6 (Log observer). The observer of a log L = Σ, L, L 0 , C, F, I, E is the TA L c := Σ, L , L 0 , C, F, I , E where

• L = L ∪ {sink} where sink / ∈ L is a fresh location;

• I = I ∪ {sink → true};

• E = E ∪ E 1 ∪ E 2 where -E 1 = { C( ,σ),σ,∅ ------→ sink | ∈ L ∧ σ ∈ Σ} where C( , σ) = ¬ {g | ∃ ∈ L : g,σ,• ---→ }. -E 2 = {sink true,σ,∅ -----→ sink | σ ∈ Σ}.
Intuitively, E 1 is the set of edges from a location in L that are not consistent with L, used to make the log observer receptive with respect to Σ obs .

Discrete abstraction.

To obtain discrete abstractions for the timed automaton A||P||L c , we use the STAB of Definition 5. Let us briefly recall the notion of time-abstracting quotient graph [START_REF] Tripakis | Analysis of timed systems using time-abstracting bisimulations[END_REF]. Given a TA over alphabet Σ with semantic LTS G = Σ ∪ R + , V, E, V 0 , V F and a partition Ṽ of V, the quotient of G with respect to Ṽ is the LTS G/ Ṽ = Σ , Ṽ, E , Ṽ0 , ṼF where • Σ = Σ ∪ {δ} where δ is a fresh symbol;

• E = {ν σ -→ ν | (ν, σ, ν ) ∈ E ∧ σ ∈ Σ} ∪ {ν δ -→ ν | ∃t > 0 : (ν, t, ν ) ∈ E}; • Ṽ0 = {ν | ν ∈ V 0 } and ṼF = {ν | ν ∈ V F }
and for ν ∈ V, ν denotes the element of Ṽ for which ν ∈ ν.

In particular, we are interested in the quotient with respect to the equivalence classes of states, called symbolic states, induced by STAB. Let [A||P||L c ] := A||P||L c /∼ be the quotient graph with respect to STAB. This quotient graph can be computed by the existing timed automata model-checkers, such as UPPAAL and Kronos [START_REF] Yovine | KRONOS: A verification tool for real-time systems[END_REF][START_REF] Larsen | Uppaal in a Nutshell[END_REF]. In this work, we use the tool Minim [START_REF] Tripakis | Analysis of timed systems using time-abstracting bisimulations[END_REF] integrated in Kronos.

Levels of choice.

In the following, we compute the level of choice on [A||P||L c ]. Intuitively, the level of choice measures how close the system is to violating the required safety property. 4. Maximality: ξ is maximal among the functions fulfilling the preceding conditions.

Definition 7 (Level of choice). Given an LTS

G = Σ, V, E, V 0 , V F , we say that ξ : V → N∪{∞} is the level of choice function if: 1. ∀ν ∈ V F : ξ(ν) = 0 2. ∀ν ∈ V such that ν is not co-reachable, ξ(ν) = ∞

Definition 8 (Effective choice). Given an LTS

G = Σ, V, E, ν 0 , V F and a level of choice function ξ : V → N ∪ {∞}, a transition s e -→ s ∈ E is an effective choice transition iff ξ(s) = 1 + ξ(s ) and ∃ρ = s e0 -→ s 1 e1 -→ ...s n ∈ run(G) such that ξ(s n ) = 0 and (max s∈ρ ξ(s)) = ξ(s ).
When such a transition exists, the state s is called an effective choice state.

Intuitively, an effective choice transition is a transition that decrements the level of choice and is prefix of a run ρ violating P along which the level of choice no longer exceeds ξ(s ).

Lemma 1. Let G = Σ, V, E, V 0 , V F and ξ the level of choice of G. Let V C = ν ∈ V | ξ(ν) ∈ N \ {0} ∧ ξ(ν) = 1 + min{ξ(ν ) | ν ∈ ν • } and V N C = ν ∈ V | ξ(ν) ∈ N \ {0} \ V C . Then E ∩ (V N C × Σ × V N C ) is acyclic.

Inria

All successors of ν are also at level n, and at least one, let us call it ν min , is strictly closer to V C n wrt d, than ν. We have either ν min ∈ V C n or (∀ν min ∈ V, ν min ∼ ν min =⇒ ξ(ν min ) = n). Let ν min the successor of ν such that ν min ∼ ν min , it exists because ν ∼ ν .

If

ν min ∈ V C n then ξ(ν min ) ≤ ξ(ν min ), therefore ξ(ν ) ≤ n + 1, therefore ξ(ν ) = n + 1 because ξ(ν ) > n. If ν min / ∈ V C n then ξ(ν min ) = ξ(ν min ) = n, therefore ξ(ν ) ≤ n + 1, therefore ξ(ν ) = n + 1. ξ(ν ) = n + 1 ∧ ξ(ν min ) ≤ n =⇒ ∃ν max ∈ ν • , ξ(ν max ) ≥ n and because ν ∼ ν , ∃ν max ∈ ν max • , ν max ∼ ν max and because ν / ∈ V C n , ξ(ν max ) = ξ(ν) = n For x, y ∈ V, let P (n, x, y) := x ∼ y ∧ ξ(x) = n ∧ ξ(x) < ξ(y) We proved that ∃ν, ν ∈ V 2 , P (n, ν, ν ) =⇒ ∃ν max , ν max ∈ ν • × ν
• , P (n, ν max , ν max ) We can iterate until we have P (n, x, y) with x ∈ V C n . There is a bounded number of iterations because of the lemma 1 there are no cycles in V N C , especially in ξ -1(n) ∩ (V N C ). We can then conclude with the same contradiction of the previous subcase.

This theorem allows us to work on the LTS further reduced with respect to strong bisimulation instead of [A||P||L c ], as we know that bisimulation preserves the level of choice.

Once we have the abstraction [A||P||L c ] and labeling with levels of choice, we are ready to extract the explanations. The basic idea is to extract, from [A||P||L c ], a graph that retains only • the states of [A||P||L c ] that are co-reachable from the final location of L c , i.e., the states that are consistent with the observed log, and

• the edges along which the level of choice decreases, i.e., the ones that bring the system closer to a violation of P.

To this end we proceed as follows.

Graph splitting.

Given an acyclic graph G = Σ, V, E, V 0 , V F equipped with a level of choice function ξ : V → N ∪ {∞}, we compute a split graph as follows. For any ν ∈ V let bounds(ν) = max{ξ(ν), bounds(ν

)} | ν ∈ ν • if ν • = ∅ {ξ(ν)} otherwise
We define the split graph G = Σ, V , E , (V ) 0 , (V ) F where

V = ν, b | ν ∈ V ∧ b ∈ bounds(ν) E = (ν, b), e, (ν , b ) | (ν, e, ν ) ∈ E ∧ b = max{b , ξ(ν) (V ) 0 = (ν, b) ∈ V | ν ∈ V 0 (V ) F = {(ν, b) | ν ∈ V F }
That is, we duplicate the states according to the maximum levels of choice that may be encountered in the future, and update the edges so as to point to the matching copy. We extend ξ to the split graph by putting ξ (ν, b) := ξ(ν). Intuitively, G accepts the same traces as G, while ensuring that each state is either effective choice or not, independent of the future behavior.

Example 1. Consider the discrete graph shown in Figure 2(a). From s 0 a fault f 1 or f 2 may occur, and f 1 may be coped with until a timeout t 1 occurs. From s 2 , a second fault f 3 will entail a system failure. However, the initial fault can be handled by primary and secondary fallback mechanisms b 1 and b 2 , until a timeout t 2 occurs. The split graph is shown in Figure 2(b).

Inria s 0 s 1 s 2 s 3 s 4 s 5 s ∞ 1 2 1 2 1 0 ∞ f 1 f 2 t 1 b 1 f 3 b 2 t 2
(a) Discrete graph with levels of choice.

s 0 , 1 s 0 , 2 s 1 , 2 s 2 , 2 s 2 , 1 s 3 , 2 s 4 , 1 s 5 , 0 0 1 1 1 2 1 2 1 f 3 t 1 b 2 t 2 (b) Split graph.
Only labels of effective choice transitions are shown.

s 0 , 1 s 2 , 1 s 5 , 0 1 1 0 f 3 (c) Subgraph 1 s 0 , 2 s 1 , 2 s 2 , 2 s 2 , 1 s 3 , 2 s 4 , 1 s 5 , 0 0 1 1 2 1 2 1 f 3 t 1 t 1 b 2 t 2 (d) Subgraph 2 {(s 0 , 1), (s 2 , 1)} {(s 5 , 0)} f 3 (e) Explanation E 1 .
The shortest explanation of the system failure is the occurrence of event f 3 .

{(s 0 , 2), (s 1 , 2), (s 2 , 2), (s 3 , 2)} {(s 2 , 1)} {(s 4 , 1)} {(s 5 , 0)} t 1 b 2 t 2 f 3 (f) Explanation E 2 .
The events that ultimately entailed the system failure are either t 1 ; f 3 or b 2 ; t 2 .

Subgraph extraction.

The explanations in the split graph are bounded in length by [ξ(ν 0 ), max ξ], where max ξ is the maximum finite level of choice in G. Our experiments suggest that explanations are easier to grasp when only explanations of the same length are presented simultaneously. We therefore extract, from the split graph G = Σ, V , E , (V ) 0 , (V ) F , for l ∈ [ξ(ν 0 ), max ξ], the graph G l of explanations of length l by restricting the LTS Σ, V , E , (V ) 0 , (V ) F where

V = (ν, b) ∈ V | b ≤ l E = E ∩ (V × Σ × V ) (V ) 0 = (ν, b) ∈ (V ) 0 | b = l (V ) F = (V ) F ∩ V
to the states that are reachable from (V ) 0 , and from which some state in (V ) F is reachable. Notice that G l is the empty graph when there is no explanation of length l. We then construct, for each (non-empty) subgraph, an explanation by applying the standard determinization (τelimination) algorithm based on subset construction [START_REF] Aho | Compilers -Principles, Techniques, and Tools[END_REF] to "collapse" the non-pertinent parts of the graph.

Example 2. From the split graph of Figure 2(b), two sub-graphs of constant height, in terms of effective choice transitions, are extracted (Figures 2(c) and 2(d)). By determinization we obtain the explanations E 1 and E 2 of Figures 2(e) and 2(f ) that highlight the decisive events for disjoint scenarios, with increasing complexity of the explanation.

Theorem 2. For each trace w ∈ Ψ(G) there exists l ∈ ξ(ν 0 ), max ξ] such that w ∈ G l .

Proof. Let n ∈ N and w = e 1 e 2 e 3 ...e n ∈ Ψ(G).

Let ρ = ν 0 e1 -→ ν 1 e2 -→ ... en -→ ν n ∈ Υ(G). Let b 0 , b 1 , ..., b n ∈ N n+1 such that ∀i ∈ [0, n], b i = max{ξ(ν j ) | j ∈ [i, n]}. Let l = max{ξ(ν i ) | i ∈ [0, n]}. We prove that ρ = (ν 0 , b 0 ) e1 -→ (ν 1 , b 1 ) e1 -→ ... en -→ (ν n , b n ) ∈ Υ(G l ).
First of all, let us prove that the states in the run ρ are in the split graph G = Σ, V , E , (V ) 0 , (V ) F . We know that ∀i ∈ [0, n], ν i ∈ V, and therefore ∀i ∈

[0, n], b i ∈ bounds(ν i ) =⇒ ∀i ∈ [0, n], (ν i , b i ) ∈ V . By induction on n -i, we prove that ∀i ∈ [0, n], b i ∈ bounds(ν i ). For i = n, ρ ∈ Υ(G) =⇒ ν n ∈ V f =⇒ bounds(ν n ) = {0} and ν n ∈ V f =⇒ ξ(ν n ) = 0, hence b n = 0 ∈ bounds(ν n ). For i < n, b i = max{ξ(ν i ), ξ(ν i+1 ), ..., ξ(ν n )} = max(ξ(ν i ), max{ξ(ν i+1 ), ..., ξ(ν n )}) = max(ξ(ν i ), b i+1 )
. By induction hypothesis we know that b i+1 ∈ bounds(ν i+1 ). Because ν i+1 ∈ ν i

• then by construction b i = max(ξ(ν i ), b i+1 ). We have that ∀i ∈ [0, n], b i ∈ bounds(ν i ) and therefore the states in ρ are state of the split graph. Now let us prove that the transitions of ρ are also in the split graph.

∀i ∈ [1, n], (ν i-1 , b i-1 ) ei -→ (ν i , b i ) ∈ E because ν i-1 ei -→ ν i ∈ E and b i = max(b i+1 , ξ(ν i )) Let G l = Σ, V , E , (V ) 0 , (V ) F be the given a sub-graph for the explanation of length l. ∀i ∈ [1, n], (ν i-1 , b i-1 ) ei -→ (ν i , b i ) ∈ E = E ∩ (V × Σ × V ) because ν i-1 ei -→ ν i ∈ E and b i ≤ l by definition of l and b i .
The run ρ is in Υ(G l ) and therefore w ∈ Ψ(G l ).

This result means that any log-consistent violation is contained in some subgraph after split and extraction. Our explanations may still encompass sequences of discretized time delays whose intermediate states are distinguished by the bisimulation. Our motivation for eliminating such sequences of delays is twofold. First, to construct a more concise explanation. In the case study, compressing δ-sequences allows us to reduce the number of transitions in the explanation from 21 to 7. Second, compressing sequences of time delays allows us to quantitatively estimate the possible time delays of the concrete runs that are summarized by the explanation.

Further Improvements

Given a sub-graph

G l = Σ, V, E, V 0 , V F , a δ + -sequence is an atomic sequence of transitions σ = ν 1 δ -→ ν 2 δ -→ ... δ -→ ν n+1 , that is, ∀i ∈ {1, ..., n} ∀e ∈ Σ ∀ν ∈ V : ν i e -→ ν =⇒ e = δ ∧ ν = ν i+1 such that ν 1 δ
-→ ν 2 is an effective choice transition. As illustrated in Figure 3, we replace each maximal δ + -sequence σ with a single transition

ν 1 δ -→ ν n+1 .
The second condition requires the first transition of the sequence to be effective choice, which ensures the information about effective choice states, used in the sequel, to be preserved. In order for the explanation to convey quantitative timing information, we estimate, for each abstract time transition ν δ -→ ν , the range of concrete delays represented by the transition, given the location invariants in ν and ν . For each state s and clock c, there exists the constants

Inria

inf s c , sup s c ∈ N ∪ {∞} such that in s, inf s c ≤ c ≤ sup s c .
If s is a time successor of s then we can estimate the delay to be between δ inf = max c∈C (inf s c -sup s c ) and δ sup = min c∈C (sup s c -inf s c ). In the case where δ inf is negative it is set to 0.

Safe alternatives.

The rationale of our construction of explanations is to highlight the events that contributed to the violation of a safety property. Complementary to this information, and equally crucial for understanding how the property was violated, is the question "how could the outcome have been avoided?". Providing this information is the goal of safe alternatives.

Definition 9 (Safe alternative).

Definition 10 (Safe alternative). A transition ν e -→ ν of an LTS G l is a safe alternative iff ν is an effective choice state and ξ(ν ) ≥ ξ(ν).

Intuitively, given a choice state, a safe alternative is a transition that would have contributed to avoiding the violation by not decreasing the level of choice.

State constraints.

So far we have focused our attention on the events of a failing run. The complementary information crucial for understanding the outcome, is in which states some relevant event took place. In this section, let us assume the TA to be equipped with a function π : L → 2 Π that labels each location with a set of atomic propositions. A straight-forward approach for displaying the states in the explanation would be to compute, for each aggregate state of the determinized graph consisting of a set Q of locations, the disjunction of the invariants (resp. of the atomic proposition) of the locations in L. This would, however, lead to unreadably complex expressions. We therefore make the design choice to label each state q = {ν 1 , ..., ν k } ∈ Q returned by determinization, with a convex predicate of the form ν 1 • • • ν k := Ĉ(q) ∧ SP (q), where Ĉ(q) is the weakest convex clock constraint that is implied by the invariants of the locations of all effective choice states in q. It is straight-forward to compute this clock constraint from the DBMs of the involved location invariants.

Similarly, for the function SP that aggregates, for a state q, atomic propositions of the states in q, multiple definitions are possible. We settle for the conjunction of the atomic propositions that hold in all effective choice states in q. This set is therefore obtained as: SP (q) = νi∈q: νi is an effective choice state ∈νi π( ) An example of the obtained state predicates is shown in Figure 7.

Implementation and Case Study

We have implemented our results in a tool written in Python. It relies on Kronos [START_REF] Yovine | KRONOS: A verification tool for real-time systems[END_REF] for the composition of timed automata, Minim for the generation of the quotient graph, and CADP [START_REF] Garavel | CADP 2011: a toolbox for the construction and analysis of distributed processes[END_REF] for reductions up to bisimulation.

We illustrate our approach on the dual-chamber implantable pacemaker model of [START_REF] Jiang | Modeling and verification of a dual chamber implantable pacemaker[END_REF]. It is a multi-component system where components are timed automata communicating over channels [START_REF] Larsen | Uppaal in a Nutshell[END_REF]. We use the model of [START_REF] Kölbl | Tartar: A timed automata repair tool[END_REF] that we have translated into the Kronos format. The model consists of 5 timed automata for the components of the pacemaker and 2 timed automata that model its environment, that is, the atrial and ventricular behavior of a heart. Whenever delays between sensed atrial or ventricular events exceed a threshold, the pacemaker produces an AP (atricular pace) or VP (ventricular pace) event.

Among the safety properties discussed in [START_REF] Jiang | Modeling and verification of a dual chamber implantable pacemaker[END_REF] we focus on the requirement that the time between two ventricular events (sensed or paced) never exceeds 1000 ms. The safety property observer is shown in Figure 5. If the heart model is safe then the system is also safe. We have therefore modified the parameters of the pacemaker so as to allow for unsafe behaviors.

Figure 4(a) shows the model of the ventricular behavior, with a frequency between Vminwait = 500 ms and Vmaxwait = 1100 ms, so as to allow a for fault. On the pacemaker model we increase the upper rate interval TURI from 400 ms to 1600 ms. This parameter determines the minimum delay between two ventricular events VP in the AVI component shown in Figure 4(b). In order to compare our results, we have taken the same parameters as in [START_REF] Kölbl | Tartar: A timed automata repair tool[END_REF]. We fix the set of observable events as the set Σ obs = {V P, V S, AS, AGET, AP, V GET } of signals exchanged between components, whereas we consider all internal events of the components as unobservable. We use Uppaal to obtain a witness trace for the violation of the property, from whose projection on the observable events we construct the timed log shown in Figure 5.

Let us now apply our approach to explain the causes of the violation. The sizes of the timed automata, discrete abstractions, and explanation are shown in Table 1.

1. The first step is to generate the log observer, which consists of 8 locations and 60 transitions.

2. We invoke Kronos to compose the components, the safety property observer, and the log observer.

3. We use Minim to compute the quotient graph with respect to strong time-abstracting bisimulation.

4. The levels of choice and safe alternatives are computed.

5. We remove the states that are not consistent with the log or the property violation. The difference in size is important because the observed behavior is only a small part of the behavior of the model.

6. In this case study the effective choice states are not ambiguous, therefore splitting does not change the graph. Similarly, the extracted sub-graph amounts to the full graph here.

7. Two maximal δ + -sequences of length 11 (resp. 6) are found, encompassing 10 (resp. 6) effective choice transitions. After δ + -compression, the quantitative time delays along the abstract delay transitions (called "time_succ" in our implementation) are computed.

8. After determinization we obtain the explanation shown in Figure 7.

In our case, the explanation is a sequence of discrete and δ-transitions. Each of them moves the system closer to the violation of the safety property, in spite of safe alternatives (shown as transitions without a target state) that would have avoided the violation. In our case the safe alternatives are mostly events sent by the heart model. This is logical because we know that VGET from the heart induces immediately a ventricular event in the PVRP component (not shown here) that would have avoided the violation. In order to understand why the pacemaker failed to adjust the ventricular events rate, we need to look at the state predicates. If we focus on the last three transitions, we see that the pacemaker waits 150 ms and takes an internal transition Comparison with TarTar [START_REF] Kölbl | Tartar: A timed automata repair tool[END_REF]. We use the same model as in [START_REF] Kölbl | Tartar: A timed automata repair tool[END_REF], up to the fact that we have increased the parameters Aminwait and Vminwait (the minimal atrial and ventricular rate of the heart model, respectively) from 1 ms to 500 ms in order to reduce the size of the quotient graph to a size that can be managed by Minim. This modification does not impact the safety violation we are interested in. TarTar focuses on fixing time delay parameters in order to repair safety violations, and proposes a repair of the bounds on TURI . Our approach is more general in the sense that it does not restrict its attention to time delays. On the other hand, it does not propose a repair. In particular, our explanations are useful to explain failures caused by nondeterministic behavior, or when there are no admissible repairs but one still wants to understand the causes of a violation.

Discussion

We have proposed a novel approach to explain the violation of a safety property by a real-time system. In essence, an explanation is formed by the parts of the behaviors that are consistent with the log, that jointly contributed to move the system into the failure state.

This work is a first step in constructing explainable cyber-physical systems. Much work remains to be done though towards this long-term goal. In particular, we need to establish formal properties of our explanations, such as soundness and completeness. We will also investigate how to construct explanations online, and how to extend our analysis to more general classes of hybrid systems.

Figure 1 :

 1 Figure 1: Overview of the approach.

3 .

 3 for all other states ν ∈ V let ξ(ν) = min + | ∃ν : ξ(ν ) = ∧ ∃e ∈ Σ : ν e -→ ν where min + (G) = min(G) if |G| ≤ 1 1 + min(G) otherwise and we set min ∅ = ∞.

Figure 2 :

 2 Figure 2: Splitting, sub-graph extraction, and explanations obtained after determinization. Dashed transitions are in the model but not consistent with the log.

4. 1 . 1

 11 Compressing δ-sequences and estimating time delays.

  Effective choice transition in red, a and b are discrete events, the transitions in black are either effective choice or not.

  δ + -compression.

Figure 3 :

 3 Figure 3: Compression of sequences of discretized time delays.

  (a) Heart ventricular component. (b) Pacemaker ventricular component AVI .

Figure 4 :

 4 Figure 4: Two components of the model.

Inria

Figure 5 :Figure 6 :

 56 Figure 5: Safety property observer.

Figure 7 :

 7 Figure 7: Pacemaker explanation

Table 1 :

 1 Sizes of the timed automata (number of locations), discrete abstractions, and resulting explanation.I _AVI . If we look at the model of the AVI component, we see that this event could only occur because we increased TURI . From this point the violation becomes unavoidable after a further delay of 400 ms.

	Automaton	#states #transitions
	A||P	96	296
	L	7	6
	L c	8	60
	A||P||L c	117	332
	[A||P||L c ]	1817	5041
	[A||P||L c ]/ ∼	1763	4931
	log-consistent	50	52
	split	50	49
	δ + -compression	35	34
	explanation	8	7

RR n°9420

Inria

Acknowledgment. The authors thanks Stavros Tripakis and Sergio Yovine for their help in using Kronos.

That is, V C is inevitable from V N C .

Proof. If there is a cycle such that all the states have the same finite level of choice, then from all those states there exists a path to V F , but there exists also a path that avoid indefinitely V F by repeating the cycle. Leaving the cycle should decrease the level of choice in the path to V F . Hence at least one of those states is in V C . Theorem 1. Given an LTS G = Σ, V, E, V 0 , V F , a level of choice function ξ on G, and a strong bisimulation ∼ on V, we have that s ∼ s =⇒ ξ(s) = ξ(s ).

Proof. Toward contradiction: Let us suppose that we have G = Σ, V, E, V 0 , V F , a level of choice function ξ on G, and a strong bisimulation ∼ on V and

Let n ∈ N be the smallest level of choice such that there exists one state at level n which is bisimilar with a state at level n > n. Formally, n is the smallest integer such that P (n) with:

The existence of n is implied by the hypothesis (H). '

by definition of the level of choice and therefore ν / ∈ V F because ν ∼ ν by definition of ∼.

ξ(ν ) > 0 implies that there exists a successors ν of ν such that ξ(ν ) > 0. Therefore from ν we can build a run where ξ -1 (0) can be avoided indefinitely (or reach a state non-coreachable wrt V F ) while from ν, all paths reach V F within a bounded number of transitions. We can build two sequentially bisimilar paths, from ν and from ν where the destinations are bisimilar but one is in V F while the other destination is not.

Case n > 0: Because n is minimal we know that for lower level of choice, bisimilarity implies same level of choice :

ν exists because P (n) is true. Subcase ν ∈ V C n : By definition of the level of choice, ξ(ν), ν has one successor ν min such that ξ(ν min ) = n -1. Let ν min ∈ ν

• such that ν min ∼ ν min a successor of ν , it exists because ν ∼ ν . ξ(ν min ) < n therefore by induction hypothesis ξ(ν min ) = ξ(ν min ) = n -1.

By definition of ξ, we have ξ(ν

We have a contradiction with ξ(ν ) > ξ(ν).

Subcase ν / ∈ V C n :


Lucas Nussbaum

Olivier Richard

Lightweight emulation to study peer-to-peer systems

Keywords: peer-to-peer, evaluation, emulation, network, virtualization, BitTorrent

The current methods used to test and study peer-to-peer systems (namely modeling, simulation, or execution on real testbeds) often show limits regarding scalability, realism and accuracy. This paper describes and evaluates P2PLab, our framework to study peer-to-peer systems by combining emulation (use of the real studied application within a configured synthetic environment) and virtualization. P2PLab is scalable (it uses a distributed network model) and has good virtualization characteristics (many virtual nodes can be executed on the same physical node by using process-level virtualization). Experiments with the BitTorrent file-sharing system complete this article and demonstrate the usefulness of this platform.

INTRODUCTION

Peer-to-peer systems have become more and more popular over the last few years, and this popularity often required changes that made them more and more complex. Due to this ever increasing complexity, the development and the study of peer-to-peer systems have become more difficult: we need ways to ensure that a peer-to-peer application will work properly on thousands of nodes, or ways to understand applications running on thousands of nodes.

Distributed applications are traditionally studied using mathematical modeling, simulation, and execution on a real system. Simulation consists in using a model of the application's code in a synthetic environment. This method is widely used, and gives valuable results easily. However, it is often difficult to simulate efficiently a large number of nodes using a complex model: a trade-off between the accuracy of the model and the number of nodes always has to be made.

The alternate solution is to run the real application to study on a real-world experimentation platform like PlanetLab [START_REF] Chun | PlanetLab: An Overlay Testbed for Broad-Coverage Services[END_REF]. But the environment is then difficult to control and to modify (since it depends heavily on the real system itself), and results are often difficult to reproduce (since the environmental conditions may vary a lot between experiments). This kind of real-world experiments is required when developing a peer-to-peer system, but it isn't enough, and developing other ways to evaluate peer-topeer systems is becoming more important as their complexity grows [START_REF] Haeberlen | Fallacies in evaluating decentralized systems[END_REF].

Between those two approaches, this paper explores an intermediate solution using emulation and virtualization, and shows that such an approach can provide interesting results when used to study peer-to-peer systems.

This paper is organized as follows. First, an overview of emulation and virtualization is provided, before related works are examined. Then, the main features of P2PLab are described and evaluated. Finally, the usefulness of P2PLab is verified by performing experiments on the BitTorrent peer-to-peer file sharing system.

EMULATION AND VIRTUALIZATION

Emulation and Virtualization have to be distinguished:

Emulation consists in providing a modified environment to the studied application, to match the conditions of the experiment. Determining which resources to emulate (and with which precision) has to be considered as a trade-off between realism and cost (a precise emulation of conditions can be very CPU-intensive). For example, when studying peer-to-peer systems, network emulation is important, while emulation of different types of hard disks is probably not necessary. Emulation is often costly, and its cost is often difficult to evaluate, because it depends both on the quality of emulation and on the emulation parameters: emulating an high-latency network will be more expensive than emulating a low-latency one.

Virtualization of resources allows to share a resource between several instances of an application. It is required to be able to study a large number of co-existing nodes. In the field of distributed systems, virtualization allows to execute several instances of the application or the operating system on the same physical machine, thus increasing the number of nodes available for the experiment. Of course, since the resources of the physical machine are shared between instances, the fairness of this share is an important issue. Like the precision of emulation, the quality of the fairness is a trade-off.

RELATED WORKS

A lot of work occurred recently in the virtualization area, with different approaches. Linux Vserver [START_REF]The Linux VServer Project[END_REF] is a patch for the Linux kernel adding contexts and managing interactions between them, allowing several environments to share the same kernel with a very low overhead. User Mode Linux [START_REF] Dike | A user-mode port of the Linux kernel[END_REF] is a port of the Linux kernel to a Linux process. And Xen [START_REF] Barham | Xen and the art of virtualization[END_REF] uses para-virtualization to give the ability to run simultaneously several operating systems. Those operating systems have to be modified to run over the Xen micro-kernel, which is in charge of sharing resources and providing virtual devices. Regarding network emulation (by far the most important resource to control while studying peerto-peer systems), there are both low-level tools which work at the packet level to emulate different network connections (varying bandwidth and latency) and higher level tools which allow to build a complex synthetic network topology.

The low level tools include Dummynet [START_REF] Rizzo | Dummynet: a simple approach to the evaluation of network protocols[END_REF], which runs on FreeBSD and is the most popular network emulator. Dummynet is integrated into the FreeBSD firewall (ipfw), and is configured by using specific firewall rules. Other tools are NISTNet [START_REF] Carson | NIST Net: a Linux-based network emulation tool[END_REF] (which runs on Linux 2.4), and Linux 2.6's Traffic Control (TC) [START_REF]Linux Advanced Routing and Traffic Control[END_REF] (using NetEm [START_REF] Hemminger | Network emulation with NetEm[END_REF]). Those tools schedule inbound and/or outbound packets to control bandwidth and delay, and emulate network problems such as packet loss.

Higher level typically tools use the former low-level tools to emulate complex topologies. NetBed [START_REF] White | An integrated experimental environment for distributed systems and networks[END_REF] combines real nodes using RTC or DSL lines, nodes using Dummynet, and simulated nodes (using Network Simulator Emulation Layer) to provide experimental environments. Modelnet [START_REF] Vahdat | Scalability and accuracy in a large-scale network emulator[END_REF] uses cluster nodes split in two groups: the application under study runs on edge nodes while the Modelnet core nodes use Dummynet to emulate a network topology. Modelnet uses a distillation phase to make a trade-off between accuracy and scalability to be able to emulate the network on a small number of nodes.

The current virtualization tools target high realism and have a relatively poor virtualization ratio (number of virtual nodes / number of physical nodes). One of the problems is that they virtualize a full operating system (kernel, libraries, application). This is often not needed for peer-to-peer applications, since they are relatively well self-contained.

Another issue is network emulation: current tools target a realistic emulation of the core network (congestion, routing, etc inside the core links). Most peer-to-peer applications are used on the edge nodes of the Internet, often on home computer with DSL connections. Therefore, even if some aspects of the Internet core are important (e.g latency, for experiments involving locality), the emphasis can be put on the emulation of the link between the edge nodes and their Internet Service Provider. This link is the bottleneck in most (if not all) cases.

P2PLAB

P2PLab is our emulation tool for studying peer-to-peer systems. It targets high efficiency (large number of virtual nodes can be studied on a low number of physical nodes), and scalability (experiments can be done with thousands of nodes).

P2PLab virtualizes at the process level, not at the system level, to allow to run a large number of virtual nodes on each physical node. It runs on FreeBSD, since it uses Dummynet for network emulation. A decentralized approach is used to emulate network topologies, allowing better scalability.

First, we will verify that FreeBSD is a suitable platform for P2PLab by checking that its scheduler is scalable and provides a good level of fairness. Then, P2PLab's virtualization system will be described, and the network emulation model of P2PLab will be presented.

Suitability of FreeBSD

While most virtualization systems virtualize on the operating system level, it is not mandatory here since the goal is to study peer-to-peer systems. It was therefore decided to virtualize the process' network identity by binding each process to its own IP address. The FreeBSD operating system was chosen for P2PLab because of the availability of Dummynet [START_REF] Rizzo | Dummynet: a simple approach to the evaluation of network protocols[END_REF], FreeBSD's network traffic shaper. But it was still necessary to test whether FreeBSD was a suitable platform to run a very large number of processes without compromising our experiment's results. FreeBSD has two schedulers: the classic 4BSD scheduler, and the more modern ULE scheduler (which is similar to Linux 2.6's scheduler). It was decided to evaluate both. The evaluation took place on nodes of the GridExplorer system, part of the French grid research project Grid5000 [START_REF] Cappello | Grid'5000: a large scale, reconfigurable, controlable and monitorable Grid platform[END_REF]. The nodes are Dual-Opteron 2 Ghz with 2 Gb of RAM and Gigabit Ethernet.

The first experiments evaluated FreeBSD's ability to run a large number of concurrent processes. In a first experiment, several instances of a non-memory-intensive program were executed (calculating Ackermann's function, requiring about 1.65 seconds to complete when run alone), and the average per process execution time was measured. Figure 1 shows that there is no overhead caused by the execution of concurrent processes. The average execution time even decreases when the number of processes increases, probably because of cache effects and costs that don't depend on the number of processes.

Then, the same experiment was done with memory-intensive processes (doing simple operations on large matrices). The results described on figure 2 are very different for Linux and FreeBSD. With Linux 2.6, the scheduler and/or the memory management prevent the execution time from increasing when all the data doesn't fit anymore in the physical memory. With FreeBSD, the execution time increases a lot as soon as virtual memory (swap) is used.

In the next experiments, we will have to make sure that we are in experimental conditions where virtual memory is not needed.

Fairness between processes is also important: some instances must not benefit from a larger share of the CPU time. To get a first idea of the level of fairness between processes, we perform the following experiment: we start at the same time * , on the same machine, 100 instances of a same CPU-intensive Figure 3 shows that with the 4BSD scheduler and Linux's scheduler, most processes finish nearly at the same time. With the ULE scheduler, bigger variations appear. Those results are different from those obtained with FreeBSD 5 in [START_REF] Nussbaum | Lightweight emulation to study peer-to-peer systems[END_REF], where, with the ULE scheduler, some processes were excessively privileged by the scheduler and were allowed to run alone on a CPU. This problem seems to have been fixed in FreeBSD 6.

Even if this approach provides satisfying results, both regarding scalability and fairness, it is somehow limited: it is not possible to perform experiments where virtual processors of different speeds are assigned to instances. This approach is therefore not suitable for the study of Desktop Computing systems. Using more complex virtualization solutions could help avoid this limitation, and also allow a more precise control of the memory.

In the following experiments, we used the 4BSD scheduler in P2PLab.

Virtualization

As said earlier, virtualization is made at the level of the process' network identity: instances on the same physical system share all resources (file system, memory etc.) as normal processes do. However, each process has its own IP address on the network. The main IP address of each physical system is kept for administration purposes. The IP addresses of the virtual nodes are configured as interface aliases as shown in figure 4 (most UNIX systems, including Linux and FreeBSD, allow each network interface to be assigned several IP addresses through an aliasing system). Evaluation showed that interface aliases produced no overhead compared to the normal assignment of an IP address to an interface.

To avoid name-space conflicts, the addresses of the virtual nodes were chosen in different subnet. Figure 4 shows an example configuration using the 192.168.38/24 network for administration and the 10.0.0.0/8 network for virtual nodes.

To bind an application to a particular IP address, we chose to intercept some network system calls (figure 5 show the order in which those system calls are used for TCP sockets). Several options were available:

• Modifying the application under study : this requires the application's source code, and the ability to recompile it. • Linking the application with an overhead library, either at compilation-time or at run-time (using the LD PRELOAD environment variable). This approach is interesting since modifying the application is not required. However, it has problems with applications which are statically compiled, or with applications using a library for network communications. • Using ptrace(). This system call enables an application to monitor another one, and to intercept its system calls (User Mode Linux, for example, uses this approach). This approach requires additional system calls, causing an important overhead. • Modifying the kernel, especially the handling of system calls. But modifying kernel code is harder and more error-prone than modifying user-level code. • Modifying the C library (libc). This approach allows to intercept all system calls made by non-statically compiled applications. In P2PLab, we chose to modify the FreeBSD C library, which provided a good compromise between complexity and efficiency. We modified the bind(), connect() and listen() library calls using a naive approach:

• When bind() is called, the my addr parameter is modified to restrict the bind to the IP address specified by the BINDIP environment variable. • When connect() or listen() are called, bind() is called before to restrict connect() or listen() to the IP address in BINDIP. If another bind() was made before, this one will fail, but we ignore the error in this case.

This approach doubles the number of system calls for connect() and listen(). A similar approach is possible for UDP. Tests showed that this libc modification was working as expected with programs in Perl, Python, Ruby, TCL, C, Java (with Sun's JDK). The only case where this approach failed to work was statically compiled C programs.

Then, we evaluated the overhead of this approach during the establishment of TCP connections. The test program was connecting to a local server and disconnecting as soon as the connection was established. We measured that the duration of a connection/disconnection cycle was 10.22µs without the modification, to compare to 10.79µs with the modification: the cost of this approach is very low, even in the worst case.

Network Emulation

Current network topology emulators like ModelNet [START_REF] Vahdat | Scalability and accuracy in a large-scale network emulator[END_REF] target a realistic emulation of the core network (routing and interactions between autonomous systems, or between the main routers). But most peerto-peer applications run on nodes on the edge of the Internet [START_REF] Foster | On death, taxes, and the convergence of peer-to-peer and grid computing[END_REF]: while the traffic in the core of the Internet can influence the peer-to-peer system behavior (congestion between providers can increase latency, for example), the main bottleneck for end nodes is often the link between the user and its Internet service provider (ISP). Therefore, in an experimental platform like P2PLab, it is possible to model the Internet by reproducing what the end node really sees, excluding what is less important from the end node point of view. Evaluations on P2PLab can be combined with experiments on real systems like PlanetLab [START_REF] Chun | PlanetLab: An Overlay Testbed for Broad-Coverage Services[END_REF] when an understanding of the influence of the core network is needed.

In P2PLab, we model the Internet from the point of view of the participating node, by excluding what is less important from this point of view. Network emulation is achieved in a decentralized way: each physical node is in charge of the network emulation for its virtual nodes. On each node, emulation is done with Dummynet [START_REF] Rizzo | Dummynet: a simple approach to the evaluation of network protocols[END_REF], the FreeBSD traffic shaper integrated into FreeBSD's firewall (IPFW). Both incoming and outgoing packets are delayed by Dummynet. Two rules are needed for each hosted virtual node (one for incoming packets, the other one for outgoing packets).

But this model only allows to set parameters for bandwidth and latency for each virtual node. It doesn't allow to model locality between virtual nodes. The notion of group of nodes is therefore added, to be able to study applications using locality. In a real system, those groups would match nodes from the same ISP, from the same country, or from the same continent. P2PLab's emulation model allows to control bandwidth, latency and packet loss rate on network links between nodes and their ISP, and latency between groups of nodes, allowing to study problems involving locality of the nodes, for example. The number of rules is the main parameter limiting the scalability of P2PLab. To determine the importance of this factor, we measure the round-trip time with ping between two nodes. When packets go out of the first node, the firewall must evaluate a varying number of rules. Figure 6 shows that latency increases nearly linearly with the number of rules, because the rules are evaluated linearly by the firewall. With IPFW, it is not possible to evaluate the rules in a hierarchical way, or with a hash table.

Figure 7 shows an example of topology that we successfully emulated with P2PLab. As an example, the physical node hosting the virtual node 10.1.3.207 will need:

• two rules for each hosted virtual node (incoming and outgoing packets) ; • one rule to add 100ms of latency for packets coming from 10.1.3.0/24 going to 10.1.1.0/24 (the opposite rule being on the nodes hosting 10.1.1.0/24) ; • one rule to add 100ms of latency for packets coming from 10.1.3.0/24 going to 10.1.2.0/24 ; • one rule to add 400ms of latency for packets coming from 10.1.0.0/16 going to 10.2.0.0/16 ; • one rule to add 600ms of latency for packets coming from 10.1.0.0/16 going to 10.3.0.0/16.

We measured the latency between nodes 10.1.3.207 and 10.2.2.117 to 853ms, which can be decomposed in:

• 20ms of delay added when the packet went out of 10.1.3.207 ; • 400ms of delay between groups 10.1.0.0/16 and 10.2.0.0/16 ; • 5ms of delay when the packet arrived on 10.2.2.117 ; • 425ms for the return trip, detailed as above ; • 3ms of overhead, because of the underlying network and the evaluation of firewall rules.

STUDY OF BITTORRENT WITH P2PLAB

In this section, we compare our emulation platform with BitTorrent, showing that P2PLab is a suitable experimentation platform to study complex peer-to-peer system. BitTorrent [START_REF] Cohen | Incentives build robustness in BitTorrent[END_REF] is a popular peer-to-peer file distribution system. It provides very good performance by ensuring that downloaders cooperate by sharing parts they have already downloaded through a complex reciprocation system. It has already been largely evaluated through analysis of large scale utilization [START_REF] Pouwelse | The Bittorrent P2P file-sharing system: Measurements and analysis[END_REF][START_REF] Izal | Dissecting BitTorrent: five months in a torrent's lifetime[END_REF], analytical modeling [START_REF] Qiu | Modeling and performance analysis of BitTorrent-like peer-to-peer networks[END_REF] or simulation [START_REF] Ashwin | Analyzing and improving BitTorrent performance[END_REF].

However, those works have only rarely been compared to large scale studies on real world systems, or to studies using emulation. BitTorrent is an engineering work, not a research prototype, and several parts of its code are very complex. The large number of constants used as parameters of all the important algorithms makes it very hard to model accurately.

A BitTorrent 4.0.4 client (written in Python by BitTorrent's original author) was used for all experiments. It was slightly modified to allow data collection (a time-stamp was added to the default output). The experiments took place on the GridExplorer system, already described previously.

P2PLab Folding Ratio

P2PLab targets an high virtualization ratio: it should be possible to run many virtual nodes on the same physical system, thus allowing to do experiments with a very large number of nodes. But the concurrent execution of several instances of the application must not affect the results.

The first experiment compares the download of a 16 MB file by 160 clients. The file size is not important in BitTorrent, since the file is always divided in pieces of 256 KB. The file is provided by 4 seeders. All nodes (both downloaders and seeders) have a network connection with a download rate of 2 mbps, an upload rate of 128 kbps, and a latency of 30 ms, reproducing the conditions of a DSL connection. The clients are started with a 10s interval. When the clients have finished the download of the file, they stay online and become seeders, continuing to upload data to the downloaders.

The 160 clients are deployed successively on 160 physical nodes, 16 physical nodes (10 virtual nodes per physical node), 8, 4 and 2 physical nodes.

Figure 8 shows the evolution of the download of all 160 clients when they are deployed on 160 physical nodes. One can see that with those parameters, all the cases of a BitTorrent download are represented: • First (short) part of the download when only initial seeders are able to upload data ; • Second part when all downloaders start contributing to each other ; • Third part when the first downloaders become seeders and help other peers finishing their download faster.

Therefore, those parameters are a realistic workload to test P2PLab's virtualization capabilities. Figure 9 shows that the experiment took place without any overhead, even with 80 virtual nodes on each physical node: results are nearly identical. The potential sources of overhead were investigated, and it was determined that the first limiting factor was the network speed: with other (slightly faster) emulated network settings, the platform's Gigabit network was saturated by the downloads.

Other overhead sources were considered: during the experiment, we monitored the system load, the memory usage, and the disk I/O on every physical node. None of them was a problem during our experiments.

P2PLab Scalability

P2PLab targets high scalability: it should be possible to run experiments with a large number of nodes. We tried to study the download of a 16 MB file by nodes, under the same network conditions as in the first experiment. The 5760 virtual nodes (5754 clients, 4 seeders, one tracker) are hosted on 180 physical nodes (32 virtual nodes per physical node). The clients are started every 0.25s. When a client finishes its download, it stays active and helps the others finish their download. The experiment succeeded, and figure 10 shows the evolution of the download on some selected clients (clients numbered 50, 100, 150, ... 5750). One can see that most clients finish their downloads nearly at the same time. This is confirmed by figure 11, which shows the number of clients having completed their download over time.

SUMMARY AND CONCLUSION

With the increase of the resources available on a single computer, virtualization and emulation have both been the target of a lot of research in the last years. Beyond their usual use case, they can be efficiently combined to build useful experimentation platforms. This paper describes P2PLab, a promising tool to study peer-to-peer systems: it allows to use the real application on a large number of nodes in a configurable environment, allowing reproduction of experiments. This paper also contributes a simple network model different from the models usually used in network emulators to model the Internet: while those models concentrate on the core of the Internet and its routing interaction, P2PLab models the Internet from the end node's point of view.

This work also shows that, while most virtualization systems concentrate on providing a very accurate image of resources, a simpler approach might be sufficient in some cases. Our emulation platform only virtualizes what is needed to make the different virtual nodes look like real separate nodes from the outside: its network identity. This lightweight virtualization allows to maximize the virtualization ratio.

Our emulation platform, P2PLab, enabled us to perform some experiments on the BitTorrent peerto-peer system. During those experiments, P2PLab proved to be scalable, easy to use and useful.

6 Figure 1 .

 61 Figure 1. Average per process execution time with a varying number of concurrent processes. Processes are CPUintensive, but not memory-intensive.

6 Figure 2 .

 62 Figure 2. Average per process execution time with a varying number of concurrent processes. Processes are CPUand memory-intensive.

Figure 3 .

 3 Figure 3. Cumulative distribution functions of the execution times with Linux 2.6 and FreeBSD's 4BSD and ULE schedulers.

Figure 4 .

 4 Figure 4. On each physical node, IP addresses for virtual nodes are configured as interface aliases.

Figure 5 .

 5 Figure 5. Network system calls used when establishing or accepting a TCP connection.

Figure 6 .

 6 Figure 6. Measured round-trip time when the number of firewall rules vary.

Figure 7 .

 7 Figure 7. Emulated topology.

Figure 8 .

 8 Figure 8. Evolution of the download of the 160 clients

  of data received by the nodes time (s) 1 client per physical node 10 clients per physical node 20 clients per physical node 40 clients per physical node 80 clients per physical node

Figure 9 .

 9 Figure 9. P2PLab folding ratio: total amount of data when downloading of a 16 MB file with 160 clients.

Figure 10 .

 10 Figure 10. Evolution of the download of a 16 MB file between 5754 clients on a few selected clients (nodes 50, 100, 150, ... 5750).

Figure 11 .

 11 Figure 11. Number of clients having completed their download.

ACKNOWLEDGEMENTS

This work has been done within the ID-IMAG laboratory, jointly supported by CNRS, INPG, INRIA, UJF and UPMF. Computer resources are provided by the Grid5000 platform (further information at http://www.grid5000.fr/).