Alberto Seeger
email: alberto.seeger@univ-avignon.fr

Mounir Torki
email: mounir.torki@univ-avignon.fr

Centers and partial volumes of convex cones I. Basic theory

Keywords: Partial volume of a convex cone, Solid angle, Volumetric center, Incenter

We study the concept of least partial volume of a proper cone in R n . This notion is a reasonable alternative to the classical concept of solid angle. In tandem, we study the concept of volumetric center of a proper cone. We compare this kind of center with the old notion of incenter.

Introduction

Let n denote the set of proper cones in R n . A closed convex cone is said to be proper if it is pointed and has nonempty interior. Perhaps the most natural way to define the "volume" of a proper cone K in R n is by setting btv(K

) := vol n (K ∩ B n ), ( 1
)
where B n is the n-dimensional closed unit ball and vol n (•) stands for the n-dimensional Lebesgue measure. By an obvious reason, one refers to the positive number (1) as the 1 ball-truncated volume of K . The expression (1) is, up to a multiplicative constant, equal to the solid angle of K . Indeed, btv

(K ) = 1 n vol n-1 (K ∩ S n ),
where S n stands for the unit sphere of R n . The computation of ball-truncated volumes in spaces of dimension higher than three has been the object of several publications in the last decade, cf. [START_REF] Gourion | Deterministic and stochastic methods for computing the volumetric moduli of convex cones[END_REF][START_REF] Ribando | Measuring solid angles beyond dimension three[END_REF]. For a vast majority of proper cones arising in practice, it is hopeless to derive an easily computable formula for evaluating the ball-truncated volume, so one has to resort to all kinds of numerical schemes: use of multivariate power series as in [START_REF] Ribando | Measuring solid angles beyond dimension three[END_REF], numerical integration methods as in [START_REF] Gourion | Deterministic and stochastic methods for computing the volumetric moduli of convex cones[END_REF], Section 3), probabilistic methods as in [START_REF] Gourion | Deterministic and stochastic methods for computing the volumetric moduli of convex cones[END_REF], Section 5), etc.

Our work has essentially two goals. The first one is to study in depth the concept of least partial volume, which is a fruitful alternative to the concept of ball-truncated volume.

Definition 1.1 The partial volume of K ∈ n relative to x ∈ R n is the possibly infinite number

v K (x) := vol n (K ∩ H x ),
where H x is the closed half-space given by H x := {u ∈ R n : x, u ≤ 1}. The finite number lpv(K ) := min

x∈S n vol n (K ∩ H x ) (2)
is called the least partial volume of K .

The functions lpv : n → R and btv : n → R share a number of properties: monotonicity with respect to set inclusion, invariance under orthogonal transformations, etc. These functions differ however in a substantial way.

As we shall see in Sect. 3, the minimization problem (2) has exactly one solution. Geometrically speaking, such solution can be viewed as a "center" of the dual cone K * := {y ∈ R n : y, x ≥ 0 for all x ∈ K }.

(3) Since ( 3) is proper as well and has K as dual cone, we suggest to consider the following definition.

Definition 1.2 Let K ∈ n . The volumetric center of K , denoted by (K ), is the unique solution to the minimization problem lpv(K * ) = min

x∈S n vol n (K * ∩ H x ). ( 4
)
The analysis and computation of volumetric centers is the second goal of our work. In particular, we discuss the link between the volumetric center and the incenter of a proper cone. The incenter of K ∈ n , denoted by ξ(K ), is defined as the unique solution to the maximization problem

r (K ) := max x∈S n ∩K dist(x, ∂ K ),
where dist(x, ∂ K ) stands for the distance from x to the boundary of K . The vector ξ(K ) belongs clearly to the interior of K . The coefficient r (K ) is called the inradius of K . The reader is conveyed to Henrion andSeeger (2010a, b, 2011), and [START_REF] Seeger | Centers of sets with symmetry or cyclicity properties[END_REF] for general material concerning the theory of incenters.

Basic facts on partial volumes

We start the discussion by recalling some basic properties of the extended real valued function v K : R n → R ∪ {∞}. Such a function is known in the optimization community, specially among practitioners of interior point methods [cf. [START_REF] Güler | Barrier functions in interior point methods[END_REF][START_REF] Nesterov | Interior-point polynomial algorithms in convex programming[END_REF][START_REF] Truong | Geometry of homogeneous convex cones, duality mapping, and optimal selfconcordant barriers[END_REF]]. For instance, Güler (1996, Theorem 4.1) has derived the integral representation formula

v K (x) = 1 n! K e -x,y dy (5)
for all x ∈ int(K * ). As a function of the vector x, the integral on the right-hand side of (5) corresponds to the Koszul-Vinberg characteristic function of K * . The next proposition sets straight a number of technical details.

Proposition 2.1 Let K ∈ n . One has:

(a) v K (x) ≥ x -n btv(K ) for all x = 0. In particular, v K is positive on R n . (b) v K (x) < ∞ if and only if x ∈ int(K * ). (c) v K (t x) = t -n v K (x) for all t > 0 and x ∈ R n . (d) v K is convex. In fact, v K is strictly log-convex on int(K * ). (e) v K is infinitely often differentiable on int(K * ).
Proof (a) For all x = 0, one has

H x ⊇ x -1 B n . Hence, v K (x) ≥ vol n K ∩ ( x -1 B n ) = vol n x -1 (K ∩ B n ) = x -n btv(K ). (b) Let x ∈ R n . The set K ∩ H x is closed, convex,
K ∩ H t x = t -1 (K ∩ H x ).
(d) and (e) See (Faraut and Korányi 1994, Proposition I.3.3) and (Faraut and Korányi 1994, Proposition I.3.1), respectively.

The function v K has many other interesting properties. For instance, it is known that v K behaves as a barrier function for K * . Such a property plays an important role in the analysis of interior point methods. The following result is a refinement of (Faraut and Korányi 1994, Proposition I.3.2).

Proposition 2.2 Let K ∈ n and {x ν } ν∈N be a bounded sequence in the interior of K * . Then

lim ν→∞ v K (x ν ) = ∞ if and only if lim ν→∞ dist(x ν , ∂ K * ) = 0. ( 6
)
Proof As pointed out in (Seeger 2012, Lemma 5.1), one has

K e -x,y dy ≤ 1 dist(x, ∂ K * ) n K e -y dy (7)
for all x ∈ int(K * ). The above inequality proves the "only if" part of ( 6). The proof of the "if" part runs as follows. Suppose that dist(x ν , ∂ K * ) goes to 0, but that

κ := lim inf ν→∞ v K (x ν )
is finite. One must arrive to a contradiction. Take a subsequence {x ϕ(ν) } ν∈N such that

lim ν→∞ v K (x ϕ(ν) ) = κ.
Without loss of generality, one may suppose that x := lim ν→∞ x ϕ(ν) exists. By passing to the limit on the right-hand side of

dist( x, ∂ K * ) ≤ x -x ϕ(ν) + dist(x ϕ(ν) , ∂ K * ),
one sees that x ∈ ∂ K * . In such a case (Faraut and Korányi 1994, Proposition I.3.2) implies that v K (x ϕ(ν) ) goes to infinity, a clear contradiction.

The "if" part of ( 6) is no longer true if the sequence {x ν } ν∈N is unbounded. The combination of Proposition 2.1(a) and the inequality (7) leads to the following sandwich for lpv(K ).

Proposition 2.3 For all K ∈ n , one has btv(K ) ≤ lpv(K ) ≤ r (K * ) -n btv(K ). ( 8
)
Proof The first inequality in (8) follows from Proposition 2.1(a). Note that

K e -y dy = ∞ 0 K ∩tS n e -t dy dt = (n -1)! vol n-1 (K ∩ S n ).
Hence, (7) can be rewritten as

v K (x) ≤ 1 dist(x, ∂ K * ) n btv(K ).
It suffices now to take the minimum with respect to x ∈ S n ∩ int(K * ).

As seen in the proof of Proposition 2.1(b), if K ∈ n and x ∈ int(K * ), then K ∩ H x is an n-dimensional convex body. Sometimes it is easier to compute the volume of a convex body by evaluating the volume of an associated convex body that has one dimension less. This is the basic idea behind the following proposition.

Proposition 2.4 Let K ∈ n and x ∈ int(K * ). Then v K (x) = 1 n x vol n-1 (K ∩ ∂ H x ), ( 9
)
with ∂ H x denoting the boundary of H x .

Proof Formula (9) appears already in the proof of (Güler 1996, Theorem 4.1), at least for the particular case in which x ∈ int(K * ) is a unit vector. If x ∈ int(K * ) is not a unit vector, then we write

v K (x) = v K x x x = 1 x n v K x x = 1 n x n vol n-1 K ∩ ∂ H x -1 x and observe that K ∩ ∂ H x -1 x = x (K ∩ ∂ H x ) . Hence, v K (x) = 1 n x n vol n-1 ( x (K ∩ ∂ H x )) = 1 n x vol n-1 (K ∩ ∂ H x ) ,
as desired.

In the sequel, GL(n) denotes the general linear group of nonsingular matrices of order n and the superscript "T" stands for transposition.

Proposition 2.5 Let K = G(Q) with G ∈ GL(n). Then, for all x ∈ int(K * ), one has v K (x) = |det G| v Q (G T x). Proof One can easily check that int(K * ) = {x ∈ R n : G T x ∈ int(Q * )}, K ∩ H x = G Q ∩ H G T x .
So, it suffices to take the n-dimensional Lebesgue measure on each side of the last equality.

Example 2.6 As pointed out in [START_REF] Güler | Barrier functions in interior point methods[END_REF]

, one has v R n + (x) = n! n i=1 x i -1 for all x ∈ int(R n + ).
Consider now an arbitrary simplicial cone, i.e., a proper cone of the form

K = G(R n + ) with G ∈ GL(n). One gets v K (x) = 1 n! |det G| n i=1 g i , x
for all x ∈ int(K * ).

Basic facts on volumetric centers

We now introduce the concept of volumetric center into the discussion. The idea is to use the following simple but fundamental fact.

Proposition 3.1 Let K ∈ n . Then v K admits a unique minimizer on S n . Furthermore, such a minimizer lies in the interior of K * .

Proof In view of the statements (a) and (c) of Proposition 2.1, the minimization problem (2) has the same optimal value and the same solution set as

minimize v K (x) x ∈ B n . ( 10
)
The solution set to (10) has at most one element, because it is a convex set contained in S n . It remains to prove that (10) has at least one solution. Let {x ν } ν∈N be a sequence in

B n ∩ int(K * ) such that lim ν→∞ v K (x ν ) = lpv(K ).
Without loss of generality, one may suppose that x := lim ν→∞ x ν exists. By using Proposition 2.2, one deduces that x is a solution to (10) and that x ∈ int(K * ).

A result similar to Proposition 3.1 is obtained by exchanging the roles of K and K * . As mentioned in Sect. 1, the unique solution to (4) is denoted by (K ) and it is called the volumetric center of K .

