Chuck Liang

Dale Miller

On Subexponentials, Synthetic Connectives, and Multi-Level Delimited Control

We construct a partially-ordered hierarchy of delimited control operators similar to those of the CPS hierarchy of Danvy and Filinski [5]. However, instead of relying on nested CPS translations, these operators are directly interpreted in linear logic extended with subexponentials (i.e., multiple pairs of ! and ?). We construct an independent proof theory for a fragment of this logic based on the principle of focusing. It is then shown that the new constraints placed on the permutation of cuts correspond to multiple levels of delimited control.

Introduction

This paper formulates a system, motivated by linear logic with multiple pairs of exponentials, with the intent of giving a Curry-Howard style basis for multiple levels of delimited control operators similar to those of Danvy and Filinski [START_REF] Danvy | Abstracting control[END_REF]. The computational interpretation of classical logic that began with Griffin [START_REF] Griffin | The formulae-as-types notion of control[END_REF] and Parigot [START_REF] Parigot | λµ-calculus: An algorithmic interpretation of classical natural deduction[END_REF] can already explain undelimited control operators such as call/cc. However, there is nothing in classical logic that can explain directly why the capturing of a continuation should be stopped by a delimiter. Continuation capture is reflected in classical proof theory by the phenomenon of contraction and scope extrusion, which are restricted in intuitionistic logic. The fine-grained control over the capture of continuations suggests a combination of classical logic with intuitionistic logic. In [START_REF] Ilik | Delimited control operators prove double-negation shift[END_REF], delimitation is explained by a transition from an intuitionistic to a non-intuitionistic mode of derivation, which necessitates a cut-elimination strategy to deal with these transitions. However, it is known that multiple levels of delimitation can be used to block control operators from crossing programming boundaries and interfering with control operators in different modules (see [START_REF] Kameyama | Axioms for delimited continuations in the cps hierarchy[END_REF]). We may even wish to have a partially ordered hierarchy of operators. For example, in the term (f i (g j [control j c. . . . control k c.s])) we can require that control j is not delimited by j but is delimited by i if i is stronger or unrelated to j. Suppose also that an external procedure is then called that contains a control k construct. We may wish to specify what, if any, part of the continuation of the calling program can be captured by this operator by designating the relationship of i and j to k.

At the proof-theoretic level, subexponential linear logic alone is not enough. Simply adding more pairs of ? and ! does not fundamentally change the cut-elimination algorithm of linear logic. We construct a stand-alone fragment of linear logic by using the principle of focusing (focalisation) in formulating synthetic connectives. The existing definitions of focusing [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF], [START_REF] Nigam | Algorithmic specifications in linear logic with subexponentials[END_REF] in linear logic are inadequate for fully exploiting the power of exponentials. Thus a new proof theory is needed.

Previous studies of Curry-Howard interpretations of classical logic using linear logic are exemplified by the systems LKT and LKQ [START_REF] Danos | LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication[END_REF]. These systems represent different focusing strategies for eliminating non-determinism in reduction (call-by-value for LKQ, by name for LKT). These uses of focusing are by now well understood and we shall not reconstruct them. What we emphasize in this paper is a different effect of subexponentials on reduction that can operate orthogonally to the elimination of nondeterminism with focusing. The use of focusing in this paper is at a deeper level.

To motivate the need for subexponentials, a naive attempt at combining classical and intuitionistic logics can easily result in a collapse into the former even within the context of linear logic. The single-conclusion characterization of intuitionistic logic was inherited by linear logic. Unfortunately, this characterization leaves little in between intuitionistic and classical logic. The representation of intutionistic implication as !A -• B is not modular. Since -• is equivalent to a disjunction ( ), its intuitionistic strength evaporates in the in the presence of multiple conclusions. However, multiple conclusions represent saved continuations in classical computation. Fortunately, there are also multiple conclusion characterizations of intuitionistic logic:

Γ A, A, ∆ Γ A, ∆ C Γ ∆ Γ A, ∆ W A, Γ B Γ A → B, ∆ IL A, Γ B, ∆ Γ A → B, ∆ CL
Structural rules are allowed and the distinction between classical and intuitionistic logics rests on the → introduction rule: the "IL" rule prevents scope extrusion since it enforces the scope of A to include only B and not also the formulas in ∆. This perspective offers a new opportunity for combining classical and intuitionistic logics. Informally, we can hope for something of the form

A, Γ B, ∆ 2 Γ A 2 → B, ∆ 1 ∆ 2
Here, the indices 1 and 2 represent different levels of modality. Introducing an implication at level 2 can require forgetting level 1 conclusions while keeping those at level 2 or higher. This is the kind of system that we can build with subexponentials.

Subexponential Linear Logic

Subexponential, or multi-colored linear logic was suggested by Girard and first described in [START_REF] Vincent Danos | The structure of exponentials: Uncovering the dynamics of linear logic proofs[END_REF]. Given a preordered set of indices, there is a ! i for each index i with ? i as it's dual: ? i A = (! i A ⊥ ) ⊥ . A ? i does not need to admit contraction or weakening. However, the availability of these structural rules must respect the ordering relation: if j ≥ i then ? j must admit all the structural rules admitted by ? i . This restriction is required to preserve the cut elimination procedure of linear logic. For all indices k, the usual dereliction rule is allowed for ? k on the right and ! k on the left. The promotion rule is generalized as follows, which we display in two forms:

? n1 A 1 , . . .? n k A k , B ? n1 A 1 , . . .? n k A k , ! j B j ≤ n 1 , . . . n k ! n1 A 1 , . . .! n k A k B ! n1 A 1 , . . .! n k A k ! j B j ≤ n 1 , . . . n k
The single sided rule is equivalent to the two-sided version with a single conclusion.

The second form is closer to what we use. The promotion rule applies dually on the left-hand side since ! j A on one side is equivalent to ? j A ⊥ on the other side.

The term subexponential was introduced in [START_REF] Nigam | Algorithmic specifications in linear logic with subexponentials[END_REF] along with a focused proof system for them. Semantically, subexponentials can be characterized as restrictions to subspaces. In phase semantics it is easily seen that ! k restricts a fact to a submonoid that corresponds to k, with the ordering of submonoids determined by inclusion.

Subexponentials appear to be a simple generalization of linear logic save for one significant fact. In most proof systems for ordinary linear logic, and for classical and intuitionistic logics, weakening can be pushed to the initial rules. There is never a need to force weakening at other points in a proof and, therefore, it can be ignored. With indexed exponentials, however, weakening cannot be pushed to the initial rules. The sequent

! 1 A, ! 2 B ! 2 C may only be provable if ! 1 A is weakened away. If a proof of ! 1 A-• ! 2 B-• ! 2 C
is represented by λxλy.t, then x cannot appear free in t. This represents a form of resource control: not how many times but where a resource can appear.

Extending The Focusing Principle

A central goal of this paper is to derive a refinement of classical logic from subexponential linear logic that is well-behaved and self-contained with respect to cut-elimination. In this regard, the principle of focusing remains important even though our target here is not a focused sequent calculus for cut-free proofs but a natural deduction system for writing programs with possibly many cuts. We wish to synthesize new connectives by combining linear logic connectives, but not every combination can be used. An important test for the integrity of synthetic introduction rules is initial elimination: that A A is provable (in sequent calculus). Attempts to create synthetic connectives that ignore the focusing principle generally end in failure. For example, we may naively wish to consider (A ⊗ B) & C as a ternary connective with the following introduction rules:

Γ1 A Γ2 B Γ1Γ2 C Γ1Γ2 (A ⊗ B) & C ⊗ &R A, B, Γ D (A ⊗ B) & C, Γ D ⊗ &L1 C, Γ D (A ⊗ B) & C, Γ D ⊗ &L2
Here, ⊗ is positive but & is negative. But it is easily seen that

