Roberto Di Cosmo
email: roberto@dicosmo.org

Jacopo Mauro
email: jmauro@cs.unibo.it

Stefano Zacchiroli

Gianluigi Zavattaro
email: zavattar@cs.unibo.it

Component reconfiguration in the presence of conflicts Technical report of the Aeolus project

Components are traditionally modeled as black-boxes equipped with interfaces that indicate provided/required ports and, often, also conflicts with other components that cannot coexist with them. In modern tools for automatic system management, components become grey-boxes that show relevant internal states and the possible actions that can be acted on the components to change such state during the deployment and reconfiguration phases. However, state-ofthe-art tools in this field do not support a systematic management of conflicts. In this paper we investigate the impact of conflicts by precisely characterizing the increment of complexity on the reconfiguration problem.

Introduction

Modern software systems are more and more based on interconnected software components (e.g. packages or services) deployed on clusters of heterogeneous machines that can be created, connected and reconfigured on-the-fly. Traditional component models represent components as black-boxes with interfaces indicating their provide and require ports. In many cases also conflicts are considered in order to deal with frequent situations in which components cannot be co-installed.

In software systems where components are frequently reconfigured (e.g. "cloud" based applications that elastically reacts to client demands) more expressive component models are considered: a component becomes a grey-box showing relevant internal states and the actions that can be acted on the component to change state during deployment and reconfiguration. For instance, in the popular system configuration tool Puppet [START_REF] Kanies | Puppet: Next-generation configuration management[END_REF] or the novel deployment management system Engage [START_REF] Fischer | Engage: a deployment management system[END_REF], components can be in the absent, present, running or stopped states, and the actions install, uninstall, start, stop and restart can be executed upon them. Rather expressive dependencies among components can be declared. The aim of these tools is to allow the system administrator to declaratively express the desired component configuration and automatically execute a correct sequence of low-level actions that bring the current configuration to a new one Work partially supported by Aeolus project, ANR-2010-SEGI-013-01, and performed at IR-ILL, center for Free Software Research and Innovation in Paris, France, www.irill.org. This is an extended version of [START_REF] Di Cosmo | Component reconfiguration in the presence of conflicts[END_REF].

satisfying the administrator requests respecting dependencies. We call reconfigurability the problem of checking the existence of such sequence of low-level actions.

Despite the importance of conflicts in many component models, see e.g. packagebased software distributions used for Free and Open Source Software (FOSS) [START_REF] Di Cosmo | Package upgrades in FOSS distributions: Details and challenges[END_REF], the Eclipse plugin model [START_REF] Clayberg | Eclipse Plug-ins (3rd Edition)[END_REF], or the OSGi component framework [START_REF]OSGi Alliance: OSGi Service Platform, Release 3[END_REF], state-of-the-arts management systems like the above do not take conflicts into account. This is likely ascribable to the increased complexity of the reconfigurability problem in the presence of conflicts. In this paper we precisely characterize this increment of complexity.

In a related paper [START_REF] Di Cosmo | Towards a formal component model for the cloud[END_REF] we have proposed the Aeolus component model that, despite its simplicity, is expressive enough to capture the main features of tools like Puppet and Engage. We have proved that the reconfigurability problem is Polynomial-Time for Aeolus -, the fragment without numerical constraints. In this paper we consider Aeolus core, the extension of this fragment with conflicts, and we prove that even if the reconfigurability problem remains decidable, it turns out to be Exponential-Space hard. We consider this result a fundamental step towards the realization of tools that manage conflicts systematically. In fact, we shed some light on the specific sources of the increment of complexity of the reconfigurability problem.

The technical contribution of the paper and its structure is as follows. In Section 2 we formalize the reconfigurability problem in the presence of conflicts. In Section 3 we prove its decidability by resorting to the theory of Well-Structured Transition Systems [START_REF] Abdulla | General decidability theorems for infinitestate systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. We consider this decidability result interesting also from a foundational viewpoint: despite our component model has many commonalities with concurrent models like Petri nets, in our case the addition of conflicts (corresponding to inhibitor arcs in Petri nets) does not make the analysis of reachability problems undecidable. The closed relationship between our model and Petri nets is used in Section 4 where we prove the Exponential-Space hardness of the reconfigurability problem by reduction from the coverability problem in Petri nets. In Sections 5 and 6 we discuss related work and report concluding remarks.

The Aeolus core model