The following result is easy and consistent with geometric intuition. The first formula in Proposition 3.2 says that lpv : n → R is invariant under orthogonal transformations. The second formula says that an orthogonal transformation acting on a proper cone modifies its volumetric center as expected. The notation O(n) refers to the set of orthogonal matrices of order n.

Proposition 3.2 Let K ∈ n . Then, for all U ∈ O(n), one has lpv(U (K )) = lpv(K ), (U (K )) = U ( (K )).

More generally, for any pair A, B of invertible matrices such that A

T A = B T B, one can write lpv(A(K )) = lpv(B(K )), (11) A -1 (A(K )) = B -1 (B(K )). (12) Proof Note that lpv(U (K )) = min{vol n [U (K ) ∩ H x ] : x ∈ S n } = min{vol n U (K ∩ H U T x ) : x ∈ S n } = min{vol n K ∩ H U T x : x ∈ S n }.
The change of variables y = U T x leads to

lpv(U (K )) = min{vol n (K ∩ H y ) : y ∈ S n } = lpv(K ),
and shows that (K ) = U T (U (K )). For proving ( 11) and ( 12), one just needs to observe that A(K ) is the image of B(K ) under the orthogonal matrix AB -1 .

The next theorem characterizes the volumetric center of K ∈ n as the unique fixed point of the gradient map

∇ K : int(K ) → R n , where K : int(K ) → R is the strictly concave function given by K (x) := - 1 n log[v K * (x)].
In view of ( 5), one has

∇ K (x) = - ∇v K * (x) nv K * (x) = 1 n K * ye -x,y dy K * e -x,y dy . For subsequence use, we recall that ⎧ ⎨ ⎩ ∇ K is a bijection between int(K ) and int(K * ), ∇ K (t x) = t -1 ∇ K (x) for all t > 0 and x ∈ int(K ), the Hessian matrix ∇ 2 K (x) is negative definite for all x ∈ int(K ). ( 13
)
The properties listed in (13) can be found for instance in (Faraut and Korányi, 1994, Section I.3).

Theorem 3.3 Let K ∈ n . Then (K ) is the unique solution to the fixed point problem x ∈ int(K ), x = ∇ K (x). ( 14
)
In particular, (K ) belongs not only to int(K ), but also to int(K * ).

Proof By writing down the optimality conditions for the minimization of the convex function v K * on the convex set B n , one sees that (K ) is equal to the unique solution to the system

x ∈ S n ∩ int(K ), -∇v K * (x) ∈ N B n (x),
where N B n (x) is the normal cone to B n at x. This system can be written in the equivalent form

x ∈ int(K ), ∇v K * (x) = ∇v K * (x), x x. ( 15
)
The equality stated in (15) contains implicitly the information that x is a unit vector. Since v K * is positively homogeneous of degree -n, the Euler equation

∇v K * (x), x = -nv K * (x)
holds for all x ∈ int(K ). Hence, the system (15) can be rewritten as in ( 14).

Remark 3.4 [START_REF] Vinberg | The theory of convex homogeneous cones[END_REF] suggested to use the unique solution to the fixed point problem ( 14) as definition of "center" for a homogeneous cone K ∈ n , but in fact one can dispense from homogeneity. One says that K ∈ n is homogeneous if, for all x, y ∈ int(K ), there exists

A ∈ GL(n) such that A(K ) = K and Ax = y.
The fixed point characterization of (K ) can be exploited in manifold ways. For instance, one can use it to derive a formula for computing the volumetric center of a Cartesian product of finitely many proper cones.

Corollary 3.5 Let n = n 1 + • • • + n q with n 1 , . . . , n q ≥ 1. Let K be the Cartesian product of the cones K 1 ∈ n 1 , . . . , K q ∈ n q . Then K ∈ n and n 1/2 (K ) = n 1/2 1 (K 1 ), . . . , n 1/2 q (K q ) , ( 16
) lpv (K ) κ n = lpv(K 1 ) κ n 1 . . . lpv(K q ) κ n q , ( 17
)
where

κ n = n n/2 /n!.
Proof Clearly, K * is the Cartesian product of the K * i 's. A matter of computation shows that, for all x = (x 1 , . . . , x q ) ∈ int(K ), one has

v K * (x) = n 1 ! . . . n q ! n! v K * 1 (x 1 ) . . . v K * q (x q ), ∇ K (x) = n 1 n ∇ K 1 (x 1 ), . . . , n q n ∇ K q (x q ) . ( 18
)
The combination of ( 13), (18), and Theorem 3.3, leads to (16). On the other hand,

v K * ( (K )) = n 1 ! . . . n q ! n! v K * 1 n 1 n (K 1 ) . . . v K * q n q n (K q ) = κ n κ n 1 . . . κ n q v K * 1 ( (K 1 )) . . . v K * q (K q ) .
In other words,

lpv (K * ) κ n = lpv(K * 1 ) κ n 1 . . . lpv(K * q ) κ n q . ( 19
)
The equality ( 17) is obtained from ( 19) by exchanging the roles of K i and K * i .

Analysis of a few particular cones

Computing a volumetric center may be difficult or not depending on the geometric nature of the cone. The computation of (K ) is greatly simplified if K ∈ n is symmetric with respect to one or several linear subspaces. Symmetry with respect to a linear subspace is understood in the classical sense, i.e., invariance with respect to reflection through that subspace [(cf. [START_REF] Barker | Generalizations of top-heavy cones[END_REF], Definition 1)].

Lemma 4.1 Let L be a linear subspace with respect to which K ∈ n is symmetric. Then (K ) ∈ L.

Proof Combine Proposition 3.2 and the symmetry principle established in (Seeger and Torki 2014, Theorem 2.4).

Let S(K ) denote the intersection of all linear subspaces with respect to which K ∈ n is symmetric. The dimension of the subspace S(K ) is called the symmetry rank of K . We mention in passing that S(K * ) = S(K ) for all K ∈ n . In particular, K * and K have the same symmetry rank.

Theorem 4.2 Suppose that K ∈ n has symmetry rank equal to 1, i.e., there exists a vector c ∈ S n such that S(K ) = Rc. Then

(K ) = (K * ) = c if c ∈ K , -c if c / ∈ K .
Proof By applying Lemma 4.1 first to K and then to K * , one gets (K ) = ±c and (K * ) = ±c, respectively. Since the unit vectors (K ) ∈ int(K ) and (K * ) ∈ int(K * ) cannot be opposite, one necessarily has (K ) = (K * ).

By the way, saying that K ∈ n has symmetry rank equal to 1 is weaker than saying that K is symmetric with respect to a one-dimensional subspace. The next two corollaries are obtained straightforwardly from Theorem 4.2. We just give short sketches of theirs proofs.

Corollary 4.3 Let K ∈ n be permutation invariant, i.e., P(K ) = K for all permutation matrix P. Then

(K ) = (K * ) = 1 n / √ n if 1 n ∈ K , -1 n / √ n if 1 n / ∈ K ,
where 1 n stands for the n-dimensional vector of ones.

(R n + ) = 1 n / √ n. Thus, lpv(R n + ) = v R n + 1 n √ n = n n/2 n! .
A top-heavy cone in R n is a proper cone that can be expressed as epigraph of a norm on R n-1 . Such class of cones has been studied in depth by [START_REF] Fiedler | Cones which are topheavy with respect to a norm[END_REF], see also [START_REF] Barker | Generalizations of top-heavy cones[END_REF].

Corollary 4.5 Let K ∈ n be top-heavy up to orthogonal transformation, i.e., there exist an orthogonal matrix U = [u 1 , . . . , u n ] of order n and a norm on R n-1 such that K = U (epi ), where

epi := x ∈ R n : (x 1 , . . . , x n-1 ) ≤ x n . Then (K ) = (K * ) = u n . Furthermore, lpv(K ) = 1 n vol n-1 (B ),
where B denotes the closed unit ball associated to .

Proof In view of Proposition 3.2, it suffices to consider the case in which U is equal to I n , the identity matrix of order n. In such a case, K is symmetric with respect to the line generated by n-th canonical vector e n := (0, . . . , 0, 1) T . Thus, (K ) = (K * ) = e n and lpv(K

) = v K (e n ) = 1 n vol n-1 K ∩ ∂ H e n .
For completing the proof we observe that K ∩ ∂ H e n is equal to B × {1}.

There are plenty of interesting proper cones that fit into the setting of Corollary 4.5. By way of example we mention

L n := ⎧ ⎨ ⎩ x ∈ R n : n-1 i=1 x 2 i 1/2 ≤ x n ⎫ ⎬ ⎭ (Lorentz or circular cone), K n, p := ⎧ ⎨ ⎩ x ∈ R n : n-1 i=1 |x i | p 1/ p ≤ x n ⎫ ⎬ ⎭ ( p -cone with 1 ≤ p < ∞), K n,∞ := x ∈ R n : max 1≤i≤n-1 |x i | ≤ x n ( ∞ -cone), E M := (z, t) ∈ R n : z, Mz ≤ t (upward ellipsoidal cone).
The upward ellipsoidal cone E M is defined in terms of a symmetric positive definite matrix M of order n -1. All the above cones have the vector e n as volumetric center.

Their least partial volumes are given by the following explicit formulas:

lpv (L n ) = π (n-1)/2 n ((n + 1)/2) , lpv K n, p = [2 (1 + 1/ p)] n-1 n (1 + (n -1)/ p) , lpv K n,∞ = 2 n-1 /n, lpv (E M ) = lpv (L n ) √ det M ,
where stands for the usual Euler gamma function.

As shown above, the least partial volume of the upward ellipsoidal cone E M can be computed in a straightforward manner. To the best of our knowledge, there is no simple formula for evaluating the ball-truncated volume of E M . Another useful proper cone that fits into the setting of Corollary 4.5 is the revolution cone rev(c, s)