(A ⊗ B) & C (A ⊗ B) & C
is not provable with these introduction rules. In contrast, connectives of the same polarity can be combined to form synthetic connectives (e.g. (A ⊗ B) ⊕ C). While this principle is clear with regard to the binary connectives, with exponentials there is more flexibility. In terms of focusing, ? builds a negative formula and ! builds a positive formula because they have the following properties (with implied duals for !) with respect to the negative (dually positive) binary connectives:

?(?A ?B) ≡ ?A ?B ?(?A &?B) ≡ ?A &?B

These properties are not ordinary logical equivalences: they express an important property in the structure of proofs, e.g., a contraction on ?(?A ?B) can be recursively replaced by contraction on its immediate subformulas. This is the basis of focusing in classical logic. To explain focusing in intuitionistic logic in terms of linear logic [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF], we also have the following property:

!(!A -• B) ≡ !(!A -• !B).
Intuitionistic implication is usually translated as !A -• B, but it is better to regard it as !(!A -• B): the outer ! is excluded because promotion on the right is always possible in simulations of LJ sequents. With subexponentials, however, this promotion may not always be possible. One can regard focusing proof systems as the application of these properties in one direction: removing as many exponentials as possible. Our usage of them is rather in the other direction: adding more exponentials harmlessly. A contraction-enabled ? must be present for a programmer to use call/cc or similar control operations.

In our system it is of crucial importance to identify the conditions under which the following properties are preserved in the presence of subexponentials:

-? i (? k A ? j B) ≡ ? k A ? j B if and only if i ≤ k and i ≤ j -! i (! k A-•! j B) ≡ ! i (! k A -• B) if and only if j ≤ k and j ≤ i.
The index names are chosen to correspond to formulas in Section 4. A consideration of the cut-free proofs of these properties shows that the restrictions on indices are necessary and sufficient. Although our use of subexponentials will be effusive, we only admit formulas that satisfy these restrictions.

Proof theoretically, the core of this paper is a rather bold proposition: a formula of the form ! i ? i (! k ? k A-•! j ? j B), provided that i ≤ k, j and j ≤ i, k, forms a valid synthetic connective. Clearly it cannot be seen as such according to the current definitions of focusing and the polarities of ! and ?. The consequence of this boldness is that we can no longer rely on the proof theory of (subexponential) linear logic. Although we use linear logic formulas, cut-elimination within our system cannot inherit the cut-elimination procedure of linear logic (the cut-free proofs will not stay within the fragment). What's needed is a new, unique proof theory that is suitable to this new sense of synthetic connective, with its own procedure for cut-elimination that is sensitive to the index restrictions on formulas. The proof theory, presented in a longer version of this paper [START_REF] Liang | On subexponentials, synthetic connectives, and multilevel delimited control -long version[END_REF], allows our system to stand independently of linear logic.

The Fragment MC: Multi-Colored Classical Logic

For our purpose, all subexponentials ? i admit both weakening and contraction (on the right). The aspect of linear logic that prevents resources from being reused is an orthogonal issue. For clarity, we assume that subexponential indices form a partial order, although some of our examples will simply use natural numbers as indices. We also assume the existence of finite joins and meets and that there is a maximum index mx and a minimum 0. We write min(a, b) for meets and max(a, b) for joins.

With a single pair of exponentials there are seven equivalence classes of exponential prefixes or modalities: ?, !, ?!, !?, ?!?, !?! and the empty prefix. This property extends to any pair of subexponentials ! i and ? k . For any prefix ν, νν ≡ ν. For example,

! i ? k ! i ? k A ≡ ! i ? k A.
Most studies of linear logic consider only a few of these modalities. The LC fragment of linear logic [START_REF] Girard | A new constructive logic: classical logic[END_REF], for example, uses only ! and ? although ?! and !? may appear applied to atoms.

Since our main connective is implication and we wish to capture (at least) classical computations, let us review how classical implication can be represented in linear logic. The most straightforward translation is !A-•?B (equivalently ?A ⊥ ?B). This representation is sufficient for cut-free proofs, but for proofs with cuts it is clearly inadequate: one cannot form a cut with a right-side ?B and a left-side !B. In the terminology of [START_REF] Danos | LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication[END_REF], we require an adequate inductive decoration. Two well-known ones are the Ttranslation: !?A-•?B, and the Q-translation !A-•?!B. In each case one modality is a suffix of the other. With subexponentials however, we need a more flexible way to switch between left and right modalities because a promotion of ? k B to ! i ? k B may not always be possible.

The modalities we use will be ! i ? k and ? k ! i ? k (for every pair of i and k). Note that since ! i ? k ! i ? k A ≡ ! i ? k A, each modality can be seen as a suffix of the other. Promotion and dereliction will be restricted to forms that render them inverse operations:

! i ? k A ? k ! i ? k A derelict ! i ? k A promote
Adding a ! i or ? k before ! i ? k or ? k ! i ? k will still result in something equivalent to one of the two forms. We only use equivalence classes of modalities and never write ! i ? k ! i ? k . The T and Q translations gave rise to LKT and LKQ respectively, which are semifocused sequent calculi, and cut-elimination for these systems distinguish between a call-by-name (T) and call-by-value (Q) strategies. On the surface, our system does not have such properties because we rely on logical equivalences, such as between ! i ? k A and ! i ? k ! i ? k A, and between ?A ?B and ?(?A ?B). The correspondence between our system and (subexponential) linear logic exists only at the level of provability, but not in the structure of cut-elimination and cut-free proofs. However, our "fragment" of linear logic in fact forms a logical system in its own right, with its own notion of what "cut free proof" means. As we show in the longer version of this paper [START_REF] Liang | On subexponentials, synthetic connectives, and multilevel delimited control -long version[END_REF], cut-elimination within this fragment requires a more delicate procedure than for unrestricted subexponential linear logic. The non-determinism eliminated by polarization and focusing can also be achieved here, but that is not the purpose of this paper. Rather it is to demonstrate the effect on cut permutation of something quite different from polarity information.

Only the form ! i ? k may appear on the left side of -• (left-side of sequents), thus we effectively use three modalities for each pair of indices i and k (? i ! k as well).

As already indicated, our "arrow" appears as follows:

! i ? i (! k ? k A-•! j ? j B) or ? i ! i ? i (! k ? k A-•! j ? j B) such that i ≤ k, j and j ≤ k, i
The index restrictions are not ad-hoc: they are motivated by focusing. Under these restrictions, we can show that the above formula is equivalent to several other forms:

! i ? i (! k ? k A-•! j ? j B) ≡ ! i (! k ? k A-•! j ? j B) ≡ ! i (! k ? k A-•? j B)
The first condition, i ≤ k, j , makes ? i gratuitous and allows us to write a synthetic introduction rule as long as the rule does not break apart ! k ? k in the premise. The second condition, j ≤ k, i, means that a conclusion ? j ! j ? j B can always be promoted to ! j ? j B (thus it does not matter if we write ! j ? j B or ? j ! j ? j B on the right of -•).

All of these conditions are required for cut elimination.

The following also hold:

! j ? j (! k ? k A-•! m ? m B) -• (! k ? k A-•! m ? m B
) (to construct a proof bottom-up, first promote ! m , then derelict ! j , then promote ? j ). This will allow us to form an adequate →-elimination rule.

For this presentation we restrict to the adequately decorated arrow as our only connective, although other connectives can be added along similar lines 3 . It is also possible to interpret sequents as formulas: a (two-sided) sequent such as Γ, ! k ? k A ! j ? j B can be interpreted recursively as Γ ! mx ? min(k,j ) (! k ? k A-•! j ? j B). This being overly cumbersome, we simplify the interpretation of sequents by also using the empty modality and the connective , but only for sequents. To formally define the language of MC, we use the following grammar:

S -→ F | F ⊥ 1 | F ⊥ 1 S | F2 S F -→ F1 | F2 F1 -→ !i? i C. F2 -→ ? i !i? i C C -→ (! k ? k C-•!j? j C) | p
The syntactic variable p ranges over atomic formulas; S ranges over formulas that represent sequents; F ranges over formulas preceded by the modalities ! i ? i or ? i ! i ? i for any i, i ; and C ranges over formulas that are not preceded by these modalities. It is also required that the restrictions on implication i ≤ k, j and j ≤ k, i are imposed recursively on ! i ? i C and on all ? i ! i ? i C. Furthermore, all end-sequents are of the form F . When we speak of a formula of the MC fragment, we are referring to a F -generated formula of the above grammar, since such formulas form end-sequents. Notice that the grammar generates at most one F 1 formula in a sequent, which means there is at most one ! i ? i C on the right-hand side (left side occurrences are represented by F ⊥ 1 ). This is the only kind of sequent that will appear in proofs starting from valid end-sequents.

Informally speaking, the index of an exponential operator indicates a resource class. A proof of ! k A can only contain resources (free variables) of class k or higher. One useful analogy is that ? represents a producer and ! represents a consumer. A formula prefixed by ! i ? k A or ? k ! i ? k A has both a consumer level i and a producer level k. The special forms of promotion and dereliction switch the formula between the producer and consumer modes. For example, a level-2 consumer will not consume level-1 products. As long as ? k hides behind ! i , it does not affect what can be consumed. But once revealed, it produces a resource, which can only be used by consumers at level k or below, i.e., appear in subproofs outside of the context of a promotion to a level higher than k. A producer has the ability to replicate itself (contraction). On the left hand side of -•, ! i ? k becomes a level i producer.

For example, the equivalence between ! i (! k A-•! j B) and ! i (! k A-•B) when j ≤ k, i can be understood using this analogy as follows. In a term λx.t representing the proof of a formula such as ! 3 (! 4 A-•! 2 B), the outer ! 3 states that no products lower than level-3 will be consumed by λx.t. The only new product in t is the variable x, which is at level 4. So of course stating that t does not use products lower than level 2 is redundant.

Natural Deduction and Proof Terms in MC

In the following we adopt the convenient notations ! ij =! i,j =! i ? j and ? jij =? j,i,j = ? j ! i ? j . So ? jij A promotes to ! ij A, for example. We revert to the unabbreviated forms for clarity when needed.

Single sided sequents suffice for classical linear logic. However, since our principal connective is an arrow, using one-sided sequents will appear awkward. Thus we shall make a small concession to Gentzen style systems and use two sided sequents with at most one formula on the right. This means that instead of Γ ? iki A, ? jmj B we write ! j ? m ! j B ⊥ , Γ ? iki A. This concession is superficial since negation in linear logic is involutive. The interpretation of a sequent A 1 , A 2 , . . . , A n B is the formula

A ⊥ 1 A ⊥ 2 , . . . , A ⊥ n B, or just A ⊥ 1 A ⊥ 2 , . . . , A ⊥ n if the right side is empty.
The concession is only one of notation. In this two-sided scenario the modalities that can appear to the right of are ! i ? k and ? k ! i ? k while those that can appear on the left are ! i ? k and ! k ? i ! k . We store multiple conclusions on the left. Since contractions are allowed, the left-hand side of a sequent can be considered a set. The notation B, Γ does not preclude the possibility that B ∈ Γ . Certain rules, such as explicit weakening and the renaming of variable indices are excluded from the system because they can be shown to be admissible. The set Γ consists of formulas ! n1 A 1 , . . .! nm A m . We write Γ (k) to indicate that k is the smallest n i . In other words, a promotion (on the right) to ! m is allowed by Γ (k) if m ≤ k. We write Γ (n1,...,n k ) to mean Γ (min(n1,...,n k )) . We refer to n and m as the maximum promotion level of their contexts. The empty context has maximum promotion level mx. The natural deduction style proof system for MC, along with their term annotations, appear in Figure 1.

We prefer natural deduction to present delimited controls operators in direct style. We refer to the implication introduction and elimination rules as Abs and App. Because of the index restrictions already imposed on formulas, no further conditions are required in App. In addition to the P roduce rule, promotion has been folded into App and, implicitly, the Id rule. P roduce does not cross ! i ? k but switches the formula from consumer to producer mode going upward. In each rule that requires promotion, implicit or otherwise, weakening is also folded in. The dereliction rule Consume can also be simulated by N ame followed immediately by U nname. However, we have included it as a separate rule for convenience. The !DR rule is only needed for atoms. The restrictions on implication means that the ? i in ! i ? i (! k ? k A-•! j ? j B) does not interfere with its introduction rule (i.e., it does not destroy focus, despite appearance).

u : Γ !i? k A [d]u : (! k ?i! k A ⊥ ) d , Γ N ame t : (! k ?i! k A ⊥ ) d , Γ µ k d.t : Γ ? k !i? k A U nname f : Γ (n) 1 !i? i (! k ? k A-•!j? j B) t : Γ (m) 2 ! k ? k A (f n t) : Γ (n) 1 Γ (m) 2 !j? j B App, n ≤ min(n, j ) t : ! k ? k A x , Γ (n) !j? j B λx.t : Γ Γ (n) !i? i (! k ? k A-•!j? j B) Abs, i ≤ n t : Γ (n) ?i! k ?iA t : Γ Γ (n) ! k ?iA P roduce (k ≤ n) t : Γ !j?iA t (≡ µ i d.[d]t) : Γ ?i!j?iA Consume x :!i?jC x , Γ !i?jC Id t : Γ !a? b q t : Γ !c? d q !DR (a ≥ c, b ≤ d, q atomic) Fig. 1. Natural Deduction in MC
However, ! a ? b q when q is an atom posses a slight problem. This is the only rule that violates focusing boundaries, but it is required for completeness, by which we mean the following (see [START_REF] Liang | On subexponentials, synthetic connectives, and multilevel delimited control -long version[END_REF] for proof):

Theorem 1. A formula of the M C fragment is provable by natural deduction in MC if and only if it is provable in subexponential linear logic.

The correctness of MC depends on not just this theorem but on proof theoretic results for its sequent calculus, with the most important difference being the restriction of Id to atoms C, plus the replacement of App with a left introduction rule:

Γ (n) ! k ? k A !j? j B, Γ (n) C !i? i (! k ? k A-•!j? j B), Γ (n) C
Cut elimination in this system requires all the index restrictions on formulas to succeed. Furthermore, one can check that instances of this rule can be stacked, i.e., focused (consider B to be another implication), by verifying the initial elimination test for synthetic connectives. These results are presented in detail in [START_REF] Liang | On subexponentials, synthetic connectives, and multilevel delimited control -long version[END_REF].

Despite the index restrictions on implication formulas, it is possible to have Γ contain formulas preceded by any ! i . For example, ! 4 ? 0 (! 5 ? 1 A-•! 3 ? 2 (! 8 ? 6 B-•! 2 ? 2 C)) is a legal formula. Observe that in the sequent

! i ? i (! k ? k A-•! j ? j (! m ? m C-•! r ? r D)),
the restriction j ≤ k, i means that the second, inner -• can be introduced immediately above the introduction of the first, because the addition of ! k ? k A to the left-side context will not prevent the promotion of ! j . Thus instances of Abs can always be stacked, i.e., focused as well. Thus focusing is possible should one pursue the extension of the proof system in that direction.