The Aeolus core model represents relevant internal states of components by means of a finite state automaton (see Fig. 1): depending on its state components activate provide and require functionalities (called ports), and get in conflict with ports provided by others (in Fig. 1 active ports are black while inactive ones are grey). Each port is identified by an interface name. Bindings can be established between provide and require ports with the same interface. Fig. 1 shows the graphical representation of a typical deployment of the popular WordPress blog. According to the Debian packages metadata, WordPress requires a Web server providing httpd in order to be installed, and an active MySQL database server in order to be in production. The chosen Web server is Apache2 which is broken into various packages (e.g. apache2, apache2-bin) that shall be simultaneously installed. Notice that Apache2 is not co-installable with other Web servers, such as lighttpd.

We now move to the formal definition of Aeolus core. We assume given a set I of interface names. -Q is a finite set of states containing the initial state q 0 ; -T ⊆ Q × Q is the set of transitions; -D is a function from Q to a 3-ple P, R, C of interface names (i.e. P, R, C ⊆ I ) indicating the provide, require, and conflict ports that each state activates. We assume that the initial state q 0 has no requirements and conflicts (i.e. D(q 0 ) = P, / 0, / 0 ).

We now define configurations that describe systems composed by components and their bindings. Each component has a unique identifier taken from the set Z . A configuration, ranged over by C 1 , C 2 , . . ., is given by a set of component types, a set of components in some state, and a set of bindings.

Definition 2 (Configuration).

A configuration C is a 4-ple U, Z, S, B where:

-U ⊆ Γ is the finite universe of the available component types; -Z ⊆ Z is the set of the currently deployed components; -S is the component state description, i.e. a function that associates to components in Z a pair T , q where T ∈ U is a component type Q, q 0 , T, D , and q ∈ Q is the current component state; -B ⊆ I × Z × Z is the set of bindings, namely 3-ple composed by an interface, the component that requires that interface, and the component that provides it; we assume that the two components are different.

Configuration are equivalent if they have the same instances up to instance renaming.

Definition 3 (Configuration equivalence). Two configurations U, Z, S, B and U, Z , S , B are equivalent ( U, Z, S, B ≡ U, Z , S , B ) iff there exists a bijective function ρ from Z to Z s.t.

-

S(z) = S (ρ(z)) for every z ∈ Z; -r, z 1 , z 2 ∈ B iff r, ρ(z 1 ), ρ(z 2 ) ∈ B .
Notation. We write C [z] as a lookup operation that retrieves the pair T , q = S(z), where C = U, Z, S, B . On such a pair we then use the postfix projection operators .type and .state to retrieve T and q, respectively. Similarly, given a component type Q, q 0 , T, D , we use projections to decompose it: .states, .init, and .trans return the first three elements; .P(q), .R(q), and .C(q) return the three elements of the D(q) tuple. Moreover, we use .prov (resp. .req) to denote the union of all the provide ports (resp. require ports) of the states in Q. When there is no ambiguity we take the liberty to apply the component type projections to T , q pairs. Example: C [z].R(q) stands for the require ports of component z in configuration C when it is in state q.

We can now formalize the notion of configuration correctness.

Definition 4 (Correctness). Let us consider the configuration C = U, Z, S, B . We write C |= req (z, r) to indicate that the require port of component z, with interface r, is bound to an active port providing r, i.e. there exists a component z ∈ Z \ {z} such that r, z, z ∈ B, C [z ] = T , q and r is in T .P(q ). Similarly, for conflicts, we write C |= cn f (z, c) to indicate that the conflict port c of component z is satisfied because no other component has an active port providing c, i.e. for every z ∈ Z \ {z} with C [z ] = T , q we have that c ∈ T .P(q ).

The configuration C is correct if for every component z ∈ Z with S(z) = T , q we have that C |= req (z, r) for every r ∈ T .R(q) and C |= cn f (z, c) for every c ∈ T .C(q). Configurations evolve at the granularity of actions.

Definition 5 (Actions).

The set A contains the following actions:

-stateChange( z 1 , q 1 , q 1 , . . . , z n , q n , q n ) where z i ∈ Z and ∀i = j . z i = z j ; bind(r, z 1 , z 2 ) where z 1 , z 2 ∈ Z and r ∈ I ; unbind(r, z 1 , z 2 ) where z 1 , z 2 ∈ Z and r ∈ I ; -newRsrc(z : T ) where z ∈ Z and T ∈ U is the component type of z; -delRsrc(z) where z ∈ Z .

