Jihene Ben Rejeb

Irinel-Constantin Morȃrescu

Jamal Daafouz

Event triggering strategies for consensus in clustered networks

This paper focuses on consensus in networks partitioned in several clusters. It uses the multi-agent framework in which the network is seen as a sum of interconnected subsystems called agents. We assume that each agent updates its state continuously by taking into account the states of some other agents belonging to the same cluster. This protocol allows reaching only local agreements in the network. In order to get consensus we endow an agent per cluster with the capacity to discretely interact outside its own cluster. The discrete interaction of one agent with agents from other clusters is modeled as a state jump or reset. The inter-clusters interactions are activated by using event dependent rules. The goal of the paper is to design event triggering reset strategies that guarantee the consensus is achieved. No global dwell time separating the reset instants is imposed but we show that a dwell time per cluster is ensured by the proposed reset strategies.

I. INTRODUCTION

Analysis and control of multi-agent systems attracted a lot of researchers during the last decade. This is certainly due to the omnipresence and variety of networks in our daily life. The multi-agent formalism allows treating applications coming from a wide spectrum of domains such as biology [START_REF] Ratmann | From evidence to inference: Probing the evolution of protein interaction networks[END_REF], [START_REF] Pavlopoulos | Using graph theory to analyze biological networks[END_REF], sociology [START_REF] Hegselmann | Opinion dynamics and bounded confidence models, analysis, and simulation[END_REF], [START_REF] Blondel | On Krause's multi-agent consensus model with state-dependent connectivity[END_REF], [START_REF] Morȃrescu | Opinion dynamics with decaying confidence: Application to community detection in graphs[END_REF], economy [START_REF] Andreoli | Coordination as negotiated transactions[END_REF] or engineering [START_REF] Tanner | Stable flocking of mobile agents part i: Dynamic topology[END_REF], [START_REF] Bullo | Distributed Control of Robotic Networks[END_REF]. Each agent has only a local, limited information on the overall network, which means it applies decentralized strategy to reach a global goal.

The most studied problem on this topic is synchronization or consensus. It was mainly studied for linear agents interacting through a directed or an undirected graph with a fixed or dynamically changing topology [START_REF] Jadbabaie | Coordination of groups of mobile autonomous agents using nearest neighbor rules[END_REF], [START_REF] Ren | Consensus seeking in multiagent systems under dynamically changing interaction topologies[END_REF], [START_REF] Moreau | Stability of multiagent systems with time-dependent communication links[END_REF]. Nevertheless, the literature on nonlinear agents is also very reach considering coupled oscillators dynamics [START_REF] Gfeller | Spectral coarse graining and synchronization in oscillator networks[END_REF], [START_REF] Steur | Semi-passivity and synchronizationof diffusively coupled neuronal oscillators[END_REF], [START_REF] Morȃrescu | Synchronization of coupled nonlinearoscillators with shifted gamma-distributed delays[END_REF], nonholonomic robots [START_REF] Tanner | Flocking in teams of nonholonomic agents[END_REF], [START_REF] Bullo | Distributed Control of Robotic Networks[END_REF] but also general dynamics encompassing the previous ones [START_REF] Bus | Consensus for black-box nonlinear agents using optimistic optimization[END_REF]. A basic assumption in most of the multi-agent systems studies is the network connectivity. There also exist works designing the controllers that are able to preserve the network connectivity [START_REF] Zavlanos | Distributed connectivity control of mobile networks[END_REF] or topology [START_REF] Fiacchini | Convex conditions on decentralized control for graph topology preservation[END_REF]. Networks that asymptotically can loose connectivity were also analyzed [START_REF] Morȃrescu | Opinion dynamics with decaying confidence: Application to community detection in graphs[END_REF], [START_REF] Touri | On approximations and ergodicity classes in random chains[END_REF].

In this paper we consider that networks are partitioned in several clusters that are almost all the time isolated one from another. Each cluster is represented by a graph that is connected in a weak manner that will be defined in the next section. The agents continuously update their state by taking into account the states of other agents belonging to the same cluster. This protocol allows reaching local agreements different from one cluster to another. To enforce consensus we assume that each cluster contains an agent endowed with better interaction capabilities that enable it to exchange information outside its cluster.

As explained in [START_REF] Bragagnolo | Lmi sufficient conditions for the consensus of linear agents with nearlyperiodic resets[END_REF], this model can be interpreted in terms of opinion dynamics. Precisely, many social networks are structured in clusters and decision making process can be simplified as rapid/continuous-time iterations inside clusters accompanied by rare/discrete-time interactions between leaders of the clusters. The model can also be used in consensus for networks of robots spatially partitioned in clusters. Due to sensing limitation and energy saving the agents interact continuously only locally -inside clusters. From time to time, discretely, long distance interactions are afforded by a small number of agents that reset their state by taking into account the information received from other agents outside their cluster.

It is worth noting that in [START_REF] Bragagnolo | Lmi sufficient conditions for the consensus of linear agents with nearlyperiodic resets[END_REF] all the resets were synchronized and the reset sequence was time dependent. The main assumptions were the time-separation and persistence of resets. Thus, the periods between consecutive resets of the overall multi-agent system were uniformly bounded. In [START_REF] Morȃrescu | Coordination in networks of linear impulsive agents[END_REF] the authors also considered time-dependent resets but the reset sequences are independently defined for each cluster. This leads to asynchronous resets satisfying a dwell-time condition only inside each cluster but a global dwell-time lower bounding the period between consecutive resets of the overall multi-agent system no longer exist.

Unlike [START_REF] Bragagnolo | Lmi sufficient conditions for the consensus of linear agents with nearlyperiodic resets[END_REF], [START_REF] Morȃrescu | Coordination in networks of linear impulsive agents[END_REF], in this paper we design event based reset sequences. Event and self triggering strategies already exists in the literature [START_REF] Dimarogonas | Distributed eventtriggered control for multi-agent systems[END_REF], [START_REF] Shi | Multi-agent robust consensus-part ii: Application to distributed event-triggered coordination[END_REF]. The main difference here is that replacing the discrete event triggering dynamics by continuous dynamics would lead in our case to system instability. The events triggering the resets are independently defined for each cluster leading to asynchronous reset sequences. The event-triggering strategy is mainly motivated by the fact that it avoids unnecessary and costly inter-clusters interactions.

The remaining paper is organized as follows. In Section II we introduce the concepts and we mathematically formalize the problem. Section III introduces the assumptions of work and recall some existing results that will be used in the sequel. The main contributions of the paper which is the design and analysis of reset strategies guaranteeing consensus are presented in Section IV. Numerical illustration are provided in Section V before concluding the paper.

Notation. The following standard notation will be used throughout the paper. The set of nonnegative integers, real and nonnegative real numbers are denoted by N, R and R + , respectively. For a vector x we denote by x its Euclidian norm. The transpose of a matrix A is denoted by A . Given a symmetric matrix A ∈ R n×n , notation A > 0 (A ≥ 0) means that A is positive (semi-)definite. By I k we denote the k × k identity matrix. 1 k and 0 k are the column vectors of size k having all the components equal 1 and 0, respectively. We also use x(t - k ) = lim t→t k ,t≤t k x(t).

II. PROBLEM FORMULATION

A. Graph theory prerequisites

We consider a network of n agents described by the digraph (i.e. directed graph) G = (V, E) where the vertex set V represents the set of agents and the edge set E ⊂ V × V represents the interactions.

Definition 1: A directed path of length p in a given digraph G = (V, E) is a union of directed edges p k=1 (i k , j k ) such that i k+1 = j k , ∀k ∈ {1, . . . , p -1}. The node j is connected with node i in a digraph G = (V, E) if there exists at least a directed path in G from i to j (i.e. i 1 = i and j p = j). A strongly connected digraph is such that any of its two distinct elements are connected. A strongly connected component of a digraph is a maximal subset of V such that any of its two distinct nodes are connected. We say node i is a parent of node j in the digraph G = (V, E) if (i, j) ∈ E. A directed tree is a directed subgraph in which there exists a single node without parents called root while all the others have exactly one parent. A directed spanning tree of a digraph is a directed tree that links all the nodes of the graph. A digraph G is called weakly connected if it contains at least one spanning tree. For a given graph G = (V, E), the subgraph induced by a subset of nodes U ⊆ V is the graph U, E ∩ U × U .

In the sequel, we consider that the vertex set V is partitioned in m clusters C 1 , . . . , C m . We denote by n i the cardinality of each cluster C i .

Let us also introduce the intra-cluster graph G L = (V, E L ) containing only the edges of G that connect agents belonging to the same cluster. That is

E L = {(i, j) ∈ E | ∃k ∈ {1, . . . , m} such that i, j ∈ C k }.

B. System dynamics

The state of each agent evolves continuously by taking into account the states of other agents belonging to their cluster. Doing so, the agents approach local agreements which can be different from one cluster to another. In order to reach the consensus in the entire network every inter-cluster connection is activated at some discrete instants. When the inter-cluster link (j, i) ∈ E \E L is activated, the state of agent i is reset to a weighted average of the states of i and j. If several links arriving at i are activated simultaneously, all the source states of these edges are considered in the weighted average. In order to keep the presentation simple each agent will have a scalar state denoted by x i . We also introduce the vectors x = (x 1 , . . . , x n ) ∈ R n collecting the states of all the agents and x Ci collecting the states of the agents belonging to cluster i, respectively.

Let T be the countable set of reset instants which are described by the diverging and increasing sequence (t k ) k . Thus, the previous discussion is formally described by the linear reset system defining the overall network dynamics:

   ẋ(t) = -Lx(t), ∀t ∈ R + \ T x(t k ) = P (t k )x(t - k ) ∀k ∈ N x(0) = x 0 (1)
where x 0 ∈ R n , L ∈ R n×n is a generalized Laplacian matrix associated to the intra-cluster graph G L and P (t k ) ∈ R n×n is a stochastic matrix associated to the inter-cluster graph

G P (t k ) = (V, E P (t k )) where E P (t k ) = ∅ is the set of inter- cluster links activated at time t k , so that E P (t k ) ⊆ {(h, l) ∈ E|∃i, j ∈ {1, . . . , m}, i = j, h ∈ C i , l ∈ C j }.
Precisely, the entries of L and P (t k ) satisfy the following relations:

         L i,j = 0, if (j, i) / ∈ E L L i,j < 0, if (j, i) ∈ E L , i = j L i,i = - j =i L i,j , ∀i ∈ {1, . . . , n}, (2)
               P i,j (t k ) = 0, if (j, i) / ∈ E P (t k ), i = j P i,i (t k ) > 0, ∀i = {1, . . . , n} P i,j (t k ) > 0, if (j, i) ∈ E P (t k ), i = j n j=1 P i,j (t k ) = 1, ∀i ∈ {1, . . . , n}. (3)
According to (3), given some i, if P i,j (t k ) = 0 for all j = i then P i,i (t k ) = 1, meaning that no jump occurs on the state of the agent i at time t k . The values L i,j and P i,j (t k ) represent the weight of the state of the agent j in the updating process of the state of agent i when using the continuous and discrete dynamics, respectively. The matrices L and P (t k ) describe the level of influence of each agent inside its cluster and outside it, respectively. So, L is constant while P varies in time depending on which agents udpate their state. The weight of influence P i,j may also vary in time for a same couple (j, i).

It is worth noting that L has the following block diagonal structure

L =    L 1 . . . L m    , L i ∈ R ni (4)
with