The proof terms here are referred to as bounded λµ-terms because we have adopted several aspects of the original λµ calculus as presented in [START_REF] Parigot | λµ-calculus: An algorithmic interpretation of classical natural deduction[END_REF]. First, we prefer to associate the proof term with the entire subproof, and not just the single formula on the right of a sequent. Secondly, Parigot referred to [d]t as a named term, which is then unnamed, or bound, by µ. If one wishes to make sense of λµ calculus in terms of intuitionistic logic, then µ must be considered a non-logical constant of type ((A → ⊥) → ⊥) → A, which would of course require a double negation/CPS translation to become intuitionistically admissible. Under this interpretation, [d]t is just (d t) where d is of type A → ⊥. This means that the answer type of a captured continuation can only be ⊥, which is a problem if the continuation is to be used as a procedure. In a logic with involutive negation, such an interpretation becomes unnecessary. The only meaningful operation that N ame embeds is a dereliction 4 . We have adopted the strategy that neither promotion nor dereliction are reflected in proof terms: they do not appear to serve any purpose. The only extra notation we add are the bounded µ k binder, superscripted by the producer class/level of its type, and the bounded reset indicator n , which is used to decorate every application term, with its subscript index indicating whether this continuation may be captured by some µ k . Unlike in other formulations of delimited control operators, n is not an independent operator but a form of type annotation.

To illustrate the system we show a generalized proof of a Peirce-like formula:

. . . ! jj (! kk (! aa P -•! bb Q)-•! aa P ) ! b ? b ! b Q ⊥ , ! aa P ! aa P ! b ? b ! b Q ⊥ , ! a ?a! a P ⊥ , ! aa P N ame ! a ?a! a P ⊥ , ! aa P ? b ! b ? b Q U nname ! a ?a! a P ⊥ , ! aa P ! bb Q P roduce, b ≤ a, a ! a ?a! a P ⊥ ! kk (! aa P -•! bb Q) Abs, k ≤ a ! a ?a! a P ⊥ , ! jj (! kk (! aa P -•! bb Q)-•! aa P ) ! aa P App ! jj (! kk (! aa P -•! bb Q)-•! aa P ) ? a ,a,a P N ame -U nname ! jj (! kk (! aa P -•! bb Q)-•! aa P ) ! aa P P roduce, a ≤ j (automatic) ! ii (! jj (! kk (! aa P -•! bb Q)-•! aa P )-•! aa P ) Abs, i ≤ max
There are only a few restrictions in addition to those already imposed on formulas (k ≤ a and b ≤ a ). One can easily choose indices that would make this proof valid, including using the same index everywhere. The proof term is λx.µ a d. where m ≤ min(j, a ). As we shall show, the µ a term is guaranteed to be able to catch continuations up to the nearest n with n ≥ a . In a linear ordering, if n = k -1, for example, then capturing the continuation beyond n would mean that the promotion to ! k (as part of the upper P roduce rule) cannot be duplicated in the proof.

Intuitionistic Logic in MC

The resource control aspect of MC generalizes intuitionistic logic. Restrict all formulas to use only the modalities ! 2 ? 1 and ? 1 ! 2 ? 1 . Then any copies of ? 1 ! 2 ? 1 must be weakened away before an implication can be introduced with the Abs rule. This corresponds to the multiple-conclusion version of intuitionistic sequent calculus, at least when restricted to the → fragment. Indeed that proof system shares the rare property with subexponential linear logic that weakening is forced beneath initial rules. Peirce's formula, ((P → Q) → P ) → P , cannot be proved using only ! ik and ? kik with i ≤ k:

! 21 (! 21 (! 21 (! 21 P -•! 21 Q)-•! 21 P )-•! 21 P )
Although promotion is applicable (backwards) on ! 21 P , any copy of P created by contraction, which will appear as ? 1 ! 2 ? 1 P (or ! 1 ? 2 ! 1 P ⊥ on the left), must be weakened away upon introduction of ! 21 (! 21 P -•! 21 Q). The only producers that do not labor in vain are those on the left side of (an odd number of occurrences of) -•. In terms of the generalized proof of Peirce's formula shown earlier, the condition k ≤ a would fail.

Contracting the entire formula first will similarly fail.

It is simple to verify that any formula where the maximum producer level is lower than the minimum consumer level can only have an intuitionistic proof. From this perspective, classical and intuitionistic logics at opposite ends of a spectrum. Intuitionistic logic allows no scope extrusion, whereas classical logic make no such restrictions. With the appropriate indexing scheme in MC, we can choose to extrude into the scope of some → while keeping others intact. MC represents a new way to combine these logics without one collapsing into the other.

Reductions for Bounded λµ

When proofs are combined by cut, the potential danger of merging two contexts

Γ (n) 1 and Γ (m) 2 into Γ 1 Γ (n,m) 2
is that the lowering of the maximum promotion level will mean that some promotions can no longer be duplicated. To determine what remains as valid reduction strategies, first we note the following, which is easily proved: Lemma 2. If Γ (n) ! i ? k A is provable without weakening (all formulas in Γ appear as free variables in the proof term), then i ≤ n.

Using this property, first we verify that β-reduction is still a valid strategy:

s : ! uu A x , Γ (n,u) 1 ! rr B λx.s : Γ (n) 1 ! vv (! uu A-•! rr B) v ≤ n t : Γ (m) 2 ! uu A s[t/x] : Γ1Γ (n,m) 2 ! rr B
We are only concerned with those branches of the left subproof where ! uu A persists (has not been weakened away). Clearly in these branches there cannot be any promotion higher than to ! u . But by Lemma 2, the right subproof either ends in weakening, which permutes easily with cut, or it holds that u ≤ m, and thus min(n, m) is not lower than min(n, u), which means these promotions can still occur after Γ (m) 2

has been added to the left subproof. Thus β-reduction is still a valid strategy.

The restriction n ≤ min(n, j ) on the App rule can be strengthened to n ≤ min(i, j ) since i ≤ n by Lemma 2.

Next, we examine the possibility of capturing the continuation in the style of the original λµ calculus. In order to not clash with β-reduction, the original λµ calculus only allowed the continuation to the right of µ to be captured, by which we mean the following scenario: into the left subproof will not prevent any promotions from being duplicated. This type of continuation capture is also valid.

w : Γ ! vv (! uu A-•! rr B) [d]w : (! v vv (! uu A-•! rr B) ⊥ ) d , Γ . . . s : (! v vv (! uu A-•! rr B) ⊥ ) d , Γ (n) 1 µ v d.s : Γ (n) 1 ? v vv (! uu A-•! rr B) Γ (n) 1 ! vv (! uu A-•! rr B) v ≤ n t : Γ (m) 2 ! uu A µ v d.
However, it was soon recognized (e.g., [START_REF] Ong | A Curry-Howard foundation for functional computation with control[END_REF]) that continuation capture need not clash with β-reduction as long as we define a (call-by-value) reduction strategy carefully. The resulting form of continuation capture can be generalized to the capture of an entire evaluation context:

f : Γ (n) 1 ! vv (! uu A-•! rr B) t : Γ ! uu A [d]t : (! u uu A ⊥ ) d , Γ . . . s : (! u uu A ⊥ ) d , Γ (m) 2 µ u d.s : Γ (m) 2 ? u uu A µ u d.s : Γ (m) 2 ! uu A u ≤ m (f k µ u d.s) : Γ1Γ (n,m) 2 ! rr B
In order to permute the cut with f into the right subproof, we need to be able to retain promotions up to level ! u . Unlike the two previous cases, however, now it would possible for this condition to be violated if n or r is smaller than u (see the proof of Peirce's formula). Thus here we mark the redex with k where k ≤ min(n, r ) (or k ≤ min(v, r )). The continuation f can be captured by µ u only if min(n, r ) ≥ u . We allow k to be less than min(n, r ) because we may decide to force β-reduction anyway. We can reserve the minimum index 0 for this purpose, and require k > 0 in all terms µ k d.t. Then (f 0 s) will always force β-reduction: we can just write (f s) in that case. If capturing f is legal, then the resulting proof can have the following form:

(f k t) : Γ (n) 1 Γ ! rr B ! r rr B ⊥ , Γ (n) 1 Γ Consume . . . ! r rr B ⊥ , Γ1Γ (n,m) 2 Γ1Γ (n,m) 2 ? r rr B null s{(f k t)/[d]t} : Γ1Γ (n,m) 2 ! rr B r ≤ m, n
Recall that merely moving a formula from one side of the sequent to the other is a null operation in linear logic due to involutive negation. It is important to note that the final promotion from ? r ! r ? r B to ! r ? r B is always valid because it is required of legal formulas that r ≤ u, v in ! vv (! uu A-•! rr B). But by Lemma 2, v ≤ n and u ≤ m, and thus r ≤ n, m which makes the promotion valid. This is a consequence of the focusingrelated property !(!A-•!B) ≡!(!A -• B) when generalized to subexponentials.

A Call-by-Value Reduction Strategy

In a term such as (f 2 (g 5 (h 4 µ 3 d.s))), µ 3 should be able to capture both h and g but not f . To formalize an evaluation strategy, we define the following.

Terms and Values:

λ-variables x, . . . and µ-variables d, . . .

Values V -→ x | λx.T Terms T -→ V | (T 1 i T 2 ) | µ k d.T | [d]T Evaluation Contexts: F k -→ [ ] | (F k n T ) | (V j F k ) (j ≥ k) E -→ [ ] | (V m E) | (E n T )
E is an evaluation context while F k is a level-k context that represents a continuation that be captured by µ k d.t in the "hole" of the context. Note that in the definition of F k there is no restriction on the index n, because forward capture is always allowed. The rules for F k implies that terms such as (µ m d.s) i (µ k d.t) will have the form F m [µ m d.s] where F m = [ ] i (µ k d.t) since µ-terms are not values: the µ k term will be part of the context captured by µ m regardless of whether i ≥ k.

Evaluation Rules:

E[(λx.t) n V )] -→ E[t{V /x}] E[V i F k [µ k d.t]] -→ E[V i t{F k [u]/[d]u}] (i ≥ k)
guarantee a static behavior. How µ-terms in the body of the substitution term F k [u] is to be delimited would depend on its surrounding context, which is not statically known. It is known that such dynamic, delimited control operators can have non-terminating behavior, even in a typed setting (see [START_REF] Ariola | A type-theoretic foundation of delimited continuations[END_REF], [START_REF] Kameyama | Typed dynamic control operators for delimited continuations[END_REF]). The following term, adopted from [START_REF] Kameyama | Typed dynamic control operators for delimited continuations[END_REF], confirms this: leading to an infinite sequence of reductions. However, the term is well-typed. Also, it does have a normal form, namely t, but this is not reachable using the call-by-value strategy. This phenomenon does not contradict cut-elimination. The reduction steps still correspond to valid proof transformations. The possibility of non-termination is hardly cause for alarm from a programming perspective, and it is entirely consistent with what we already know to be possible with delimited control operators. A static behavior can be simulated using (λx.x) 0 [ ], changing the continuation capture rule to:

E[V i F k [µ k d.t]] -→ E[V i t{(λx.x) 0 F k [u]/[d]u}] (i ≥ k)
A call-by-name strategy can likewise avoid non-termination but then we can only capture continuations in the form of the original λµ-calculus, which is very limited for direct style programs. Call-by-value offers a much more general way to capture continuations. Forcing a particular evaluation strategy proof theoretically can be accomplished through focusing and this is well known. What we have shown here is that, however a continuation capturing strategy was chosen, the presence of subexponentials in MC forces it to be delimited.

Conclusion

The casual reader who opens this article to an arbitrary page may become dismayed by the large numbers of ? i ! k ? i and ! j ? j that appear in formulas. Beneath this apparent chaos, however, are the fundamental proof-theoretic principles of adequate inductive decoration, cut-elimination, and focusing. We have extended these principles to a fragment of subexponential linear logic that enhances classical logic. In the MC fragment intuitionistic logic is found not as a restriction on proofs but as a restriction on formulas. This represents a new way to combine classical with intuitionistic logic which is quite different from the polarization approach of other systems. Although MC is defined using the formulas of subexponential linear logic, and is consistent with it in terms of provability, it is self-contained as a logical system, with its own, rather unique proof theoretic properties. The hierarchy of subexponentials naturally leads to a hierarchy of delimited control operators.

  [d](x m (λy.µ b e.[d]y))

(

  λx.x) 0 ((λz.µ i d.(λy.[d]t) i [d]t) i (µ i d.(λy.[d]t) i [d]t))Here, t can be any value of type ! j ? i A while y and z are vacuous. Let V represent the value λz.(µ i d.(λy.[d]t) i [d]t), then F i = V i [ ]and the term reduces to (λx.x) 0 ((λy.V i t) i (µ i d.(λy.[d]t) i [d]t))

  Again relevant are the branches of the left subproof that contains ! v vv (! uu A-•! rr B) ⊥ , which means that there can only be promotions up to level ! v . But v ≤ u is required of well-formed formulas and by Lemma 2, u ≤ m. So once again substituting Γ

	s{[d]wt/[d]w} : Γ1Γ	(n,m) 2	! rr B
			(m)
			2

Adding second-order quantifiers will, however, encounter problems similar to those found in polarized settings: how can one enforce the index restrictions on the bound variable when they are instantiated. First-order ∀ can be represented by !i? i ∀x.! k ? k A where i ≤ k and k ≤ i. These restrictions guarantee ? i ∀x.? k A ≡ ∀x.? k A and !i∀x.! k A ≡ !i∀x.A.

When restricted to the modalities !i? i and ? i !i? i , dereliction can be expressed by the axiom !A → A: this is an intuitionistic implication, which surely has proof λx.x.

Acknowledgments. The authors wish to thank the reviewers of this paper for their comments, and to Danko Ilik for valuable discussion. This work was funded by the ERC Advanced Grant ProofCert.

A term of the form (λx.u) n V or

There is no evaluation rule for when i ≥ k, which forces F k to represent the maximum context that can be captured. If no µ k appears in a term, then the second evaluation rule will never be used, the k labels are universally ignored and standard call-by-value reduction takes place.

All application terms include a i , which can act as a delimiter, stopping the capture of continuations by µ k with i ≥ k. Instead of a null evaluation rule i (V ) -→ V , which is found in most other systems, in our system β-reduction simply ignores the symbol.

We are missing an evaluation rule for when the entire term is of the form F n [µ n d.t]. However, a λx.x can always be added in front of such a term. We can require that the minimum index 0, or some reserved index unrelated to any k that may appear in µ k d.t, is reserved for the purpose of forcing β-reduction. For example, (λx.x) 0 µ n d.t, with n > 0, reduces to (λx.x) 0 t{u/[d]u} (because here F n = [ ]). In other words it simply deletes the annotations placed on t.

The following key lemma illustrates the workings of the contexts and evaluation rules. A proof term is closed if all variables are bound by some λ or µ. Our results are for closed terms (which are the only proofs possible for end-sequents of the form F ), but they can also be generalized.

Lemma 3. Decomposition. For all non-value, closed terms T , either T is of the form

where r is a redex. Furthermore, E or F k is uniquely determined.

The proof is by induction on the structure of T . It follows easily from the property established by the lemma that if we placed an extra λx.x before a term t then all non-value, closed terms have uniquely determined redexes. If t has type ! k ? k A, then (λx.x) n t is well-typed for all n ≤ k . The lemma also implies the following: Corollary 4. Progress. If s = (λx.x) 0 t is a closed proof term, then s = E[r] where r is a redex. Furthermore, r is unique.

Thus evaluation is deterministic. The following lemma shows that evaluation is typesafe, and forms part of the Subject Reduction proof.