:= {x ∈ R n : s x ≤ c, x },
where c ∈ S n determines the revolution axis and s ∈]0, 1[ is a parameter reflecting the degree of aperture of the cone. One gets

(rev(c, s)) = c, lpv (rev(c, s)) = 1 s 2 -1 n-1 2 lpv (L n ) .
The next proposition concerns the case of a general ellipsoidal cone, i.e., not necessarily upward. By definition, an ellipsoidal cone in R n is an image of the Lorentz cone L n under a nonsingular matrix, cf. [START_REF] Stern | Invariant ellipsoidal cones[END_REF]. Ellipsoidal cones have been studied under different angles by a number of authors, see for instance [START_REF] Bhattacharya | Ellipsoidal cones and rendezvous of multiple agents[END_REF] for an application of ellipsoidal cones in control theory.

Proposition 4.6 Let K = G(L n ) with G ∈ GL(n). Then lpv (K ) = (-μ) n/2 |det G| lpv (L n ) ,
where μ is the smallest eigenvalue of the symmetric matrix

G := G -T (I n -2e n e T n )G -1 .
Furthermore, (K ) is an eigenvector of G associated to the eigenvalue μ. More precisely, (K ) is the unique solution to

G x = μ x, x = 1, G -T e n , x > 0. ( 20
)
Proof Following similar steps as in (Seeger 2013, Lemma 5), one can check that

K = U (E M ) (21)
for some U ∈ O(n) and some positive definite symmetric matrix M of order n -1. We briefly explain the construction of U and M. The matrix G is clearly symmetric. Let

λ 1 (G ) ≥ . . . ≥ λ n-1 (G ) ≥ λ n (G )
be the eigenvalues of G arranged in nonincreasing order. By applying Silvester's inertia theorem, one sees that μ = λ n (G ) is negative and all the other eigenvalues of G are positive. Hence, the diagonal matrix

M := -μ -1 Diag λ 1 (G ) , . . . , λ n-1 (G )
is positive definite. Let the columns of U be formed with an orthonormal basis of eigenvectors of G . As last column of U we take the vector x ∈ R n which solves (20). Such choices of M and U lead to the representation formula ( 21), from where one gets (K ) = U e n = x and

lpv(K ) = lpv(E M ) = lpv (L n ) √ det M . ( 22
)
It remains now to substitute det M = (det G) -2 (-μ) -n into ( 22).

The dual of an ellipsoidal cone is an ellipsoidal cone. The next corollary is a consequence of the representation formula ( 21) and the fact that

(E M ) * = E M -1 .
Corollary 4.7 Let K be an ellipsoidal cone in R n . Then

(K * ) = (K ), ( 23
) lpv(K * ) lpv(K ) = lpv(L n ) 2 . ( 24
)
Proof One can represent K as in ( 21). In such a case, K * = U (E M -1 ) and

U T (K * ) = (E M -1 ) = (E M ) = U T (K ).
This proves (23). On the other hand,

lpv(K * ) lpv(L n ) = lpv(E M -1 ) lpv(L n ) = 1 det(M -1 ) = 1 √ detM -1 = lpv(E M ) lpv(L n ) -1 = lpv(K ) lpv(L n ) -1
.

This proves (24).

Continuity issues

Let n denote the set of nontrivial closed convex cones in R n . Recall that a closed convex cone is nontrivial if it is different from the zero cone and the whole space. Topological and continuity issues on n are relative to the spherical metric δ. By definition, the spherical distance between a pair P, Q of elements in n is the number

δ(P, Q) := haus(P ∩ S n , Q ∩ S n ),
δ bt (P, Q) := haus(P ∩ B n , Q ∩ B n ).
In fact, one has

δ bt (P, Q) ≤ δ(P, Q) ≤ 2δ bt (P, Q)
for all P, Q ∈ n . Convergence with respect to the spherical metric is also equivalent to convergence in the Painlevé-Kuratowski sense.

A nontrivial closed convex cone is said to be solid if it has nonempty interior. Since the sets ptd

n := {K ∈ n : K is pointed}, sol n := {K ∈ n : K is solid}
are open in the metric space ( n , δ), so does their intersection n = ptd n ∩ sol n . A natural question to ask is whether lpv : n → R and : n → R n are continuous functions. The situation is well understood in what concerns ball-truncated volumes, inradiuses, and incenters. For instance, Gourion and Seeger (2012, [Theorem 2.3]) proved that btv : n → R is Lipschitzian. Proposition 5.1 There exists a constant n such that

|btv(P) -btv(Q)| ≤ n δ(P, Q) for all P, Q ∈ n .
The real valued function btv(•) is well defined not just on n , but also on the larger set n . The following Lipschitzness result is a direct consequence of (Iusem and Seeger 2008, Proposition 13).

Proposition 5.2 For all P, Q ∈ n , one has

|r (P) -r (Q)| ≤ 2δ(P, Q).
The vector ξ(K ) is well defined as long as K belongs to sol n . The continuity of the incenter function ξ : sol n → R n has been established in (Henrion and Seeger 2010a, Theorem 2.9). Recently, Seeger (2014, Theorem 7) proved that the incenter function is not merely continuous, but also locally Hölderian.

Proposition 5.3 For all P, Q ∈ sol n , one has

ξ(P) -ξ(Q) ≤ 4 √ r (P) + r (Q) [δ(P, Q)] 1/2 .
In particular, ξ : sol n → R n is locally Hölderian with Hölder exponent 1/2. The next theorem is the main result of this section. It shows that lpv(K ) and (K ) behave in a continuous manner with respect to perturbations in the argument K ∈ n . We state first three useful lemmas. The first lemma concerns n-dimensional volumes of symmetric differences of compact convex sets. Recall that the circumradius of a convex body ⊆ R n is defined as the radius of the smallest closed ball containing .

Lemma 5.4 Let ⊆ R n be a convex body with circumradius equal to ρ. Then

vol n (C D) ≤ (3ρ) n -1 ρ vol n (B n ) haus(C, D)
for any pair C, D of nonempty compact convex subsets of .

Proof There exists a unique z ∈ R n , called the circumcenter of , such that

⊆ z + ρB n . Let t = haus(C, D). Since D ⊆ C + tB n , one has vol n (D\C) ≤ vol n ((C + tB n )\C) = vol n (C + tB n ) -vol n (C). But vol n (C + tB n ) = n k=0 k (C) t k ,
where 0 (C), . . . , n (C) are the coefficients in the Steiner polynomial associated to C. The coefficients k (C) are nonnegative and depend not just on C, but also on the dimension n of the ambient space. In fact,

k (C) = n! k!(n -k)! V (C, . . . , C n-k , B n , . . . , B n k ) ,
where V (C 1 , . . . , C n ) stands for the mixed volume of the convex bodies C 1 , . . . , C n .

In particular, 0 (C) = vol n (C). As mentioned in (Gardner 1995, Appendix A.3), the function V is nondecreasing in each argument with respect to set inclusion. It follows that

vol n (D\C) ≤ n k=1 k (C) t k ≤ n k=1 k (z + ρB n ) t k-1 t ≤ 1 2ρ n k=1 k (z + ρB n ) (2ρ) k t. ( 25
)
The last equality is due to the fact that t ≤ 2ρ, because C and D are subsets of . By equating coefficients in the polynomials

vol n (z + ρB n + tB n ) = (ρ + t) n vol n (B n ), vol n (z + ρB n + tB n ) = n k=0 k (z + ρB n ) t k , one gets k (z + ρB n ) = n! k!(n -k)! ρ n-k vol n (B n ).
Substituting this information into (25) and simplifying, one obtains

vol n (D\C) ≤ (3ρ) n -1 2ρ vol n (B n ) t.
The same estimate holds for the n-dimensional volume of C\D.

The second lemma is a technical result concerning the distance from a point to the boundary of a convex cone.

Lemma 5.5 Let K ∈ n . Then, for all x ∈ R n and r ≥ x , one has

dist(x, r B n ∩ ∂ K ) = dist(x, ∂ K ) ≤ x .
Proof Take any y 0 ∈ ∂ K such that dist(x, ∂ K ) = xy 0 . Since ∂ K is stable under multiplication by positive scalars, one has xy 0 , y 0 = 0. By using Pythagoras rule

x -y 0 2 + y 0 2 = x 2 , one gets y 0 ≤ x and dist(x, ∂ K ) ≤ x . One also obtains dist(x, r B n ∩ ∂ K ) = dist(x, ∂ K ), because y 0 ∈ r B n ∩ ∂ K .
The third and last lemma concerns the convergence of boundaries of converging cones. As a consequence of Lemma 5.6, one sees that:

If {K ν } ν∈N ⊆ n converges to K ∞ ∈ n , then lim ν→∞ haus(S n ∩ ∂ K ν , S n ∩ ∂ K ∞ ) = 0.
Lemma 5.6 For all P, Q ∈ n , one has

haus(S n ∩ ∂ P, S n ∩ ∂ Q) ≤ 2δ bt (P, Q). ( 26
)
Proof It suffices to proves that dist(x, ∂ Q) ≤ 2δ bt (P, Q) for all x ∈ S n ∩ ∂ P. Let x be as just mentioned. Note that C := 2B n ∩ P and

D := 2B n ∩ Q are convex bodies in R n . Since ∂ D = (2B n ∩ ∂ Q) ∪ (2S n ∩ Q), one has dist(x, ∂ D) = min {dist(x, 2B n ∩ ∂ Q), dist(x, 2S n ∩ Q)} . Clearly, dist(x, 2S n ∩ Q) ≥ dist(x, 2S n ) = 1, dist(x, 2B n ∩ ∂ Q) = dist(x, ∂ Q) ≤ 1,
the second line being a consequence of Lemma 5.5. It follows that

dist(x, ∂ Q) = dist(x, ∂ D) ≤ max z∈S n ∩∂ P dist(z, ∂ D) ≤ max z∈∂C dist(z, ∂ D) ≤ haus(C, D),
where the last inequality is obtaining by applying (Wills 2007, Theorem 14). Finally, by using a simple positive homogeneity argument, one sees that haus(C, D) = 2δ bt (P, Q).

We do not know if the inequality (26) remains true for P, Q in the larger set n . Anyway, we now are ready to state: Theorem 5.7 The functions lpv : n → R and : n → R n are continuous.

Proof Let {K ν } ν∈N be a sequence in n converging to a certain K ∞ ∈ n , i.e., lim

ν→∞ δ(K ν , K ∞ ) = 0. ( 27
)
We must prove that

lim ν→∞ lpv(K ν ) = lpv(K ∞ ) (28) lim ν→∞ (K ν ) = (K ∞ ). ( 29
)
For the sake of clarity in the exposition, we divide the proof into several steps.

Step 1 We prove that {lpv(K ν )} ν∈N is bounded. For each ε positive, let ε (K ∞ ) denote the smallest closed convex cone containing the compact set K ∞ ∩ S n + εB n . We take ε sufficiently small in order to ensure that ε (K ∞ ) is proper. One has

K ν ∩ S n ⊆ K ∞ ∩ S n + δ(K ν , K ∞ )B n ⊆ K ∞ ∩ S n + εB n ⊆ ε (K ∞ )
for all ν large enough. In particular,

K ν ⊆ ε (K ∞ ) and lpv(K ν ) ≤ lpv( ε (K ∞ )).
Step 2 We prove that for each sequence {x ν } ν∈N satisfying

x ν ∈ S n ∩ int(K * ν ), (30) x ∞ := lim ν→∞ x ν exists and belongs to int(K * ∞ ), (31)
there exists a constant s ∈ ]0, 1[ such that

K ν ∪ K ∞ ⊆ rev(x ν , s) (32)
for all ν large enough. Thanks to the Walkup-Wets isometry theorem (cf. [START_REF] Walkup | Continuity of some convex-cone-valued mappings[END_REF], Theorem 1]), the condition ( 27) is equivalent to

lim ν→∞ δ(K * ν , K * ∞ ) = 0. (33) Since x ∞ ∈ int(K * ∞ )
, there exists a small positive s such that

x ∞ + 2sB n ⊆ int(K * ∞ ).
By combining (33) and a standard stability result for Painlevé-Kuratowski limits (cf. [Rockafellar and Wets 1998, Proposition 4.15]), one gets