L i 1 ni = 0 ni and P (t k )1 m = 1 m .

III. PRELIMINARIES

In this section we introduce the assumptions required for the development presented in the next section and we recall the main result in [START_REF] Morȃrescu | Coordination in networks of linear impulsive agents[END_REF] which is the basis of our stability analysis.

A. Work assumptions

In order to prove that the reset algorithm (1) guarantees asymptotic consensus for every initial condition x 0 we have to impose some standard assumptions. The first one concerns a minimal connectivity property of the whole network and of each cluster.

Assumption 1 (Network structure):

The graph G = (V, E) is such that • For each cluster C i , the induced graph C i , E L ∩ C i × C i
contains a spanning tree with the root r i ,

• eventually re-ordering the clusters, the following holds: for all i ≥ 2 there exist j < i and l i ∈ C j such that (l i , r i ) ∈ E. We denote by

E T = {(l i , r i )|i ∈ {2, . . . , m}}
the set of these m -1 such edges. The previous assumption implies that G contains a spanning tree having the root in C 1 (formed by the union of the spanning trees in each cluster together with the edges in E T ). The assumption is satisfied if the induced graph of each cluster is strongly connected and so is G. It also holds if the graph induced by the set of roots of all clusters contains a spanning tree. The first part of Assumption 1 has a direct consequence on the continuous dynamics since equation ( 2) imposes L i,j < 0 when (j, i) ∈ E L . The second part of Assumption 1 guarantees the existence of the inter-cluster interaction structure formed by E T . The next hypothesis of this work is standard in the literature (see [START_REF] Blondel | Convergence in multiagent coordination, consensus, and flocking[END_REF]) and it ensures a minimal influence of the states implicated in the reset process of the agents.

Assumption 2 (Minimal influence): There exists a constant α ∈ (0, 1) such that, for all reset times t k , if P i,j (t k ) = 0 and (i, j) ∈ E T then P i,j (t k ) ≥ α.

Remark 1: As stated at the end of the previous section, P i,j can vary in time. Thus P i,j , (i, j) ∈ E \ E L can converge to zero. However, in order to reach consensus, the interaction between clusters should not completely vanish. In this context, Assumption 2 guarantees a minimal influence of one cluster on the root of some other cluster at the reset time.

In order to emphasize that agents belonging to the cluster C i reset their state at time t k , we use extraction function φ i defined such that t φi(h) , h ∈ N is the h-th time an agent in cluster C i resets its state, i.e.

φ i (h) = min{k > φ i (h-1)|∃j ∈ C i , ∈ V\C i , P j, (t k ) > 0}.
where for consistency, we imposed φ i (-1) = -1, for all i ∈ {1, . . . , m}.

B. Sufficient condition for consensus

In order to guarantee consensus, two supplementary assumptions have been imposed in [START_REF] Morȃrescu | Coordination in networks of linear impulsive agents[END_REF]. They simply state that inter-cluster influence is persistent in time and the root of one cluster does not present accumulations of reset instants (Zeno phenomenon). In the sequel, instead of imposing these assumptions we design event-triggering reset strategies that will satisfy them. In the following we recall the main result in [START_REF] Morȃrescu | Coordination in networks of linear impulsive agents[END_REF] as well as the required assumptions.

Assumption 3: There exists a positive constant δ max > 0 satisfying the following: for all (l, r) ∈ E T ,

• there exists k ∈ N such that t k ≤ δ max and (l, r) ∈ E P (t k ), • if (l, r) ∈ E P (t k ) there exists τ ∈ [t k , t k + δ max ] such that (l, r) ∈ E P (τ ). Assumption 4: There exists a positive constant δ < δ max such that t φi(k+1) -t φi(k) ≥ δ, ∀i ∈ {1, . . . , m}. In other words, there exists a lower bound for the period between the consecutive reset instants on the state of agents belonging to the same cluster. Notice that according to Assumptions 1 and 3, all clusters in {2, . . . , m} reset an infinite number of times, so that for these clusters, φ i is well defined. Cluster C 1 may not reset an infinite number of times. In this case, t φ1 (k) is only defined for k smaller than some finite bound, and should still satisfy Assumption 4 for these k.

Let us introduce now the global diameter of the network at the time t ∈ R + :

∆(t) = max i∈V x i (t) -min i∈V x i (t)
Theorem 2 (Theorem 9 in [START_REF] Morȃrescu | Coordination in networks of linear impulsive agents[END_REF]): Suppose that Assumptions 1, 2, 3 and 4 hold. There exists some positive decay rate β ∈ [0, 1) such that for all t ∈ R + ,

∆(2(m + 1)δ max + t) ≤ β∆(t)
guaranteeing the consensus is asymptotically reached in the overall network.

IV. DESIGN OF EVENT TRIGGERED RESET RULE FOR

CONSENSUS

In order to avoid unnecessary inter-cluster communications we can define the reset sequence using an event-based strategy. In this section we propose two event based rules and we prove that they define reset sequences satisfying assumptions 3 and 4. This allows applying Theorem 2 to prove consensus subject to these reset rules. The first rule defining the reset sequence is not fully decentralized. Each reseting element r i needs to know the states of all the agents in its own cluster C i at the reset instants t φi(k) . This information is used to compute the local agreement value x * i (t k ). It is worth noting that this information, which is centralized at cluster level, is needed only at isolated instants corresponding to resets. Indeed, the function x * i (•) is constant on the interval [t φi(k) , t φi(k+1) ). The second rule defining the reset sequence is fully decentralized since it requires only local/decentralized information. The reseting element r i of cluster C i needs to know only the state of its neighbors. Nevertheless, each reseting element r i has to compute the maximal distance to its neighbors at every instant t ∈ [t φi(k) , t φi(k+1) ).

In the following we use the following instrumental assumption:

Assumption 5: The components of the Laplacian matrix L are uniformly bounded i.e. there exists α > 0 finite real number such that |L i,j | ≤ α, ∀i, j ∈ {1, . . . , n}. This is necessary to ensure that during the continuous dynamics, the agents do not approach one to another indefinitely fast. We can notice that, in practice, this assumption is very natural and is almost always satisfied.

A. Semi-decentralized event-triggered resets

First, let us introduce the diameter of the cluster C i as

∆ i (t) = max j∈Ci x j (t) -min j∈Ci x j (t).
Definition 3: The distance between the node r i and the local agreement value of the cluster C i at time t is denoted by

d i (t) =| x ri (t)-x * i (t) |.
Considering > 0 a fixed scalar, the reset sequence (t k ) k∈N associated with the dynamics ( 1) is defined as follows: for all i ∈ {1, . . . , m} and for all k ≥ 0,

• if d i (t φi(k-1) ) > we define t φi(k) = min t≥t φ i (k-1) d i (t) ≤ d i (t φi(k-1) ) a i , • otherwise, t φi(k) = t φi(k-1) + δ with δ = min i∈{1,...,m} a i -1 a i 2n i ᾱ∆ i (0) ,
where the a i > 1 are design parameters fixed a priori. (We recall that for consistency, we denote t φi(-1) = 0). Remark 2: In our numerical illustrations we consider a i = a j , ∀i, j ∈ {1, . . . , m} but these values can be used by the designer to change the reset frequency of some/all clusters.

Proposition 4: Let us consider the dynamics (1) under Assumptions 1, 2 and 5. Then, the associated reset sequence introduced by Definition 3 satisfies the Assumptions 3, 4.

Proof: If d i (t φi(k) ) ≤ , the second point in Definition 3 applies and Assumptions 3, 4 hold. Otherwise, the first point applies and for a fixed cluster C i , i ∈ {1, . . . , m} we have to show that the reset sequence satisfies Assumptions 3, 4.

• Again, we start by proving that Assumption 4 holds. This means, a dwell time δ exists between a reset time t φi(k) and the first time t such that when

d i (t) ≤ d i (t φi(k) ) a i .
We recall that for all t

∈ [t φi(k) , t φi(k+1) ) one has ẋ * i (t) = 0 and ẋri (t) = - j∈Ci L ri,j (x j (t) -x ri (t))
Thus, using Assumption 5, one obtains that between two reset instants the following holds:

ḋi (t) ≥ -n i ᾱ∆ i (t).
Moreover, since ∆(•) is non-increasing function one obtains that ḋi (t) ≥ -n i ᾱ∆ i (0).

Integrating the last equation we finally get that

d i (t) ≥ d(t φi(k) ) -n i ᾱ∆ i (0)(t -t φi(k) ).
Thus, in order to have

d i (t) ≤ d i (t φi(k) ) a i one needs d i (t φi(k) ) a i ≥ d(t φi(k) ) -n i ᾱ∆ i (0)(t -t φi(k) )
which is equivalent with

(t -t φi(k) ) ≥ a i -1 a i d(t φi(k) ) n i ᾱ∆ i (0) > a i -1 a i n i ᾱ∆ i (0)
This part of the proof finishes by choosing

δ = min i∈{1,...,m} a i -1 a i n i ᾱ∆ i (0) .
• Let us show now that Assumption 3 also holds. Between d i (t φi(k) ) and d i (t φi(k+1) ) the overall dynamics of the cluster C i is described by a fixed Laplacian matrix

ẋCi (t) = -L i x Ci (t).
Thus, there exists M i > 0 and ρ i > 0 such that

∆ i (t) ≤ M i e -ρi(t-t φ i (k-1) ) ∆ i (t φi(k) ) (5)
where ρ i is the convergence speed (see for instance [START_REF] Olshevsky | Convergence speed in distributed consensus and averaging[END_REF]) associated with the matrix L i .

Moreover, one has d i (t) ≤ ∆ i (t), ∀i ∈ {1, . . . , m} and ∀t ≥ 0. Combining this with (5) yields

d i (t) ≤ M i e -ρi(t-t φ i (k-1) ) ∆ i (t φi(k) ) (6)
Using ( 6), straightforward mathematical manipulation shows that