Each part is proved by induction on the context. The difference between sequents Γ A and A ⊥ , Γ is merely notational in classical linear logic. The central argument is similar to the reductions at the end of Section 7. Type soundness then follows: Theorem 6. Subject Reduction. If s : Γ A is provable and s -→ t using the evaluation rules, then t : Γ A is also provable.

In terms of the existing literature on delimited control operators, the behavior of our operators is dynamic as opposed to static: they are closer to the control/prompt of [START_REF] Felleisen | The theory and practice of first-class prompts[END_REF]. Since we do not interpret k as an independent operator, we cannot use it to


Eddy Caron
email: eddy.caron@ens-lyon.fr

Maurice Djibril

Ousmane Thiaré
email: ousmane.thiare@ugb.edu.sn

Autonomic Management using Self-Stabilization for Hierarchical and Distributed Middleware

Keywords: Middleware, Autonomic System, Self-stabilization, Simulation, Finite State Machine, Cloud, Distributed Computing

Dynamic nature of distributed architecture is a major challenge to avail the benefits of distributed computing. An effective solution to deal with this dynamic nature is to implement a self-adaptive mechanism to sustain the distributed architecture. Self-adaptive systems can autonomously modify their behavior at run-time in response to changes in their environment. This capability may be included in the software systems at design time or later by external mechanisms. Our paper describes the selfadaptive algorithm that we developed for an existing middleware. Once the middleware is deployed, it can detect a set of events which indicate an unstable deployment state. When an event is detected, some instructions are executed to handle the event.

We have designed a simulator to have a deeper insights of our proposed self-adaptive algorithm. Results of our simulated experiments validate the safe convergence of the algorithm.

I. INTRODUCTION

Distributed environments are complex systems. They are available in different flavors like Grid Computing, Cloud Computing, Desktop Computing, etc. Middleware are used to manage the complex access of the advantages which are provided by these distributes environments. Thus the deployment of the middleware is mandatory. Once the middleware is deployed, how it adapt the changes in dynamic environment? If the deployment is static, it may be necessary to redo all the deployment process, which is a costly operation. A better solution would be to make the deployment self-adaptive [START_REF] Kephart | The Vision of Autonomic Computing[END_REF], [START_REF] De Lemos | Software engineering for self-adaptive systems: A second research roadmap[END_REF]. This paper describes our work which aims to add selfadaptive capabilities to an existing middleware [START_REF] Caron | Cloud Computing Resource Management through a Grid Middleware: A Case Study with DIET and Eucalyptus[END_REF] so that its deployment becomes self-adaptive. The middleware is hierarchical and is composed of a finite set of component type. Thus, we have designed a self-adaptive algorithm that encapsulates the behaviour of each component instances with respect to component type. The algorithm is a set of rules. Each rule consists of an event (a guard) and a set of instructions. The detection of a rule event triggers the execution of the rule instructions. The middleware deployment is unstable when at least one rule is enabled, that is , the rule event is detected and the corresponding rule instructions are being executed. If no rule is enabled, the middleware deployment is stable. To have a deeper insight of the algorithm behaviour (for example the number of time units an unstable deployment takes to become stable), we have designed a simulator and we have used Finite State Machines (FSMs) [START_REF] Vidal | Probabilistic finite-state machines-part ii[END_REF] to model the middleware instances. The simulation results validate the safe convergence of the algorithm. This paper is organized as follows: Section II presents the architecture of the targeted middleware we rely on for this work. Section III presents the self-adaptive algorithm. The section IV describes the simulation (IV-A-simulator description, IV-B-simulator environment and simulation results). Section V presents related work and section VI presents conclusion and future work.

II. ARCHITECTURE OF THE TARGETED MIDDLEWARE

This paper introduces an autonomic solution to maintain an existing middleware in a correct configuration. DIET (Distributed Interactive Engineering Toolbox) [START_REF] Caron | DIET: A Scalable Toolbox to Build Network Enabled Servers on the Grid[END_REF] is focused on the development of a scalable middleware with initial efforts relying on distributing the scheduling problem across a hierarchy of agents. The middleware is built for distributed environment from cluster to Grid and Cloud [START_REF] Caron | Cloud Computing Resource Management through a Grid Middleware: A Case Study with DIET and Eucalyptus[END_REF].

The DIET component architecture is illustrated in Fig. 1. The DIET framework is composed of four element types: The first element is a Client, an application that uses the DIET infrastructure to solve problems using a GridRPC approach [START_REF] Nakada | A GridRPC Model and API for End-User Applications[END_REF]. The second is the SED (Server Daemon) which acts as the service provider, exposing functionalities through a standardized computational service interface; the third element of the DIET architecture are the agents which facilitate the service location and invocation interactions between clients and SEDs. Collectively, a hierarchy of agents provides higher-level services such as scheduling and data management. These services become scalable by distributing them across a hierarchy of agents composed of one or more Master agents (MA) and several Local agents (LA).

III. SELF-ADAPTIVE ALGORITHM

The self-adaptive algorithm described below allows a selfadaptive behaviour of a deployment. Only events related to the middleware components are managed (joining of new isolated instances, deletion of existing instances, link lost between to instances, etc.).

The self-adaptive algorithm is defined by a set of rules. From the middleware perspective, the rules we defined below can also detect inefficient deployments (when at least one rule is enabled). Each time a rule is enabled, the corresponding rule actions are executed. The objective of a rule actions is to lead the deployment through a stable state. An efficient and stable middleware deployment is one in which no rule is being executed. A set of rules are defined for each middleware component type.

Client rules: 3 rules are defined for the Client:

Client rule R1 defines how a Client instance reacts when it detects a connection lost with a MA instance when at least one other MA instance exists.

Client rule 1: R1