Notice that we consider a set of state changes in order to deal with simultaneous installations like the one needed for Apache2 and Apache2-bin in Fig. 1. The execution of actions is formalized as configuration transitions.

C stateChange( z 1 ,q 1 ,q 1 ,..., z n ,q n ,q n ) --------------------→ U, Z, S , B if ∀i . C [z i ].state = q i and ∀i . (q i , q i ) ∈ C [z i ].trans and S (z ) = C [z i ].type, q i if ∃i . z = z i C [z ] otherwise C bind(r,z 1 ,z 2 ) -------→ U, Z, S, B ∪ r, z 1 , z 2 if r, z 1 , z 2 ∈ B and r ∈ C [z 1 ].req ∩ C [z 2 ].prov C unbind(r,z 1 ,z 2 ) --------→ U, Z, S, B \ r, z 1 , z 2 if r, z 1 , z 2 ∈ B C newRsrc(z:T ) --------→ U, Z ∪ {z}, S , B if z ∈ Z, T ∈ U and S (z ) = T , T .init if z = z C [z ] otherwise C delRsrc(z) -----→ U, Z \ {z}, S , B if S (z ) = ⊥ if z = z C [z ] otherwise and B = { r, z 1 , z 2 ∈ B | z ∈ {z 1 , z 2 }}
We can now define a reconfiguration run as the effect of the execution of a sequence of actions (atomic or multiple state changes).

Definition 7 (Reconfiguration run).

A reconfiguration run is a sequence of reconfigurations C 0

α 1 -→ C 1 α 2 -→ • • • α m -→ C m such that C i is correct, for every 0 ≤ i ≤ m.
As an example, a reconfiguration run to reach the scenario depicted in Fig. 1 starting from a configuration where only apache2 and mysql are running and apache2-bin is installed is the one involving in sequence the creation of wordpress, the bindings of wordpress with mysql and apache2, and finally the installation of wordpress.

We now have all the ingredients to define the reconfigurability problem: given a universe of component types and an initial configuration, we want to know whether there exists a reconfiguration run leading to a configuration that includes at least one component of a given type T in a given state q.

Definition 8 (Reconfigurability problem). The reconfigurability problem has as input a universe U of component types, an initial configuration C , a component type T , and a state q. It returns as output true if there exists a reconfiguration run C

α 1 -→ C 1 α 2 -→ • • • α m -→ C m and C m [z] = T , q , for some component z ∈ C m . Otherwise, it returns false.
The restriction to only one component in a given state is not limiting: we can encode any given combination of component types and states by adding dummy provide ports enabled only by the final states of interest, and a target dummy component with requirements on all such provide ports.

Reconfigurability is decidable in Aeolus core

We demonstrate decidability of the reconfigurability problem by resorting to the theory of Well-Structured Transition Systems (WSTS) [START_REF] Abdulla | General decidability theorems for infinitestate systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

A reflexive and transitive relation is called quasi-ordering. A well-quasi-ordering (wqo) is a quasi-ordering (X, ≤) such that, for every infinite sequence x 1 , x 2 , x 3 , • • • , there exist i < j with x i ≤ x j . Given a quasi-order ≤ over X, an upward-closed set is a subset I ⊆ X such that the following holds: ∀x, y ∈ X :

(x ∈ I ∧ x ≤ y) ⇒ y ∈ I. Given x ∈ X, its upward closure is ↑ x = {y ∈ X | x ≤ y}.
This notion can be extended to sets in the obvious way: given a set Y ⊆ X we define its upward closure as ↑ Y = y∈Y ↑ y. A finite basis of an upward-closed set I is a finite set B such that I = x∈B ↑ x. Definition 9. A WSTS is a transition system (S , →, ) where is a wqo on S which is compatible with →, i.e., for every s 1 s 1 such that s 1 → s 2 , there exists s 1 → * s 2 such that s 2 s 2 (→ * is the reflexive and transitive closure of →). Given a state s ∈ S , Pred(s) is the set {s ∈ S | s → s} of immediate predecessors of s. Pred is extended to sets in the obvious way: Pred(S) = s∈S Pred(s). A WSTS has effective pred-basis if there exists an algorithm that, given s ∈ S , returns a finite basis of ↑ Pred(↑ s).

The following proposition is a special case of Proposition 3.5 in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