x ∞ + 2sB n ⊆ int(K * ν )
for all ν greater than a certain integer ν 0 . Since {x ν } ν∈N converges to x ∞ , it follows that

x ν + sB n ⊆ K * ∞ and x ν + sB n ⊆ K * ν
for all ν greater than another integer ν 1 ≥ ν 0 . By passing to dual cones in

R + (x ν + sB n ) ⊆ K * ∞ and R + (x ν + sB n ) ⊆ K * ν ,
one gets the reverse inclusions rev(x ν , s) ⊇ K ∞ and rev(x ν , s) ⊇ K ν . This proves (32).

Step 3 We show that, for any {x ν } ν∈N as in Step 2, one has

lim ν→∞ v K ν (x ν ) = v K ∞ (x ∞ ). ( 34
)
As we saw already, x ν ∈ int(K * ∞ ) for all ν large enough. Hence, one can write

|v K ν (x ν ) -v K ∞ (x ∞ )| ≤ |v K ν (x ν ) -v K ∞ (x ν )| + |v K ∞ (x ν ) -v K ∞ (x ∞ )|. Since v K ∞ : int(K * ∞ ) → R is continuous, one has lim ν→∞ v K ∞ (x ν ) = v K ∞ (x ∞
). On the other hand, thanks to (5), one gets

n! |v K ν (x ν ) -v K ∞ (x ν )| ≤ a ν with a ν := D ν e -x ν ,y dy and D ν := K ν K ∞ .
By using (32), one obtains

a ν ≤ D ν e -s y dy = 1 s n D ν e -y dy = 1 s n ∞ 0 D ν ∩tS n e -t dy dt = 1 s n ∞ 0 e -t vol n-1 (D ν ∩ tS n )dt = (n -1)! s n vol n-1 (D ν ∩ S n ). But vol n-1 (D ν ∩ S n ) = n vol n (D ν ∩ B n ) = n vol n ((K ν ∩ B n ) (K ∞ ∩ B n )) .
By applying Lemma 5.4 with = B n , one sees that

lim ν→∞ vol n-1 (D ν ∩ S n ) = 0.
Hence, lim ν→∞ a ν = 0 and lim

ν→∞ v K ν (x ν ) = v K ∞ (x ∞ ).
This completes the proof of (34).

Step 4 We show that, for any {x ν } ν∈N as in Step 2, one has

lim ν→∞ ∇v K ν (x ν ) = ∇v K ∞ (x ∞ ).
We start by writing

∇v K ν (x ν )-∇v K ∞ (x ∞ ) ≤ ∇v K ν (x ν )-∇v K ∞ (x ν ) + ∇v K ∞ (x ν )-∇v K ∞ (x ∞ ) . The continuity of ∇v K ∞ : int(K * ∞ ) → R n yields lim ν→∞ ∇v K ∞ (x ν ) -∇v K ∞ (x ∞ ) = 0.
On the other hand, Step 5 We prove a technical inequality relating v K (x) and dist(x, ∂ K * ). To be more precise, we show that One obtains (35) by combining above inequality and the fact that vol n (M) = vol n (ξ(K ) + r (K )B n ) + α -1 x vol n-1 (r (K )B n-1 ) ≥ α -1

n! ∇v K ν (x ν ) -∇v K ∞ (x ν ) = K ν ye -x ν ,y dy - K ∞ ye -x ν ,
v K (x) ≥ vol n-1 (B n-1 ) n! [r (K )] n-1 e -2 x -1 dist(x, ∂ K * ) ( 35
x [r (K )] n-1 vol n-1 (B n-1 ) .

Step 6 Finally, we prove ( 28) and (29). To do this, we work with the sequence {x ν } ν∈N given by x ν := (K * ν ).

(36)

The condition ( 30) is clearly in force. One may assume that x ∞ := lim ν→∞ x ν exists, otherwise one works with a convergent subsequence {x ϕ(ν) } ν∈N and the corresponding subsequence {K ϕ(ν) } ν∈N . Clearly, x ∞ ∈ K * ∞ . We claim that x ∞ ∈ int(K * ∞ ). Suppose, to the contrary, that

x ∞ ∈ ∂ K * ∞ . One has dist(x ν , ∂ K * ν ) ≤ x ν -x ∞ + dist(x ∞ , ∂ K * ν ) ≤ x ν -x ∞ + ζ ν with ζ ν := max x∈S n ∩ ∂ K * ∞ dist(x, ∂ K * ν ).
By exploiting the convergence condition (33) and Lemma 5.6, one sees that lim ν→∞ ζ ν = 0. Hence, lim ν→∞ dist(x ν , ∂ K * ν ) = 0. But, thanks to Step 5, one has

lpv(K ν ) = v K ν (x ν ) ≥ vol n-1 (B n-1 ) n!e 3 [r (K ν )] n-1 dist(x ν , ∂ K * ν )
.

The inradius function r : n → R is known to be continuous. Since lim ν→∞ r (K ν ) = r (K ∞ ) = 0, it follows that lim ν→∞ lpv(K ν ) = ∞, contradicting the result of Step 1. Summarizing, the special sequence (36) satisfies ( 30) and (31). By passing to the limit in the optimality condition

∇v K ν (x ν ) = ∇v K ν (x ν ), x ν x ν , one gets ∇v K ∞ (x ∞ ) = ∇v K ∞ (x ∞ ), x ∞ x ∞ .
This and x ∞ ∈ int(K * ∞ ) imply that x ∞ = (K * ∞ ). We have shown in this way that lim ν→∞ (K * ν ) = (K * ∞ ).

The equality ( 29) is then obtained by exchanging the roles of K ν and K * ν . Finally, observe that

  stands for the classical Pompeiu-Hausdorff distance between a pair C, D of nonempty compact subsets of R n . Convergence with respect to the spherical metric is equivalent to convergence with respect to the ball-truncated metric

  y dy ≤ b ν with b ν := D ν y e -x ν ,y dy.One proves that lim ν→∞ b ν = 0 by using a similar technique as in Step 3. Indeed, vol n-1(D ν ∩ tS n ) dt = n! s n+1 vol n-1 (D ν ∩ S n ).

  ) for all K ∈ n and x ∈ int(K * ). The term dist(x, ∂ K * ) is clearly positive and equal toα x := min u∈K ∩ S n u, x . Let u x ∈ K ∩ S n be such that u x , x = α x . The set M := ξ(K ) + r (K )B n + α -1 x co{0, u x } is contained in K , and max y∈M y, x = ξ(K ), x + r (K ) x + 1 ≤ 2 x + 1. Hence, n! v K (x) ≥ M e -y,x dy ≥ e -2 x -1 vol n (M).

  Proof As shown in(Seeger and Torki 2014, Example 2.5), if K ∈ n is permutation invariant, then S(K ) is equal to the line generated by 1 n . Since R n + is permutation invariant and contains 1 n , one has

	Example 4.4

This completes the proof of the theorem.

The inequality (35) has further consequences. For instance, it can be used to derive the following generalization of Proposition 2.2. A sequence

Uniform solidity is an assumption arising naturally in a number of situations, cf. (Henrion and Seeger 2011, Theorem 3.4).

Proposition 5.8 Let {K ν } ν∈N be a sequence in n satisfying the uniform solidity condition (37). Let {x ν } ν∈N be a bounded sequence in R n such that x ν ∈ K * ν . Then

Proof The "only if" part is a consequence of the inequality

and the boundedness of {btv(K ν )} ν∈N . The "if" part follows from

and the hypothesis (37).

We do not know whether : n → R n is locally Hölderian or not. This difficult question is left open for the time being. What is clear however is that lpv : n → R is not Lipschitzian. The next example illustrates this point.

Example 5.9 Let K = L n and K ν = rev(e n , cos θ ν ) with θ

Hence, lim ν→∞ lpv(K ν )lpv(K ) δ(K ν , K ) = ∞.


Rim Abid

Gwen Salaün

Noel De Palma

Asynchronous Synthesis Techniques for Coordinating Autonomic Managers in the Cloud

Keywords: Asynchronous Coordination, Autonomic Managers, Distributed Cloud Applications, Synthesis Techniques

Cloud computing allows the delivery of on-demand computing resources over the internet on a pay-for-use basis. From a technical point of view, cloud applications usually consist of several software components deployed on remote virtual machines. Managing such applications is a challenging problem because manual administration is no longer realistic for these complex distributed systems. Thus, autonomic computing is a promising solution for monitoring and updating these applications automatically. This is achieved through the automation of administration functions and the use of control loops called autonomic managers. An autonomic manager observes the environment, detects changes, and reconfigures dynamically the application. Multiple autonomic managers can be deployed in the same system and must make consistent decisions. Using them without coordination may lead to inconsistencies and error-prone situations. In this article, we first present a simple language for expressing coordination constraints given a set of autonomic managers. Second, given a coordination expression written with that language, we propose new synthesis techniques for automatically generating an asynchronous controller. These synthesis techniques work in two steps by successively generating a model of the controller and a Java object corresponding to this model. This Java code is finally used for deploying the generated controller. As far as evaluation is concerned, we validated our approach by using it for coordinating real-world cloud applications.

Introduction

Managing complex distributed applications is a challenging problem because manual administration is no longer realistic for complex systems. Autonomic computing is a promising solution for automating the administration functions, which focus particularly on replicating virtual machines, destroying or adding them, and handling virtual machine failures in the cloud. These operations are executed by different autonomic managers considered as control loops. Each manager observes the application execution, ensures a continuous monitoring, and immediately reacts to changes by automatically executing reconfiguration tasks. Several managers can be deployed to supervize the same application and must make consistent decisions. Nonetheless, using them without coordination may lead the system into inconsistencies and error-prone situations (e.g., removing a server that is necessary). As a consequence, the use of multiple managers (e.g., self-repair and self-sizing managers) implemented in the same system requires taking globally consistent decisions. Hence, a manager should be aware of decisions of all managers before reacting.

We present in this article our synthesis techniques for generating a controller, which aims at coordinating several managers. The generated controller prevents every manager from violating global objectives of all the managers. Figure 1 shows an example with two managers (M1 and M2) administrating an application. The right hand part of this figure particularly illustrates the interest of the controller for taking globally consistent decisions (by filtering some event for instance as shown in this example). Our controller synthesis techniques assume that all participants (managers and generated controller) interact using asynchronous communication semantics. This means that all the messages transmitted from/to the managers (controller, resp.) are stored/consumed into/from FIFO buffers. It is worth emphasizing that our approach is twice asynchronous in the sense that it applies on asynchronous systems (no global clock) and it relies on asynchronous communication semantics (communication via buffers).