1 if Client ∧ (M A lost == T rue) ∧ (#M A > 0) then 2 select one MA and connect; 3 end
Client rule R2 defines how a Client instance reacts when it detects a connection lost with a MA instance and there is no other MA instance. MA rule R4 defines how a MA instance reacts when it detects that it has no child and knows that there is at least one other MA instance than itself.

MA rule 4: R4

1 if M A ∧ (#M A children == 0) ∧ (#M A > 1) then 2 #M A = #M A -1 ; 3 end
MA rule R5 defines how a MA instance reacts when it detects that it has neither child nor other MA instance.

MA rule R6 defines how a MA instance reacts when it detects that it has a unique agent child. The M erge(x, y)

MA rule 5: R5 1 if M A ∧ (#M A children == 0) ∧ (#M A == 1) then 2 add a SED as MA child ; 3 end MA rule 6: R6 1 if M A ∧ (#M A children == 1) ∧ (M A child type == (M A ∨ LA)) then 2
M erge(M A, M A child) ; 3 end function (line 2, R6) remove y and connects children of y as new children of x.

MA rule R7 defines how a MA instance reacts when it detects that there is at least another tree with a MA instance as root but the two trees are not connected.

MA rule 7: R7

1 if M A ∧ ({#f ather / f atherT ype = M A} == 0) ∧ ({#tree / treeRootT ype = M A} > 1) then 2
select one tree root of type MA as MA father ; 3 end MA rule R8 defines how a MA instance reacts when it detects it is overloaded. The LA rules are almost the same as the MA rules because both are agent and play almost the same role. LA has 6 rules instead of 5 like the MA. This additional rule for LA is LA rule R13 which illustrates the case when a LA instance detects it has no father and gets the information there is no MA in the system. The others LA rules, R9, R10, R11, R12, R14 can be respectively interpreted as MA rules R4, R5, R6, R7, R8 by replacing MA by LA and agent (which may be a MA or a LA) by LA.

MA rule 8: R8 1 if M A ∧ (M A load ≥ M A load threshold) then 2 divide the MA children in two sets A, B: | card(A) -card(B) | ≤ 3 ;
LA rule 9: R9

1 if LA ∧ (#LA children == 0) ∧ (#LA > 1) then 2 #LA = #LA -1 ; 3 end LA rule 10: R10 1 if LA ∧ (#LA children == 0) ∧ (#LA == 1) then 2
add a SED as LA child ; 3 end SED rules: 3 rules are defined for the SED.

The SED rule R15 illustrates the reaction of SED which is not currently executing a job, has no father, included in a deployment with zero agent.

LA rule 11: R11

1 if LA ∧ (#LA children == 1) ∧ (LA child type == LA) then 2 M erge(LA, LA child) ; 3 end LA rule 12: R12 1 if LA ∧ (#LA f ather == 0) ∧ (#{tree : treeRootT ype = (LA ∨ M A)} > 1) then 2
select one tree root (of type MA or LA) as LA father; 3 end LA rule 13: R13

1 if LA ∧ (#LA f ather == 0) ∧ (#{tree : treeRootT ype = (LA ∨ M A)} == 1) then 2
add one MA as LA father ; 3 end LA rule 14: R14

1 if LA ∧ (LA load ≥ LA load threshold) then 2 divide the LA children in two sets A, B: | card(A) -card(B) | ≤ 3 ;
1 if SED ∧ (#SeD f ather == 0) ∧ (is computing == F alse) ∧ (#{M A, LA} == 0) then 2 add one MA as SeD father; 3 end
The SED rule R16 illustrates the reaction of SED which is not currently executing a job, has no father, included in a deployment which contains at least one agent.

SED rule 16: R16

1 if SED ∧ (#SeD f ather == 0) ∧ (is computing F alse) ∧ (#{M A, LA} > 0) then 2 select one agent (MA or LA) as SED father ; 3 end
The SED rule R17 illustrates the reaction of SED which has no father but is currently executing a job.

SED rule 17: R17

1 if SED ∧ (#SeD f ather == 0) ∧ (is computing == T rue) then 2
compute for max of T (user defined parameter) units of time after which the current computation is supposed to be over. / * there is no unbounded computation: all * / / * are terminated after a unit of time * / 3 end

The effects of each of the above rules are summarized in Table I.

IV. SIMULATION

A. Simulator description

We have designed a simulator for the purpose of validating the self-adaptive algorithm and especially study the convergence. The simulator is coded with the Erlang programming language [START_REF] Cesarini | Erlang Programming[END_REF].

R2 #MA + 1 R3 re-submit request MA R4 #MA -1 R5 #SED + 1 R6 #agent -1 R7 #tree -1 R8 #agent + 2 LA R9 #LA -1 R10 #SED + 1 R11 #LA -1 R12 #tree -1 R13 #MA + 1 R14 #LA + 2 SED R15 #MA + 1 R16 #tree -1 R17
T unit of time computing

The Simulator can:

Create a predefined or a random deployment; Generate simulation events which can trigger self-adaptive behaviours (rules) of the instances; Display the global state of the deployment (if the deployment is stable or unstable) with the number of stable and unstable instances; count the number of hops (the deployment takes to recover after a simulation event). The simulator is composed of 3 main parts: A deployment server which serves as an oracle and acts as a resource discovery service. It keeps a runtime image of the deployment. A stability detection server which serves to detect the global state of a deployment, i.e, if the deployment is stable or unstable. A description of the stability detection algorithm is given at Section IV-A4 A Deployment which Consists of an hierarchy of instances linked between them. The hierarchy is created by the simulator randomly or from a predefined description.

1) Middleware objects representation:

As described in section II, the middleware is composed of four types of basic components (Client, MA, LA, SED). We used Finite State Machine (FSM) [START_REF] Vidal | Probabilistic finite-state machines-part ii[END_REF] to model each of these four elements. A FSM contains a finite number of states and produces outputs on state transitions after receiving inputs.

2) FSM state management:

The internal state of a FSM is described by a set of local variables which are used to calculate the FSM state. A state calculation is triggered by the reception of a state calculation message. A state calculation message can only be sent by an instance to itself. A state calculation message can be sent after a periodic test (neighbours link) or after the management of an incoming message which may modify the instance state. Fig. 2 highlights the behaviour of a generic FSM instance and the kind of states transition a FSM instance can do. The value of k depend on the element type and is equal to the number of rules defined for this element (each rule detects an unstable state). We have used a non-deterministic FSM model. When a process is in one of the k unstable states, it can make a transition from its current state to the same unstable state (statu quo) or to another unstable state. it can also make a transition to the stable state.

3) Deployment stability definition: A deployment corresponds to an hierarchy of instances (modeled as FMSs ), deployed on Erlang nodes. A deployment is stable when each instance is in its stable state (e.g., is not executing a rule actions). In this case, #{unstable instances} = 0. Once the deployment is stable, it remains stable and its number of instances is constant in the absence of external events.

4) Deployment stability detection:

For simulation purposes, we need to be able to detect a stable deployment. A stable deployment is a global state, and the deployment stability detection can understood as a termination detection algorithm [START_REF] Dhamdhere | Distributed termination detection for dynamic systems[END_REF]. Termination detection determines whether a distributed algorithm has terminated. We want to detect the self-adaptive algorithm termination, which corresponds to a stable deployment. To detect a stable deployment, we used a stability detection server (Section IV-A). It has two internal variables which are updated as descibed in the Listing 1, where: UnstableInstanceCount and Sta-bleInstanceCount are positive integer variables, initialized to zero when the server is launched (before the creation of any instance). These two variables are intended to count respectively the current number of unstable and stable instances. The server reads periodically the values of these two variables and display the global state of the deployment (stable when U nstableInstanceCount = 0, unstable otherwise). Each time an instance calculates its state for any reason, it records its previous state and after calculating its current state, it compares the two states. If a state variation (a transition from state s i to s j with s i = s j ) is noticed, the instance sends an update message to the stability detection server. If s i = initial state, it means that the instance recalculates its state for the first time after its initialization. The message depends on the variation type, it can lead to the increment and/or decrement of UnstableInstanceCount and/or StableInstanceCount. When the test is done inside the termination function (the last function a dying instance can execute), an update message is sent to the stability detection server according to the last state the instance has before it died.

B. Results

All simulations were performed on a computer with the following information: Debian GNU/Linux 7 (wheezy) operating system, Intel(R) Xeon(R) CPU X5570 @ 2.93GHz with 16 cores and 33 GB of RAM, Erlang R15B01 (erts-5.9.1).

For all simulations, we used 4 Erlang virtual machines (Erlang nodes), deployed as an Erlang cluster on one physical machine. Each Erlang Node is connected to all others nodes in a fully connected graph.

4 simulations were performed.

The first simulation always starts with a stable system with six (6) elements: One MA and five SEDs. From this stable system and for each X ∈ {5, 10, 50, 100, 200, 500, 600, 700}, X new SEDs are added in the system (the newly created SEDs are unstables and will try to become stables) and we counted the number of hops the system takes to recover a stable state. For each X, the simulation is executed 5 times and the Mean of the 5 values (number of hops) is computed. The Fig. 3 shows the ratio between the Mean value of hops and the corresponding X.

For the 2 nd simulation, we tried to have a stable system with a quiet large number of SEDs. For this purpose, this simulation always starts with a stable system obtained by adding 500 SEDs to an predefined stable system with six (6) elements: 1 MA and 5 SEDs. The resulting stable system is not always the same (even if two stable systems have the same number of objects, their topologies may be different), but it is obtained by the same operations. When a stable system is reached, then for each X ∈ {5, 10, 50, 100, 200, 500}, X SEDs are killed (randomly chosen in the system) and we count : the number of hops the system takes to recover a stable state, the total number of instances (also called FSMs in this paper) before the "kill X SEDs " action, the total number of instances when the system recovers its stable state after the "kill X SEDs " action (the end of the simulation). For each X, the simulation is executed 5 times and the Means of the 5 values (number of hops, number of FSMs at the beginning of the simulation, number of FSM at the end of the simulation) are computed. The Figure 4 show the results of this simulation. The in Fig. 4 (a) represent the mean of FSMs at the beginning of the simulation, at the end of the simulation, and the difference between these two values for each X. The curve in Fig. 4 (b) represents for each X, the ratio between the mean of hops and X.

For the 3 th simulation, we start with a stable system obtained by adding 250 SEDs to an predefined stable system with six (6) elements: One MA and five SEDs. The resulting stable system have 408 instances. From this stable system, we kill 100 SEDs (randomly chosen) and wait until the system becomes stable again, then we add 100 SEDs, and we repeat these two simulation events one after another and always when the system is stable. The number of stable instances, the number of unstable instances are recorded every unit of time (hop). Fig. 5 shows the results of this simulation. The curve in Fig. 5 shows that, after every simulation action ("kill" or "add"), the system recovers a stable state, that is, the number of unstable instances is equal to zero. The 4 th simulation is like the 2 nd with the following differences: Instead of killing X SEDs, it is X% of SEDs which are killed and X ∈ {5, 20, 25, 35, 40, 50, 65, 75, 80, 100}. For each X ∈ {5, 20, 25, 35, 40, 50, 65, 75, 80, 100}, X% of SEDs are killed; the simulation is executed 5 times and the following values are recorded: The number of hops the system takes to become stable; the total number of instances (FSMs) before the "kill X% SEDs " action; the total number of instances when the system recovers its stable state after the "kill X% SEDs " action.For each X, the mean of the 5 values obtained during the 5 simulations for each of the recorded parameters ((number of FSMs at the beginning of the simulation, number of FSMs at the end of the simulation)are computed. Fig. 6 shows the results of this simulation. V. RELATED WORK Distributed software systems like middleware are usually deployed on distributed and dynamic infrastructures. Once a software system was deployed, then how it will adapt the changes from the infrastructure? A solution to overcome this challenge is to make these software systems autonomic (at design time or later by external mechanisms). Autonomic computing [START_REF] Kephart | The Vision of Autonomic Computing[END_REF] is a vision to make a software self-adaptive [START_REF] De Lemos | Software engineering for self-adaptive systems: A second research roadmap[END_REF]. A self-adaptive system have the capability to autonomously modify its behaviour at run-time in response to changes in its environment. The enforcement of this vision for software systems raises some challenges [START_REF] Salehie | Self-adaptive software:landscape and research challenges[END_REF]. Like our algorithm which is intended to maintain a topology, many self-stabilizing topology control algorithms were proposed to construct and/or maintain differents topologies. We can cite [START_REF] Ben-Othman | Self-stabilizing algorithm for efficient topology control in wireless sensor networks[END_REF] for graphs, [START_REF] Jacob | A Self-stabilizing and Local Delaunay Graph Construction[END_REF] gives a solution for Delaunay graph construction, skip graphs are solved by [START_REF] Jacob | SKIP+: A Self-Stabilizing Skip Graph[END_REF], skip list in [START_REF] Clouser | Tiara: A self-stabilizing deterministic skip list and skip graph[END_REF], trees are done in [START_REF] Caron | When self-stabilization meets real platforms: An experimental study of a peer-to-peer service discovery system[END_REF], hyperTree in [START_REF] Dolev | Hypertree for self-stabilizing peer-to-peer systems[END_REF], spanning tree [START_REF] Kravchik | Time optimal synchronous self stabilizing spanning tree[END_REF] or ring [START_REF] Ooshita | On the self-stabilization of mobile oblivious robots in uniform rings[END_REF].

Our work takes benefit of these previous works and adapt the methodology to a given middleware. Beyond the contribution for the DIET middleware, the reader should see this paper as a proof of concept and a way to begin from theoretical work and usage in a real environment.

VI. CONCLUSION

In this paper, we addressed the problem of adding selfadaptive capabilities to an hierarchical grid and cloud middleware. For this purpose, we have proposed a distributed selfadaptive algorithm. The algorithm objective is qualitative and effective in maintaining a stable deployment. The processes which execute the algorithm are able to self-adapt themselves when a faulty state is detected. To validate the self-adaptive algorithm, a simulator was designed to simulate the dynamic behaviour. The simulations show that the algorithm is selfadaptive with respect to the set of faults we used for simulation. Currently, processes rely on their local knowledge (as far as it is possible) to self-adapt themselves. However, they sometimes need to interact with the deployment server, which acts as a centralized resource discovery service. As future work, we plan to integrate a distributed resource discovery, for example , using gossiping algorithms. In addition to the simulations, which give us an idea of the algorithm convergence, we will prove that the algorithm is self-stabilizing [START_REF] Dolev | Self-Stabilization[END_REF], that is, following the defined rules, an unstable deployment can achieve stable state within an arbitrary but finite time.

Fig. 1 .

 1 Fig. 1. DIET multi-hierarchy.

Client rule 2 :

 2 R2 1 if Client ∧ (M A lost == T rue) ∧ (#M A == 0) then 2 create one MA as the client Child ; 3 end Client rule R3 defines how a Client instance reacts when it detects a connection lost with a SED instance. Client rule 3: R3 1 if Client ∧ (SeD lost == T rue) then 2 submit the request again ; 3 end MA rules: 5 rules are defined for the MA:

3

  create one agent as father of all the instances in each set ; 4 the roots (2 agents) of newly created trees becomes MA Children 5 end LA rules: 6 rules are defined for the LA.

3

  create one LA as father of all the instances in each set ; 4 the roots (2 LA) of newly created trees becomes LA Children 5 end SED rule 15: R15

1 c 2 / 3 / 6 { 7 S 9 / 12 { 15 / 18 {

 123679121518 a s e { p r e v i o u s S t a t e , c u r r e n t S t a t e } o f * c a s e s t a t e t r a n s i t i o n * / * t r a n s i t i o n f r o m s t a b l e s t a t e t o one o f 4 t h e u n s t a b l e s t a t e s * / 5 s t a b l e , u n s t a b l e } : U n s t a b l e I n s t a n c e C o u n t ++; t a b l e I n s t a n c e C o u n t --; 8 * t r a n s i t i o n f r o m one o f t h e u n s t a b l e 10 s t a t e s t o s t a b l e s t a t e * / 11 u n s t a b l e , s t a b l e } : S t a b l e I n s t a n c e C o u n t ++; 13 U n s t a b l e I n s t a n c e C o u n t --; 14 * d y i n g u n s t a b l e s t a t e . i n s t a n c e i n i t s 16 t e r m i n a t i o n f u n c t i o n * / 17 u n s t a b l e , d y i n g i n s t a n c e } : U n s t a b l e I n s t a n c e C o u n t --; 19 20 / * d y i n g s t a b l e s t a t e . i n s t a n c e i n i t s t e r m i n a t i o n f u n c t i o n * / 21 22 { s t a b l e , d y i n g i n s t a n c e } : S t a b l e I n s t a n c e C o u n t --;

Fig. 3 .

 3 Fig. 3. Add X SEDs simulation: Ratio between Mean hops and X.

Fig. 4 .Fig. 5 .

 45 Fig. 4. Kill X SEDs simulation

Fig. 6 .

 6 Fig. 6. Kill X percent SEDs simulation: Mean of SEDs at the simulation Start and at the simulation end.

TABLE I

 I

		.	RULES EFFECTS
	Element	RULE Id	RULE Effects
	Client	R1	#tree -1

ACKNOWLEDGEMENT

The authors of this paper would like to thank the African Center of Excellency (CEA-MITIC) Project supported by World Bank and managed by University Gaston Berger through UFR SAT. Thanks to Pushpinder K. Chouhan for the review.