Proposition 1. Let (S , →, ) be a finitely branching WSTS with decidable and effective pred-basis. Let I be any upward-closed subset of S and let Pred * (I) be the set {s ∈ S | s → * s} of predecessors of states in I. A finite basis of Pred * (I) is computable.

In the remainder of the section, we assume a given universe U of component types; so we can consider that the sets of possible component types T and of possible internal states q are both finite. We will resort to the theory of WSTS by considering an abstract model of configurations in which bindings are not taken into account.

Definition 10 (Abstract Configuration

). An abstract configuration B is a finite multiset of pairs T , q where T is a component type and q is a corresponding state. We use Con f to denote the set of abstract configurations.

A concretization of an abstract configuration is simply a correct configuration that for every component-type and state pair T , q has as many instances of component T in state q as pairs T , q in the abstract configuration.

Definition 11 (Concretization). Given an abstract configuration B we say that a correct configuration C = U, Z, S, B is one concretization of B if there exists a bijection f from the multiset B to Z s.t. ∀ T , q ∈ B we have that S( f ( T , q )) = T , q . We denote with γ(B) the set of concretizations of B. We say that an abstract configuration B is correct if it has at least one concretization (formally γ(B) = / 0).

An interesting property of an abstract configuration is that from one of its concretizations it is possible to reach via bind and unbind actions all the other concretizations up to instance renaming. This is because it is always possible to switch one binding from one provide port to another one by adding a binding to the new port and then removing the old binding.

Property 1. Given an abstract configuration B and configurations C 1 , C 2 ∈ γ(B) there exists α 1 , . . . , α n sequence of binding and unbinding actions s.t.

C 1 α 1 -→ . . . α n -→ C ≡ C 2 .
We now move to the definition of our quasi-ordering on abstract configurations. In order to be compatible with the notion of correctness we cannot adopt the usual multiset inclusion ordering. In fact, the addition of one component to a correct configuration could introduce a conflict. If the type-state pair of the added component was absent in the configuration, the conflict might be with a component of a different type-state. If the type-state pair was present in a single copy, the conflict might be with that component if the considered type-state pair activates one provide and one conflict port on the same interface. This sort of self-conflict is revealed when there are at least two instances, as one component cannot be in conflict with itself. If the type-state pair was already present in at least two copies, no new conflicts can be added otherwise such conflicts were already present in the configuration (thus contradicting its correctness).

In the light of the above observation, we define an ordering on configurations that corresponds to the product of three orderings: the identity on the set of type-state pairs that are absent, the identity on the pairs that occurs in one instance, and the multiset inclusion for the projections on the remaining type-state pairs. Definition 12 (≤). Given a pair T , q and an abstract configuration B, let # B ( T , q ) be the number of occurrences in B of the pair T , q . Given two abstract configurations B 1 , B 2 we write B 1 ≤ B 2 if for every component type T and state q we have that

# B 1 ( T , q ) = # B 2 ( T , q ) when # B 1 ( T , q ) ∈ {0, 1} or # B 2 ( T , q ) ∈ {0, 1}, and # B 1 ( T , q ) ≤ # B 2 ( T , q ) otherwise.
As discussed above, this ordering is compatible with correctness.

Property 2. If an abstract configuration B is correct than all the configurations B such that B ≤ B are also correct.

Another interesting property of the ≤ quasi-ordering is that from one concretization of an abstract configuration, it is always possible to reconfigure it to reach a concretization of a smaller abstract configuration. In this case it is possible to first add from the starting configuration the bindings that are present in the final configuration. Then the extra components present in the starting configuration can be deleted because not needed to guarantee correctness (they are instances of components that remain available in at least two copies). Finally the remaining extra bindings can be removed.

Property 3. Given two abstract configurations B 1 , B 2 s.t. B 1 ≤ B 2 , C 1 ∈ γ(B 1 ), and C 2 ∈ γ(B 2 ) we have that there exists a reconfiguration run C 2 α 1 -→ . . . α n -→ C ≡ C 1 .
We have that ≤ is a wqo on Conf because, as we consider finitely many component type-state pairs, the three distinct orderings that compose ≤ are themselves wqo. The equality on bit vectors of length k (a and b are indeed of length k) is a wqo as there are only finitely many such vectors (namely, 2 k ). Dickson's lemma [START_REF] Dickson | Finiteness of the Odd Perfect and Primitive Abundant Numbers with n Distinct Prime Factors[END_REF] states that a product of wqo is a wqo, thus ≤ k is a wqo too. We can conclude that the ordering on the triples is a wqo by applying again Dickson's lemma.