Let us now present our solution with more details, as depicted in Figure 2, which gives an overview of our approach. We consider as input a set of autonomic managers. Each manager is described using a formal model, namely a Labelled Transition System (LTS). As a first contribution, we define a set of reaction rules and regular expressions to specify the coordination requirements and interaction constraints. This simple language aims at expressing in an abstract way the relationship between the managers and the behaviour we expect from the controller to be generated. Given a set of manager LTSs and the coordination requirements, we propose synthesis techniques for generating an abstract model (LTS) for our controller. To do so, we rely on an encoding of our inputs (LTS models and coordination requirements) into the LNT specification language [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4)[END_REF]. LNT is expressive enough for representing all the inputs and the way they interact together. Moreover, LNT is equipped with a rich toolbox, called CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], that is used for automatically obtaining an LTS model from the LNT specification. The generated LTS corresponds to all possible executions of the controller. It is worth noting that since we rely on formal techniques and tools, all the verification techniques available in the CADP toolbox can be used for validating the generated controller. Once we have synthesized the controller LTS, a Java program is obtained using a code generator we developed. This Java program is necessary to finally deploy and use the synthesized controller for coordinating real applications. In this article, we present a typical example of a N-tier Web application for illustration purposes. We have validated our approach on several variants of this distributed application involving several instances of autonomic managers, such as self-sizing or self-repair managers. Note that our approach covers the whole development process from the expression of the requirements to the final implementation and deployment of our solution.

This article is an extended version of a conference paper published in [START_REF] Abid | Asynchronous Coordination of Stateful Autonomic Managers in the Cloud[END_REF]. The key additions of this journal version are as follows: (i) a more in-depth presentation of the process algebra encoding, (ii) a refined description of the controller LTS and of its generation process, and (iii) the full development of our approach on a real-world case study.

The rest of this article is structured as follows. In Section 2, we introduce our formal model for autonomic managers and the coordination language. In Section 3, we present our synthesis techniques that mainly rely on an encoding into process algebra and on LTS manipulations. Section 4 introduces the code generation techniques for obtaining Java code from controller models. Section 5 illustrates our approach on a multi-tier Web application. We discuss related work in Section 6 and we conclude in Section 7.

Formal Models

In this section, we first introduce the abstract model that we used to represent an autonomic manager. Second, we propose reaction rules and regular expressions for specifying how the involved managers are supposed to interact together through the controller that we want to generate. The models of the managers and the coordination expression are used as input to the synthesis techniques introduced in Section 3.

Autonomic Manager Model

Autonomic managers (also called administration loops) describe the causal ordering of events raised and emitted to the system. Such a behaviour is described using Labelled Transition System (LTS) because this is a simple and graphical model for specifying sequential behaviour, non-deterministic choice, and loops. Each autonomic manager is modelled as an LTS, which consists of a set of states and a set of transitions that connect those states. Formally, an LTS is defined as follows: Definition 1. A Labelled Transition System is a tuple defined as a tuple (Q, A, T, q 0 ) where Q is a finite set of states, A = A ! ∪ A ? is an alphabet partitioned into a set of send and received messages, T ⊆ Q × A × Q is a transition relation, and q 0 ∈ Q is the initial state.

A send message m ∈ A ! is written m! and corresponds to a message destinated to another manager or to the controller. A received message m ∈ A ? is written m? and corresponds to a message to be consumed by the actual manager. A transition relating two states is represented as q l -→ q ∈ T where q, q ∈ Q and l ∈ A. We assume that managers are deterministic, which can be easily obtained using standard determinization algorithms [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF].

Given a set of manager LTSs defined as (Q i , A i , T i , q 0 i ), we assume that each message should have a unique sender and a unique receiver: ∀i, j ∈ 1..n, i = j, A ! i ∩ A ! j = ∅ and A ? i ∩ A ? j = ∅. Furthermore, each message is exchanged between two different managers: A ! i ∩ A ? i = ∅ for all i. The uniqueness of messages can be achieved via renaming.

Coordination Requirements Specification

Our approach aims at generating a controller that acts as an orchestrator for coordinating the execution of the autonomic managers. In the coordinated system, all the messages emitted by the managers are caught by the controller, which can take global decisions for the whole system. In order to describe the behaviour one expects from the controller, we use a simple coordination language, which consists of reaction rules and regular expressions with their basic operators (sequence, choice, and iteration). We define a reaction rule as a set of receive messages followed by a set of send messages. Definition 2. Given a set of managers {M 1 , . . . , M n }, M i = (Q i , A i , T i , q 0 i ), a reaction rule R is defined as a 1 ?, ..., a m ? → b 1 !, ..., b p ! where a j (1 j m) corresponds to a message received from a manager M i (a j ∈ A ! i because this message is emitted by M i ) and b k (1 k p) corresponds to a message emitted to a manager M l (b k ∈ A ? l because this message is received by M l ).

Informal semantics. Such a rule expresses that when the controller receives a set of messages from the managers within a certain period of time, it must send all the messages specified in the second set, once the period is expired. A rule is triggered when the received messages match the exact set of input messages (left part of a rule). If there are two rules with the same left part, this introduces some non-deterministic behaviour in the system. If there is no rule with the set of received messages as left part, no rule is triggered. All the messages involved in those rules are prefixed by the manager identifier for avoiding name clashes. Note that the period is implicit in these rules. The real period will be chosen during the deployment phase.

Example. Let us imagine the following example of reaction rule: m1 msg1?, m2 msg2? → m3 msg3!. This rule indicates that when the controller to be generated receives a message msg1 from manager m1 and a message msg2 from manager m2 within a same period of time, then it reacts by emitting a message msg3 to manager m3. It is worth emphasizing that these messages are reversed in the controller with respect to the managers. As an example message msg1 is a send message (msg1!) in the m1 LTS model whereas this is a receive message in the controller model (msg1?).

In some cases, one may want to specify a specific order of application of those rules. This can be achieved in our coordination language using regular expressions of reaction rules. Thus, the specification of the behaviour one expects from the controller is expressed using a coordination expression C defined as follows: Definition 3. A coordination expression C is a regular expression over reaction rules R:

C ::= R | C 1 .C 2 | C 1 + C 2 | C * where C 1 .C 2 represents a coordination expression C 1 followed by C 2 , C 1 + C 2
represents the choice between C 1 and C 2 , and C * presents a repetition of C zero or several times.

Note that all the participants, namely the autonomic managers and the controller to be generated, communicate asynchronously exchanging messages via FIFO buffers [START_REF] Charron-Bost | Synchronous, Asynchronous, and Causally Ordered Communication[END_REF]. Each participant is equipped with one input buffer. This buffer stores all the messages sent to that participant. Therefore, a participant consumes messages from its buffer and sends messages that are added to the input buffers of the message's recipients. Once the controller is generated (as described in Section 3) and is part of the system, all the managers communicate through it. This means that the controller acts as a centralized orchestrator for the whole system, as shown in Figure 1. Last but not least, we assume reliable communication, that is, messages are guaranteed to reach their destination (no message loss), in the order they were sent. We use the same communication model in all the steps of our approach (synthesis, implementation, deployment) presented in the rest of this article.

Our main motivation for the coordination language we propose in this section was simplicity. This is why we chose message matching and regular expressions. We validated the usability of this formalism by asking engineers with cloud computing background to use our language on real-world examples. The language turned out to be intuitive and simple enough for specifying coordination requirements for those real-world systems.

In the next section, we will show how, from such an abstract specification of the coordination requirements, we automatically generate an abstract model of the corresponding controller.

Asynchronous Synthesis Techniques

In this section, we present new asynchronous controller synthesis techniques, which rely on an encoding of our models (aut format1 ) and coordination requirements into the LNT specification language. From this LNT specification, we can generate the corresponding LTS model of the controller using CADP compilers, hiding, and reduction techniques. We also use CADP verification tools to validate the generated controller. All the steps presented in this section are fully automated using a tool that we developed in Python. This tool generates the LNT code as well as SVL scripts that are used for invoking CADP exploration and reduction tools, which finally results in the generation of the controller LTS.

Process Algebra Encoding

We present successively in this section the encoding into LNT of the different parts of our system, i.e., autonomic managers, coordination requirements, and architecture. We chose LNT for several reasons. First, LNT is an expressive behavioural specification language with user-friendly syntax and operational semantics. Second, LNT is supported by CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], a toolbox that provides optimized state space exploration techniques and verification tools. CADP tools allow us to compile the LNT specification into an LTS, which represents all the possible executions of the corresponding specification.

The behavioural part of the LNT specification language consists of the following constructs: action with input/output parameters, assignment (:=), sequential composition (;), conditional structure (if), loop (loop), parallel composition (par), non-deterministic choice (select), and empty statement (null). Each process defines an alphabet of actions, a list of typed parameters, and a behaviour built using the aforementioned operators. Communication is carried out by rendezvous on actions with bidirectional transmission of multiple values. The parallel composition explicitly declares the set of actions on which processes must synchronize. If the processes evolve independently from one another (interleaving), this set is empty. For details about the LNT syntax and semantics, the reader may refer to [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4)[END_REF].

Autonomic manager encoding. An LNT process is generated for each state in the manager LTS. Each process is named using the identifier of the corresponding state. The alphabet of the process consists of the set of send and receive messages appearing on the LTS transitions. The behaviour of the process encodes all the transitions of the LTS going out from the corresponding state and if necessary calls the processes encoding the target states of those transitions. If there is no such transition, the body of the process is the null statement. If there is a single transition, the body of the process corresponds to the message labelling this transition, followed by a call to the process encoding the target state of the transition. Finally, if there is more than one transition, we use the select operator, which corresponds to a non-deterministic choice between several possible behaviours (similarly to '+' or '[]' in the CCS [START_REF] Milner | Communication and concurrency[END_REF] and CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF] process algebras, resp.). Let us assume that two transitions q l -→ q', q l -→ q'' ∈ T have the same source state q. The behaviour of the process encoding q in LNT is:

select l; q' [...] [] l'; q''[...] end select
where select encodes a choice between l and l', and q' and q'' are two processes encoding the behaviour of both target states.

Since a message name can be used in different autonomic manager LTSs, each message is prefixed with the manager name to avoid further name clashes. We encode emitted messages (received messages, resp.) with a EM ( REC, resp.) suffix. These suffixes are necessary because LNT symbols ! and ? are used for the data transfer only. As an example, m1 ∈ A ! is encoded as m1 EM, and m2 ∈ A ? is encoded as m2 REC. Figure 3 shows the LTS model of a manager example, as well as the encoding of its initial state P0 into the LNT process algebra. We observe that the process name is the same as the identifier of that state, whereas the process alphabet is composed of all the messages appearing in the LTS, prefixed with the name of the manager (M1) and suffixed by EM in the case of a send message and by REC in the case of a receive message. As far as process alphabets are concerned, they consist of all messages appearing in the LTS because, for each state there is a call to the target state. This means that from any state you need in the alphabet all messages reachable from that state, and since in most cases managers are encoded as looping behaviours, we need to have all messages in the alphabet of each process.

