Armando Gonçalves Da Silva Junior

Pierre Deransart
email: pierre.deransart@inria.fr

Luis Carlos Menezes

Marcos Aurélio

Almeida Da Silva

Jacques Robin
email: jacques@gmail.com

Armando Gonçalves Da

Silva Junior

Towards a Generic Trace for Rule Based Constraint Reasoning

Keywords: Trace, CHR, CHR ∨, Tracer, Generic Trace, Analysis Tool, Observational Semantics, Debugging, Programming Environment, Constraint Programming, Validation trace, CHR, CHR ∨, traceur, trace générique, analyseur, sémantique observationnelle, déboggage, environnement de programmation, programmation par contraintes, validation

CHR is a very versatile programming language that allows programmers to declaratively specify constraint solvers. An important part of the development of such solvers is in their testing and debugging phases. Current CHR implementations support those phases by offering tracing facilities with limited information. In this report, we propose a new trace for CHR which contains enough information to analyze any aspects of CHR ∨ execution at some useful abstract level, common to several implementations. This approach is based on the idea of generic trace. Such a trace is formally defined as an extension of the ω ∨ r semantics of CHR. We show that it can be derived form the SWI Prolog CHR trace.

Introduction

CHR (Constraint Handling Rules) [9] is a uniquely versatile and semantically well-founded programming language. It allows programmers to specify constraint solvers in a very declarative way. An important part of the development of such solvers is in their testing and debugging phases. Current CHR implementations support those phases by offering tracing facilities with limited information.

In this report, we propose a new trace for CHR which contains enough information, including source code ones, to analyze any aspects of CHR ∨ execution at some abstract level, general enough to cover several implementations and source level analysis. Although the idea of formal specification based tracer is not new (see for example [13]), the main novelty lies in the generic aspect of the trace. Most of the existing implementations of CHR like in [11,12,2,[START_REF] Wielemaker | SWI-Prolog 5.6 Reference Manual[END_REF]] include a tracer with specific CHR trace events, but without formal specification, nor consideration with regards to different kind of usages other than debugging.