We now define a transition system on abstract reconfigurations and prove it is a WSTS with respect to the ordering defined above. ). Since |B 2 | > 3k there are three components z 1 , z 2 and z 3 having the same component type and internal state. We consider two subcases. Case 1. z 1 , z 2 and z 3 do not perform a state change in the action α. W.l.o.g we can assume that z 3 does not appear in α (this is not restrictive because at most two components that do not perform a state change can occur in an action). We can now consider the configuration C 1 obtained by C 1 after removing z 3 (if there are bindings connected to provide ports of z 3 , these can be rebound to ports of z 1 or z 2 ). Consider now C 1 α -→ C 2 and the corresponding abstract configurations B 1 and B 2 . It is easy to see that 2 the thesis is proved, otherwise we repeat this deletion of components. Case 2. There are no three components of the same type-state that do not perform a state change. Since |B 2 | > 2k 2 + 2 we have that α is a state change involving strictly more than 2k 2 components. This ensures the existence of three components z 1 , z 2 and z 3 of the same type that perform the same state change from q to q . As in the previous case we consider the configuration C 1 obtained by C 1 after removing z 3 and α the state change similar to α but without the state change of z 3 . Consider now C 1 α -→ C 2 and the corresponding abstract configurations B 1 and B 2 . As above,

B 1 - → B 2 , B 1 ≤ B 1 , B 2 ≤ B 2 and |B 2 | < |B 2 |. If |B 2 | ≤ 3k + 2k
B 1 ≤ B 1 , B 2 ≤ B 2 and |B 2 | < |B 2 |. If |B 2 | ≤ 3k + 2k 2 the
thesis is proved, otherwise we repeat the deletion of components.

We are now in place to prove that (Conf , -→, ≤) has effective pred-basis.

Lemma 4. The transition system (Conf , -→, ≤) has effective pred-basis.

Proof. We first observe that given an abstract configuration the set of its concretizations up to configuration equivalence is finite, and that given a configuration C the set of preceding configurations C such that C α -→ C is also finite (and effectively computable). Consider now an abstract configuration B. We now show how to compute a finite basis for ↑ Pred(↑ B). First of all we consider the configuration B if |B| > 3k + 2k 2 , the (finite) set of configurations B such that B ≤ B and |B | ≤ 3k + 2k 2 otherwise. Then we consider the (finite) set of concretizations of all such abstract configurations. And finally we compute the (finite) set of the preceding configurations of all such concretizations. The set of abstract configuration corresponding to the latter is a finite basis for ↑ Pred(↑ B) as a consequence of Lemma 3.

We are finally ready to prove our decidability result.

Theorem 1. The reconfigurability problem in Aeolus core is decidable.

Proof. Let k be the number of distinct component type-state pairs according to the considered universe of component types. We first observe that if there exists a correct configuration containing a component of type T in state q then it is possible to obtain via some binding, unbinding, and delete actions another correct configuration with k or less components. Hence, given a component type T and a state q, the number of target configurations that need to be considered is finite. Moreover, given a configuration C ∈ γ(B ) there exists a reconfiguration run from

C ∈ γ(B) to C iff B ∈ Pred * (↑ B ).
To solve the reconfigurability problem it is therefore possible to consider only the (finite set of) abstractions of the target configurations. For each of them, say B , by Proposition 1, Lemma 2 and Lemma 4 we know that a finite basis for Pred * (↑ B ) can be computed. It is sufficient to check whether at least one of the abstract configurations in such basis is ≤ w.r.t. the abstraction of the initial configuration.

Reconfigurability is ExpSpace-hard in Aeolus core