Coordination requirements encoding. The coordination requirements specified using reaction rules and regular expressions give an abstract view of the controller to be generated. These requirements are encoded into an LNT process called coordination. The process alphabet is composed of all the messages exchanged between the controller and the involved managers, that is, all the messages appearing in the reaction rules. The body of this process encodes the regular expression of reaction rules. Each reaction rule is translated to LNT separating both sides of the rule (i.e., left hand part and right hand part) using the LNT sequential composition (;). In order to make explicit in the controller LTS the logical interval of time that will be chosen at the implementation step and during which the controller receives messages, the left hand part of the reaction rule starts with an action TBEGIN and ends with an action TEND. Those time delimiters are used by the controller to give the pace at which the coordinator reacts. The left hand part of the rule (inside TBEGIN and TEND) is translated using the par operator without synchronization (pure interleaving) since all the messages can be received in any order (see Fig. 4). After the execution of the TEND action, the right hand part of the reaction rule is translated using the sequential composition to avoid unnecessary interleavings of actions, which would result in larger LTSs.

As far as the regular expression is concerned, a sequence (.) of rules is encoded using the sequential composition (;) and a choice (+) between several rules is translated using the select construct. An iteration ( * ) is encoded using the loop operator as follows, where "..." stands for the translation of the expression on which the operator "*" applies:

loop L1 in select break L1 [] ... end select end loop
Architecture encoding. In this section, we present how all the participants, i.e., managers and coordination expression, are composed altogether. The communication between them is achieved asynchronously. The coordination expression represents an abstract description of the future controller that we aim to generate, and all the messages must go through this controller, which acts as a centralized orchestrator. Each participant is equipped with an input FIFO buffer. When a participant wants to read a message, it consumes the oldest message from its buffer. When it sends a message to another participant, the message is stored in the input buffer of that participant. LNT functions are used to describe basic operations on these buffers (e.g., addition and retrieval of messages). We present below, an example of function that removes a message from a FIFO buffer (i.e., from the beginning). The function takes as input a buffer (q) of type TBuffer, which consists of a list of messages (TMessage). If the buffer is empty, nothing happens. If it is not empty, the first message is removed.

It is worth noting that our synthesis techniques allow one to choose buffer bounds. One can either decide to fix an arbitrary bound for buffers or to use unbounded buffers. In the first case, the only constraint is that the same buffer bound should be used when deploying the controller. Otherwise if at some point it must be changed (e.g., after a modification in memory requirements), unexpected behaviours and erroneous situations may occur. In the second case (unbounded buffers), the risk is to attempt to generate a controller whose corresponding state space is infinite [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. As an intermediate solution, one can use the recent results presented in [START_REF] Akroun | Automated Analysis of Asynchronously Communicating Systems[END_REF] for identifying whether the interactions between managers with unbounded buffers can be mimicked with bounded buffers. If this is the case, the lower bound returned by these techniques should be used as the minimum buffer bound for both our synthesis techniques and the deployment of the application.

We remind that parallel composition in LNT is described using the par construct. This operator consists of a set of messages (m i below) on which processes (p j ) in parallel must synchronize:

par m 1 , ..., m n in p 1 [...] || ... || p k [...] end par
A buffer in LNT is first encoded using an LNT list and classic operations on it. Then, for the behavioural part, a buffer is encoded using a process with a buffer data type as parameter. This process can receive messages from the other participants, and synchronizes with its own participant when that one wants to read a message. We generate a process encoding each couple (participant, buffer ) that corresponds to a parallel composition (par) of the participant with its buffer. The synchronization set contains messages consumed by the participant from its buffer.

Finally, the whole system (main process in LNT, see below) consists of the parallel composition of the couple (coordination, buffer ) with all the couples (manager i , buffer i ) generated for all the managers. Note that since autonomic managers communicate via the controller, they evolve independently one from another and are therefore composed using the par operator without synchronizations. In contrast, the couple (coordination, buffer ) must synchronize with all the other couples on all send messages from the managers/to the buffers, and this is made explicit in the corresponding synchronization set of this parallel composition (message p , .., message k ).

Controller Generation and Verification

Generation of the controller LTS. The controller model is an LTS consisting of messages to be consumed from its buffer and messages to be sent to the other participants. The controller LTS also keeps track of the messages received by its own local buffer. This information is useful in some specific cases (non-determinism for instance) in which the controller can execute different actions and, depending on the buffer content, it will decide what behaviour must be executed. By looking at the buffer content, the controller can make the right decision and avoid engaging in a branch that may lead to an erroneous execution of the whole system (impossibility to read some action for example). Definition 4. A controller LTS is a tuple (S, s 0 , Σ, T ) where: S is a set of states, s 0 ∈ S is the initial state, Σ = Σ ! ∪ Σ ? ∪ Σ B is a finite alphabet partitioned into a set Σ ! (Σ ? , resp.) of send (receive, resp.) messages and a set of messages received by its buffer Σ B , and T ⊆ S × Σ × S is the transition function.

Once all the inputs (models and coordination requirements) are encoded into LNT, we can use compilers available in the CADP tools to obtain the controller LTS corresponding to all behaviours of the LNT specification. More precisely, we preserve local send/receive messages from the coordination expression point of view (messages shown in the dashed grey rectangle in Fig. 5) and the receive messages from all the managers. To do so, we hide all message exchanges corresponding to consumptions of the managers from their buffers. All these messages are replaced by internal actions τ . Then, we use the reduction techniques available in CADP for getting rid of internal actions, removing duplicated paths, and determinizing the final LTS. The reductions can be achieved using on-the-fly techniques modulo: (1) strong equivalence for replacing duplicated sequences of transitions by a single sequence and (2) weak trace equivalence for determinizing the generated LTS.

Verification of the generated controller. Since the writing of the coordination expression is achieved manually by a designer, this step of our approach may lead to an error-prone controller. Indeed, the designer can provide a wrong specification of the coordination requirements, which does not satisfy the global objectives of all the managers. However, we can take advantage of the encoding into LNT to analyze and validate either the controller LTS alone (and thus the coordination expression) or the LTS corresponding to the final system (i.e., the composition of all the participants). To do so, one can use the CADP model checker (Evaluator), which takes as input an LTS model and temporal properties specified in MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF]. We distinguish two types of properties:

1. properties which depend on the application, e.g., the controller must eventually transmit a specific message to a certain manager;

2. properties which do not depend on the application, e.g., checking the absence of deadlock.

We would like to recall that actions TBEGIN and TEND are parts of both the controller LTS and of the LTS corresponding to the whole system. Therefore, one can also verify properties using those specific actions. For instance, one can formalize in the MCL logic properties such as "there is never two actions A and B in sequence without an action TEND in-between" or "an action C is always systematically followed by an action TEND". Those kinds of properties are useful if the designer wants to check that some situation will never occur (safety properties) or will eventually occur (liveness properties).

Another source of error may occur when one action appears unexpectedly between TBEGIN and TEND. In that case, no reaction rule would match the exact set of events, resulting in a deadlocking behaviour. This erroneous case can be detected using verification techniques by checking for the presence of deadlock in the controller LTS. Once detected, the solution for solving this problem is to add a reaction rule to the coordination expression for handling this specific case.

Java Code Generation and Deployment

We present in this section our techniques for automatically generating the Java code, which corresponds to the controller LTS obtained during the synthesis phase (see Section 3.2). This Java code is generated without human intervention and allows one to deploy controllers in the context of real-world applications as we will show in Section 5.

Java Code

Our Java code generation techniques are based on the use of objectoriented programming. They take as input the controller LTS synthesized beforehand and automatically generate all Java classes, methods, and types necessary for deploying it. The controller LTS is encoded as an instance of a Java class LTS. This class relies on two classes, namely a class State and a class Transition representing the transitions between the states. The LTS class also defines an attribute cstate representing the current active state in the controller model. This variable is initialized with the LTS initial state. Some additional Java code is necessary to interface the controller with the running application. We particularly define a method called react that takes as input a list of messages received within a period of time and triggers successive moves in the controller according to the current state of the controller and to the received messages. This method computes the messages that the controller has to send as a reaction to these received messages and updates the current state of the controller.

Deployment

Our generated Java code can be deployed and applied on concrete applications using the event-based programming paradigm. The period of time described using special actions TBEGIN and TEND in the controller LTS has to be instantiated with a real value. The choice of this period cannot be made during the synthesis phase and is achieved just before deployment. This period is computed using sampling techniques and implemented using the sleep method in the LTS class introduced previously. By sampling techniques, we mean simulation and empirical study in order to determine the best period of time with respect to the application being monitored. The choice of this period mainly depends on the occurrence rate of events raised by the system. The goal of this step is to find the best trade-off between stability and reactivity. To put it another way, the more unstable the system is, the shortest the period of time should be. If two events appear one after the other very closely but on two periods of time whereas we would like to catch them on a same period, we will miss the problem and eventually add then remove an unnecessary server for instance. However, these boundary cases do not occur frequently if the period is chosen as explained above and for those cases our approach converges quickly to a stable situation. Convergence is ensured if the coordination expression also takes the original automomic manager behaviours into account, that is, allows the managers to behave as originally designed without coordination. In that case, the system will work, not optimally from a reconfiguration point of view (possible addition of unnecessary servers for instance), but it will make the required modification imposed by the (uncoordinated) managers.

The main behaviour of the controller (run method) consists of an infinite reactive loop, which successively receives events from the application and computes reactions (messages to be sent by the controller). The result produced by each call of the run method (i.e., controller reactions) has to be interpreted and executed. Therefore, all the messages returned by that method are encoded as events too. A part of the Java program is dedicated to handling the events raised by the application by converting them into the input format of the react method, and conversely handling the output of the react method by translating it into a list of events executed by the system. Each event contains the corresponding message and additional information, for instance, a failure event also has as parameter the impacted server and further information (identifier, port, etc.). Therefore, all the messages received/emitted by the generated controller are related to the corresponding events. As far as asynchronous communication is concerned, different existing software can be used, such as RabbitMQ, which is a classic industrial solution for implementing message queuing interactions.

A Multi-tier Application Supervised by Autonomic Managers

We introduce in this section a JEE multi-tier application supervised by two sorts of autonomic managers, namely a self-repair and a self-sizing manager. We illustrate our approach on this example, by presenting successively the application, the coordination requirements, the encoding into LNT, the controller model generation, and the final deployment of the controller.

Multi-Tier Application

The JEE multi-tier application (Fig. 6) consists of an Apache Web server, a set of replicated Tomcat servers, a MySQL proxy server, and a set of replicated MySQL databases. The Apache server receives incoming requests and distributes them to the replicated Tomcat servers. The Tomcat servers access the database through the MySQL proxy server that distributes the SQL queries to a tier of replicated MySQL databases fairly.

The Managers Role

The dynamic sizing plays an important role in the load balancing and energy consumption of the replicated servers on this type of application. When starting the application, it is difficult to predict the number of requests and to estimate the number of required servers. Therefore, adjusting dynamically the number of replicated servers according to the number of requests is necessary. Moreover, once a server fails, the failure must be immediately detected and repaired in order to preserve the application consistency. Managers are used to optimize the load balancing and preserve the application consistency. To sum up, a self-sizing manager handles the dynamic sizing of the application and a self-repair manager is in charge of detecting failures and repairing them.