The notion of generic trace has been informally introduced and used for defining portable CLP(FD) tracer and portable applications [1,[START_REF] Langevine | A Generic Trace Schema for the Portability of CP(FD) Debugging Tools[END_REF]. We propose here to use this approach to specify a tracer for rule based inference engine like CHR ∨ . A generic trace has three main characteristics: it is "high level" in the sense that it is independent from particular implementations of CHR, it has a specified semantics (Observational Semantics) and can be used to implement debugging tools or applications. An important property of the proposed generic trace is that it contains as many information on the solver behaviour as the one contained in the operational semantics. This property is called "faithfulness" of the observational semantics.

In this report, we present a generic trace for CHR ∨ based on its refined operational semantics ω ∨ r [5], and describe a first prototype developed for SWI-Prolog CHR ∨ engine. The implementation consists of combining the original trace of the SWI engine with source code information to get generic trace events, and then, allowing the user to filter these events using an SQL-based language.

This report is organized as follows. Section 2 gives a short introduction to generic traces, observational semantics and faithfulness. Section 3 presents CHR ∨ , the formal specification of its operational semantics, based on the ω ∨ r semantics, and the requirements for the generic trace, as its syntax as well. Section 4 presents the observational semantics of CHR ∨ , OS-CHR ∨ , defining formally the generic trace, and shows its faithfulness. Section 5 introduces an executable operational semantics of CHR ∨ defined in SWI Prolog (the code is in the annex) and used to test its formal semantics. Section 6 describes the CHR-SWI-Prolog based prototype of the generic trace. Section 7 presents some experimentation. Discussion and conclusions are in the two last sections.

Generic Trace, Observational Semantics and Subtrace

The concept of generic trace has been first introduced in [START_REF] Langevine | A Generic Trace Schema for the Portability of CP(FD) Debugging Tools[END_REF], formally defined in [6,7], and a first application to CHR presented in [START_REF] Oliveira | Towards a Generic Framework to Generate Explanatory Traces of Constraint Solving and Rule-Based Reasoning[END_REF]. A generic trace is a trace with a specification based on a partial operational semantics applicable to a family of processes. We give here its main characteristics and the way to specify a generic trace.

Preliminaries

A trace consists of an initial state s 0 followed by an ordered finite or infinite sequence of trace events, denoted < s 0 , e >. T is a set of traces (finite or infinite). A prefix (finite, of size t) of a Process Obs.

T^v T^w T^v Rebuilder Extractor

E I

Figure 1: Extraction, Reconstruction, Faithfulness Property trace T =< s 0 , e n > (finite or infinite, here of size n ≥ t) is a partial trace U t =< s 0 , e t > which corresponds to the t first events of T , with an initial state at the beginning. T may contain any prefixes of its elements.

A trace can be decomposed into segments containing trace events only, except prefixes which start with a state. An associative operator of concatenation will be used to denote sequences concatenations (denoted ++). It will be omitted if there is no ambiguity. The neutral element is [] (empty sequence). A segment (or prefix) of size 0 is either an empty sequence or a state.

Traces are used to represent the evolution of systems by describing the evolution of their state. A state of the system is described by a given finite set of parameters and a state corresponds to a set of values of parameters. Such states will be said virtual as they correspond to states of the observed system, but they are not actually traced. We will thus distinguish between actual and virtual traces.

• the actual traces (T w ) are a way to observe the evolution of a system by generating traces.

The events of an actual trace have the form e = (a) where a is an actual state described by a set of attributes values. An actual states is described by a finite set of attributes. Actual traces corresponds to sequences of events produced by a tracer of an observed system. They usually encode virtual states changes in a synthetic manner.

• the virtual traces (T v ) corresponds to the sequence of the virtual states such that for each transition in the system between two virtual states, it corresponds an actual trace event.

The virtual trace events have the form e = (r, s) where r is a type of action associated with a state transition and s, called virtual state, the new state reached by the transition and described by a set of parameters. Virtual traces correspond to sequences of virtual states of the observed system which produced the actual trace, together with the kind of action which produced the virtual state transition.

The correspondence between both kinds of traces is specified by two functions E : T v → T w and I : T w → T v , respectively the extraction and the reconstruction function, as illustrated by the figure 1.

The idea is that the actual generated trace contains as much information as possible in such way that the virtual trace can be reconstructed from the actual one. In other words, the extraction is done without loss of information. Such a property of the traces is called faithfulness and, if we denote Id v (resp. Id w ) the identity between virtual traces (resp. actual traces), it states that E • I = Id v (composition) or E = I -1 , and

I • E = Id w (or I = E -1 ).
Finally, each trace event is numbered by a chrono, which is an integer incremented by 1 at each new event. It will be ignored in formal presentations, but will be used as a unique identifier of the trace events in the implementations.

Components in Trace Design

When designing a trace, several components must be taken into consideration. They are depicted in the Figure 2. The observed process whose behavior is modeled by a virtual trace (sequence of successive virtual states) T v .

2. An extractor component which encodes the virtual trace into the actual one T w . This component corresponds in practice to the tracer formalized by the extraction function E.

3. The driver which realizes the actual trace filtering according to some trace query. In this report we limit its role to select a subtrace of the so called full trace.

4. The rebuilder which may reconstruct from a full or partial actual trace a full or partial virtual trace. This is possible only if there is no loss of information (faithfulness property).

The rebuilder is formalized by the reconstruction function I.

5.

The analyzer, which corresponds to some debugging tool or particular application, working with the full trace or a partial one.

Notice that in practice the three first components may be interleaved in the sense that for a given query the driver may select directly a subset of the virtual trace, thus avoiding to extract and encode a full actual trace before selecting a subtrace.

In this report we focus on three components (observed process, extractor and rebuilder) and a property. Their description consists in a faithful observational semantics.

Observational Semantics (OS)

The evolution of a system defined by its virtual traces and the production of the corresponding actual trace can be described by a so called Observational Semantics as follows. More general definitions can be found in [7].

Definition 1 (Observational Semantics) An observational semantics consists of < S, R, A, T, E, I, S 0 >, where

• S: domain of virtual states, a subset of the Cartesian product of domains of parameters.

• R: finite set of action types, set of identifiers labeling the transitions.

• A: domain of actual states, a subset of the Cartesian product of domains of attributes.

• T r: state transition function 1 T r : R × S → S, characterized as T r(r i , s i-1 ) = s i , where (s i-1 , s i ) is the i th transition starting from an initial state s 0 , and labeled by r i .

1 It can be a relation in case of a non deterministic transitions.

RR n°7939

• E l : local trace extraction function E l : S × R × S × T w → A, which is defined for all r, s, s ′ such that T r(r, s) = s ′ and characterized as E l (s i-1 , r i , s i , T w i-1 ) = a i , where a i is the i th actual trace event generated after the initial state s 0 . In this definition the extraction may use all information accumulated in the already generated actual trace

T w i-1 . • I l : local trace reconstruction function I l : S×T w → R×S is characterized as I l (s i-1 , T w i ) = (r i , s i ).
The extraction function is "local" if it uses a terminal bounded subsequence of T w i . Here it will use the last actual trace event only

a i 2 (T w i = T w i-1 a i ). • S 0 ⊆ S, set of initial states.
The local extraction and reconstruction functions can be extended to obtain the functions E (resp. I) between sets of virtual and actual traces, as follows:

E(T v n ) = s 0 E l (s 0 , r 1 , s 1 , T w 0 )...E l (s i-1 , r i , s i , T w i-1 )...E l (s n-1 , r n , s n , T w n-1 ) = T w n , as E l (s i-1 , r i , s i , T w i-1 ) = a i and T w i = s 0 a 1 ...a i . And I(T w n ) = s 0 I l (s 0 , T w 1 )...I l (s i-1 , T w i )...I l (s n-1 , T w n ) with I l (s i-1 , T w i ) = (r i , s i ). The Observational Semantics is faithful if E and I satisfy the faithfulness property, i.e. if ∀T v , T w f inite, E(T v ) = T w ∧ I(T w ) = T v .

Exemple 1

The figure 3 illustrates the following simple automaton (arrows are labeled by type of actions).

• S = {s 0 , s 1 , s 2 },

• R = {a, b},

• A = {a, b},
• ∀s, T (b, s) = s 1 , T (a, s 1 ) = s 2 ,

• E l (s, r, s ′ ) = r (the generated actual trace is not used),

• ∀s, I l (s, b) = (b, s 1 ), I l (s 1 , a) = (a, s 2 ) (the last actual trace event only is used),

• S 0 = {s 0 }.

The virtual traces are: s 0 (b, s 1 ) + {(a, s 2 )(b, s 1 ) + } * . The actual traces are:

s 0 b + (ab + ) * . s 1 s 2 b b b a s 0 Figure 3: Exemple 1: Finite State Automaton
It is straightforward to see that this OS is faithful, using the regular expression form of the traces.

Faithful Trace Specification

We first give a condition for an OS to be faithful.

Proposition 1

Given an OS < S, R, A, T r, E l , I l , S 0 >, E and I the extensions of E l and I l as above, if the following condition holds: ∀r, s, s ′ , a, T w , T r(r, s) = s ′ ⇒ (E l (s, r, s ′ , T w ) = a ∧ I l (s, T w a) = (r, s ′ )), where T w is a finite actual trace generated by successive applications of the transition function T r from an initial state s 0 until an ultimate state s, then the OS is faithful, i.e. ∀T v , T w f inite, E(T v ) = T w ∧ I(T w ) = T v , where T v is a virtual trace corresponding to successive applications of the transition function T r from an initial state s 0 until an ultimate state s.

Proof 1 The proof is by induction on the size of the traces. By definition with each new transition actual and virtual traces are increased by one event only. Initially: (traces of size 0)

E(s 0 ) = s 0 ∧ I(s 0 ) = s 0 .
Let us assume the property holds for a trace of size n:

(1) E(T v n ) = T w n ∧ I(T w n ) = T v n (2)
. ( 1) means, according to the definition of E, that T w n is the actual trace generated by n successive applications of T r function from a state s 0 until some ultimate state s n by using the local extraction function E l at each step.

(2) means, according to the definition of I, that T v n is the virtual trace reconstructed from the actual trace T w n . The holding conjunction means that the reconstructed virtual trace is the same as the one used to produce the actual one, therefore I(T w n ) ends in a state s n , the same as for T v n .

One shows that (++ concatenation and list constructor are omitted for singletons)

(1') E(T v n+1 ) = T w n+1 ∧ I(T w n+1 ) = T v n+1 ( 2
E(T v n+1 ) = E(T v n (r n+1 , s n+1 )) = T w n E l (s n , r n+1 , s n+1 , T w n ) = T w n a n+1 = T w n+1
, by hypothesis (1) and where the last argument of E l , T w n , is the actual trace resulting from E(T v n ). (2') holds:

I(T w n+1 ) = I(T w n a n+1 ) = T v n I l (s n , T w n ) = T v n (r n+1 , s n+1 ) = T v n+1
, by hypothesis (2) and the definition of I l .

The proposition 1 shows how to design a faithful observational semantics: by specifying together the local extraction and reconstruction functions, verifying at each step defined by the transition function that the generated trace allows to reconstruct the same reached state as the one specified by the transition function.

This results can be extended to actual subtraces (defined as traces obtained by considering a subset of attributes of the actual traces), provided that there are sufficiently many attributes in the subtrace to recompute parameters (then the corresponding virtual subtrace is a virtual trace with a subset of parameters) 3 . This is illustrated in the figure 2. A query applied to the actual trace selects a partial actual trace in such a way that the resulting partial trace can be reconstructed as a partial virtual trace (the one from which the partial actual trace could be extracted). In practice, the generic trace specification consists of an operational semantics corresponding to some abstract level of process observation, instrumented to produce an actual trace. The level of description (granularity of the events) should be chosen in such a way that this abstract operational semantics can be abstracted from each particular semantics of each process of the family. Symmetrically, it is requested that the abstract operational semantics can be "implemented" in each process of the family.

The faithfulness property of the observational semantics guarantees that the generic actual trace preserves the whole information concerning the process behavior, in such a way that all desirable properties of the semantics can be studied just by looking at the trace.

Generic Trace for CHR ∨

In this section we introduce the generic trace proposed for CHR ∨ . It is based on the refined Theoretical Operational Semantics for CHR, ω ∨ r , as defined in [5]. Such semantic is declarative enough to cover most of the CHR implementations. It is the case for ECLiPSe Prolog [2] and SWI-Prolog [START_REF] Wielemaker | SWI-Prolog 5.6 Reference Manual[END_REF] whose operational semantics can be viewed as a refinement of ω ∨ r (conversely ω ∨ r can be viewed as an abstraction of the semantics of these implementations).

Introducing CHR ∨

Constraint Handling Rules emerges in the context of Constraint Logic Programming (CLP) as a language for describing Constraint Solvers. In CLP, a problem is stated as a set of constraints, a set of predicates and a set of logical rules. Problems in CLP are generally solved by the interaction of a logical inference engine and constraint solving components. The logical rules (written in a host language) are interpreted by the logical inference engine and the constraint solving tasks are delegated to the constraint solvers. We borrow from [START_REF] Oliveira | Towards a Generic Framework to Generate Explanatory Traces of Constraint Solving and Rule-Based Reasoning[END_REF] some elements of presentation.

The following rule base handles the less-than-or-equal problem:

a n t i s y m m e t r y @ leq ( X , Y ) , leq ( Y , X ) <=> X = Y . reflexivi t y @ leq ( X , X ) <=> true . idempoten c e @ leq ( X , Y ) \ leq ( X , Y ) <=> true . t r a n s i t i v i t y @ leq ( X , Y ) , leq ( Y , Z ) ==> leq ( X , Z ) .

This CHR program specifies how leq simplifies and propagates as a constraint. The rules implement reflexivity, antisymmetry, idempotence and transitivity in a straightforward way. The ref lexivity rule states that leq(X, Y ) simplifies to true, provided it is the case that X = Y . This test forms the (optional) guard of a rule, a precondition on the applicability of the rule. Hence, whenever we see a constraint of the form leq(X, X) we can simplify it to true.

The antisymmetry rule means that if we find leq(X, Y ) as well as leq(Y, X) in the constraint store, we can replace it by the logically equivalent X = Y . Note the different use of X = Y in the two rules: in the ref lexivity rule the equality is a precondition (test) on the rule, while in the antisymmetry rule it is enforced when the rule fires. (The reflexivity rule could also have been written as ref lexivity@leq(X, X) <=> true.)

The rules ref lexivity and antisymmetry are simplification rules. In such rules, the constraint found are removed when the rule applies and fires. The rule idempotence is a simpagation rule, Inria only the constraint in the right part of the head will be removed. The rule says that if we find leq(X, Y ) and another leq(X, Y ) in the constraint store, we can remove one.

Finally, the transitivity rule states that the conjunction leq(X, Y ), leq(Y, Z) implies leq(X, Z). Operationally, we add leq(X, Z) as (redundant) constraint. without removing the constraints leq(X, Y ), leq(Y, Z). This kind of rule is called propagation rule.

The CHR rules are interpreted by a CHR inference engine by rewriting the initial set of constraints by the iterative application of the rules. Its extension with disjunctive bodies, CHR ∨ boosts its expressiveness power, turning it into a general programming language (with no need of an host language). Summarizing, there are three kinds of rules in CHR as in CHR ∨ : simplification, propagation and simpagation.

The simpagation rules are the most general category of rules and they have the following form r@H k \H r ⇔ G|B., where r is an identifier for the rule, H r and H k are the heads of the rule (in the following they will be denoted respectively as keep and remove), G is the guard, and B is the body. If the guard is true, it can be omitted.

The operational semantics of such rule is that if H k and H r are found in the constraint store and the guard G is entailed by it, the constraints in H r should be removed and the constraints in the body B should be added to the constraint store. If H k is empty, this rule is called a Simplification Rule, and this part of the rule is omitted. On the other side, if H r is empty, this rule is called a Propagation Rule. In this case, the second part of the head of the rule is omitted and the ⇔ is replaced by the symbol ⇒.

In CHR ∨ , we distinguish two kinds of constraints: Rule defined constraints (RDC), which are declared in the current program and defined by CHR rules, and built-in constraints (BIC), which are predefined in the host language or imported CHR constraints from some other module. Furthermore, in CHR ∨ , bodies may contain disjunctions.

Exemple 2

The following CHR ∨ rule defines the append(X,Y,Z) constraint:

r1 @ append(X,Y,Z) <=> (X = [], Z = Y); (X = [H|L1], Z = [H|L2], append(L1,Y,L2)).
In this rule, Z is a list composed by the elements of the list X followed by the elements of the list Y. If append(X,Y,Z) holds, we have two options: (i) X=[] and, therefore, Z=Y; or (ii) X is a list in the form [H|L1], and thus, Z is composed by H followed by L1 and then followed by the elements in Y.

We illustrate the CHR ∨ solver behavior, by showing the effect of successive applications of the CHR ∨ rules on the constraint store. Let us suppose the initial state of the constraint store is append([1], [2], Z). The actual execution of this rule base is represented by the following set of transitions. The notation G 0 ; . . . ; G n represents the alternative stores. The transition → r1 represents the application of r 1 and the transition → * the removal of failed stores. Notice that from the final state we can conclude Z = [1, 2]:

append([1], [2], Z) →r 1 [1] = [], Z = [2] ; [1] = [1|[]], Z = [1|L2], append([], [2], L2) → * [1] = [1|[]], Z = [1|L2], append([], [2], L2) →r 1 [1] = [1|[]], Z = [1|L2], [] = [], L2 = [2] ; RR n°7939 [] = [H|L1], L2 = [H|L2 ′ ], append(L1, [2], L2 ′ )) → * [1] = [1|[]], Z = [1|L2], [] = [], L2 = [2] 3.2 Operational Semantics ω ∨ r
The ω ∨ r semantics given here is adapted from [9]. We define CT as the constraint theory which defines the semantic of the built-in constraints and thus models the internal solver which is in charge of handling them. We assume it supports at least the equality built-in. We use [H|T ] to indicate the first (H) and the remaining (T ) terms in a list or stack, + for pushing elements into stack (there may be several pushed elements represented as a list), ++ for sequence concatenation and [] for empty sequences. We use the notation {a 0 , . . . , a n } for both bags and sets. Bags are sets which allow repeats. We use ∪ for set union and ⊎ for bag union, {} to represent both the empty bag and the empty set, and E -E ′ to remove all occurrences of elements of E ′ from E. The identified constraints have the form c#i, where c is a user-defined constraint and i a natural number. They differentiate among copies of the same constraint in a bag. We also use the functions chr(c#i) = c and id(c#i) = i with their natural extension to lists of constraints and of identifiers.

A CHR program is a sequence of rules, and the head and body of a rule are considered sequences of atomic constraints. A number is associated with every atomic head constraint, called the occurrence. Head constraints are numbered per functor, starting from 1,in top-down order from the first rule to the last rule, and from left to right. However, removed head constraints in a simpagation rule are numbered before kept head constraints. This numbers will be used to show in witch position the active constraint is (the j indicator).

An execution state E is a tuple A, S, B, T n , where • A is the execution stack;

• S is the UDCS (User Defined Constraint Store), a bag of identified user defined constraints;

• B is the BICS (Built-in Constraint Store), a conjunction of constraints;

• T is the Propagation History, a set of sequences for each recording the identities of the user-defined constraints which fired a rule;

• n is the next free natural used to number an identified constraint.

Current alternatives are denoted as ordered sequence of execution states,

L = [E 1 , E 2 , ...E n ]
where E 1 is the active execution state and [E 2 , ..., E n ] the remaining alternatives.

The initial configuration is represented by

L 0 = [ A, {}, true, {} 1 ].
The top of execution stack A is a "goal" constraint (the one corresponding to the initial goal of the program) that will be processed.The transitions are applied non-deterministically until no transition is applicable anymore.

The formal description of the transitions is done in the form of rules: for each type of action r ∈ R there is a rule of the form r s → s ′ , such that T r(r, s)

= s ′ . Inria Solve+Wake [ [c|A], S, B, T n |L] → [ A ′ + A, S, c ∧ B, T n |L],
where c is built-in and A ′ = wakeup(S, c, B) where wakeup is a function that implements the wake-up policy [9] whose result is a list of constraints of S woken by adding c to B.

Activate

[ [c|A], S, B, T n |L] → [ [c#n : 1|A], c ⊎ S, B, T n+1 |L],
where c is userdefined constraint.

Reactivate

[ [c#i|A], S, B, T n |L] → [ [c#n : 1|A], S, B, T n |L],
where c is userdefined constraint.

Apply.1 [ [c#i : j|A], H1 ⊎ H2 ⊎ S, B, T n |L] → [ [c#i : j|A], H1 ⊎ H2 ⊎ S, B, T n |L]
where the j th occurrence of a constraint with same functor as c exists in the head of a fresh variant of a rule r@H ′ 1 \H ′ 2 ⇔ g|C and a matching substitution modulo B, e a , such that chr(H1) = e(H ′ 1 ), chr(H2) = e(H ′ 2 ) and {(r, id(H1)++id(H2))} / ∈ T .

Apply.2 [ [c#i : j|A], H1 ⊎ H2 ⊎ S, B, T n |L] → [ C + H + A, H1 ⊎ S, e ∧ B, T ′ n |L]
where the j th occurrence of a constraint with same functor as c exists in the head of a fresh variant of a rule r@H ′ 1 \H ′ 2 ⇔ g|C and a matching substitution moduloB, e a , such that chr(H1) = e(H ′ 1 ), chr(H2) = e(H ′ 2 ) and {(r, id(H1)++id(H2))} / ∈ T and CT |= ∃(B) ∧ ∀B ⊃ ∃(e ∧ g) and T ′ = T ∪ {(r, id(H1)++id(H2))}, and

H = c#i : j if c is in H1, H = [] if c is in H2, and c ∈ H1∨H2. Drop [ [c#i : j|A], S, B, T n |L] → [ A, S, B, T n |L],
where there is no occurrence j for c in the program. This semantics is adapted from [9], it differs mainly by two additional type of actions: Apply.1 (Apply.2 corresponds to the original Apply rule) and Fail. Apply.1 corresponds to an attempt of using a CHR rule and will be applied only once for each j, H1, H2 occurrence. If the transition Apply.2 is applied, there was an application of Apply.1 for the same occurrence j, but the converse does not hold. The Fail case corresponds to a failed computation. In this case, other alternatives are explored.

Default [ [c#i : j|A], S, B, T n |L] → [ [c#i : j + 1|A], S, B, T n |L], if no other tran- sition is possible in the current state. Split [ [c1 ∨ ... ∨ cm|A], S, B, T n |L] → [σ1, ...,

Generic Trace

We introduce here the generic actual trace of CHR ∨ informally. Each transition in the ω ∨ r semantics should generate an actual trace event. Here are the expected types of actions together with the other possible attributes. There are two categories of attributes: those coding the virtual states which may serve for the reconstruction, some others may bring useful information for potential applications.

Each transition corresponding to the type of action r generates an actual trace event whose first attribute characterizes r uniquely. A subset of the attributes only is attached to a specific type of event. Attributes are as follows:

• Port, or Event Name: p. It belongs to {W ake, ActivateRDC, ReactivateRDC, T ryRule, ApplyRule, Drop, Def ault, Split, F ail}.

There is an obvious bijection between R (the set of type of actions) of the OS and this set of event names. It belongs to all events and is always the first attribute.

• Constraint instance of some type w where the constraint is a term c before the first activation, or c#i : j in the other cases, where i and j are integers. A constraint will be represented by a list of form [p, t • Reference to a previous trace event: ref, where ref has the form @i and i is an integer identifying a previous actual trace event (a previous chrono).

• Rule name: r@, where r@ is the name of a rule in the source program.

• State number: n. An integer corresponding to the parameter numbering a solver virtual state. It belongs to all events and is always the last attribute. This is formalized in the following tables. The first table is a context free syntax of the generic trace. Terminals are between brackets. Non terminals corresponding to attributes are names of attributes. Optional items are between square brackets (those which are not in terminals), options are separated by vertical bars. Brackets after ∈ denote a set (to avoid multiplicity of rules). The following lists all attributes (specific or other) for each actual trace event corresponding to some type of action. All examples4 are extracted from a generic trace of the section 6.3.

• Solve+Wake (port W ake): a built-in constraint (BIC) is solicited and some constraints are woken 2 attributes (total 5):

-Cons: the built-in constraints being "executed".

-Woken: the (possibly empty) list of the constraints woken by the wake-up policy. -Cinst: the user defined constraint which is "introduced" and "executed". The attribute value is the created instance of this constraint.

Example: GT: [3,ActivateRDC,[edge,r1,r9,332],333]

• Reactivate (port ReactivateRDC): Activate a Rule defined constraint with justification 2 attributes (total 5):

-Cinst: the user-defined constraints instance being "re-executed", which became active.

-Ref: a reference to the Solve+Wake event where this constraint has been woken (form of justification).

Example: GT:[62,Reactivate,[node,r1,a0,359],@61,360]

• Apply.1 (port T ryRule): attempt to apply a Rule; it may be followed by an Apply.2 event in case of successful application, or another event in case it cannot by applied. 5 attributes (total 8):

-RuleName: the name of the tried rule in the source code.

-Cinst: the active user-defined constraint instance (the one at the top of the execution stack).

-Keep: the keep constraints of the store used to match the head of the tried rule.

-Remove: the remove constraints of the store used to match the head of the tried rule.

-Guard: the guard constraints of the tried rule (as in the source program). This information may be useful in case of failure.

Example -Ref: a refence to the previous Apply.1 event where the name of the applied rule, the active constraint and some other information can be found.

-Addrdc: the user-defined constraints instances of the body of the applied rule, pushed on the stack.

-Addbic: the built-in constraints instances of the body of the applied rule, pushed on the stack.

-Keep: the keep constraints of the store used to match the head of the tried rule.

-Remove: the remove constraints of the store used to match the head of the tried rule.

-Match: the successful matching equations (a way to give the current substitution).

-Cinst: the active user-defined constraint instance (the one at the top of the execution stack). • Drop (port Drop): drop a constraint. The currently active constraint c#i : j is removed from the stack. There is no more occurrences j for c in the program. 1 attribute (total 4):

-Cinst: the constraint which is popped from the execution stack.

Example: GT: [4,Drop,[edge,r1,r9,332],333]

• Default (port Def ault): The occurrence index j of the active constraint c#i : j is incremented (proceed to the next occurrence of the constraint instances in the program). There is no more occurrences j for c in the program. 2 attributes (total 5):

-Cinst: the last used constraint occurrence.

-Index: The occurrence Index j is incremented (proceed to the next occurrence of the constraint instances in the program.

Example: GT: [28, Def ault, [node, r7, r, 5, 386], 6, 388]5

• Split (port Split): create a disjunction. Occurs when a rule is disjunctive. 1 attribute (total 4):

-Ref: a reference to the most recent Apply.2 event with the rule whose body contains the disjunction.

Example: GT: [60,Split,@59,360]

• Fail (port F ail): the referred rule application fails. It Occurs when the Built-In store has been tested false.

1 attribute (total 4):

-Ref: a reference to the most recent failed Apply.2 event.

Example: GT: [104,F ail,@103,376]

All the variables which occur in the initial goal will keep their original name in all their occurrences in the generic trace. Each actual trace event has a unique identifier, called the chrono, which is an integer incremented by 1 at each new event.

The formal definition of trace generation will be given in section 4.1.

4 Observational Semantics of CHR ∨ (OS-CHR ∨ )

We specify the observational semantics of CHR ∨ , OS-CHR ∨ , on the top of the operational semantics of section 3.2, by specifying the transition function and the local functions of extraction E l and of reconstruction I l . The resulting OS, called OS-CHR ∨ , is faithful by construction (by property 1).

According to the definition 1, the observational semantics consists of < S, R, A, T r, E l , I l , S 0 >. The definition of the transition function T r is given by the operational semantics. The definitions of E l , I l are given in the next two sections. The others elements are as follows.

• S: domain of virtual states. It the set of configurations defined as a list of execution states, where an execution state E is defined by the A, S, B, T n as described in the section 3.2.

• R: finite set of action types: {Solve+Wake, Activate, Reactivate, Apply.1, Apply.2, Drop, Default, Split, Fail}

• A: domain of actual states: each state consists of a tuple of values of a subset of the attributes. All attributes are defined in the section 3.3.

• S 0 ⊆ S, set of initial states, specified below.

In this presentations the chrono is omitted.

OS-CHR ∨ : Extraction (T r, E l )

This description is based on the transitions as described in the table 3.2. Each item corresponds to a type of action and it specifies the new generated actual trace event, using the previous state, the reaches state and the previously generated actual trace. The current generated actual trace is denoted N , an ordered sequence of the trace events. It has the form, for each type of action r and transition T r(r, s) = s ′ : E l (s, r, s ′ , N ) = a, which will be represented by a rule:

r s, N → s ′ , N ++a
The initial configuration will be represented as

L 0 = [ A, {}, true, {} 1 ], N = [] Solve+Wake [ [c|A], S, B, T n |L], N → [ A ′ + A, S, c ∧ B, T n |L], N ++[W ake, c, wakeup(S, c, B), n], where SolveCond. Activate [ [c|A], S, B, T n |L], N → [ [c#n : 1|A], c ⊎ S, B, T n+1 |L],
N ++[ActivateRDC, c, n], where c is a rule-defined constraint

Reactivate [ [c#i|A], S, B, T n |L], N → [ [c#n : 1|A], {c#n} ⊎ S, B, T n |L], N ++[ReactivateRDC, c, wake(c, N )],
where CondReac (see below)

Apply.1 [ [c#i : j|A], H1 ⊎ H2 ⊎ S, B, T n |L], N → [ [c#i : j|A], H1 ⊎ H2 ⊎ S, B, T n |L],
N ++[T ryRule, r, c#i : j, H1, H2, g, n] where CondApp1 (see below). The conditions appearing in our observation semantics are defined as follows: SolveCond: c is built-in, and A ′ = wakeup(S, c, B) defines which CHR constraints of S are woken by adding the constraint c to the built-in store B.

CondReac: the function wake : Constraint, T race → W ake is responsible for selecting the Wake event that justifies the Reactivate.

CondApp1: where the j th occurrence of a constraint with same functor as c exists in the head of a fresh variant of a rule r@H ′ 1 \H ′ 2 ⇔ g|C and a matching substitution e, such that chr(H 1 ) = e(H ′ 1 ), chr(H 2 ) = e(H ′ 2 ) and {(r, id(H 1 )++id(H 2 ))} / ∈ T . CondApp2: C is the body of the rule r@H ′ 1 \H ′ 2 ⇔ g|C. The tryRule : T race → T ryRule will retrieve the TryRule event generated by Apply.1. It will search for the event in the trace log, normally the event TryRule will be one step back. addRDCs : Body → Sequence(RDC) will select only the RDCs on the body; the function addBICs : Body → Sequence(BIC) will select the BICs on the body. Same conditions of Apply.1 plus CT |= ∃(B) ∧ ∀B ⊃ ∃(e ∧ g) , T ′ = T ∪ {(r, id(H 1 )++id(H 2 ))}, and

H = c#i : j if c is in H 1 , H = [] if c is in H 2 , and c ∈ H 1 ∨H 2 .
CondSplit: where σ i = [A i |A], S, B, T n , for 1 ≤ i ≤ m, and rule : T race → ApplyRule is a function that will retrieve the cause of the split, a disjunctive rule.

CondF ail: n is the numbering of the failed state E, and rule(N ) is a function that will retrieve the cause of the failure. We show here, by specifying a local reconstruction function I l , that the observationa semantics is faithful, i.e. that the extracted (actual) generic trace contains all information needed to reconstruct the original virtual trace (the trace semantics equivalente to the given operational semantics).

The local reconstruction function takes a current state s and the generated actual trace including the last generated event a, N ++a; it identifies the type of action r and produces the new virtual state s ′ . It has the form, for each type of action r: I l (s, N a) = (r, s ′ ), which will be represented by a rule:

r s, N ++a → s ′ with a = [r|a ′ ].
The initial configuration will be represented as

L 0 = [ A, {}, true, {} 1 ], N = []
For each item corresponding to a type of action, the reconstructed state s ′ is the same as the new state obtained by the corresponding transition T r(r, s) = s ′ as described in the table 3.2. This constitutes the proof of faithfulness of OS-CHR ∨ , by property 1.

The conditions consists of an optional condition part and a computation part. They are just used here to express computations.

Solve+Wake [ A, S, B, T n |L], N ++[W ake, c, C, n ′ ] → [ C + A ′ , S, c ∧ B, T n ′ |L], if SolveCond. Activate [ A, S, B, T n |L], N ++[ActivateRDC, c, n ′ ] → [ [c#n ′ : 1|A ′ ], c ⊎ S, B, T n+1 |L], if ActiCond. Reactivate [ A, S, B, T n |L], N ++[ReactivateRDC, c#i, wakeEvent, n ′ ] → [ [c#n ′ : 1|A ′ ], {c#n ′ } ⊎ S, B, T n ′ |L], if CondReac.
] → [ C + A, H1 ⊎ S ′ , e ∧ B, T ′ n |L], if CondApp2. Drop [ A, S, B, T n |L], N ++[Drop, c#i : j, n ′ ] → [ A ′ , S, B, T n ′ |L], if DropCond. Default [ A, S, B, T n |L], N ++[Def ault, c#i : j, j ′ , n ′ ] → [ [c#i : j ′ |A ′ ], S, B, T n ′ |L], if Def Cond. Split [ A, S, B, T n |L], N ++[Split, r, n ′ ] → [σ1, ..., σm|L ′ ], if CondSplit. Fail [ A, S, B, T n |L], N ++[F ail, r, n ′ ] → L, if CondF ail. SolveCond: A = [c|A ′ ] ∧ n = n ′ ∧ C = wakeup(S, c, B). ActiCond: A = [c|A ′ ] ∧ n = n ′ . CondReac: A = [c#i|A ′ ] ∧ wakeEvent = wake(c, N ) ∧ n = n ′ . CondApp1: A = [c#i : j|A ′ ] ∧ S = H 1 ⊎ H 2 ⊎ S ′ ∧ n ′ = n. CondApp2: A = H +A ′ , C is the body of the rule r@H ′ 1 \H ′ 2 ⇔ g|C ∧S = H 1 ⊎H 2 ⊎S ′ ∧T ′ = T ∪ {(r, id(H 1 ) + id(H 2 ))} ∧ n ′ = n, and H = c#i : j if c is in H 1 , H = [] if c is in H 2 and c ∈ H 1 ∨H 2 .. DropCond: A = [c#i : j|A ′ ] ∧ n ′ = n. Def Cond: A = [c#i : j|A ′ ] ∧ j ′ = j + 1 ∧ n ′ = n. CondSplit: A = [A 1 ∨ ... ∨ A m |A ′ ], S, B, T n ∧σ i = [A i |A], S, B, T n , for 1 ≤ i ≤ m∧n ′ = n. CondF ail: n ′ = n.
Notice that the local reconstruction function does not use the full generated trace, but the last actual trace event only. This guarantees a better efficiency for analysis. However this is obtained at the cost of including specific details into the generic trace. For example the attribute n (state indicator) could be retrieved from the current virtual state; the fact to have it in the current actual trace event avoids some computation.

Prototyping the Operational Semantics of CHR ∨

The objective of building a prototype of the operational semantics described in the section 3.2 is to produce tests of trace generation, in order to improve the quality of the design. In fact there is no way to prove that the specification given in an algebraic style, with some implicit or informal parts, is sound. Indeed the simple fact to implement in Prolog an executable specification with which it is possible to simulate the extraction of the generic trace is a step towards a better quality of the proposed formal specification.

The SWI-Prolog implementation of the operational semantics of CHR ∨ is built with the feature to produce the generic trace. The following subsections illustrate the architecture of the proposed implementation. The full program is given in the annexe.

CHR ∨ Syntax and Rule Compilation

Listing 1: CHR ∨ Syntax :op ( 1 1 0 0 , xfx , \ ) . :op ( 1 1 8 0 , xfx ,==>) . :op ( 1 1 8 0 , xfx ,<=>) . :op ( 1 1 9 0 , xfy , @ ) .

The CHR ∨ Syntax is represented Prolog infixed operators as presented in Listing 1. This syntax accepts CHR ∨ rules like in the following CHR program: t r a n s i t i v i t y @ leq ( vX , vY ) , leq ( vY , vZ ) ==> leq ( vX , vZ ) . idempoten c y @ leq ( vX , vY ) / leq ( vX , vY ) <==> true . a n t i s y m m e t r y @ leq ( vX , vY ) , leq ( vY , vX ) <==> vX=vY .

However, the CHR ∨ Operational Semantics does not search rules individually. It searches for the i-th occurrence of some constraint operator in program. In order to provide the appropriate information, the CHR ∨ implementation generates a compiled version of this CHR ∨ program as presented below: the predicate rule(Op,Ind,Rule,Args,Remove,Keep,Guard,Body) identifies the CHR ∨ rule that contains the Indth occurrence of Op in its head.

Auxiliary Functions

To implement CHR ∨ Operational Semantics, it was necessary to define some auxiliary functions responsible for variable management and built-ins implementation.

Variables

In the proposed CHR ∨ implementation variables can be classified as local or global. Local variables are used in CHR ∨ Rules and should be replaced by global variables or constants when the rule is executed. CHR ∨ variables are not directly implemented using Prolog's variables because it was desirable to give more informations about variable names to trace and the search method.

In the implementation, variable can be any Prolog's atom. The predicates global_variable\1 and local_variable are used to decide if some term represents a global or local variable, respectively. In the initial implementation local variables are atoms whose first letter is "v" and the second is a upper-case letter. Global variables are terms in the form v(_) or atoms initiated with "v", followed by a lower-case letter.

Local variables should be replaced by constants or global variables when a CHR ∨ is executed. The predicate: instantiate_locals(T1,T2,Binds) replaces the local variables found in T1 by other values, producing the term T2; the argument Binds contains the performed substitutions. In T1 local variables are not replaced by a constant, the instantiable_locals predicate replaces the local variable by an undefined prolog variable. The auxiliary predicate allocate_unusedvars, instantiates these undefined variables with free global variables.

Built-ins Constraint

The equality constraint (=) is the only built-in constraint implemented. The built-in memory contains a list of normalized equalities in the form: GlobalVariable = (GlobalVariable | Constant).

To manipulate the built-in memory, two auxiliary functions are defined:

• solve_builtin(C,B1,B2,UDC1,UDC2): inserts the built-in constraint C in the built-in memory B1, producing the built-in memory B2. If the memory becomes inconsistent, the resultant memory produced is false. When the built-in constraint is inserted in memory, the User Defined Constraints Memory UDC1 is analyzed and the constraints affected by the built-in insertion are listed in UDC2.

• replace(T1,B,T2): replaces the global variables in T1 by their values (if they are defined), producing the term T2.

CHR ∨ Operational Semantics Implementation

The CHR ∨ Operational Semantics implementation is similar to the semantics proposed in Section 3.2. To illustrate this implementation, Listing 2 presents the Prolog implementation of the rules bf Solve+Wake and Activate.

Listing 2: Solver+Wake Rule

%S o l v e+Wake Rule [ ( [ C | A ] , UDC , B , H , N ) | Tl ]-->[(A2 , UDC2 , B2 , H , N ) | Tl ] :- is_builtin ( C ) , s o l v e _ b u i l t i n ( C , B , B2 , UDC , Wokeup ) , merge ( Wokeup , A , A2 ) , remove ( UDC , Wokeup , UDC2 ) . %A c t i v a t e Rule [ ( [ C | Tl ] , UDC , B , H , N ) | T ] ---> ( [ ( [ ( C3#0) | Tl ] , [ C3 | UDC ] , B←֓ , H , N2 ) ] | T ) :- is_UDC ( C ) , replace ( C , B , C2 ) , C3 = C2^N , N2 i s N + 1 .

Generic Trace Extraction

To generate the generic trace in the executable operational semantics, the predicate: gentrace(Id,Data) in added. It generates a trace with the information contained in Data. The Id represents the ordering number of the generated trace. To illustrate this, Listing 3 contains the modified version of the rules presented in Listing 2.

Listing 3: Solver+Wake Rule

%S o l v e+Wake Rule [ ( [ C | A ] , UDC , B , H , N ) | Tl ] ---> ( [ ( A2 , UDC2 , B2 , H , N ) | Tl ] ) ) ←֓ :- is_builtin ( C ) , s o l v e _ b u i l t i n ( C , B , B2 , UDC , Wokeup ) , i n s e r t _ r e f e r e n c e ( Wokeup , Pos , RefWokeup ) , merge ( RefWokeup , A , A2 ) , remove ( UDC , Wokeup , UDC2 ) , gentrace ( Pos , [ wake , C , [ wokeup , Wokeup ] ] ) . %A c t i v a t e Rule [ ( [ C | Tl ] , UDC , B , H , N ) | T ] ---> ( [ ( [ ( C3#0) | Tl ] , [ C3 | UDC ] , B←֓ , H , N2 ) | Tl ] ) :- isUDC ( C ) , replace ( C , B , C2 ) , C3 = C2^N , N2 i s N + 1 , gentrace ( _ , [ activate , C , N ] ) .

Inria

Executing a CHR ∨ Program

The CHR ∨ Operational Semantics is a small-step semantics: it describes a single computation step in program execution. To execute a CHR ∨ program, the implementation defines the operator (--*->) that executes continuously the Operational Semantics Operator (--->).

6 Prototyping of the generic CHR ∨ Trace Using SWI Prolog

A generic CHR ∨ tracer for SWI-Prolog was developed, as the default trace output contains most of the necessary info to build the GT. In Section 6.1, we introduce the SWI Prolog debug output trace produced when executing CHR rule bases. In the section 6.2, we explain the SWI CHR trace; Section 6.3 presents the way to map the SWI produced trace into OS-CHR ∨ , the actual generic trace.In the last two sections we present some trace queries and an example 6 .

Running Example

The generic trace will be illustrated on a simple disjunctive graph-coloring problem. The following CHR ∨ rules define a graph coloring solution:

node1@ node(r1,C) ==> (C = r ; C = b ; C = g). node2@ node(r2,C) ==> (C = b ; C = g). node3@ node(r3,C) ==> (C = r ; C = b). node4@ node(r4,C) ==> (C = r ; C = b).
node5@ node(r5,C) ==> (C = r ; C = g). node6@ node(r6,C) ==> (C = r ; C = g; C = t). node7@ node(r7,C) ==> (C = r ; C = b). startGraph@ edges<=> edge(r1,r2), edge(r1,r3), edge(r1,r4), edge(r1,r7), edge(r2,r6), edge(r3,r7), edge(r4,r5), edge(r4,r7), edge(r5,r6), edge(r5,r7). wrong@ edge(Ri,Rj), node(Ri,Ci), node(Rj,Cj) ==> Ci = Cj | false. l1@ l([ ],[ ]) <=> true. l2@ l([R|Rs],[C|Cs]) <=> node(R,C), l(Rs,Cs).

This CHR base handles a graph-coloring problem with at most 3 colors where any two nodes connected by a common edge must not have the same color. The constrain node(r1,C) means that node r1 has color C, the startGraph rule defines edges between nodes of a graph and the wrong rule assures that two nodes will have different colors. A small part of the SWI trace of the execution of the following goal "edges, l([r1,r7,r4,r3,r2,r5,r6],[C1,C7,C4,C3,C2,C5,C6])." is depicted here: (3) Apply: node(r7,_G9235) # <386> ==> _G9235=r;_G9235=b. CHR:

(4) Wake: node(r7,r) # <386> CHR:

(4) Try: node(r1,r) # <384>, edge(r1,r7) # <376>, node(r7,r) # <386> ==> r=r | false. CHR:

(4) Apply: node(r1,r) # <384>, edge(r1,r7) # <376>, node(r7,r) # <386> ==> r=r | false. CHR:

(3) Fail: node(r7,r) # <386> CHR:

(4) Wake: node(r7,b) # <386> ... This subset of the execution is responsible for trying the value C1 and C7 as red then backtracking because C1 and C7 cannot have the same colors.

Informal definitions of the trace events of SWI-Prolog can be found here 7 . Some problems occur when an analysis of the trace is needed: the try/apply transition has no rule name, it's very difficult to link the name of the generated var with the name of the variable passed as goal since all vars were renamed and there isn't an efficient way to query it.

Understanding SWI-Prolog Trace

The SWI-Prolog debugging output will produce a trace according to the following grammar depicted in table 3.

SWI-Prolog's default search strategy implemented is depth-first, the parameter depth indicates the transaction's actual level in the search tree and id is the constraint's unique identifier.

Small parts of the trace will be shown and explained.

CHR: (0) Insert: edges # <372> CHR: (1) Call: edges # <372>

The trace produced by these two ports are responsible for removing a constraint from the goal and insert in execution stack. Notice that in SWI's trace they always appear together.

CHR: (2) Exit: edge(r1,r2) # <373>

The computation over the active constraint is finished.

CHR: (3) Try: node(r7,_G9235) # <386> ==> _G9235=r;_G9235=b. CHR: (3) Apply: node(r7,_G9235) # <386> ==> _G9235=r;_G9235=b.

The trace produced by Try and Apply ports only happens together and it means that a rule was tried and applied respectively. CHR: (4) Wake: node(r7,r) # <386>

The Wake port is traced when a built-in is solved, in this case the constraint was reactivated because C7 = r.

Transforming SWI Tracer into OS-CHR ∨

The SWI's output is not enough to perform a translation to OS-CHR ∨ . We do need information about what was the goal passed (to map all variables) and access to the source-code (get the rule names). The inputs and outputs of the algorithm is illustrated by figure 4. The Translator's algorithm will be explained by example. Some ports have direct connection with OS-CHR ∨ : Call and Exit. All others ports will need a computation using the generated SWI trace. The Insert port is ignored because is redundant with the port Call.

CHR:

(1) Call: edges # <330> -> GT: [START_REF] Activaterdc ; Leq | [END_REF]ActivateRDC,[edges,330],331]

For the tryRule map, we have to look the source code and try to find what is the rule name for that transition, and while generating the trace we keep track of the active constraint.

CHR: (7) The Exit port has a direct map with OS-CHR ∨ .

CHR:

(2) Exit: edge(r1,r9) # <332> -> GT: [4,Drop,[edge,r1,r9,332],333]

The Fail port will produce a Fail event with its cause, a rule witch body contains the f alse built-in.

CHR:

(6) Fail: node(r5,a0) # <375> -> [109,Fail,@108,376]

Trace Querying

The produced generic trace is represented by a sequence of java objects. The language we choose for querying the trace is the SQL for Java Objects (JoSQL), its implementation can be found here 8 .

These are some examples of query in JoSQL: (on a trace of example 6)

• SELECT * FROM trace WHERE type ='ApplyRule' AND (name='wrong@' OR name='node1@' OR name='node2@') Will select the trace of the execution of rules: wrong, node1,node2.

• SELECT * FROM trace WHERE type ='Split' OR type ='Fail' Will select all split and fail transition.

• SELECT addrdc,remove,addbic FROM trace WHERE type ='ApplyRule'

The last query is more general and can by used by any application which need to handle a current state of the constraint store. production of the SWI trace (trace on), the third the time in generic trace mode, and the last column gives the ratio between the sizes of both traces. We observe that there is an (expected) slowdown in debugging modes (SWI trace and generic trace). It is slightly higher for the generic trace as it uses the SWI trace. Querying the generated trace does not slowdown more, since it can be done in paralel with trace generation.

For the selection of subtraces, tests executed on JoSQL show that that a list of 1,000,000 generic trace events can be queried in about 1.5s.

It must be noted that we limit the queries to patterns attached to a single event, limiting thus the complexity of the queries. Sophisticated queries envolving undetermined number of trace events could speed up seriously the performances.

Discussion

Several aspects of such a generic trace were explored on [START_REF] Oliveira | Towards a Generic Framework to Generate Explanatory Traces of Constraint Solving and Rule-Based Reasoning[END_REF], in particular its relations with components software development, the use of the fluent calculus to prototype traces and the use of object oriented specification methods. The generic trace presented in that work is thus limited to the simple theoretical operational semantics ω t [10] and therefore is less precise than the one given here.

Our approach of the observational semantics relies to abstract interpretation. The OS is similar to the "Observable Semantics" of Lucas [16] or the partial trace semantics of Cousot [3]. The parameters used to describe the execution states are, as expressed by Lucas, "syntactic objects used to represent the conduct of operational mechanisms". The traces are abstract representations of CHR ∨ semantics which allow to take into account the sole details we want to consider as common to different implementations. The (abstraction) relations between a generic trace and the traces of specific implementations of solvers are explored in [6], together with a compliance proof method. Furthermore the generic trace contains a set of details considered as useful in several debugging tasks with several levels of refinement or observation. It could be Inria enriched according to different needs10 , or refined without changing the semantics of the already existing one.

This way to proceed is opposite to the frequently adopted approach as, in particular, in [START_REF] Simonis | A Generic Visualization Platform for CP[END_REF], where a set of (visual) debugging tools is defined together with their input data, which consists of a restricted trace containing the minimal needed information. In our approach, we specify a semantically rich trace which can be used as input data for a potentially larger set of tools. The choice of the data to trace is made on the basis of a high level operational semantics, not on the basis of some specific debugging need. However the generic trace is designed in such a way that most of debugging tools devoted to the analysis of CHR resolution behavior may find in this trace what they need. As a consequence, based on this observational semantics, the work of implementation of the tracer and the work of designing debugging tools can be performed independently.

One may however feel that implementing a full generic trace is too much work demanding or that the resulting tracer performance will be considerably slow down. It has been shown in [15] that a generic approach may have more advantages than drawbacks in the sense that there may be a good trade-off between a very detailed generic trace (based on a more refined operational semantics) and the use of a trace driver able to query efficiently the generic trace, with a significant improvement in portability of debugging tools. We have shown here, that the implementation of the CHR ∨ generic trace in SWI-Prolog CHR implementation can easily be performed on the top of an existing tracer, resulting in a generic tracer practically as efficient as the original one on which it is based.

Conclusion

We have presented a first observational semantics of CHR ∨ (a formal specification of a CHR ∨ generic tracer), and two prototypes; the first is an executable operational semantics in Prolog which may produce a virtual generic trace; the second is a generic tracer of SWI CHR, based on the CHR SWI Prolog trace. The first helped to improve the quality of the formal operational semantics (in fact several corrections and/or improvements have been detected). The SWI CHR generic trace prototype shows that the generic trace can be easily and efficiently implemented on existing CHR ∨ implementations. The interest of the "generic approach" leads in the portability of analysis tools developed on the basis of this trace and the variety of possible trace based applications.

We do not claim that the CHR ∨ observational semantics which is presented here is the ultimate one. More refined observational semantics could be considered, including several levels of refinements (for example combining with Prolog semantics in Prolog based implementations); we just have shown that this approach can be realistic and useful in a great variety of CHR based software development.

Future work will concern more experimentation and improvements of the generic trace, OO based CHR implementation including a generic trace, and generic trace for hybrid constraint solvers. % testCase(ConstraintName,Index,Arguments,RuleName,Keep,Remove, % Guard,Body,returnFlag) :-dynamic(rule/9). % A Global variable a term v(N) or vU where U is not a uppercase % letter. global_variable(v(_)) :-!. global_variable(X) :-atom(X),atom_codes(X,[118,L|_]), (L<65 ; L>90). % A Local variable a term vUxxx where U is an uppercase letter local_variable(X) :-atom(X),atom_codes(X,[118,L|_]), L>=65, L=<90.

Figure 2 :

 2 Figure 2: Components in Trace Design

  Gen. traceT ::= Ev_1...Ev_m, m ≥ 0 Ev ::= {GT: [} Chrono {,} Port [Other] Spec_Attr {,} StateNumber {]} Chrono ::= {integer} Port ∈ { W ake, ActivateRDC, RectivateRDC, T ryRule, ApplyRule, Drop, Def ault, Split, F ail } Other ::= Ref | RuleName | Indice | CT | CTIJ Ref ::= {, @ integer} RuleName ::= {, identifier @} Indice ::= {, integer} Spec_Attr ::= ǫ | {,} SpecAttr Spec_Attr SpecAttr ::= {[} Attr ListCT {]} Attr ∈ { Woken, Addrdc, Addbic, Keep, Remove, Guard, Match } ListCT ::= ǫ | {,} (CT | CTIJ) ListCT) CT ::= {[ predicate, t_1, ..., t_n ]} CTIJ ::= {[ predicate, t_1, ..., t_n, i, j ]} StateNumber ::= {integer}

Example:

  GT: [61,Wake,[=,C1,a0],[woken,[[node,r1,C1,359]]],360] • Activate (port ActivateRDC): activate a Rule Defined Constraint (RDC) getting the RDC c#i : j from the top of the execution stack and activating it. 1 attribute (total 4):

Example:

  GT: [103,ApplyRule,@102,[addrdc],[addbic,[fail,fail]], [keep,[[node,r4,a0,371], [edge,r4,r5,340], [node,r5,a0,375]]], [remove,[]],[match,[edge(Ri,Rj)=node(,r4,a0)], [node(Ri,Ci)=edge(,r4,r5)], [node(Rj,Cj)=node(,r5,a0)]], [node,r5,a0,375],376]

Apply. 2

 2 [ [c#i : j|A], H1 ⊎ H2 ⊎ S, B, T n |L], N → [ C + [H|A], H1 ⊎ S, e ∧ B, T ′ n |L], N ++[ApplyRule, tryRule(N ), addRDCs(C), addBICs(C), H1, H2, e, H, n] where CondApp2 (see below).Drop [ [c#i : j|A], S, B, T n |L], N → [ A, S, B, T n |L], N ++[Drop, c#i : j, n]. Where c is an active constraint. Default [ [c#i : j|A], S, B, T n |L], N → [ [c#i : j + 1|A], S, B, T n |L], N ++ [Def ault, c#i : j, j + 1, n]. Split [ [c1 ∨ ... ∨ cm|A], S, B, T n |L], N → [σ1, ..., σm|L], N ++[Split, rule(N ), n],where CondSplit (see below).Fail [E |L], N → L, N ++[F ail, rule(N ), n], where CondF ail (see below).

Inria

4. 2

 2 OS-CHR ∨ : Reconstruction (I l )

Apply. 1 [

 1 A, S, B, T n |L], N ++[T ryRule, r, c#i : j, H1, H2, g, n ′ ] → [ [c#i : j|A ′ ], H1 ⊎ H2 ⊎ S ′ , B, T n |L], if CondApp1. Apply.2 [ A, S, B, T n |L], N ++[ApplyRule, r, RDCs, BICs, H1, H2, e, H, n ′

  {P 1 ...P m }, m ≥ 0 Ports P ::= C|E|F |R|W |I|RE|T Y |A Call C ::= "CHR : (depth)Call : "CT Exit E ::= "CHR : (depth)Exit : "CT Fail F ::= "CHR : (depth)F ail : "CT Redo R ::= "CHR : (depth)Redo : "CT Wake W ::= "CHR : (depth)W ake : "CT Insert I ::= "CHR : (depth)Insert : "CT Remove RE ::= "CHR : (depth)Remove : "CT Constraint CT ::= constraintN ame(

Figure 4 :

 4 Figure 4: Translator structure For the Wake port the we have to look to previous values of the trace and determine what BIC solving fired this transition and also a Reactivate event will be produced. In this case C1 = a0 was the cause. CHR: (3) Wake: node(r1,a0) # <359> -> [61,Wake,[=,C1,a0],[woken,[[node,r1,C1,359]]],360] ++ [62,Reactivate,[node,r1,a0,359],@61,360]

  replace(T1,[],T1). replace(T1,[(K=V)|M],T2) :-replace(T1,K,V,T_), replace(T_,M,T2). %% For all local variables not initialized in the Head or Guard, %% it creates a new global variable to replace this local one allocate_unusedvars([]). allocate_unusedvars([(_K=V)|TL]) :-var(V), counter(lastGlobalAllocated,N), V=v(N), allocate_unusedvars(TL). allocate_unusedvars([(_K=V)|TL]) :-nonvar(V), allocate_unusedvars(TL). % Creates a Map that assigns all local_variables of T1 to % an undefined value and T1 is the term T1 with these replacements % applied instantiate_locals(T1,T2,Map) :-local_variable(T1), !, at(Map,T1,T2). instantiate_locals(T1,T2,Map) :-T1=..[F|Arg1], instantiate_list_locals(Arg1,Arg2,Map), T2=..[F|Arg2]. instantiate_list_locals([],[],_). instantiate_list_locals([H1|T1],[H2|T2],M) :-instantiate_locals(H1,H2,M),instantiate_list_locals(T1,T2,M). Compiler code (compiler.pl): %% CHR Syntax :-op(1100,xfx,\ ). :-op(1180,xfx,==>). :-op(1180,xfx,<=>). :-op(1190,xfy,@). % Transforms CHR sequences (A,B,C) in Prolog Lists [A,B,C] makelist(true,[]) :-!. makelist((X,Y),L) :-!,makelist(X,L1),makelist(Y,L2), merge(L1,L2,L). makelist(L,[L]).

2 . 2 7 3 17 5

 22717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Components in Trace Design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Observational Semantics (OS) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.4 Faithful Trace Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Generic Trace for CHR ∨ 8 3.1 Introducing CHR ∨ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Operational Semantics ω ∨ r . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.3 Generic Trace . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4 Observational Semantics of CHR ∨ (OS-CHR ∨ ) 15 4.1 OS-CHR ∨ : Extraction (T r, E l ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2 OS-CHR ∨ : Reconstruction (I l ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . Prototyping the Operational Semantics of CHR ∨ 18 5.1 CHR ∨ Syntax and Rule Compilation . . . . . . . . . . . . . . . . . . . . . . . . . 18 5.2 Auxiliary Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 5.3 CHR ∨ Operational Semantics Implementation . . . . . . . . . . . . . . . . . . . . 20 5.4 Generic Trace Extraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 5.5 Executing a CHR ∨ Program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 6 Prototyping of the generic CHR ∨ Trace Using SWI Prolog 21 6.1 Running Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 6.2 Understanding SWI-Prolog Trace . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 6.3 Transforming SWI Tracer into OS-CHR ∨ . . . . . . . . . . . . . . . . . . . . . . 23 6.4 Trace Querying . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 6.5 Trace Analyzer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  1 , t 2 , ..., t m ] or [p, t 1 , t 2 , ..., t m , i, j]. w is cons in the former case and cinst in the later. • List of constraints instances of some type w: w-lc. It may be a list of terms or a list of the form [w, [[c 1 ], ..., [c m ]]], each element represented by a list as above. w is the kind of constraints. It may be woken, addrdc, addbic, keep, remove or guard constraints, or a matching substitution match, represented by a list of equations.

Table 1 :

 1 Syntax of the Generic Trace GrammarInriaThe following table gives the list of the attributes other than Chrono, Port and StateNumber for each type of event. The firts item is the transition name (∈ R), the second item the corresponding port (value of the attribute Port) and the last item is the list of attributes.

	r ∈ R	Port	Specific Attributes
	Solve+Wake W ake	Cons, Woken
	Activate	ActivateRDC	Cinst
	Reactivate	ReactivateRDC Cinst, Ref
	Apply.1	T ryRule	RuleName, Cinst, Keep, Remove, Guard
	Apply.2	ApplyRule	Ref, Addrdc, Addbic, Remove, Match, Cinst
	Drop	Drop	Cinst
	Default	Def ault	Index
	Split	Split	Ref
	Fail	F ail	Ref

Table 2 :

 2 Specific Attributes for each type of event (except chrono and state number)

  Inria rule ( leq , 1 , transitivity , [ vX , vY ] , [ ] , [ leq ( vX , vY ) , leq ( vY , vZ ) ] , [ ] , [ leq ( vX , vZ ) ] ) . rule ( leq , 2 , transitivity , [ vY , vZ ] , [ ] , [ leq ( vX , vY ) , leq ( vY , vZ ) ) ] , [ ] , [ leq ( vX , vZ ) ] ) . rule ( leq , 3 , idempotency , [ vX , vY ] , [ leq ( vX , vY ) ] , [ leq ( vX , vY ) ] , [ ] , [ true ] ) . rule ( leq , 4 , idempotency , [ vX , vY ] , [ leq ( vX , vY ) ] , [ leq ( vX , vY ) ] , [ ] , [ true ] ) . rule ( leq , 5 , antisymmetry , [ vX , vY ] , [ active , leq ( vY , vX ) ] , [ ] , [ ] , [ vX=vY ] ) rule ( leq , 5 , antisymmetry , [ vY , vX ] , [ leq ( vX , vY ) , leq ( vY , vX ) ] , [ ] , [ ] , [ vX=vY ] )

Table 3 :

 3 t 1 ...t n )"# < id > " Swi-Trace's Grammar

	Try	T Y	::= T Y propagation |T Y simplif ication |T Y simpagation
	Try2	T Y propagation	::= "CHR : (depth)T ry : "H k " ==> "G"|"B|
	Try3	T Y simplif ication ::= "CHR (depth)T ry : "H r " <=> "G"|"B|
	Try4	T Y simpagation	::= "CHR : (depth)T ry : "H k \H r " <=> "G"|"B
	Apply	A	::= A propagation |A simplif ication |A simpagation
	Apply2	A propagation	::= "CHR : (depth)Apply : "H k " ==> "G"|"B|
	Apply3 Apply4 Head	A simplif ication A simpagation H	::= "CHR : (depth)Apply : "H ′ r <=> ′ G"|"B| ::= "CHR : (depth)Apply : "H ′ k \ ′ H r " <=> "G"|"B ::= CT | CT ", "H
	Constraint2	CT 2	::= constraintN ame(t 1 ...t n )
	Body or BIC G, B	::= CT 2 | CT 2 ", "G
	CHR:

  ApplyRule is the most complicated map, we have to link(@) with the tryRule and check if it has a disjunctive body, if it is we have keep track to link correctly with a possible failure status; it can generate a lot of trace event depending on how many constraints were added/removed and possibly a split transition. The link function will recover the real name of the variable, in this case _G9245 = C8

		Try: node(r4,a0) # <371>, edge(r4,r5) # <340>,
	node(r5,a0) # <375> ==> a0=a0 | fail.
	->
	GT: [102,TryRule,failure@,[node,r5,a0,375],[keep,[[node,r4,a0,371],
	[edge,r4,r5,340], [node,r5,a0,375]]],[remove,[]],
	[guard,[[=,a0,a0]]],376]
	CHR:	(9) Apply: node(r8,_G9245) # <390> ==> _G9245=a0;
	_G9245=a1;_G9245=a2;_G9245=a3.
	->
	[141,ApplyRule,@140,[addrdc],[addbic,[=,C8,a0],[=,C8,a1],
	[=,C8,a2],[=,C8,a3]],[keep,[[node,r8,C8,390]]],
	[remove,[]],[match,[node(_,C)=node(r8,C8)]],
	[node,r8,C8,390],391]
	++
	GT: [142,Split, @141, 391]

RR n°7939

In general a bounded number of element should be used, but also some forward elements like a i+1 ... For more details see[7].Inria

This implies some restrictions on the kind of queries (in case of dependencies between parameters or attributes) which are not detailed here. For more details see[7].RR n°7939

The Prototype does not generate the j index of the constraint, therefore there isn't any example with this info.RR n°7939

It's a hand-made example. Although, It's not difficult to compute how many Default transitions was applied before the Drop or Apply.2. For the prototype this transition is negligible.Inria

http://www.swi-prolog.org/pldoc/doc_for?object=section(2,'7.4',swi('/doc/Manual/debugging.html')) Inria

http://josql.sourceforge.net/ Inria

An extensive study about the needs for constraint debugging can be found in[8].RR n°7939

RR n°7939RESEARCH CENTRE PARIS -ROCQUENCOURTDomaine de Voluceau, -Rocquencourt B.P. 105 -78153 Le Chesnay Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

A ANNEX: Operational Semantics in Prolog

The following is an implementation of the refined operational semantics of CHR ∨ in SWI-Prolog. There are 6 files and 390 lines of Prolog's code.

util.pl code:

:-dynamic(val/2). counter(Name,C) :-val(Name,C), !, retract(val(Name,C)), C2 is C + 1, assert(val(Name,C2)). counter(Name,0) :-assert(val(Name,1)).

% Auxiliary list functions elem(E,[E|_]). elem(E,[_|T]) :-elem(E,T). subset([],_). subset([H|T],L) :-elem(H,L),subset(T,L). alldifferent([]). alldifferent([H|T]

) :-\+ elem(H,T), alldifferent(T). Inria gentrace(Idx,X) :-counter(trace_number,Idx),mywrite('['), mywrite(Idx), forall(elem(N,X),(mywrite(','),mywrite(N))),write(']\n'). trace(X) :-mywrite(X), mywrite('\n'). Test code (test.pl):

:-[chr].


D Papadimitriou

A Cabellos

Stability Analysis of Path-vector Routing

Keywords: Path-vector, routing, stability, metrics

Most studies on path-vector routing stability have been conducted empirically by means of ad-hoc analysis of BGP data traces. None of them consider prior specification of an analytic method including the use of stability measurement metrics for the systematic analysis of BGP traces and associated meta-processing for determining the local state of the routing system. In this paper, we define a set of metrics that characterize the local stability properties of path-vector routing such as BGP (Border Gateway Protocol). By means of these stability metrics, we propose a method to analyze the effects of BGP policy-and protocol-induced instability on local routers.

Introduction

Research efforts to understand BGP's instability led to classify them as policy-or protocol-induced to account for the distinction between protocol operation and the inherent behavior of the underlying path-vector routing algorithm: 1) Policyinduced instabilities: addressing routing stability consistently with planned BGP routing policy implies eliminating nondeterministic routing states resulting from policy interactions and in particular, non-deterministic and unintended but unstable states. Griffin et al.'s seminal work [START_REF] Griffin | The Stable Paths Problem and Interdomain Routing[END_REF] modeled BGP as a distributed algorithm for solving the Stable Paths Problem, and derived a general sufficient condition for BGP stability, known as "No Dispute Wheel". This sufficient condition guarantees the existence of a stable solution to which BGP always converges. Informally, this sufficient condition allows nodes to have more expressive and realistic preferences than always preferring shorter routes to longer ones. The game theoretic approach introduced in [START_REF] Levin | Interdomain routing and games[END_REF] relies on the best-reply BGP dynamics: a convergence game model in which each Autonomous System (AS) is instructed to continuously execute the following actions: i) receive update messages from BGP peering nodes announcing their routes to the destination, ii) choose a single peering node whose route is most preferred to send traffic to, iii) announce the new route to peering nodes. However, as proved in [START_REF] Levin | Interdomain routing and games[END_REF], best-reply BGP dynamics is not incentivecompatible even if No Dispute Wheel condition holds: even if all but one AS are following the BGP rules, the remaining AS may not have the incentive to follow them. Interestingly, as demonstrated in [START_REF] Levin | Interdomain routing and games[END_REF], incentive compatibility of best-reply BGP dynamics requires combining an additional global condition (Route Verification) together with the "No Dispute Wheels" to guarantee stability. Consequently, all known conditions for global stability are sufficient but not necessary conditions (checking them is an NP-hard problem and enforcing them requires a global deployment of an additional mechanism); on the other hand, local instability effects have yet to be characterized; 2) Protocol-induced instabilities: BGP is an inter-AS pathvector routing protocol subject to Path Exploration phenomenon like any other path-vector algorithm. Indeed, BGP routers may announce as valid, routes that are affected by a topological change and that will be withdrawn shortly after subsequent routing updates. This phenomenon is the main reason for the large number of routing updates received by BGP routers which exacerbate inter-domain routing system instability and processing overhead [START_REF] Huston | Damping BGP[END_REF]. Both result in delaying BGP convergence time upon topology change/failure [START_REF] Labovitz | Delayed Internet Routing Convergence[END_REF]. Several mitigation mechanisms exist to partially limit the effects of path exploration; however, none actually eliminate its effects. Hence, BGP is intrinsically subject to instability. The objectives for investigating path-vector routing stability are to 1) Develop a method to process and interpret the data part of BGP routing information bases in order to identify and characterize occurrences of BGP routing system instability; such characterization can be used as a comparison point for the stability of the newly developed schemes (candidate to replace BGP) and characterize instability phenomena any routing system would have to cope with; 2) Determine a set of stability metrics and develop methods for using them in order to provide a better understanding of the BGP routing system's stability; 3) Investigate how path-vector routing behavior and network dynamics mutually influence each other. The proposed method aims to bring rigor and consistency to the study of routing stability.

Routing Stability and Metrics

Preliminaries

The AS topology of the routing system is described as a graph G = (V,E), where the vertices (nodes) set V, |V| = n, represents the AS, and the edges set E, |E| = m, represents the links between AS. At each node u ∈ V, a route r per destination d (d ∈ D) is selected and stored as an entry in the local routing table (RT) whose total number of entries is denoted by N, i.e., |RT| = N. At node u, a route r i to destination d at time t is defined by r i (t) = {d, (v k =u, v k-1 ,…,v 0 =v), A} with k > 0 | ∀ j, k ≥ j > 0, {v j , v j-1 } ∈ E and i ∈ [1,N], where (v k =u, v k-1 ,…,v 0 =v) represents the AS-path, v k-1 the next hop of v along the AS-path from node u to v, and A its attribute set. Let P (u,v),d denote the set of paths from node u to v towards destination d where each path p(u,v) is of the form {(v k =u, v k-1 ,…,v 0 =v), A}. A routing update leads to a change of the AS-path (v k , v k-1 ,…,v 0 ) or an element of its attribute set A. A withdrawal is denoted by an empty AS-path (ε) and A = ∅: {d,ε,∅}. According to the above definition, if there is more than one AS-path per destination d, they will be considered as multiple distinct routes.

Stability definitions

The stability of a routing system is characterized by its response (in terms of processing of routing information) to inputs of finite amplitude. Routing system inputs may be classified as i) internal system events such as routing protocol configuration change or ii) external events such as those resulting from topological changes. Both types of events lead to the exchange of routing updates that may result in routing states changes. Indeed, BGP (and in general any path-vector routing) does not differentiate routing updates with respect to their root cause, their identification (origin), etc. during its selection process.

Definition 1: Let RT(t) represent the routing table at some time t. At time t+1, RT(t+1) = RT 0 (t) ⊕ ∆RT(t+1) where, RT 0 (t) is the set of routes that experience no change between time t and t+1, and ∆RT(t+1) accounts for all route changes (additions, deletions, and changes to previously existing routes) between time t and t+1. The magnitude of the output of a stable routing system should be small whenever the input is small. That is, a single routing information update shall not result in output amplification. Equivalently, a stable system's output will always decrease to zero whenever the input events stop. A routing system, which remains in an unending condition of transition from one state to another when disturbed by an external or internal event, is considered to be unstable. Provide means for measuring the magnitude of the output is the main purpose of the metric referred to as "stability of the selected route". For this purpose, we define the criteria for qualifying the effect of a perturbation on the local routing table so as to locally characterize the stability of the routing system. More precisely, let |∆RT(t+1)| be the magnitude of the change to the routing table (RT) between time t = t 0 + k to t +1 = t 0 + (k +1), where t 0 is the starting time of the measurement sequence, we distinguish three different equilibrium states for the routing table: Definition 2: when disturbed by an external and/or internal event, a RT is considered to be stable if the following condition is met: |∆RT(t+1)| ≤ α, t → ∞, where α > 0 is small. In these conditions, if the routing system returns locally to its initial equilibrium state, it is considered to be (asymptotically) stable. Definition 3: when disturbed by an external and/or internal event, a RT is considered to be marginally stable if the following condition is met: α < |∆RT(t+1)| ≤ β, t → ∞, where β > 0 is small, α < β.In these conditions, if the routing system transitions locally to a new equilibrium state, it is considered to be marginally stable. Definition 4: when disturbed by an external and/or internal event, a RT is considered to be unstable if the following condition is met: |∆RT(t+1)| > β, t → ∞. In these conditions, the routing system remains locally in an unending condition of transition from one state to another and it is considered to be locally unstable The values α and β shall be set based on operational criteria. Among other factors, α and β depend on the observation sampling period that must be set to the Minimum Routing Advertisement Interval (MRAI) in order to ensure one routing update per sampling period. A similar reasoning to the one applied for the Loc_RIB stability (that corresponds to the BGP routing table) can be applied to the Adj_RIB_In (which stores incoming routes from neighbors). It is also interesting to measure the instability induced by the BGP selection process.

Stability metrics

To measure the degree of stability of the Loc_RIB, Adj_RIB_In, and determine how close the routing system is to being unstable the following stability metrics are defined.

The stability ϕ i (t) of selected routes r i (t) characterizes the stability of the routes r i (i ∈ [1,|D|]) stored at time t in the Loc_RIB (|Loc_RIB| = N) by quantifying the magnitude of change for these routes from time t to t+1. This metric quantifies the magnitude of change for these routes between time t = t 0 +k to t+1 = t 0 +(k+1), where t 0 is the starting time of the measurement sequence (time units are counted by default in terms of minimum routing advertisement interval (MRAI)), and the integer k accounts for the number of MRAI times that have elapsed since the starting time of the measure sequence. The latter determines the minimum amount of time that must elapse between a routing advertisement of a route to a particular destination by a BGP peer. This metric quantifies thus the magnitude of change to route r i , and a routing table with a periodicity determined by the MRAI time. This metric can be directly computed by using the algorithm described in Fig. 1.

When route r i is created: ϕ i (t) ← 0 if r i experiences a path or an attribute change (r i (t+1) ≠ r i (t)) then ϕ i (t+1) ← ϕ i (t) + 1 else /* r i experiences no changes */ if ϕ i (t) = 0 then ϕ i (t+1) ← 0 else if ϕ i (t) > 0 then ϕ i (t+1) ← ϕ i (t) -1 end if end if end if Fig.

-Stability of individual routes

The computation of the stability metric for an entire routing table (RT) can then be derived from the stability of its individual routes (see Fig. 2). Let |∆r i (t+1)| denote the change in stability metric for a single route r i from time t to t+1. These values are used to compute |∆RT(t+1)| defined as the change in stability metric for the entire routing table from time t to t+1. Moreover, |∆RT(t+1)| is normalized so that 0 ≤ |∆RT(t+1)| ≤ 1, where 0 implies perfect stability, and 1 indicates complete instability.

The most stable route in the Adj_RIB_In (|Adj_RIB_In| = M) quantifies the relative stability between incoming routes to the same destination d as learned from all upstream BGP peers (i.e., downstream from the point of view of the AS-path towards destination d) and the one amongst them determined at time t as the most stable. For this purpose, let W u ⊂ V denote the set of node's u BGP peers, |W u | = W ≤ M, and w one of its elements such that (u,w) ∈ E. Let ϕ i,j (t) denote the stability of the route r i (t) to destination d as received by peering router j (j ∈ [1,W]) at time t. At node u, r' i,stable (t)=min{ϕ i,j (t), ∀j ∈ [1,W] | {(v k =u,v k-1 =w,…,v 0 =v),A} ∈ P (u,v),d , ∀w ∈ W u } defines -independently of the BGP route selection rules-the selectable route that is the most stable for destination d at time t. Next, we define ∆ϕ i as the relative measure of route r i stability ϕ i,j at time t+1 with respect to stability ϕ i,stable of the most stable route r' i,stable at time t for the same destination d.

For i=1 to N /* total number of routes in RT(t+1) */ if r i (t+1) is a new route then |∆r i (t+1

)| ← 0 else if ϕ i (t)=0 & ϕ i (t+1)=0 then |∆r i (t+1)| ← 0 else if ϕ i (t+1) > ϕ i (t) then |∆r i (t+1)|←[ϕ i (t)+1]/[ϕ i (t+1)+1] else |∆r i (t+1)|←[ϕ i (t)]/[ϕ i (t+1)] end if end if end if end i loop µ = |∆RT(t+1)| ← Σ i ∆r i (t+1)/N σ 2 ← Σ i (∆r i (t+1) -|∆RT(t+1)|) 2 /N
∆Φ i (t+1) ← Σ j ∆ϕ i,j (t+1)/|W u | end i loop µ = ∆Φ(t+1) ← Σ i ∆Φ i (t+1)/N σ 2 ← Σ i (∆Φ i (t+1) -∆Φ(t+1)) 2 /N

Fig. 3 -Most stable route

The best selectable route from the Adj_RIB_In quantifies the relative stability between incoming routes to the same destination d as learned from all upstream peers and the one amongst them selected by BGP at time t as the best route (thus, following BGP route selection rules). The computational procedure is the same as Fig. 3 if one replaces ϕ i,stable by ϕ i,selected .

The differential stability between the most stable route in the Adj_RIB_In and the selected route stored in the Loc_RIB for the same destination d characterizes the stability of the currently selected routes for a given destination d against most stable routes as learned from upstream neighbors. This metric provides a measure of the stability of the learned routes compared to the stability of the currently selected route. A variant of this metric, denoted δϕ i (i ∈ [1,|D|]), characterizes the stability of the newly selected path p*(u,v) at time t for destination d against the stability of the path p(u,v) that is stored as time t in the Loc_RIB for destination d and that would be replaced at time t+1 by the path p*(u,v): δϕ i (t) = ϕ i (t) -ϕ i *(t). In turn, if δϕ i (t) > 0, then the replacement of r i (t) by r i *(t) increases stability of the route to destination d; otherwise, the safest decision is to keep the currently selected route r i (t) stored in the Loc_RIB. Application of the metric δϕ i during the BGP selection process would prevent replacement of more stable routes by less stable ones but also enable selection of more stable routes than the currently selected routes. However, for this assumption to hold, we must prove the consistency of the stability-based selection with the existing preferential-based route selection model that relies on a path ranking function (i.e., a non-negative, integervalue function λ u , defined over P (u,v),d , such that if p 1 (u,v) and p 2 (u,v) ∈ P (u,v),d and λ u (p 1 ) < λ u (p 2 ) then p 2 (u,v) is said to be preferred over p 1 (u,v)). The route selection problem is consistent with the stability function δϕ(t) if ∀ u ∈ V and p 1 (u,v) and (u,v), then the route selection problem is consistent with the stability function δϕ and the route selection is stretch decreasing.

p 2 (u,v) ∈ P (u,v),d (1) if λ u (p 1 ) < λ u (p 2 ) then δϕ(t) = ϕ 1 (t) -ϕ 2 (t) ≥ 0 and (2) if λ u (p 1 ) = λ u (p 2 ) then δϕ(t) = 0. We show in [6] that if p 1 (u,v) and p 2 (u,v) ∈ P (u,v),d ∧ p 2 (u,v) is embedded in p 1

Measurement results

This section presents the experimental results obtained by applying the metrics defined in Section 2 to real-world BGP data. The dataset we used was obtained from the Route Views project [5] that comprises archives containing BGP feeds from a set of worldwide distributed Linux PCs running Zebra. As the only policy applied by Route Views sets the next hop to the peer IP address, only Adj_RIBs_In is accessible. As a consequence, the Loc RIB was inferred from the Adj_RIBs_In by implementing a selection process used by Zebra routers. Fig. 4 shows that incoming routes stored in Adj_RIB_In have on average slowly decreasing stability compared to the most stable route (a value close to 1 indicates that incoming routes are nearly as stable as the most stable route). As a result, the plot has a small but positive slope. The average of the maximum metric value per destination d shows a positive but larger slope: the most unstable routes have a faster paced decreasing stability (and spiky pattern confirms their unstable behavior). Further, during the entire observation duration (40 days), a subset of routes continuously presented instabilities leading to a monotonic increase of the metric. It can be seen from Fig. 4 that the BGP selected route has on average a better stability than the other routes out of which it is selected (a value close to 1 indicates that incoming routes are nearly as stable as the best selectable route). Comparison between Fig. 4 and Fig. 6 reveals though that local maxima for the selected route exhibits more spaced and less intensive variations than the most stable route (a lower metric value indicates a higher stability). One can also observe the same monotonously increasing trend of the metric for both the average and the maximum, due to routes with sustained instability. Local maxima in Fig. 7 indicate large changes in local route stability, i.e., more routes than the average experienced instabilities but BGP quickly converges to a new stable state since part of the affected routes return to their initial state (thanks to the presence of more stable routes in the Adj_RIB_In, as indicated in Fig. 5). Interestingly, Fig. 7 shows also that the intensity of the instability increases over time indicating that more routes get affected by the change. Fig. 8 shows the difference between the cumulated percentage of routes against the AS_path length difference between the selected and the most stable route. A positive difference indicates that the replacement of the selected route (using the path ranking function) by the most stable route would decrease the AS_path length compared to the selected route whereas a negative difference indicates that such replacement would increase the AS_path length. From this figure, we can deduce that such replacement would be advisable for about 90% of the selected routes and for 25% percent this replacement would also lead to an AS_path length decrease. Interestingly, only 10% of the routes would be affected by an AS_path length increase if selected based on the stability criteria. Among these 10%, we can also observe from this figure that a significant fraction of the routes is covered if an AS_path length increase of one-hop is acceptable. On the other hand, by admitting a stretch increase corresponding to one additional AS-hop in the AS_path, only a minor fraction of the routes (about 2%) would be penalized by a higher stretch increase (two AS-hops and above). This observation can be seen as the experimental proof that enforcing stability would not come at the detriment of increasing the stretch of most AS-paths.

Conclusion and perspectives

In this paper, we propose several stability metrics to characterize the local effects of BGP policy-and protocol-induced instabilities on the routing tables. Our experimental results show that the proposed method enables detecting instability events affecting the routing tables, and deriving their impact on the local stability of the routing system. We have also determined a differential stability-based decision criterion that can be taken into account as part of the route selection process. Ongoing work includes verifying the trade-offs between stability-based route selection and the resulting stretch increase/decrease factor on the selected routing paths. Moreover, the relationship between local and global stability will be further elaborated to characterize the effects resulting from the selection of a route that is more stable locally onto the global stability of the routing system, and the model extended to discriminate between protocol-and policy-induced instabilities.

Fig. 2 -

 2 Fig. 2 -Stability computation for a set of routing entries For i=1 to N /* |destinations in Adj_RIB_In| = |Loc_RIB| */ for j=1 to |W u | /* number of peers for i th destination */ ∆ϕ i,j (t+1)←[ϕ i,j (t+1)+1]/[ϕ i,stable (t)+1] end j loop

Fig. 4 :Fig. 8 :Fig. 6 :

 486 Fig.4: Most stable route metric measure Fig.5: Cum.variance against most stable route