We prove that the reconfigurability problem in Aeolus core is ExpSpace-hard by reduction from the coverability problem in Petri nets, a problem which is indeed known to be ExpSpace-complete [START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. We start with some background on Petri nets.

A Petri net is a tuple N = (P, T, m 0 ), where P and T are finite sets of places and transitions, respectively. A finite multiset over the set P of places is called a marking, and m 0 is the initial marking. Given a marking m and a place p, we say that the place p contains a number of tokens equal to the number of instances of p in m. A transition t ∈ T is a pair of markings denoted with • t and t • . A transition t can fire in the marking m if • t ⊆ m (where ⊆ is multiset inclusion); upon transition firing the new marking of the net becomes n = (m\m ) m (where \ and are the difference and union operators for multisets, respectively). This is written as m ⇒ n. We use ⇒ * to denote the reflexive and transitive closure of ⇒. We say that m is reachable from m if m ⇒ * m . The coverability problem for marking m consists of checking whether m 0 ⇒ * m for some m ⊆ m .

We now discuss how to encode Petri nets in Aeolus core component types. Before entering into the details we observe that given a component type T it is always possible to modify it in such a way that its instances are persistent and unique. The uniqueness constraint can be enforced by allowing all the states of the component type to provide a new port with which they are in conflict. To avoid the component deletion it is sufficient to impose its reciprocal dependence with a new type of component. When this dependence is established the components be deleted without violating it. In Fig. 2 we show an example of how a component type having two states can be modified in order q 0 f e q q 0 q 0 q' 0 q f e e η Fig. 2 to reach our goal. A new auxiliary initial state q 0 is created. The new port e ensures that the instances of type T in a state different from q 0 are unique. The require port f provided by a new component type T aux forbids the deletion of the instances of type T , if they are not in state q 0 . We assume that the ports e and f are fresh.

In the following we can therefore consider w.l.o.g. components that, when deployed, are unique and persistent. Given a component type T we denote this component type transformation with η(T ).

We now describe how to encode a Petri net in the Aeolus core model. We will use three types of components: one modeling the tokens, one for transitions and one for defining a counter. The components for transitions and the counter are unique and persistent, while those for the tokens cannot be unique because the number of tokens in a Petri net can be unbounded.

The simplest component is the one used to model a token in a given place. Intuitively one token in a place is encoded as one instance of a corresponding component type in an on state. There could be more than one of these components deployed simultaneously representing multiple tokens in a place. In Fig. 3a we represent the component type for the tokens in the place p of the Petri net. The initial state is the off state. The token could be created following a protocol consisting of requiring the port a p and then providing the port b p to signal the change of status. Similarly a token can be deleted requiring the port c p and then providing the port d p . Even if multiple instances of the token component can be deployed simultaneously, the conflict ports a p and c p guarantee that only one at a time can initiate the protocol to change its state. We denote with token(p) the component type representing the tokens in the place p. In order to model the transitions with component types without having an exponential blow up of the size of the encoding we need a mechanism to count up to a fixed number. Indeed a transition can consume and produce up to a given number of tokens. To count a number up to n we will use C 1 , . . . ,C log(n) components; every C i will represent the i-th less significant bit of the binary representation of the counter that, for our purposes, needs just to support the increment and reset operations. In Fig. 3b we represent one of the bits implementing the counter. The initial state is 0. To reset the bit it is possible to provide the reset counter i port while to increment it the up counter i should be provided. If the bit is in state 1 the increment will trigger the increment of the next bit except for the component representing the most significant bit that will never need to do that. We transform all the component types representing the counter using the η transformation to ensure uniqueness and persistence of its instances. The instance of η(C i ) can be used to count how many tokens are consumed or produced checking if the right number is reached via the ports counter i (1) and counter i (0).

A transition can be represented with a single component interacting with token and counter components. The state changes of the transition component can be intuitively divided in phases. In each of those phases a fixed number of tokens from a given place is consumed or produced. The counter is first reset providing the reset counter i and requiring the reset counter i ports for all the counter bits. Then a cycle starts incrementing the counter providing and requiring the ports up counter 1 and up counter 1 and consuming or producing a token. The production of a token in place p is obtained providing and requiring ports a p and b p while the consumption providing and requiring the ports c p and d p . The phase ends when all the bits of the counter represent in binary the right number of tokens that need to be consumed or produced. If instead at least one bit is wrong the cycle restarts. In Fig. 4 we depict the phase of a consumption of n tokens.

Starting from the initial state of the component representing the transition, the consumption phases need to be performed first. When the final token has been produced the transition component can restart from the initial state. Given a transition t we will denote with transition(t) the component type explained above. Definition 14 (Petri net encoding in Aeolus core). Given a Petri net N = (P, T, m 0 ) if n is the largest number of tokens that can be consumed or produced by a transition in T , the encoding of N in Aeolus core is the set of component types

Γ N = {token(p) | p ∈ P} ∪ {η(C i ) | i ∈ [1.. log(n) ]} ∪ {η(transition(t)) | t ∈ T }.
An important property of the previous encoding is that it is polynomial w.r.t. the size of the Petri net. This is due to the fact that the counter and place components have a constant amount of states and ports while the transition components have a number of states that grows linearly w.r.t. the number of places involved in a transition.

The proof that the reconfiguration problem for Aeolus core is ExpSpace-hard thus follows from the following correspondence between a Petri net N and its set of component types Γ N : every computation in N can be faithfully reproduced by a corresponding reconfiguration run on the components types Γ N ; every reconfiguration run on Γ N corresponds to a computation in N excluding the possibility for components of kind token(p) to be deleted (because η is not applied to those components) and of components transition(t) to execute only partially the consumption of the tokens (because e.g. some token needed by the transition is absent). In both cases, the effect is to reach a configuration in which some of the token was lost during the reconfiguration run, but this is not problematic as we deal with coverability. In fact, if a configuration is reached with at least some tokens, then also the corresponding Petri nets will be able to reach a marking with at least those tokens (possibly more).

Theorem 2. The reconfiguration problem for Aeolus core is ExpSpace-hard.

Proof. Consider a Petri net N and a marking m. We first construct a new Petri net N with a place p such that m can be covered in N iff a token can be introduced in p . The net N is the same as N but with an additional place p and a transition t such that • t = m and t • = {p }. Note that this transformation increases the size of the Petri net by a constant. We now consider the set of component types Γ N , i.e. the encoding of N . As observed above the size of this set is polynomial in the size of N .

Let us consider an extension M of Petri nets defined in the same way, with the unique difference that tokens can be deleted in a non-deterministic manner. It is easy to see that coverability in M is equivalent to coverability in Petri nets. Indeed if a marking is reachable in a Petri net then the same marking can be reached considering the M model and assuming that no token is lost. Hence, if a marking can be covered by a Petri net it can be covered also when the M model is considered. Also the vice versa holds. In fact if tokens are deleted in the M model, the only effect is that a "smaller" marking is reached with respect to the marking reached by the Petri net that executes the same firing sequence.

The thesis follows from the observation that, considering the M model, given a net N and the corresponding component types Γ N , a token can be produced in a place p iff one component of type place(p ) can be deployed in its state on starting from a configuration containing only the token components representing the initial marking m 0 .

Consider a firing sequence of the net. The execution of a transition t can be reproduced in the corresponding reconfiguration run by considering the transition component η(transition(t)) that simulates the production and consumption of tokens by changing the state of token components from off to on and from on to off . In case no sufficient instances of the token components in state off are available, new ones are deployed. Note that, on the contrary, the presence of a sufficient number of token components in state on is guaranteed otherwise the transition could not be fired in the net. The nondeterministic deletion of one token from place p is reproduced in the reconfiguration run as the deletion of one instance of the component type token(p) in state on (such components can be deleted because non persistent and not needed to satisfy requirements of other components in the configuration).

Consider now a reconfiguration run. A corresponding firing sequence can be obtained in the net as follows. A full cycle of a transition component is reproduced by the firing of the corresponding net transition. Deletion of token components (the unique non persistent component type) is reproduced by a non-deterministic deletion of the corresponding net token. Non completed cycles of transition components can be of two kinds: those that do not complete the deletion phase, and those that complete the deletion but not the production phase. In the first case, the net simulates the same behaviour by considering non-deterministic deletion of the corresponding tokens. In the second case, the net can fire the transition and immediately after lose those tokens that were not produced by the transition component in the reconfiguration run.

Related work

Engage [START_REF] Fischer | Engage: a deployment management system[END_REF] is very close to Aeolus purposes: it provides a declarative language to define resource configurations and a deployment engine. However, it lacks conflicts. This might make a huge computational differences, as it is precisely the introduction of conflicts that makes reconfigurability ExpSpace-hard in Aeolus core (the problem is polynomial in Aeolus - [START_REF] Di Cosmo | Towards a formal component model for the cloud[END_REF]). ConfSolve [START_REF] Hewson | A declarative approach to automated configuration[END_REF] is a DSL used to specify system configurations with constraints suitable for modern Constraint Satisfaction Problems solvers. Conf-Solve allocates virtual machines to physical ones considering constraints like CPU, RAM, . . . . This differs from reconfigurability in Aeolus. Package-based software management [START_REF] Abate | Dependency solving: a separate concern in component evolution management[END_REF][START_REF] Di Cosmo | Package upgrades in FOSS distributions: Details and challenges[END_REF] is a degenerate case of Aeolus reconfigurability. Package managers are used to compute a new configuration, but they use simple heuristics to reach it, ignoring transitive incoherences met during deployment.

Conclusions

The need to reconfigure software systems has become increasingly important with the generalization of distributed and dynamic architectures popularized by modern "cloud" infrastructures. At the same time, the need to mark the incompatibilities among the growing number of available components makes it necessary to handle conflicts in component models. Existing tools for the management of distributed applications are not yet satisfactory from this perspective.

In this work we have studied the impact of adding conflicts to a realistic component model, onto the complexity of reconfigurability: the problem remains decidable-while in other models, like Petri nets, the addition of tests-for-absence makes the model Turing powerful-but becomes ExpSpace-hard.

Fig. 1 :

 1 Fig. 1: Typical Wordpress/Apache/MySQL deployment, modeled in Aeolus core.

Definition 6 (

 6 Reconfigurations). Reconfigurations are denoted by transitions C α -→ C meaning that the execution of α ∈ A on the configuration C produces a new configuration C . The transitions from a configuration C = U, Z, S, B are defined as follows:

Lemma 1 .

 1 ≤ is a wqo over Conf . Proof. The proof is based on a representation of abstract configurations as 3-ples of tuples: namely, given B ∈ Conf we represent it as the triple a, b, c where a is used to represent the component type-state pairs with cardinality 0 in B, b represents those with cardinality 1, and c describes all the other pairs. Formally, let k be the possible component type-state pairs and assume a total ordering on them. The three elements a, b and c are vectors of arity k such that a[i] = 1 (resp. b[i] = 1) if the i-th component type-state pair has cardinality 0 (resp. 1) in B and a[i] = 0 (resp. b[i] = 0) otherwise, while c[i] contains the cardinality of the i-th pair in B if it is greater or equal to 2 and c[i] = 0 otherwise. Consider now two abstract configurations B 1 , B 2 ∈ Conf and the corresponding triple representations a 1 , b 1 , c 1 and a 2 , b 2 , c 2 . We have that B 1 ≤ B 2 iff a 1 = a 2 , b 1 = b 2 and c 1 ≤ k c 2 (where ≤ k is the extension of the standard ordering on natural numbers to vectors of length k).

:Fig. 3 :

 3 Fig. 2: Example of a component type transformation η( )

Fig. 4 :

 4 Fig.4: Consumption phase of n tokens from place p for a transition t (k = log(n) and h i is the i-th least significative bit of the binary representation of n)

  By Property 3 and Lemma 1 we have the following. The ≤ is a wqo for Conf by Lemma 1. To prove the thesis we need to prove that ≤ is compatible with -→ (i.e. if B 1 ≤ B 2 and B 1 -→ B 1 then B 2 -→ * B 2 for some B 2 s.t. B 1 ≤ B 2 ). This is straightforward since we have B 2 -→ * B 1 (by Property 3), B 1 -→ B 1 (by hypothesis), and B 1 ≤ B 1 (by reflexivity of ≤).The following lemma is rather technical and it will be used to prove that (Conf , -→ , ≤) has effective pred-basis. Intuitively it will allow us to consider, in the computation of the predecessors, only finitely many different state change actions. Lemma 3. Let k be the number of distinct component type-state pairs. If B 1 -→ B 2 then there exists B 1 -→ B 2 such that B 1 ≤ B 1 , B 2 ≤ B 2 and |B 2 | ≤ 3k + 2k 2 . Proof. If |B 2 | ≤ 3k + 2k 2 the thesis trivially holds. Consider now |B 2 | > 3k + 2k 2 and a transition C 1

	Lemma 2. The transition system (Conf , -→, ≤) is a WSTS.
	Proof.
	Definition 13 (Abstract reconfigurations). We write B -→ B if there exists C	α -→ C
	for some C ∈ γ(B) and C ∈ γ(B ).

α -→ C 2 such that C 1 ∈ γ(B 1 ) and C 2 ∈ γ(B 2

We consider our decidability and hardness proofs useful for at least two future intertwined research directions. On the one hand, we plan to extend existing tools with techniques inspired by our decidability proof in order to also deal with conflicts and produce a reconfiguration run. On the other hand, the hardness proof sheds some light on the specific combination of component model features that make the reconfigurability problem ExpSpace-hard. We plan to investigate realistic restrictions on the Aeolus component model for which efficient reconfigurability algorithms could be devised.