Figure 7 shows how the architecture of the managers is based on the MAPE-K model (Monitor Analyse Plan Execute -Knowledge). For instance, the self-sizing manager continuously observes a load of replicated servers through the Monitor function. It computes the average of the load and detects the presence of an overload or an underload through the Analyze function. Once an overload (underload, resp.) is detected, the manager makes a decision about the addition or removal of a server through the Plan function. This decision is executed by the Execute function.

The Managers Models

We describe the managers behaviours using several LTS models. First, we model the behaviour of the Monitor, Analyse, and Execute functions of the managers by what we call the application manager (Fig. 8, right), which sends messages when a change occurs in the system and receives messages indicating actual administrative changes to perform on the application. As for the Plan functions, we use two models called self-sizing and self-repair managers, resp. The generated controller aims at coordinating the messages transmitted from the Analyze function to the Plan function and from the Plan function to the Execute function.

The self-sizing manager. The self-sizing is in charge of adapting the number of replicated servers dynamically by sending the message add! (remove!, resp.) to the system when detecting an overload (underload, ). The overload (underload, resp.) is detected when the average of the load exceeds (is under, resp.) a maximum (minimum, resp.) threshold (Fig. 8,middle). We associate one instance of the self-sizing manager to the Tomcat servers and another instance to the MySQL databases. We distinguish these two instances of the same manager as follows: both models have the same states and transitions as the LTS shown in Figure 8 (middle), but suffixed by tc ( mq, resp.) when the instance is associated with the Tomcat servers (MySQL databases, resp.).

The self-repair manager. The self-repair manager detects failures and requires the creation of new instances of the failed servers (Fig. 8, left). We have four instances of the self-repair manager, one per tier. Therefore, we consider here that we have four managers. All the models have the same states and transitions as the LTS shown in Figure 8 (left), but suffixed by ap ( tc, pq, mq, resp.) when the instance is associated to the Apache server (Tomcat servers, MySQL proxy server, MySQL databases, resp.).

Coordination Problems

The absence of coordination between these managers may lead the whole system to some undesired situation such as adding two new servers whereas one was enough or removing a server that is needed as a result of a server failure. We distinguish two types of problems: those occurring in the same tier (i.e., the replicated servers) and those occurring in different tiers.

Coordination problems in the same tier. A failure of a server in a set of replicated servers triggers an overload of the remaining servers. When the self-repair manager receives a message indicating the detection of this failure, it sends a message to the application manager requesting it to repair the failure by creating a new replica. Before completion of this repair phase, the other replicated servers receive more requests than before the failure, which causes an overload. Upon reception of this overload detection from the application manager, the self-sizing manager sends a message back asking the addition of another server. In this scenario, as a result of a server failure, two new servers are added to the application whereas one was enough.

Coordination problems in different tiers. A failure of a server, which is hosted on the first tier and connected to other servers hosted on another tier, triggers an underload in the second tier. When the self-repair manager receives a message indicating the detection of this failure, it sends a message to the application manager requesting it to repair the failure by creating a new replica. Before completion of this reparation, the servers hosted on the second tier receive fewer requests than before the failure, which causes an underload. Upon reception of this underload detection from the application manager, the self-sizing manager sends a message back calling for the removal of a server. Then, once the failed server is repaired, the servers hosted on the second tier receive more requests than before the reparation, which causes an overload and therefore the addition of another server by the self-sizing manager. Therefore two unnecessary reconfiguration operations (removal and addition of a server) are executed as a result of a server failure in that example.

Managers Coordination

We present below an excerpt of the requirements for the controller we want to generate for our example. These rules ensure that all the managers globally satisfy the coordination objectives. Each line presents the actions that can be received by the controller in a period T (left parts of reactions rules). At the end of each period, if the received messages match the left part of one fireable rule, it reacts by emitting the messages appearing in the right part of that rule. All the messages are prefixed by the manager name (app stands for the application manager) and suffixed by the name of the tier to which is associated the manager.

( app_failure_ap? -> repair_failure_ap! () + app_failure_tc? -> repair_failure_tc! () + app_overload_tc? -> sizing_overload_tc! () + app_underload_tc? -> sizing_underload_tc! () + app_failure_mysql? -> repair_failure_mysql! () + app_failure_px?
-> repair_failure_px! () + app_failure_ap?, app_underload_tc? -> repair_failure_ap! () + app_failure_tc?, app_overload_tc? -> repair_failure_tc! () + ... ) * tier of the Tomcat servers. This manager synchronizes with its buffer on the repair failure tc REC message, which is emitted by the buffer and received by the manager. Note that the buffer process (buffer repair tc) is equipped with a parameter corresponding to the buffer data type, that is, the structure where messages are stored, initialized to nil. After generating all the couples (autonomic manager/buffer, application manager/buffer, and controller/buffer), the main process is encoded using parallel compositions. The managers do not interact directly together. Therefore, the couples (manager, buffer) are translated using the par construct without synchronization (pure interleaving). All the managers communicate together through the controller. These interactions are expressed using another parallel composition where the synchronization set makes explicit all the messages sent by the managers to the controller buffer, or sent by the controller to the managers buffers.

process

Controller Generation and Verification

CADP compilers take as input the specification corresponding to the LNT encoding and compute as output the corresponding LTS describing the whole system for our example. Then, we apply hiding and minimization techniques on that LTS to generate the LTS corresponding to the controller. The final controller LTS consists of 28,992,305 states and 46,761,782 transitions. An excerpt of the controller LTS, which focuses on the failure and overload detection of a Tomcat server in the same period of time, is shown in Figure 9. We recall that we use specific labels (namely TBEGIN and TEND) for characterizing the messages received during a same period of time. This LTS shows that when the controller receives a failure and an overload message (of a Tomcat server in this example) during a same period, it forwards only the failure message and drops the overload message. In contrast, when the controller receives these two messages in two different periods, it forwards them to the repair and sizing manager, resp.

We use the Evaluator model checker to verify temporal properties expressed in the MCL logic. For illustration purposes, we present two examples of liveness properties. The first one is checked on the controller LTS and the second one holds on the LTS of the whole system:

• The reception of a failure message by the controller is eventually followed by the sending of a repair message to the application manager in order to request it to repair the Tomcat server • The emission of an overload message by the application manager is eventually followed by an emission of a reparation or addition message by the controller, but not both messages

[true* .app_overload_tc_EM] inev (app_repair_tc_EM xor app_add_tc_EM)
This property shows that the overload message is always handled, either by the repair manager when both Tomcat failure and overload occur within a same period of time, or by the sizing manager.

Both properties use the macro inev (M), which is used especially when specifying liveness properties that are inevitability assertions. Inevitability assertions can be expressed using fixed point operators that indicate that a transition labelled with M eventually occurs. The inev macro is defined as follows:

macro inev (M) = mu X .( < true > true and [ not (M) ] X ) end macro

Our approach was applied for validation purposes on many illustrative examples of our dataset (managers and coordination requirements). Table 1 summarizes some of our experiments. Each managed application used as input is characterized using the number of managers and the coordination requirements. We give the size of the LTS (states/transitions) of the whole Let us now shortly comment on the results presented in Table 1. First of all, when using acyclic managers (see, e.g., the 3 rd example in Table 1), the size of the generated controller LTSs and the time required for computing those LTSs are very small. In contrast, we observe that these numbers grow importantly for other examples (gray lines). In those cases, the increase in LTS size and computation time is due to the presence of looping behaviours in manager models (as those presented in Figure 7). Since we rely on enumerative techniques for generating LTSs, looping behaviours induce more possible combinations of correct executions, resulting in larger LTSs than for acyclic models. We also see that LTS sizes and generation times increase with the number of managers in parallel (see, e.g., the last line of Table 1).

Deploying and Running the Generated Controller

In this section, we present some experiments we performed when deploying and running our controller for the multi-tier application introduced previously (see Fig 6). To do so, we use a virtualized experimental platform based on Openstack2 , which consists of six physical machines on which we instantiate virtual machines with 1 vCPU, 2GB of memory and 8GB of disk.

The JEE multi-tier application is initially configured and deployed with a server at each tier, i.e., an Apache Web server, a Tomcat server, a MySQL proxy, and a MySQL database. The initial deployment phase is automated using a dynamic management protocol allowing us to connect and start the involved servers and database in the right order [START_REF] Abid | Verification of a Dynamic Management Protocol for Cloud Applications[END_REF]. In a second step, we use the Apache JMeter application to inject increasing load on the Apache server and thus to simulate the clients that send HTTP requests on the managed system. Once we have at least two active Tomcat servers and two MySQL databases, we start simulating failures using a failure injector. When we start injecting failures, we stop augmenting the workload on the Apache server and keep the same load for the rest of the execution. The failure injector is flexible and can be used for affecting any active server (Apache, Tomcat, MySQL, etc.), any number of times (single failure or multiple failures of the same or of different servers), and at any time (same period of time, different periods of time, etc.). We conducted our experiments on applications with or without controller. We have considered various scenarios with failures of the Apache server and of the MySQL proxy as well as failures/load variation of the Tomcat servers and of the MySQL databases. We made long-running experiments for validation of our approach where we ran the application for hours with random injection of failures.

Figure 10 shows an excerpt of the system behaviour after 500 minutes since the application deployment. We observe that, at this moment, the application is composed of five Tomcat servers and three MySQL databases. Figure 10 presents several cases of failure injection. As an example, at minute 508, a failure of a replicated MySQL database causes a workload increase on the other replicated servers. These two actions happen in the same period, and the controller forwards only the failure detection to the repair manager. Accordingly, a single MySQL is added by the repair manager and the workload returns at once to its average value.

We made several experiments in which we varied the number of failures, the Apache load, and the minimum/maximum thresholds of the Tomcat servers and of the MySQL databases. In all these cases, we observe that the controller succeeds in detecting and correcting the problems while avoiding undesired reconfiguration operations, that is, the unnecessary addition/removal of servers/databases. Figure 11 shows experimental results obtained with different numbers of failures. For instance, we see that when injecting 14 failures to our running application, the controller applies 18 reconfiguration operations on the system, i.e., 18 addition or removal of The results presented in Figure 11 were obtained by running one simulation for each number of failures (3, 6, 10, 14, etc.). This figure shows that the number of reconfiguration operations decreases importantly by using our controller-based solution. Without coordination, the number of reconfigurations is at least twice larger. However, in the coordinated case, the number of unnecessary reconfiguration operations is not completely removed and is therefore not optimal. Indeed, there are situations when there are several failures in a row or when messages arrive on two periods of time as discussed in Section 4. In those cases we cannot avoid unnecessary reconfiguration operations and this explains the variation in our results for instance between 30 failures (about 30 reconfiguration operations in the coordinated case) and 50 failures (about 70 reconfiguration operations in the coordinated case).

Related Work