d i (t) > di(t φ i (k) ) ai implies t -t φi(k-1) < 1 ρ i ln a i M i ∆ i (t φi(k) ) d i (t φi(k) ) < 1 ρ i ln a i M i ∆ i (0 .
The proof ends by defining

δ max = max i∈{1,...,m} 1 ρ i ln a i M i ∆ i (0 .
B. Fully decentralized event-triggered resets Definition 5: The distance between the node r i and its fairest neighbor in cluster C i at time t is denoted by

di (t) = max j such that (ri,j)∈E L | x ri (t) -x j (t) | .
Considering > 0 a fixed scalar, the reset sequence (t k ) k∈N associated with the dynamics (1) is defined as follows: for all i ∈ {1, . . . , m} and for all k ≥ 0,

• if di (t φi(k-1) ) > we define t φi(k) = min t≥t φ i (k-1) di (t) ≤ di (t φi(k-1) ) a i , • otherwise, t φi(k) = t φi(k-1) + δ with δ = min i∈{1,...,m} a i -1 a i n i ᾱ∆ i (0) ,
where the a i > 1 are design parameters fixed a priori. (We recall that for consistency, we denote t φi(-1) = 0). Remark 3: Once again we can fix a i = a j , ∀i, j ∈ {1, . . . , m} or we can use a i to change the reset frequency of some/all clusters.

Proposition 6: Let us consider the dynamics (1) under Assumptions 1, 2 and 5. Then, the associated reset sequence introduced by Definition 5 satisfies the Assumptions 3, 4.

Proof: The proof is similar to the one of Proposition 4. Nevertheless, some technical details have to be pointed out. If di (t φi(k) ) ≤ , the second point in Definition 3 applies and Assumptions 3, 4 hold. Otherwise, the first point applies and for a fixed cluster C i , i ∈ {1, . . . , m} we have to show that the reset sequence satisfies Assumptions 3, 4.

• We start by proving that Assumption 4 holds. For any j ∈ C i such that (r i , j) ∈ E l we define di,j (t φi(k) ) = x ri (t φi(k) ) -x j (t φi(k) ) .

Let j ∈ C i be one neighbor of r i such that di (t φi(k) ) = di, j (t φi(k) ). We emphasize that for all t ∈ [t φi(k) , t φi(k+1) ) one has

ẋri (t) = - j∈Ci L ri,j (x j (t) -x ri (t)) ẋj (t) = - j∈Ci L j,j (x j (t) -x j (t))
yielding, as in the proof of Proposition 4, ḋi, j (t) ≥ -2n i ᾱ∆ i (0).

Integrating this equation we get di, j (t) ≥ di, j (t φi(k) ) -2n i ᾱ∆ i (0)(t -t φi(k) ).

But di (t) ≥ di, j (t), ∀t ≥ 0 and di (t φi(k) ) = di, j (t φi(k) ) which leads as to di (t) ≥ di (t φi(k) ) -2n i ᾱ∆ i (0)(t -t φi(k) ).

From this point we continue by mimicking the proof of Proposition 4. In order to have di (t) ≤ di (t φi(k) )

a i one needs di (t φi(k) ) a i ≥ d(t φi(k) ) -2n i ᾱ∆ i (0)(t -t φi(k) )
which is equivalent with

(t -t φi(k) ) ≥ a i -1 a i d(t φi(k) ) 2n i ᾱ∆ i (0) > a i -1 a i 2n i ᾱ∆ i (0) This part of the proof finishes by choosing δ = min i∈{1,...,m} a i -1 a i 2n i ᾱ∆ i (0) .
• To prove that Assumption 3 also holds, we simply notice that di (t) ≤ ∆ i (t), ∀i ∈ {1, . . . , m}. Thus the arguments in the proof of Proposition 4 can be applied exactly in the same manner to define

δ max = max i∈{1,...,m} 1 ρ i ln a i M i ∆ i (0
that upper-bounds all the intervals [t φi(k) , t φi(k+1) ).

V. ILLUSTRATIVE EXAMPLE

In the following we consider a toy example that numerically validates the results reported in the paper. In this example the network contains 5 agents and it is partitioned in two clusters of 2 and 3 agents respectively. The directed graph capturing the interconnections during the continuous dynamics is described by the following generalized Laplacian matrix

L =       4 -2 -2 0 0 -1 1 0 0 0 0 -2 2 0 0 0 0 0 3 -3 0 0 0 -1 1      
which has a block diagonal structure corresponding to the two clusters. Each cluster contains only one node able to interact with agents outside its own cluster (node 1 in the first cluster and node 4 in the second cluster). The reset dynamics of the node 1 and 4 are:

x 1 (t φ1(k) ) = 0.45x 1 (t - φ1(k) ) + 0.55x 5 (t - φ1(k) ) x 4 (t φ2(k) ) = 0.25x 3 (t - φ2(k) ) + 0.75x 4 (t - φ2(k) ).
Starting with the initial condition x = [8, 7, 9, 2, 3] and a 1 = a 2 = 2, using the first reset rule we get the overall behavior of the network depicted in Figure 1 . On this figure one can observe that reset instants are not synchronized and we may have several resets of the root of one cluster before the root of the second cluster jumps. In order decrease the reset frequency and make even more clear the asynchrony of reset instants, we have changed the parameters occurring in the reset rule as follows a 1 = 200, a 2 = 2. The behavior of the network is correspondingly modified as can be seen in Figure 2 .

Similar tests have been done for the same network with fully-decentralized reset instants and the results are presented in Figure 3.

It is worth noting that consensus value depends not only on the initial condition and interconnection topology but also on the reset sequence.

VI. CONCLUSIONS

In this paper we have analyzed the consensus in networks partitioned in several clusters. Each agent continuously interacts inside its cluster and some of them discretely reset their state by taking into account information from other clusters. Thus, we end up with heterogeneous networks of agents having linear dynamics and impulsive ones. We impose that the network satisfies some weak connectivity and bounded influence assumptions. In this framework the consensus is guaranteed as far as the reset sequence for each cluster is divergent and the period between two reset instants of the same cluster is lower-bounded by a strictly positive dwell-time. In order to define the sequences satisfying the aforementioned properties we use event-dependent and decentralized rules. A numerical example illustrates the results.

Fig. 1 .

 1 Fig. 1. Consensus of the five agents grouped in 2 clusters when the resets are defined by the semi-decentralized rule with a 1 = a 2 = 2.

Fig. 2 .

 2 Fig. 2. Consensus of the five agents grouped in 2 clusters when the resets are defined by the semi-decentralized rule with a 1 = 200, a 2 = 2.

Fig. 3 .

 3 Fig. 3. Consensus of the five agents grouped in 2 clusters when the resets are defined by the fully-decentralized rule with Up: a 1 = a 2 = 2. Down: a 1 = 200, a 2 = 2

This work was funded by the ANR project COMPACS -"Computation Aware Control Systems", ANR-13-BS03-004.


Nebras Gharbi
email: gharbi@cril.fr

Fred Hemery
email: hemery@cril.fr

Christophe Lecoutre
email: lecoutre@cril.fr

Olivier Roussel
email: roussel@cril.fr

Sliced Table Constraints: Combining Compression and Tabular Reduction

Many industrial applications require the use of table constraints (e.g., in configuration problems), sometimes of significant size. During the recent years, researchers have focused on reducing space and time complexities of this type of constraint. Static and dynamic reduction based approaches have been proposed giving new compact representations of table constraints and effective filtering algorithms. In this paper, we study the possibility of combining both static and dynamic reduction techniques by proposing a new compressed form of table constraints based on frequent pattern detection, and exploiting it in STR (Simple Tabular Reduction).

Introduction

Table constraints, i.e., constraints given in extension by listing the tuples of values allowed or forbidden for a set of variables, are widely studied in constraint programming (CP). This is because such constraints are present in many realworld applications from areas such as design and configuration, databases, and preferences modeling. Sometimes, table constraints provide the unique natural or practical way for a non-expert user to express her constraints. So far, research on table constraints has mainly focused on the development of fast algorithms to enforce generalized arc consistency (GAC), which is a property that corresponds to the maximum level of filtering when constraints are treated independently. GAC algorithms for table constraints have attracted considerable interest, dating back to GAC4 [START_REF] Mohr | Good old discrete relaxation[END_REF] and GAC-Schema [START_REF] Bessiere | Arc consistency for general constraint networks: preliminary results[END_REF]. Classical algorithms iterate over lists of tuples in different ways ; e.g., see [START_REF] Bessiere | Arc consistency for general constraint networks: preliminary results[END_REF][START_REF] Lhomme | A fast arc consistency algorithm for n-ary constraints[END_REF][START_REF] Lecoutre | Generalized arc consistency for positive table constraints[END_REF]. A recent AC5-based algorithm has been proposed in [START_REF] Mairy | An optimal filtering algorithm for table constraints[END_REF], and has been shown efficient on table constraints of small arity. For tables constraint of large arity, it is recognized that maintaining dynamically the list of supports in constraint tables does pay off: these are the variants of simple tabular reduction (STR) [START_REF] Ullmann | Partition search for non-binary constraint satisfaction[END_REF][START_REF] Lecoutre | STR2: Optimized simple tabular reduction for table constraints[END_REF][START_REF] Lecoutre | A path-optimal GAC algorithm for table constraints[END_REF].

Table constraints are important for modeling parts of many problems, but they admit practical boundaries because the memory space required to represent them may grow exponentially with their arity. To reduce space complexity, researchers have focused on various forms of compression. Tries [START_REF] Gent | Data structures for generalised arc consistency for extensional constraints[END_REF], Multi-valued Decision Diagrams (MDDs) [START_REF] Cheng | An MDD-based generalized arc consistency algorithm for positive and negative table constraints and some global constraints[END_REF] and Deterministic Finite Automata (DFA) [START_REF] Pesant | A regular language membership constraint for finite sequences of variables[END_REF] are general structures used to represent table constraints in a compact way, so as to facilitate the filtering process. Cartesian product is another classical mechanism to represent compactly large sets of tuples. For instance, it has been applied successfully for handling sets of solutions [START_REF] Hubbe | An efficient cross product representation of the constraint satisfaction problem search space[END_REF], symmetry breaking [START_REF] Focacci | Global cut framework for removing symmetries[END_REF][START_REF] Fahle | Symmetry breaking[END_REF], and learning [START_REF] Katsirelos | Generalized nogoods in CSPs[END_REF][START_REF] Lecoutre | Transposition Tables for Constraint Satisfaction[END_REF]. So far, this form of compression has been used in two distinct GAC algorithms for table constraints: by revisiting the general GAC-schema [START_REF] Katsirelos | A compression algorithm for large arity extensional constraints[END_REF] and by combining compressed tuples with STR [START_REF] Xia | Optimizing STR algorithms with tuple compression[END_REF]. The latter work shows how variants STR2 and STR3 can advantageously benefit from compressed tuples when the compression ratio is high.

Recently, we have proposed an original compression approach based on datamining algorithms [START_REF] Gharbi | Optimizing STR algorithms with tuple compression[END_REF], where all occurrences of the most frequent patterns in a table are replaced by their indices in a so-called patterns table. Using datamining techniques for compressing table constraints has also been studied in [START_REF] Jabbour | A mining-based compression approach for constraint satisfaction problems[END_REF], but in a very different manner since additional variables and values are needed, and constraints are reformulated. The same authors also studied compression of SAT clauses in [START_REF] Jabbour | Mining-based compression approach of propositional formulae[END_REF]. In [START_REF] Gharbi | Optimizing STR algorithms with tuple compression[END_REF], a pattern was defined as a sequence of consecutive values, which prevented us from benefiting of optimized STR variants. In this paper, we propose to relax this condition (of consecutive values), considering any sub-tuple as a possible frequent pattern, and identifying the most frequent ones by means of data-mining techniques. Consequently, every table can be "sliced", where each slice associates a pattern µ with a sub-table containing all extensions of µ that can be found in the original table. We propose an algorithm to deal with sliced table constraints: we build it on the basis of the optimized algorithm STR2.

The paper is organized as follows. After recalling some technical background in Section 1, we present, in Section 2, a compression process for table constraints, detailing the algorithm used to obtain the new form of sliced table constraints. Next, we describe, in Section 3, an optimized algorithm to enforce GAC on sliced table constraints. Finally, after giving some experimental results in Section 4, we conclude.

Technical Background

A (discrete) constraint network (CN) N is a finite set of n variables "interconnected" by a finite set of e constraints. Each variable x has a domain which is the finite set of values that can be assigned to x. The initial domain of a variable x is denoted by dom init (x) whereas the current domain of x is denoted by dom(x); we always have dom(x) ⊆ dom init (x). Each constraint c involves an ordered set of variables, called the scope of c and denoted by scp(c), and is semantically defined by a relation, denoted by rel(c), which contains the set of tuples allowed for the variables involved in c. A (positive) table constraint c is a constraint such that rel(c) is defined explicitly by listing the tuples that are allowed by c ; an example is given below. The arity of a constraint c is the size of scp(c), and will usually be denoted by r.

Example 1. Let c be a positive table constraint on variables x 1 , x 2 , x 3 , x 4 , x 5 with dom(x 1 ) = dom(x 2 ) = dom(x 3 ) = dom(x 4 ) = dom(x 5 ) = {a, b, c}. Table 1 represents the constraint c with 7 allowed tuples.

x1 x2 x3 x4 x5 τ1 (c, b, c, a, c) τ2 (a, a, b, c, a) τ3 (a, c, b, c, a) τ4 (b, a, c, b, c) τ5 (b, a, a, b, b) τ6 (c, c, b, c, a) τ7 (a, c, a, c, a) Table 1. Table constraint c on x1, x2, x3, x4, x5
Let X = {x 1 , . . . , x r } be an ordered set of variables. An instantiation I of X is a set {(x 1 , a 1 ), . . . , (x r , a r )} also denoted by {x 1 = a 1 , . . . , x r = a r } such that ∀i ∈ 1..r, a i ∈ dom init (x i ); X is denoted by vars(I) and each a i is denoted by

I[x i ]. An instantiation I is valid iff ∀(x, a) ∈ I, a ∈ dom(x).
An r-tuple τ on X is a sequence of values (a 1 , . . . , a r ) such that ∀i ∈ 1..r, a i ∈ dom init (x i ) ; the individual value a i will be denoted by τ [x i ]. For simplicity, we shall use both concepts of instantiation and tuple interchangeably. For example, an r-tuple τ on scp(c) is valid iff the underlying instantiation is valid. An r-tuple τ on scp(c) is a support on the r-ary constraint c iff τ is a valid tuple which is allowed by c. If τ is a support on a constraint c involving a variable x and such that τ [x] = a, we say that τ is a support for (x, a) on c. Generalized Arc Consistency (GAC) is a well-known domain-filtering consistency defined as follows: Definition 1. A constraint c is generalized arc consistent (GAC) iff ∀x ∈ scp(c), ∀a ∈ dom(x), there exists at least one support for (x, a) on c. A CN N is GAC iff every constraint of N is GAC.

Enforcing GAC is the task of removing from domains all values that have no support on a constraint. Many algorithms have been devised for establishing GAC according to the nature of the constraints. For table constraints, STR [START_REF] Ullmann | Partition search for non-binary constraint satisfaction[END_REF] is such an algorithm: it removes invalid tuples during search of supports using a sparse set data structure which separates valid tuples from invalid ones. This method of seeking supports improves search time by avoiding redundant tests on invalid tuples that have already been detected as invalid during previous GAC enforcements. STR2 [START_REF] Lecoutre | STR2: Optimized simple tabular reduction for table constraints[END_REF], an optimization of STR, limits some basic operations concerning the validity of tuples and the identification of supports, through the introduction of two important sets called S sup and S val (described later). In the extreme best case, STR2 can be r times faster than STR.

We now introduce the concepts of pattern and sub-table that will be useful for compression. Definition 2. A pattern µ of a constraint c is an instantiation I of some variables of c. We note scp(µ) its scope, which is equal to vars(I), |µ| its length, which is equal to |scp(µ)|, and nbOcc(µ) its number of occurrences in rel(c),

which is |{τ ∈ rel(c) | µ ⊆ τ }|.
Example 2. In Table 1, µ 1 ={x 1 = a, x 4 = c, x 5 = a} and µ 2 ={x 3 = c, x 5 = c} are patterns of respective lengths 3 and 2, with scp(µ 1 )={x 1 , x 4 , x 5 } and scp(µ 2 )={x 3 , x 5 }. Definition 3. The sub-table T associated with a pattern µ of a constraint c is obtained by removing µ from tuples of c that contain µ and ignoring other tuples.

T = {τ \ µ | τ ∈ rel(c) ∧ µ ⊆ τ } The scope of T is scp(T ) = scp(c) -scp(µ) Example 3.
=(x 1 = a, x 4 = c, x 5 = a) of c, described in Table 1. x2 x3 a b c b c a Table 2.
The sub-table T1 associated with the pattern µ1 of c Definition 4. An entry for a constraint c is a pair (µ, T ) such that µ is a pattern of c and T is the sub-table associated with µ.

Since the set of tuples represented by an entry (µ, T ) represents in fact the Cartesian product of µ by T , we shall also use the notation µ ⊗ T to denote a constraint entry. Notice that after the slicing process of a constraint into a set of entries, the set of tuples which are not associated with any pattern can be stored in a so called default entry denoted by (∅, T ).

Example 4. The pattern µ=(x 1 = a, x 4 = c, x 5 = a) of the constraint c, depicted in Figure 1(a), appears in tuples τ 2 , τ 3 and τ 7 . Thus, µ and the resulting sub-table form an entry for c, as shown in Figure 1(b).

Testing the validity of classical or compressed tuples is an important operation in filtering algorithms of (compressed) table constraints. For sliced table constraints, we extend the notion of validity to constraint entries. Definition 5. An entry (µ, T ) is valid iff at least one tuple of the Cartesian product µ ⊗ T is valid. Equivalently, an entry is valid iff its pattern is valid and its sub-table contains at least one valid sub-tuple.

Compression Method

Several data mining algorithms, such as Apriori [START_REF] Agrawal | Fast algorithms for mining association rules in large databases[END_REF] and FP-Growth [START_REF] Han | Mining frequent patterns without candidate generation[END_REF] among others, can be used to identify frequent patterns. Since our objective is compression, we do not have to identify each possible frequent pattern but only the ones that are useful for compression, and specifically at most one pattern per tuple. The construction of an FP-Tree (Frequent-Pattern Tree) which is the first step in the FP-Growth algorithm is especially well suited to this goal since it identifies each long and frequent pattern. This construction requires only three scans of the table.

We briefly explain the construction of the FP-Tree in the context of table compression, using the constraint given in Table 1 as an example. Details of the general method can be found in [START_REF] Han | Mining frequent patterns without candidate generation[END_REF][START_REF] Han | Mining frequent patterns without candidate generation: A frequent-pattern tree approach[END_REF]. The algorithm takes one parameter minSupport (minimum support) which is the minimal number of occurrences of a pattern that we require to consider it as frequent. In our example, we shall use minSupport=2 to identify patterns which occur at least twice.

In a first step, we collect the number of occurrences of each value. By abuse of terminology, we shall call frequency the number of occurrences of a value. This step requires one scan of the table. The result on our example is given in Figure 2(a). Then, in a second scan, we sort each tuple in decreasing order of frequency of values. The result is given in Figure 2(b) where the frequency of a value is given in parentheses. Values which have a frequency below the threshold minSupport are removed from the tuple (they are identified in bold face) because they cannot appear in a frequent pattern. Once a tuple is sorted and possibly reduced, it is inserted in the FP-Tree which is essentially a trie where each branch represents the frequent part of a tuple and each node contains the number of branches which share that node. Each edge from a parent to its child is labeled with a value. The root node does not have any label.

Figure 3(a) represents the FP-tree obtained on our running example. The first tuple inserted in the tree is the beginning of τ 1 , that is (x 1 = c, x 3 = c, x 5 = c). This creates the leftmost branch of the tree. Each node of this branch is given a frequency of 1. The second tuple inserted is (x 4 = c, x 5 = a, x 1 = a, x 2 = a, x 3 = b) which creates the third leftmost branch in the tree (each node having a frequency of 1 at this step). When τ 3 is inserted, the new branch (x 4 = c, x 5 = a, x 1 = a, x 2 = c, x 3 = b) shares its first three edges with the last branch, hence the frequency of the corresponding nodes is incremented and becomes 2. The other tuples are inserted in the same way. In the end, nodes with a frequency below the threshold minSupport are pruned. The remaining tree is depicted with thick lines and circled by a dashed line in Figure 3(a).

x1 x2 x3 x4 x5 a 3 3 2 1 4 b 2 1 3 2 1 c 2 3 2 4 2 (a) frequencies τ1 (2) x1 = c (2) x3 = c (2) x5 = c (1) x2 = b (1) x4 = a τ2 (4) x4 = c (4) x5 = a (3) x1 = a (3) x2 = a (3) x3 = b τ3 (4) x4 = c (4) x5 = a (3) x1 = a (3) x2 = c (3) x3 = b τ4 (3) x2 = a (2) x1 = b (2) x3 = c (2) x4 = b (2) x5 = c τ5 (3) x2 = a (2) x1 = b (2) x3 = a (2) x4 = b (1) x5 = b τ6 (4) x4 = c (4) x5 = a (3) x2 = c (3) x3 = b (2) x1 = c τ7 (4) x4 = c (4) x5 = a (3) x1 = a (3) x2 = c (2) x3 = a
We now have to identify patterns in the FP-tree which are relevant for compression. Each node of the tree corresponds to a frequent pattern µ which can be read on the path from the root to the node. The frequency f of this pattern is given by the node itself. The savings that can be obtained by factoring this frequent pattern is |µ| × (f -1) values (we can save each occurrence of the pattern but one). In our example, we can see that the pattern (x 4 = c, x 5 = a) can save 6 values, the pattern (x 4 = c, x 5 = a, x 1 = a) can also save 6 values but the pattern (x 4 = c, x 5 = a, x 1 = a, x 2 = c) can save only 4 values. Therefore, we further prune the tree by removing nodes that save less values than their parent. The leaves of the tree we obtain represent the frequent pattern used in the compression: (x 4 = c, x 5 = a, x 1 = a) and (x 2 = a, x 1 = b).

To complete the compression, we create an entry for each frequent pattern we have identified and fill them in a last scan of the table. For each tuple, we use the FP-tree to identify if the (sorted) tuple starts with a frequent pattern, in which case we add the rest of the tuple to the corresponding sub-table. Tuples which do not start with a frequent pattern are added to the default entry.

Algorithm 1 summarizes the different steps of the compression process.

Algorithm 1: compress(T: table, minSupport: integer)

1 compute the frequency of each value of T

2 for i ∈ 1..|T | do 3 τ ← T [i]

Filtering Sliced Table Constraints

In order to enforce GAC on sliced table constraints, our idea is to adapt Simple Tabular Reduction (STR), and more specifically the optimized variant STR2, on the compressed form of this kind of constraint. As a sliced table constraint is composed of several entries, each one composed of both a pattern and a subtable, the filtering process we propose acts at two distinct levels. At a high level, the validity of each entry is checked, and at a low-level, the validity of each pattern and each sub-tuple is checked. Remember that an entry is valid iff both its pattern is valid and at least one tuple from its sub-table is valid (See Definition 5). In this section, we first describe the employed data structures, then we introduce our GAC algorithm, and finally we give an illustration.

Data structures

A sliced table constraint c is represented by an array entries[c] of p entries. Managing the set of valid entries, called current1 entries, is performed as follows:

- Each entry in entries can be represented as a record composed of a field pattern and a field subtable. More precisely:

the field pattern stores a partial instantiation µ, and can be represented in practice as a record of two arrays: one for the variables, the scope of the pattern, and the other for the values. the field subtable stores a sub-table T , and can be represented in practice as a record of two arrays: one for the variables, i.e., the scope of the sub-table T , and the other, a two-dimensional array, for the sub-tuples.

In our presentation, we shall directly handle µ and T without considering all implementation details ; for example, T will be viewed as a two-dimensional array. Managing the set of valid sub-tuples, called current sub-tuples, of T , is performed as follows:

limit[T ] is the index of the last current sub-tuple in T . The elements in T at indices ranging from 1 to limit[T ] are the current sub-tuples of T . removing a sub-tuple (that has become invalid) at index i is performed by a call of the form removeSubtuple(T, i). Such a call swaps the sub-tuples at indices i and limit[T ], and then decrements limit[T ]. Note that the initial order of sub-tuples is not preserved. restoring a set of sub-tuples can be performed by simply changing the value of limit[T ].

Note that the management of both current entries and current sub-tuples is in the spirit of STR. Also, as in [START_REF] Lecoutre | STR2: Optimized simple tabular reduction for table constraints[END_REF], we introduce two sets of variables, called S val and S sup . The set S val contains uninstantiated variables (and possibly, the last assigned variable) whose domains have been reduced since the previous invocation of the filtering algorithm on c. To set up S val , we need to record the domain size of each modified variable x right after the execution of STR-slice on c: this value is recorded in lastSize[x]. The set S sup contains uninstantiated variables (from the scope of the constraint c) whose domains contain each at least one value for which a support must be found. These two sets allow us to restrict loops on variables to relevant ones. We also use an array gacValues[x] for each variable x. At any time, gacValues[x] contains all values in dom(x) for which a support has already been found: hence, values for a variable x without any proved support are exactly those in dom(x) \ gacValues[x]. Note that the sets S val and S sup are initially defined with respect to the full scope of c. However, for each sub-table we also shall use local sets S lval and S lsup of S val and S sup as explained later.

Algorithm

Algorithm 2 is a filtering procedure, called STR-slice, that establishes GAC on a specified sliced table constraint c belonging to a CN N . Lines 1-10, which are exactly the same as those in Algorithm 5 of [START_REF] Lecoutre | STR2: Optimized simple tabular reduction for table constraints[END_REF], allow us to initialize the sets S val , S sup and gacValues. Recall that S val must contain the last assigned variable, denoted by lastPast(P ), if it belongs to the scope of c. Lines 11-22 iterate over all current entries of c. To test the validity of an entry, we check first the validity of the pattern µ (Algorithm 3), and then, only when the pattern is valid, we check the validity of the sub-table T by scanning it (Algorithm 4). If an entry is no more valid, it is removed at line 22. Otherwise, considering the values that are present in the pattern, we have to update gacValues as well as S sup when a first support for a variable is found. Lines 23-30, which are exactly the same as those in Algorithm 5 of [START_REF] Lecoutre | STR2: Optimized simple tabular reduction for table constraints[END_REF], manage the reduction of domains: unsupported values are removed at line 25 and if the domain of a variable x becomes empty, an exception is thrown at line 27. Also, the set of variables X evt reduced by STR-slice is computed and returned so that these "events" can be propagated to other constraints.

Algorithm 4 is an important function, called scanSubtable, of STR-slice. Its role is to iterate over all current (sub)tuples of a given sub-table, in order to collect supported values and to remove invalid tuples. Note that when this function is called, we have the guarantee that the pattern associated with the sub-table is valid (note the "and then" short-circuit operator at line 14 of Algorithm 2). The first part of the function, lines 1-10, allow us to build the local sets S lval and S lsup from S val and S sup . Such sets are obtained by intersecting S val with scp(T ) and S sup with scp(T ), respectively. Once the sets S lval and S lsup are initialized, we benefit from optimized operations concerning validity checking and support seeking, as in STR2. The second part of the function, lines 9-21, consists in iterating over all current sub-tuples of T . This is a classical STR2-like traversal of a set of tuples. Finally, line 22 returns true when there still exists at least one valid sub-tuple.

It is interesting to note the lazy synchronization performed between the global unique set S sup and the specific local sets S lsup (one such set per sub-table). When a variable x is identified as "fully supported", it is immediately removed from S sup (see line 19 of Algorithm 2 and line 18 of Algorithm 4). Consequently, that means that the next sub-tables (entries) will benefit from such a reduction, but the information is only transmitted at initialization (lines 6-8 of Algorithm 4). On the other hand, once initialized, the global set S val is never modified during the execution of STR-slice.

Backtracking issues: In our implementation, entries and tuples can be restored by modifying the value of the limit pointers (entriesLimit[c] and limit[T ] Algorithm 2: STR-slice(c: constraint) Input : c is a sliced table constraint of the CN N to be solved Output : the set of variables in scp(c) with reduced domain // Initialization of sets S val and S sup , as in STR2

1 S val ← ∅ 2 S sup ← ∅ 3 if lastPast(P ) ∈ scp(c) then 4 S val ← S val ∪ {lastPast(P )} 5 foreach variable x ∈ scp(c) | x / ∈ past(P ) do 6 gacValues[x] ← ∅ 7 S sup ← S sup ∪ {x} 8 if |dom(x)| = lastSize[c][x] then 9 S val ← S val ∪ {x} 10 lastSize[c][x] ← |dom(x)| // Iteration over all entries of c 11 i ← 1 12 while i ≤ entriesLimit[c] do 13 (µ, T ) ← entries[c][i]
// ith current entry of c 14 if isValidPattern(µ) and then scanSubtable(T ) then Algorithm 5: isValidSubtuple(S lval : variables, τ : tuple): Boolean

15 foreach variable x ∈ scp(µ) | x ∈ S sup do 16 if µ[x] ∈ gacValues[x] then 17 gacValues[x] ← gacValues[x] ∪ {µ[x]} 18 if |dom(x)| = |gacValues[x]| then 19 S sup ← S sup \ {x} 20 i ← i + 1
1 foreach variable x ∈ scp(µ) do 2 if µ[x] / ∈ dom(
S lval ← ∅ 2 foreach variable x ∈ S val do 3 if x ∈ scp(T ) then 4 S lval ← S lval ∪ {x} 5 S lsup ← ∅ 6 foreach variable x ∈ S sup do 7 if x ∈ scp(T ) then 8 S lsup ← S lsup ∪ {x} // Iteration over all (sub)tuples of T 9 i ← 1 10 while i ≤ limit[T ] do 11 τ ← T [i] // ith current sub-tuple of T 12 if isValidSubtuple(S lval , τ ) then 13 foreach variable x ∈ S lsup do 14 if τ [x] ∈ gacValues[x] then 15 gacValues[x] ← gacValues[x] ∪ {τ [x]} 16 if |dom(x)| = |gacValues[x]| then 17 S lsup ← S lsup \ {x} 18 S sup ← S sup \ {x} 19 i ← i + 1
1 foreach variable x ∈ S lval do 2 if τ [x] / ∈ dom(x) then 3 return false 4 return true
for each sub-table T of c), recorded at each search depth. Restoration is then achieved in O(1 + p) (for each constraint) where p is the number of entries. However, by introducing a simple data structure, it is possible to only call the restoration procedure when necessary, limiting restoration complexity to O(1) in certain cases: it suffices to register the limit pointers that need to be updated when backtracking, and this for each level. When the search algorithm back-tracks, we also have to deal with the array lastSize. As mentioned in [START_REF] Lecoutre | STR2: Optimized simple tabular reduction for table constraints[END_REF], we can record the content of such an array at each depth of search, so that the original state of the array can be restored upon backtracking.

As GAC-slice is a direct extension of STR2, it enforces GAC.

Illustration

x 1 x 4 x 5 a c a Figures 4 and 5 illustrate the different steps for filtering a sliced table constraint, when STR-slice is called after an event. In Figure 4, considering that the new event is simply x 3 = a (i.e., the removal of the value a from dom(x 3 )), STRslice starts checking the validity of the current entries (from 1 to entriesLimit). So, for the first entry, the validity of the pattern µ={x 1 = a, x 4 = c, x 5 = a} is first checked. Since µ remains valid (our hypothesis is that the event was only x 3 = a), the sub-table of the first entry is scanned. Here, only the sub-tuple {x 2 = c, x 3 = a} is found invalid, which modifies the value of limit for the sub-table of this first entry. After the call to STR-slice, the constraint is as in Figure 4(b).

In Figure 5, considering now that the new event is x 3 = b, we start again with the first current entry. Figuring out that the pattern is still valid, we check the validity of the associated sub-tuples. Since the sub-tuple {x 2 = a, x 3 = b} is no more valid, it is swapped with {x 2 = c, x 3 = b}. This latter sub-tuple is then also found invalid, which sets the value of limit to 0. This is illustrated in Figure 5(a). As the sub-table of the first entry is empty, the entry is removed by swapping its position with that of last current entry. After the call to STR-slice, the constraint is as in Figure 5(b) (note that a second swap of constraint entries has been performed).

x 1 x 4 x 5 a c a

Experimental results

In order to show the practical interest of our approach to represent and filter sliced table constraints, we have conducted an experimentation (with our solver AbsCon) using a cluster of bi-quad cores Xeon processors at 2.66 GHz node with 16GiB of RAM under Linux. Because STR2 and STR3 belong to the state-of-theart GAC algorithms for table constraints, we compare the respective behaviors of STR2, STR3 and STR-slice on different series of instances2 involving positive table constraints with arity greater than 2. STR1 is also included as a baseline.

For STR-slice, we select exclusively frequent patterns with a number of occurrences at least equal to 10% of the number of tuples in the table. This value was obtained after several experiments, similarly we chose 10 for the minimum size of sub-tables. Automatically tuning, on a specific instance, the frequency threshold for patterns and the minimum sub-table size is part of our future work.

We use MAC with the dom/ddeg variable ordering and lexico as value ordering heuristic, to solve all these instances. A time-out of 1, 200 seconds was set per instance. The two chosen heuristics guarantee that we explore the very same search tree regardless of the filtering algorithm used. Table 3 shows mean results (CPU time in seconds) per series. For each series, the number of tested instances is given by #ins ; it corresponds to the number instances solved by all three variants within 1, 200 seconds. Note that the mean compression ratios and CPU times (in seconds) are also given for STRslice between parentheses. We define the compression ratio as the size of the sliced tables over the size of the initial tables, where the size of a (sliced) table is the number of values over all patterns and (sub-)tables. The results in Table 3 show that STR-slice is competitive with both STR2 and STR3. Surprisingly, although the compression ratio obtained for the instances of the series renault is rather encouraging, the CPU time obtained for STR-slice is disappointing. We suspect that the presence of many constraints with small tables in the renault instances is penalizing for STR-slice because, in that case, the overhead of managing constraint entries is not counterbalanced by the small absolute spatial reduction. Table 4 presents the results obtained on some instances.

In term of space, STR3 is the variant that uses the most amount of memory (sometimes by a very large factor). STR-slice, although requiring a few additional data structures is the cheapest STR variant in term of memory (approximately as indicated by the compression ratio in Tables 3 and4). Note that other compression approaches of the literature such as those based on MDDs [START_REF] Cheng | An MDD-based generalized arc consistency algorithm for positive and negative table constraints and some global constraints[END_REF] may outperform STR variants when the compression ratio is (very) high. This is the case, for example, on the instances of series a7-v24-d5-ps05. However, on other series such as crossword, the MDD approach can be outperformed by a large factor by the STR variants (on hard crossword instances, STR2, STR3 and STR-slice are usually about 5 times faster than MDD).

A general observation from this rather preliminary experimentation is that STR-slice is a competitor to STR2 and STR3, but a not a competitor that takes a real advantage. Several perspectives to improve this situation are developed in the conclusion.

Conclusion

In this paper, we have presented an original approach for filtering table constraints: it combines a new compression technique using the concept of sliced table constraints and an optimized adaptation of the tabular reduction (as in STR2). Our preliminary experimentation shows that STR-slice is a competitor to the state-of-the-art STR2 and STR3 algorithms. To make STR-slice indispensable, many further developments are necessary. First, we think that the tuning of the parameters used for guiding compression should be automatized (possibly, employing some machine learning techniques). STR-slice could then benefit from a better compression. Second, we believe that, in the rising context of big data, new constraint problems should emerge rapidly where constraints could be of (very) large arity and involve very large tables. STR-slice could advantageously handle such "huge" constraints, especially if we consider that slicing could be conducted recursively on the sub-tables (another perspective of this work). Finally, we think that the concept of sliced table constraints is interesting on its own for modeling, as certain forms of conditionality can be represented in a simple and natural way, directly with sliced table constraints.

Fig. 1 .

 1 Fig. 1. Example of a constraint entry

Fig. 2 .

 2 Fig. 2. First two steps of the compression

Fig. 3 .

 3 Fig. 3. FP-tree and compressed table

4 9 τ

 9 sort τ by decreasing order of value frequency and remove values less frequent than minSupport 5 add τ to the FP-Tree (will update the nodes frequency)6 tmp[i] ← τ7 prune the tree by removing nodes which are less frequent than minSupport or such that |µ| × (f -1) is smaller than for their parent8 for i ∈ 1..|T | do ← tmp[i]10 lookup in the tree if τ starts with a frequent pattern µ. If it does not, µ ← ∅ 11 add T [i] \ µ to the sub-table corresponding to µ

  entriesLimit[c] is the index of the last current entry in entries[c]. The elements in entries[c] at indices ranging from 1 to entriesLimit[c] are the current entries of c. removing an entry (that has become invalid) at index i is performed by a call of the form removeEntry(c, i). Such a call swaps the entries at indices i and entriesLimit[c], and then decrements entriesLimit[c]. Note that the initial order of entries is not preserved. restoring a set of entries can be performed by simply changing the value of entriesLimit[c].

21 else 22 removeEntry

 2122 (c, i) // entriesLimit[c] decremented // domains are now updated and Xevt computed, as in STR2 23 Xevt ← ∅ 24 foreach variable x ∈ S sup do 25 dom(x) ← gacV alues[x] 26 if dom(x) = ∅ then 27 throw INCONSISTENCY 28 Xevt ← Xevt ∪ {x} 29 lastSize[c][x] ← |dom(x)| 30 return Xevt Algorithm 3: isValidPattern(µ: pattern): Boolean

20 else 21 removeSubtuple

 2021 (T, i)) // limit[T ] decremented22 return limit[T ] > 0

x 2 x 3 a b c b c a x 1 x 2 b a x 3 x 4 x 5 c b c a b b x 1 x 2 x 3 x 4 x 5 cx 3 x 4 x 5 c b c a b b x 1 x 2 x 3 x 4 x 5 cFig. 4 .

 554 Fig. 4. STR-slice called on a slice table constraint after the event x3 = a

Fig. 5 .

 5 Fig. 5. From 4(b), STR-slice called after the event x3 = b

  Table 2 represents the sub-table associated with the pattern µ 1

  : T is a sub-table coming from an entry of the constraint c Output : true iff there is at least one valid tuple in the sub-table T // Initialization of local sets S lval and S lsup from S val and S sup 1

x) then 3 return false Algorithm 4: scanSubtable(T : sub-table): Boolean Input

Table 3 .

 3 Mean CPU time (in seconds) to solve instances from different series (a timeout of 1,200 seconds was set per instance) with MAC. Mean compression ratio and CPU time are given for STR-slice between parentheses.

	Instance	#ins	STR1 STR2 STR3	STR-slice
	a7-v24-d5-ps05	11	298.05 147.73 189.14 115.30 (66% -5.74)
	bdd	70	44.53 13.44 99.21	20.35 (86% -0.59)
	crossword-ogd	43	90.05 39.35 25.69 29.59 (75.51% -0.36)
	crossword-uk	43	95.20 45.88 44.33 47.21 (88.69% -0.18)
	renault	46	19.66 14.39 13.37 17.20 (47.15% -0.67)
	Instance	STR1 STR2 STR3	MDD	STR-slice
	a7-v24-d5-ps0.5-psh0.7-9	879	334	367	25.5	200 (69% -5.41)
	a7-v24-d5-ps0.5-psh0.9-6	353	195	324	16.6	174 (62% -5.82)
	bdd-21-2713-15-79-11	78.5 23.5	48.5	82.6 31.7 (88.05% -0.28)
	crossword-ogd-vg12-13	799	342	208 > 1, 200 242 (73.46% -0.74)
	crossword-uk-vg10-13	1,173	576	589 > 1, 200 598 (89.63% -0.48)

Table 4 .

 4 CPU time (in seconds) on some selected instances solved by MAC.

Current entries correspond to valid entries at the end of the previous evocation of the algorithm.

Available at http://www.cril.univ-artois.fr/CSC09.

Acknowledgments

This work has been supported by both CNRS and OSEO within the ISI project 'Pajero'.


Hajer Herbegue

Mamoun Filali

Hugues Cassé

Formal Architecture Specification for Time Analysis

Keywords: Hardware, microarchitecture, pipeline, WCET, architecture language, formalization, constraints

WCET calculus is nowadays a must for safety critical systems. As a matter of fact, basic real-time properties rely on accurate timings. Although over the last years, substantial progress has been made in order to get a more precise WCET, we believe that the design of the underlying frameworks deserve more attention. In this paper, we are concerned mainly with two aspects which deal with the modularity of these frameworks. First, we enhance the existing language Sim-nML for describing processors at the instruction level in order to capture modern architecture aspects. Second, we propose a light DSL in order to describe, in a formal prose, architectural aspects related to both the structural aspects as well as to the behavioral aspects.

Introduction

System-on-chip and processor modeling methodologies are continuously improved to overcome the increasing complexities of critical embedded systems. Designers have to deal with complex features of new architectures and develop application/domain specific processors. It is highly desirable, as intending to reduce the costs and time-to-market, that the software design tool can be synthesized automatically from high level processor specifications. In this scope, there is a surge in architecture description languages. ADLs have been used in retargetable tools generation, design space exploration, hardware synthesis, verification and time analysis [START_REF] Li | Modeling out-of-order processors for WCET analysis[END_REF][START_REF] Mishra | Modeling and validation of pipeline specifications[END_REF]. In order to have reliable and powerful design and analysis flows, ADLs have to convey the informal processor specification provided by vendors to the development tools, as closely as possible. Furthermore, the validation (and verification) is an important task in the system-on-ship design process, that ensures the correction of the system with respect to the correctness requirements and real-time constraints. Such a task is arduous because of the architecture complexity and lack of clear and explicit syntax and semantics in currently used architecture languages. Indeed, to ensure the completeness of the architecture requirements at the design stage, it is essential to have a precise and formal processor specification. ADL-driven flows for worst case execution time (WCET) analysis, like the OTAWA framework [START_REF] Ballabriga | OTAWA: An Open Toolbox for Adaptive WCET Analysis[END_REF], need a clear and explicit syntax and semantics for the architecture description to provide the required accuracy.

At the present time, OTAWA allows the time analysis using a constraint-based approach, in addition to the validation and the animation of time results [START_REF] Herbegue | A constraint-based wcet computation framework[END_REF] and the generation of fine-grained simulators at pipeline level. In this paper, we enhance the OTAWA work flow with a logic-based description that formalize the architecture properties. This description is used, with the architecture model described in the Sim-nML language, to generate a constraint-based description for the WCET computation. We first present how advanced architecture features, specially instruction with complex behaviors, can be handled by the OTAWA ADL description. Second, we give, in a formal prose, the operational properties of the hardware components and the instruction set. These properties describe the instructions behavior regarding to resources allocation, dependencies, parallel execution, etc. This description also provides a good basis for formal verification of time analysis methods.

The paper is organized as follows. Section 2 gives an overview of the ADLbased approach and our contribution. In Section 3, we present the Sim-nML language and its extension to describe advanced features of real-life architectures. In Section 4, we present the logic-based description, illustrated through a processor use case. In Section 5, we present an overview of related works and draw a comparison between their respective description languages. Section 6 concludes the paper.

ADL-Based Approach for Time Computation

OTAWA [START_REF] Ballabriga | OTAWA: An Open Toolbox for Adaptive WCET Analysis[END_REF] is a framework dedicated to WCET computation of a program executed on a given processor. The time analysis is based on an abstraction of the target architecture and the binary. The WCET of a program corresponds to the execution time of the longest execution path, which is identified on the control flow graph (CFG) of the program. An execution path is a sequence of code snippets, called basic blocks. The WCET is a function of the time cost of the basic blocks and their execution counts [START_REF] Wilhelm | The Worst-Case Execution-Time problem-overview of methods and survey of tools[END_REF]. In this paper, we focus on the computation of the basic block execution time. The pipeline analysis consists of modeling the instruction behavior of the pipeline and evaluating the impact of the hardware features on the instruction execution times [START_REF] Rochange | A context-parameterized model for static analysis of execution times[END_REF]. The framework OTAWA was enhanced with an ADL-based approach [START_REF] Herbegue | Hardware architecture specification and constraint based wcet computation[END_REF] that aims at computing the time cost of a basic block considering the pipeline features. The carried analysis considers as input (1) the program binary, (2) the basic block as an instruction sequence and (3) the architecture description in the Sim-nML language [START_REF] Fauth | Describing instruction set processors using nML[END_REF] (see figure 1). Sim-nML was extended to support, in addition to the ISA description, the micro-architecture description of the target processor. The architecture description includes the resources accessed by the instructions such as pipeline stages, buffers, etc. and the execution model of instructions. The execution model describes the instruction behavior in terms of resource allocation. From the Sim-nML language and the binary, we generate an internal representation of the architecture and of the basic block. Then, a constraintbased description is automatically generated from the execution models of the instructions and the pipeline description. These constraints are combined to formulate a constraint satisfaction problem (CSP) [START_REF] Beldiceanu | Global constraint catalogue: Past, present and future[END_REF], whose resolution provides the time cost of the basic block.

In this paper, we intend to provide a formal description of the architecture constraints, in which we can express the architecture elements and properties, regardless of the resolution method and the language used later for time computation. We propose a domain specific language that allows a logic description of the architecture properties. The idea is to provide a library in which the architect-user can find a set of reusable quantitative properties that assist him in (1) the definition of architecture high-level constraints that would be used for time analysis and (2) the validation of the correctness and the consistency of the architecture model with respect to the initial specification. Indeed, according to the initial Sim-nML description and what is provided in the properties library, the user defines a set of properties that will be used further to compute WCETs.

The Sim-nML Description Language Extension

Sim-nML [START_REF] Fauth | Describing instruction set processors using nML[END_REF] is a hierarchical and a highly structured language that describes the processor at instruction level, using an attributed grammar. The instructions and the addressing modes are described using pre-defined attributes. The syntax attribute defines the assembly representation of the instruction. The attribute image gives the binary representation and action defines the semantics of the instruction (register transfer). Our extension to the Sim-nML language [START_REF] Herbegue | Hardware architecture specification and constraint based wcet computation[END_REF] allows the definition of the processor resources and the execution model of the instruction set, giving how and when the resources are accessed by each instruction. The properties of the hardware components are specified as attributes. So, we can declare stages, buffers, registers and memories. Concerning stages, we can specify out-of-order execution, superscalarity, cache characteristics, if relevant for time analysis, etc. The instructions definition is extended with an attribute uses that describes the execution model. In fact, to start execution on a stage, an instruction has to wait for its resources to be available, including the operands, the executing stage, the memory, etc. Therefore, the execution time of an instruction is impacted by the resources state. The uses attribute defines, in a timed sequence called clause, the resources required by an instruction in each step of its execution. A sequence is defined using commas. Every clause in a sequence represents a step of the instruction execution. In every step, one or more resources are required, and access can be in read or write mode. Parallel access is expressed by the operator &. Access to some resources takes a fixed duration t, that is specified as #{t}. An example of a 2-scalar out-of-order processor is illustrated in figure 2 and described in Sim-nML in lines 1-12 of listing 1.1. The language extension was amenable to describe some complications of instruction set architectures. In next paragraphs, we show how we extend the Sim-nML in order to handle pipelines with complex and long-running instructions.

Not-fully symmetric ALU. Specialized functional units are designed for specific operation patterns to achieve shorter delays. In the processor of figure 2, we assume that the first ALU occurrence implements a multiplier component executing multiply operations and ordinary data processing operations. Usually, processors include only one specialized ALU because it is expensive and there are more additions than multiply operations. Thus, arithmetic instructions are executed by any of the ALU . So no occurrence is specified in the ADD execution model (lines 18-19 of listing 1.1). While, in the execution model of M U L, we specify ALU [0] as the required stage occurrence (lines 23-24 of listing 1.1). This will be used when scheduling instructions to be issued to the ALU units. Different latencies has been associated to the execution of the ADD and M U L instructions on the ALU unit. Multi-cycle instructions. Some complicated arithmetic operations, such as multiply, divide and floating point operations, can require complex hardware with significantly longer delays than a single ALU . One solution is to have parallel pipelines for different multi-stage instructions. For example, division is frequently implemented using this scheme even in high performance superscalar processors. In addition, such an instruction stays many cycles on the same stage, mostly the first. In the pipeline of figure 3, we have a pipelined multiply/divide functional unit M D. The ALU unit executes simple operations. Instructions are issued in the M D floating point pipeline out-of-order. The listing 1.2 presents the execution model of the divide and multiply instructions. The DIV and M U L instructions have different latencies on the first stage of the pipelined M D unit. In fact, stages with different latencies is also a relevant pipeline property for hazards detection and the instructions scheduling, which is critical in an outof-order issue processor. These latencies will be considered when generating the timing constraints to compute the execution time of instructions. Micro-coded Instructions. Multiple register transfer instructions provide an efficient way of moving the contents of several registers to and from memory. These instructions take one cycle to issue but then use multiple memory cycles to load/store all the registers. We consider the pipeline of the figure 2. The load multiple instruction is given in lines 27-30 of listing 1.1. The list of registers to load is given by the operand rl coded on 16 bits. Every bit refers to a register and is set to one if the register is to load. So, if the register is loaded, then we have a clause in which the M EM unit, the memory and the register with the appropriate access mode are required. Otherwise, we have an empty clause. In order to have a wellformed final clause, with a valid pipeline path, we defined a semantic rule that states that: in a clause sequence, if a clause is empty, then it is removed from the sequence: cl , ∅ , cl ′ ⇒ cl , cl ′ . For example, we have the following instantiated clause for the instruction ldmia r13, {, r11, r13, r15}: FE & PC.read&FBuf, DE , MEM&M.read&R [START_REF] Hohenauer | A methodology and tool suite for c compiler generation from adl processor models[END_REF].read&R [START_REF] Herbegue | Hardware architecture specification and constraint based wcet computation[END_REF].write&RoB , MEM&M.read& R [START_REF] Hohenauer | A methodology and tool suite for c compiler generation from adl processor models[END_REF].read&R [START_REF] Hohenauer | A methodology and tool suite for c compiler generation from adl processor models[END_REF].write&RoB ,MEM&M.read&R [START_REF] Hohenauer | A methodology and tool suite for c compiler generation from adl processor models[END_REF].read&PC.write&RoB , CM.

Branch Instruction. Some processors resolve branch target at the decode stage. The branch instruction is no longer used on next stages. So a branch instruction is dropped after the decode stage (lines 33-35 of listing 1.1). This is useful in out-of-order pipelines, since it reduces the structural hazards on functional units.

Formal Architecture Description

We formalize an architecture description through the architecture denoted by A and the instruction clauses of the basic block BB. We generate an equation system Eq(BB, A) representing the analyzed BB, with respect to A. In Eq(BB, A), the execution times are not computed. In order to do that, we formulate a set of structural and temporal high-level constraints Constraints A. The resolution of Eq(BB, A) and Constraints A provides an equation system where the instructions execution times have been computed (figure 4). We introduce a light DSL (Domain Specific Language) for expressing the architecture and basic block properties. We derive from every instruction of the basic block a set of tasks that are divided into levels:

-ISA level. The task represents the lifetime of the instruction on the pipeline.

It starts when the instruction enters the pipeline and finishes when it leaves. The task is given by the instruction index in the basic block. -Step level. The task models the execution of an instruction on a stage or a functional unit, what we call a step. Hereinafter, we use processing units to refer to stages or functional units. -Resource level. Basic tasks or leaves represent the resource allocation within an instruction step. This includes stages, functional units, buffers, registers and memory allocation.

The lifetime of every task is modeled using an interval. Table 1 summarizes the architecture DSL. We also consider the predefined functions scal(st) and nb(r) returning respectively a stage scalarity and a resource occurrences number. We consider the instruction sequence of figure 5 executed on the processor of figure 2 as a use case. From the Sim-nML description, the non terminal Stage , Register and M emory are instantiated as in (1).

= {F Buf, RoB} (1)
We assume the following semantic sets that we automatically generate from the architecture and the basic block:

-I denotes the set of tasks of the ISA level.

-S denotes the set of steps of all the instructions in the basic block, -L denotes the set of synthesized leaves, -U denotes the subset of leaves concerning stages or functional units, -B, R and M denote respectively the subset of leaves concerning buffers, registers and memories.

We consider the following dedicated quantifiers where ∀ I , ∀ S , ∀ L , ∀ U , ∀ B quantifies respectively over the basic block instructions, the steps, the leaves, the processing units and the buffers. We also use the predefined functions Last S (i), Buf f er(i, s) and U nit(i, s) that return respectively the last step task of i, the set of buffers and processing units of i at the step s.

I = {o t 0 0 , o t 1 1 , o t 2 2 } , S = S 0 ∪ S 1 ∪ S 2 , L = L 0 ∪ L 1 ∪ L 2
In the following, we detail the sets S 2 , U 2 ,R 2 ,B 2 and M 2 which are respectively the set of steps, stages, registers, buffers and memories of o 2 . The instruction o 2 is a load multiple and loads 3 registers from memory. So, we can observe that, based on the execution model in listing 1.1, 6 steps are generated, including 3 relative to the execution on the M EM unit. The instruction decomposition is illustrated in figure 6.

S 2 = {s t 2 0 2,0 , s t 2 1 2,1 , s t 2 2 2,2 , s t 2 3 2,3 , s t 2 4 2,4 , s t 2 5 2,5 } L 2 = U i2 ∪ R i2 ∪ B i2 ∪ M i2 U 2 = { 0 F E tu 2 0 2,0 , 0 DE tu 2 1 2,1 , 0 MEM tu 2 2 2,2 , 0 MEM tu 2 3 2,3 , 0 MEM tu 2 4 2,4 , 0 CM tu 2 5 2,5 } R 2 = { r 0 P C tr 2 0 2,0 , r 13 R tr 2 2 2,2 , w 11 R tr 2 2 2,2 , r 13 R tr 2 3 2,3 , w 13 R tr 2 3 2,3 , r 13 R tr 2 4 2,4
,

w P C tr 2 4 2,4 } B 2 = { ? F Buf tb 2 0 2,0 , ? RoB tb 2 2 2,2
, ? RoB tb 2 3 2,3

, ? RoB tb 2 4 2,4 } M 2 = { r 0 M tm 2 2 2,2 , r 0 M tm 2 3 2,3 , r 0 M tm 2 4

Architecture Properties

In this section we give a set of structural and dynamic properties that describes the architecture and instruction behavior. We use Allen intervals to express temporal relations between intervals. The properties are parametrized by the architecture and the basic block equations presented in the previous section.

Instruction Continuity. An instruction starts when its first step (s = 0) starts and terminates when its last step terminates. Considering two successive steps of an instruction, a current step finishes when the next step starts (2).

∀ I o t i . ∀ S s t ′ i,0 . t Starts t ′ ∀ S s t i,s . ∀ S s ′ t ′ i,s+1 . t Meets t ′ ∀ I o t i . ∀ S s t ′ i,Last S (i) . t Finishes t ′ (2)
Instruction Support. We assume that, within a step, an instruction requires one and only one stage and at the most one buffer resource (3a). This is a structural property used for architecture correctness validation. Two cases arise. First, if a buffer is required within a step, then this buffer is unique and is the support of the instruction during that step. Indeed, the instruction is contained in the buffer slot throughout the step. The buffer is allocated since the instruction starts execution within the step, and remains so until the resources on the next step become available. The buffer is released when the instruction starts the next step (3b). Second, if no buffer is used, thus, the stage is the instruction support. It is blocked until the instruction starts the next step, i.e. next step resources are available (3c).

∀i. ∀s. card (Buf f er(i, s)) ≤ 1 ∧ card (U nit(i, s)) = 1 (3a) ∀ S s t i,s . card (Buf f er(i, s)) = 1 ⇒ ∃! ? b t ′ i,s ∈ Buf f er(i, s). t = t ′ (3b) ∀ S s t i,s . card (Buf f er(i, s)) = 0 ⇒ ∃! o st t ′ i,s ∈ U nit(i, s). t = t ′ (3c)
Resources Allocation Policy. An instruction executes on a given stage, once it gets all its required resources, including the stage. Thus, all required resources are allocated at the beginning of the step (4a). After the execution latency elapses, all or some of the owned resources are released. Actually, we assume that an instruction keeps the resources that are going to be asked on further steps. This allocation policy is defined to avoid deadlocks. Such a situation occurs when a micro-coded instruction, as the multiple load presented in section 3, uses the same register on several successive steps. Such instruction must not be preempted during its execution on the processing unit. When an instruction uses a resource through two successive steps, we force the temporal continuity on the allocation intervals, as presented in the constraint (4b). Some resources, like stages and buffers, can be required in non-deterministic way: the instruction requests for any of the available occurrences, or in a deterministic way: the instruction requests for a specific occurrence. For a resource r, we have to insure that no more then nb(r) occurrences are allocated at the same time. This contention problem occurs in case of non-deterministic resources with dynamic scheduling. Currently, the property (4c) concerns stages and buffers.

∀ S s t i,s . ∀ L a o res t ′ i,s . t Starts t ′ ∧ t ′ During t (4a) ∀ L a o r t i,s . ∀ L a o r t ′ i,s+1 . t Meets t ′ (4b) ∀ U ∪B o x t i,s . card ({ o x t ′ i ′ ,s ′ ∈ U ∪ B | t Overlaps t ′ }) ≤ nb(x) (4c)
Stage Specific Constraints. These constraints depend on the stages execution features. For a simple-scalar stage with in-order execution, only one instruction is issued to the stage per cycle and is issued before its successor in the program (5a).

∀ U o st t i,s . ∀ U o st t ′ i ′ ,s ′ . i < i ′ ⇒ t Before t ′ (5a) ∀ U o st t i,s . card ({ o st t ′ i ′ ,s ′ ∈ U | t Overlaps t ′ }) ≤ scal(st) (5b) ∀ U o st t i,s . ∀ U o st t ′ i ′ ,s ′ . i ′ < i + scal(st) ⇒ t StartsBeforeBegin t ′ (5c) ∀ U o st t i,s . ∀ U o st t ′ i+scal(st),s ′ . t Before t ′ (5d)
In case we have a super-scalar stage st, at most scal(st) successive instructions can be issued in parallel (5b). However the overall program order must be maintained. Thus, an instruction of index i can be executed in parallel with an instruction of index j such that j < i + scalst. We introduce a new time relation StartsBef oreBegin that define a priority relation between two intervals (5c). The scalarity limit of the stage is expressed by a forced precedence between instruction i and instruction i + scal(st) (5d). For out-of-order stages, no precedence is defined except those implied by the data dependencies. Data Dependencies. Memories and registers can be owned in a read or a write mode. For example, when a register is accessed by two successive instructions such that the first request is a read access and the second is a write access, then, the read access must occur before the write access. Read After Write (RAW) hazards are explicited when instructions access registers and memories. Write After Write (WAW) hazards must be explicited for memory accesses.

∀ R r o reg el i,s . ∀ R w o reg el ′ i ′ ,s ′ . i ≤ i ′ ⇒ el Before el ′ ∀ R a o m el i,s . ∀ R w o m el ′ i ′ ,s ′ . i ≤ i ′ ⇒ el Before el ′ (6)
To elaborate the constraints Constraints A, we instantiate all (or some of) the constraints presented in equations from 2 to 6, with respect to the architecture A and the basic block sets. We detail here the constraints of the instruction o 0 which is a branch (the corresponding execution model is in listing 1.1):

( These high-level constraints are used to generate a constraint description to be processed by a given solver. In [START_REF] Herbegue | Hardware architecture specification and constraint based wcet computation[END_REF], we show how to solve these constraints with the CSP/CHOCO [START_REF] Choco | An Open Source Java Constraint Programming Library[END_REF]. The resolution of the constraints for the basic block of the figure 5 executed on the processor of figure 2 gives the following values, among others :t 0 = [0, 2] ; t 1 = [2, 6] and t 2 = [START_REF]L3: An ISA Specification Languag[END_REF][START_REF] Dalsgaard | METAMOC: Modular execution time analysis using model checking[END_REF]. In [START_REF] Herbegue | A constraint-based wcet computation framework[END_REF], we also show how to animate such properties through the timed automata provided by the UPPAAL tool [START_REF] Behrmann | QEST[END_REF].

2) → t 2 Starts t 2 0 ∧ t 2 0 Meets t 2 1 ∧ . . . t 2 1 Finishes t 2 (3) → tb 2 0 = t 2 0 ∧ tu 2 1 = t 2 1 ∧ tb 2 2 = t 2 2 ∧ tb 2 3 = t 2 3 ∧ . . . (

Related Work

There have been a lot of research efforts in architecture description languages that aim to formalize the processor specification provided in user manuals. Most of these efforts was based on ADLs like ArchC [START_REF] Miele | An framework for the simulation of mapping solutions on heterogeneous mpsocs[END_REF], LISA [START_REF] Hohenauer | A methodology and tool suite for c compiler generation from adl processor models[END_REF], HARMLESS [START_REF] Béchennec | Extending harmless architecture description language for embedded real-time systems validation[END_REF] and Sim-nML [START_REF] Herbegue | Hardware architecture specification and constraint based wcet computation[END_REF], that was used to generate retargetable tools. Since these ADLs are actually mature regarding the ISA level description, modern ISAs are currently supported and accurate simulators can be generated. Nevertheless, these approaches assume simple pipelines like DLX, since the micro-architecture is not handled or limited to its structure. Our general approach based on Simsupports the retargetable tool generation, in addition to complex instruction execution models. Retargetable WCET analysis tools based on processor description are presented, among others, in [START_REF] Li | Modeling out-of-order processors for WCET analysis[END_REF] [19] [6] [START_REF] Dalsgaard | METAMOC: Modular execution time analysis using model checking[END_REF]. Timed automata was observed in [START_REF] Béchennec | Computation of wcet using program slicing and realtime model-checking[END_REF] [9] as a formal processor description. This model is difficult to elaborate and is hand-made, which limits experimentations to simple five stage pipelines with in-order execution. Our approach offers a high-level processor description that can be used to generate timed automata. The work of [START_REF] Xianfeng | A retargetable software timing analyzer using architecture description language[END_REF] is close to ours. The authors use the EXPRESSION language to describe the ISA and the micro-architecture and generates execution graphs for the analysis. However, the ADL description only includes the pipeline structure. The hardware components behavior, such as out-of-order execution and superscalarity, are specified in C++ external libraries. The use of many formalisms to processor description makes it not suitable for validation. Other methods verify program behavior and the memory design [START_REF] Alglave | The semantics of power and arm multiprocessor machine code[END_REF] on PowerPC and ARM architecture using a formalization. This approach uses the L3 language [START_REF]L3: An ISA Specification Languag[END_REF] for the ISA description and the generation of a HOL specification used for verification. The formal description is limited to the ISA level and cannot be used for time analysis. The table 2 summarizes the architecture languages capabilities. Time analysis

• • • Formalization • • • • • Verification/Validation • • •
Out-of-order pipeline

• • • Superscalar pipeline • • • • • Complex instruction set • • • •

Conclusion

In this paper, we have showed how advanced architecture features can be described through an extension of the Sim-nML architecture description language.

We have presented the syntax for describing advanced pipelines structure and instructions with complex execution models. We have also presented a specification language that aims to formalize the architecture features. We have elaborated a set of generic properties that can be used for the generation of architecture constraints for time analysis and the validation. This formalization can be a basis for formal verification, required to obtain certified WCET computation methods. The proposed approach for time analysis is modular since it is based on the hardware description and the basic block, each one independent from the other. also comes from the fact that the Sim-nML description of the ISA the micro-architecture are separated in implementation terms, so that the same ISA description can be reused for different pipelines. High-level constraint description present a significant advantage since the user is free to choose the resolution method for WCET computation. We have drawn a comparison between currently used description languages and formalism. In this paper we have used a processor model that possess real word processor features to test our approach. We are currently validating our formalization on real-life processors that are rolling out on the market, among which the Cortex-A8.

Fig. 1 .

 1 Fig. 1. ADL-based flow for time analysis

1 Fig. 2 .Fig. 3 .

 123 Fig. 2. An out-of-order superscalar processor

Listing 1 . 1 . 8 b 10 reg

 11810 Sim-nML processor description 1 s t a g e FE , DE , ALU[START_REF]L3: An ISA Specification Languag[END_REF] , MEM , CM 2 e x t e n d FE , DE , CM 3 c a p a c i t y = 2 // super -s c a l a r i t y d e g r e e 4 i n o r d e r = t r u e // in-o r d e r s t a g e s 5 e x t e n d ALU , MEM i n o r d e r = f a l s e // out-o f-o r d e r s t a g e s 7 u f f e r FBuf [ 4 ] , RoB [ 8 ] // Fetch B u f f e r and Re-o r d e r B u f f e r 9 PC [ 1 , card ( 3 2 ) ] // 32-b i t PC r e g i s t e r 11 reg R [ 1 6 , card ( 3 2 ) ] // 16 r e g i s t e r s o f 32 b i t s 12 mem M [ 3 2 , card ( 8 ) ] // a memory o f 2ˆ32 8-b i t words 13 14 op ADD ( r d : card ( 4 ) , r s : card ( 4 ) , r n : card ( 4 ) ) 15 syntax = f o r m a t ( " add r%d r%d r%d" , rd , r s , r n ) 16 image = f o r m a t ( "00%2b%2b%2b" , rd , r s , r n ) 17 action = {R [ r d ] = R [ r s ] + R [ r n ] ; } 18 u s e s= FE & FBuf & PC. r e a d , DE, ALU & RoB & R [ r s ] . r e a d &R [ r n ] . r e a d 19 & R [ r d ] . w r i t e #{1} , CM 20 21 // M u l t i p l y i n s t r u c t i o n e x e c u t e d on t h e s p e c i l i z e d ALU 22 op MUL 23 u s e s= FE & FBuf & PC. r e a d , DE, ALU [ 0 ] & R [ r d ] . w r i t e & R [ rm ] . r e a d 24 & R [ r s ] . r e a d & RoB#{5} ,CM 25 26 // l o a d m u l t i p l e i n s t r u c t i o n 27 op l o a d m u l t i p l e ( r l i s t : card ( 1 6 ) , r n : card ( 4 ) ) 28 u s e s = FE & PC. r e a d & FBuf , DE , 29 i f r l <0..0>==1 t h e n MEM & M. r e a d & R [ r n ] . r e a d & R [ 0 ] . w r i t e & RoB e n d i f , 30 i f r l <1..1>==1 t h e n MEM & M. r e a d & R [ r n ] . r e a d & R [ 1 ] . w r i t e & RoB e n d i f , . . ,CM 31 32 // branch i n s t r u c t i o n dumped a f t e r decode 33 v a r t a k e n [ 1 , u1 ] 34 e x t e n d B Cond 35 u s e s = FE & PC. r e a d & FBuf ,DE & ( i f ( t a k e n ==1) t h e n PC. w r i t e e n d i f )

Listing 1 . 2 . 3 c a p a c i t y = 2 // 2 -s u p e r s c a l a r s t a g e s 4 e 6 e x t e n d MUL 7 u 9 e x t e n d DIV 10 u

 12322467910 Floating point pipeline 1 s t a g e FE, DE, ALU, MD0 , MD1 , MD2 , MD3, CM 2 e x t e n d FE , DE , CM x t e n d ALU , MD0 5 i n o r d e r = f a l s e // out-o f-o r d e r s t a g e s s e s= FE#{1} , DE#{1} , MD0 & R [ r d ] . w r i t e & R [ rm ] . r e a d & R [ r s ] . r e a d #{1} , MD1#{1} , MD2#{1} , MD3#{1} , CM#{1} s e s= FE#{1} , DE#{1} , MD0 & R [ r d ] . w r i t e & R [ r n ] . r e a d & R [ rm ] . r e a d #{21} , 11 MD1#{1} , MD2#{1} , MD3#{1} , CM#{1}

Fig. 4 .

 4 Fig. 4. Formal approach for time analysis 4.1 A Light DSL for Architecture Constraints

2 , 4 }Fig. 5 .

 245 Fig. 5. Basic block

Fig. 6 .

 6 Fig. 6. Decomposition of instruction o 2

Table 1 .

 1 Architecture DSL

	ISA	interval instruction		Step	interval instruction , step
	Resource level tasks (leaves):
	occurrence|? Stage	interval instruction , step |	[r|w] occurrence|? Resource	interval instruction , step

Architecture domain Stage , Register , M emory , Buf f er , Resource ::= Register | Buf f er | M emory Basic block domain (of length n) instruction ::= nat , step ::= nat , interval ::= string ISA level tasks:

Step level tasks:

Stage ::= {F E, DE, ALU, M EM, CM } , Register ::= {R, P C}, M emory ::= {M }, Buf f er ::

Table 2 .

 2 Architecture languages summary table

		ArchC Chronos LISA Harmless Expression L3 Otawa
	Code optimization
	Simulation	•	•	•	•	•
	Retargetable tool generation