Controller synthesis techniques. Controller synthesis for discrete event systems was originally introduced by Ramadge and Wonham [START_REF] Wonham | On the Supremal Controllable Sublanguage of a Given Language[END_REF][START_REF] Ramadge | The Control of Discrete Event Systems[END_REF]. In [START_REF] Wonham | On the Supremal Controllable Sublanguage of a Given Language[END_REF], the authors present a controllable language as a solution for the supervisory of hybrid control systems. This solution generates controllers from a given system called plant and designed as a finite automaton. [START_REF] Ramadge | The Control of Discrete Event Systems[END_REF] proposes a supervisor synthesis algorithm for automatically generating a controller from a plant modelled as a finite automaton and properties to be ensured by the controller. The generated controller permits all possible legal executions. This synthesis approach is based on a classical two-person game approach. These approaches can be characterized as restrictive because they directly influence and impact the controlled system.

In [START_REF] Delaval | Contracts for Modular Discrete Controller Synthesis[END_REF], the authors introduce an approach based on contract enforcement and abstraction of components to apply a modular discrete controller synthesis on synchronous programs. These programs are presented by Synchronous Symbolic Transition Systems. The authors integrate this approach in a high-level programming language combining data-flow and automata. Another decentralized supervisory control approach for synchronous reactive systems is presented in [START_REF] Belhaj Seboui | An Approach for The Synthesis of Decentralised Supervisors for Distributed Adaptive Systems[END_REF]. This work is based on finite state machines and computes local controllers that act on the subsystems to ensure a global property. The local controllers are automatically generated and this approach was applied to several examples for validation purposes. This approach allows decentralized control whereas we generate a centralized controller. Moreover, they rely on synchronous systems and synchronous communication semantics, whereas we assume asynchronous systems and communication, meaning that the controllability hypothesis is impossible in our context.

Coordination of autonomic managers. In [START_REF] De Oliveira | Synchronization of Multiple Autonomic Control Loops: Application to Cloud Computing[END_REF], the authors propose a generic integration model that focuses, first, on categorizing all autonomic loops in terms of reciprocal interference. This generic model can be used to manage the synchronization and coordination of multiple control loops, and it was applied to a scenario in the context of cloud computing and evaluated under simulation-based experiments. This paper does not provide any synthesis techniques for coordinating the multiple loops, and coordination is achieved in a rather manual way.

[24] presents a framework for the coordination of multiple autonomic managers in the cloud computing context. Managers are classified in two categories: application-related and infrastructure-related managers. These works use a protocol based on synchronous mechanisms and inter-manager events and actions along with synchronization mechanisms for coordinating these managers. The main difference compared to our work is that this paper focuses on quality of service whereas we provide controller generation techniques considering behavioural and functional aspects of the system execution.

Other recent works [START_REF] Delaval | Modular Coordination of Multiple Autonomic Managers[END_REF][START_REF] Gueye | Coordinating Multiple Administration Loops Using Discrete Control[END_REF][START_REF] Gueye | Discrete Control for the Coordination of Administration Loops[END_REF] propose some techniques based on synchronous discrete controller synthesis for coordinating autonomic managers, such as self-repair and self-sizing managers. The communication between the generated controller and the managers is synchronous and uses a synchronous language BZR, which cannot impose a specific order between requirements and contains multiple and complicated operations. This approach uses a background in synchronous systems and languages, whereas we focus on asynchronous systems and assume that communication is achieved asynchronously. Our approach is thus tailored for these hypotheses.

Configuration of cloud applications. [START_REF] Di Cosmo | Aeolus: A Component Model for the Cloud[END_REF] presents the Aeolus component model and explains how some activities, such as deployment, reconfiguration, and management phases of complex cloud applications, can be automated in this model. Aeolus takes as inputs high-level application designs, user needs, and constraints (e.g., the number of required ports that can be bound to a client port) to provide valid configuration environments. This work presents some similarities with ours, but does not propose solutions for verifying that the constraints are satisfied in the target configurations. Beyond Aeolus, other frameworks have attempted to provide deployment and reconfiguration algorithms for distributed cloud applications, see, e.g., [START_REF] Krause | Modeling Dynamic Reconfigurations in Reo Using High-Level Replacement Systems[END_REF][START_REF] Fischer | Engage: A Deployment Management System[END_REF][START_REF] Etchevers | Reliable Self-deployment of Cloud Applications[END_REF][START_REF] Durán | Robust and Reliable Reconfiguration of Cloud Applications[END_REF].

In [START_REF] Brogi | Modelling the Behaviour of Management Operations in Cloud-based Applications[END_REF], the authors present an extension of TOSCA (OASIS Topology and Orchestration Specification for Cloud Applications) in order to model the behaviour of component's management operations. More precisely, they specify the order in which the management operations of an instantiated component must be executed. In this work, the authors explain how management protocols are described as finite state machines, where the states and transitions are associated with a set of conditions on the requirements and capabilities of the components.

Coordination of component-based systems. In [START_REF] Parashar | AutoMate: Enabling Autonomic Applications on the Grid[END_REF], the authors introduce AutoMate, a framework for coordinating multiple autonomic components hosted on Grid applications, using high-level rules for their dynamic composition. The rules are executed using a decentralized deductive engine, called RUDDER, and composed of distributed specialized agents. RUDDER deploys the rules and coordinates their execution. It assigns priorities to these rules in order to resolve conflicting decisions between them. However, it uses a manual administration to evaluate and update the interaction rules.

[4] presents an approach relying on the GCM/ProActive execution environment, where applications are composed of distributed components communicating by asynchronous requests with futures. The components take adaptation decisions and evolve in an autonomic way employing features designed to describe their behaviours. This approach relies on loosely coupled components, which communicate asynchronously by message sending and share references for the futures. The two main differences between this work and ours is in the communication model and in the way control/reconfiguration is implemented ( [START_REF] Baude | Programming Distributed and Adaptable Autonomous Components -The GCM/ProActive Framework[END_REF] relies on the notion of membrane to do so).

Conclusion

We have focused in this article on the coordination of several autonomic managers in the context of cloud applications. We have proposed in this article new asynchronous synthesis techniques for generating a controller allowing the monitoring and orchestration of such autonomic managers. These techniques take as input a set of abstract behavioural models for the managers as well as the coordination requirements described as reaction rules. Then, the synthesis process works in two successive steps. We first generate a controller model using as intermediate step a process algebra encoding. Second, we rely on Java code generation techniques for deploying the generated controller in order to coordinate real-world applications. The generated and deployed controller interacts asynchronously with the managers via FIFO buffers and allows them to take globally coherent decisions.

This article shows how the approach covers the whole development process from an expression of the requirements to the final implementation and deployment of the synthesized controller, which helps to coordinate at runtime real-world applications. In addition, these synthesis techniques can be used to control other applications where components are modelled as LTSs and communicate asynchronously. This is the case in application areas such as Web services, multi-agent systems, or hardware protocols.

As far as future is concerned, we plan first to extend our coordination language in order to specify concurrent flows (e.g., by means of fork/join operators), which are quite common in orchestration and distributed coordination. Furthermore, our coordination expressions cannot describe specific requirements (e.g., elastic behaviours with oscillations or cool-down periods). Expressing this type of needs requires the extension of our coordination language and LTS models with data-awareness and real-time constraints. The addition of such numerical values and constraints may, however, result in larger state spaces, especially when addressing more complicated applications with an important number of managers. To tackle the state space explosion problem and to be able to handle larger systems, we plan to integrate alternative generation and model checking techniques, such as symbolic approaches with OBDDs and partial order reductions [START_REF] Clarke | Model Checking and the State Explosion Problem[END_REF]. Another idea to reduce the size of the generated controller is to adopt a distributed coordination solution (divide and conquer). The main advantage of this distribution is that every controller is much smaller in terms of states and transitions compared to a unique centralized controller. This generation is however not that easy be-cause those distributed controllers need to interact together at certain points in time in order to apply the coordination requirements in a consistent way from a global point of view. We plan to add these synchronization points at the process algebra encoding level.

Figure 1 :

 1 Figure 1: Administration tasks without or with coordination

Figure 2 :

 2 Figure 2: Overview of our approach

Figure 3 :

 3 Figure 3: Example of a manager modelled as an LTS (left), and the LNT process encoding the initial state (right)

Figure 4 :

 4 Figure 4: Example of coordination requirements encoded into an LNT process

Figure 5 :

 5 Figure 5: Exchange of messages between the coordination expression and the managers

Figure 6 :

 6 Figure 6: A multi-tier application

Figure 7 :

 7 Figure 7: Architecture of the self-sizing (left) and of the self-repair (right) manager

Figure 8 :

 8 Figure 8: (left) Self-repair manager LTS, (middle) Self-sizing manager LTS, (right) Application manager LTS

Figure 9 :

 9 Figure 9: Excerpt of the controller LTS for the example

Figure 10 :

 10 Figure 10: Tomcat and MySQL failure/overload in a coordinated environment

Figure 11 :

 11 Figure 11: Number of reconfiguration operations with/without coordination and number of undesired operations avoided by coordination

  process main [message 1 :any, ..., message n :any] is par message p , ..., message k in

	couple_buffer_coordination [...]
	||
	par
	couple_buffer_manager 1 [...]
	|| ... ||
	couple_buffer_manager n [...]
	end par
	end par
	end process

  couple buffer repair tc [repair failure tc REC: any, repair repairing tc EM: any, repair failure tc EM: any] is par repair failure tc REC is R0 tc [repair failure tc REC, repair repairing tc EM] || buffer repair tc [repair failure tc EM, ...] (nil)

	end par
	end process

Table 1 :

 1 Experimental results: LTSs size and synthesis time system as well as the controller LTS obtained after minimization (wrt. strong and weak trace relations). The last column gives the overall time to synthesize the controller.

	|Managers|	Whole system LTS	Controller LTS	Time
		|states|	|transitions| |states| |transitions|	(m:s)
	2	2,424	12,518	1,124	5,140	0:10
	3	103,725	365,845	9,744	31,636	2:39
	4	145	267	38	44	0:06
	5	10,063,873 39,117,110	85,297	621,482	389:65
	6	1,900	4,945	186	285	0:08
	10	300,000	1,686,450	1,786	3,471	6:54

The aut format is the textual format used to represent automata in the CADP toolbox, see http://cadp.inria.fr/man/aut.html

https://www.openstack.org/

We distinguish two kinds of rules:

1. those where a unique message appears in the left part of the reaction rule (see, e.g., , ). In that case, the corresponding controller transfers that message to the manager;

2. those encoding the coordination we want to impose on managers, e.g., rule permits to generate a controller that can avoid to add two Tomcat servers by forwarding only one of the two received messages on a same period of time.

Last, since there is no specific order between all these rules, we use a simple regular expression where all the rules can be fired at any time (combination of + and * operators).

Encoding into LNT

Let us first show some excerpts of LNT obtained when calling our LNT code generator on this example. We first show the LNT processes encoding an instance of the repair manager, which handles the tier of the Tomcat servers. The first process has the same name as the initial state identifier R0 tc. The process alphabet is the set of labels used in this manager LTS (repair failure tc REC and repair repairing tc EM). Each message is prefixed with the manager name. The body of the first process, for instance, consists of a failure receive message (repair Failure tc REC) followed by a call to the process encoding the target state, that is, R1 tc. We show now an example of process encoding a couple (manager, buffer), particularly the couple corresponding to the repair manager handling the