Mario Coppo

Mariangiola Dezani-Ciancaglini

Luca Padovani

Nobuko Yoshida

Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions

Keywords:

Conventional session type systems guarantee progress within single sessions, but do not usually take into account the dependencies arising from the interleaving of simultaneously active sessions and from session delegations. As a consequence, a well-typed system may fail to have progress, even assuming that helper processes can join the system after its execution has started. In this paper we develop a static analysis technique, specified as a set of syntax-directed inference rules, that is capable of verifying whether a system of processes engaged in simultaneously active multiparty sessions has the progress property.

. Calculus of multiparty sessions (syntax).

Introduction

A system of multiparty sessions has the global progress property if all processes in the system that are involved in ongoing sessions do not get stuck waiting for a message that is never sent and if every message sent is eventually consumed. On the one hand, this notion of progress is stronger than requiring that a non-terminated system can always reduce. For example, a system containing two processes engaged in an "infinite chatter" (like two non terminating threads which communicate with each other) does not have the progress property if some other process involved in an open session is stuck and unable to complete its own task. On the other hand, this notion of progress is weaker than requiring that all processes in the system must be able to reduce. For example, a system with an incomplete session, i.e. a session that has not been initiated and for which some participants are missing, does have the progress property if it can be completed with the missing participants to a system that has the progress property.

Communication type systems such as those introduced in [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF] can check that processes behave correctly with respect to the protocols associated with the single sessions. The same type systems can also assure a local progress property within the single sessions, but they fall short in assuring the global progress property when several multiparty sessions are interleaved with each other or the communication topology of the system changes as a consequence of delegations across these sessions.

In previous work [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF] we have defined an interaction type system that, when used in conjunction with the communication type system, can assure the global progress property for processes in a calculus of asynchronous multiparty sessions. The interaction type system pivots around three different typing rules for service initiations. To build the type deduction for a process, provided that one exists, it is crucial, for each service occurring in the process, to choose the right typing rule. In practice, this means that the interaction type system can be efficiently used only for verifying whether a given process has a given type. A naive type inference algorithm based directly on the rules of the type system would require backtracking, resulting in an exponential explosion of the search space. The contribution of the present paper is the definition of a deterministic, compositional inference algorithm which is proved to be sound and complete with respect to the interaction type system of [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF]. The algorithm is presented in a "natural deduction" style, as a set of inference rules that can be evaluated in a single-pass analysis according to the structure of processes. The complexity is quadratic in the size of processes, since the application of the rules requires evaluations of linear functions. The basic idea is to devise a suitable data structure that stores the information about all the possible ways a service initiation can be typed in the interaction type system, postponing the commitment to a specific typing rule as long as possible. The inference algorithm refines the information in this data structure discarding the typing rules of service initiations that are found to be incompatible with the structure of the processes being analyzed.

In §2 we define syntax and reduction semantics of the calculus of multiparty sessions. In §3 we illustrate, through a number of smaller examples, various behavioral patterns that we want to consider and how and when these may cause deadlocks. This tutorial informally hints at the information available to the inference algorithm that helps preventing deadlocks and how such information can be inferred from the structure of processes. The inference algorithm and the data structures it uses are described in §4, which ends by showing the algorithm at work on a few examples. Related work is discussed in §5, while §6 concludes with a summary of the results and an account of ongoing and future work.

The Calculus of Multiparty Sessions

Syntax. We begin by fixing some notation for the following sets: service names are ranged over by a, b, . . . ; value variables are ranged over by x, x , . . . ; identifiers, i.e., service names and variables, are ranged over by u, w, . . . ; channel variables are ranged over by y, z, t, . . . ; labels, functioning like method selectors, are ranged over by l, l , . . . ; we write S for the set of all service names and V for the set of all channel variables. Processes, ranged over by P, Q, . . . , and expressions, ranged over by e, e , . . . , are given by the grammar in Table 1, where the syntax occurring only at runtime appears shaded .

The process u [p](y).P initiates a new session through an identifier u with the other participants, each of the form u[q](y).Q q where 1 ≤ q ≤ p -1. The (bound) variable y is the channel used for the private communications inside the session. We call p, q, . . . (ranging over natural numbers) the participants of the session and we use Π, Π to denote finite, non-empty sets of participants.

Communications that take place inside an established session are represented using the next three pairs of primitives: the sending and receiving of a value; the sending and receiving of a session channel (where the sender delegates the receiver to participate in a session by passing a channel associated with the session); selection and branching (where the former chooses one of the branches offered by the latter). All these operations specify the channel and the index of the sender or the receiver. Thus, c! Π, e sends a value on channel c to all the participants in Π, while c?(p, x) denotes the intention of receiving a value on channel c from the participant p. The same holds for delegation/reception (but the receiver is only one) and for selection/branching. We write c! p, e .P and c⊕ p, l .P in place of c! {p}, e .P and c⊕ {p}, l .P. An output action is a value sending, session sending or label selection. An input action is a value reception, session reception or label branching; an input process is a process prefixed by an input action. The service restrictions are decorated with the global types of the services. Global types describe the communication protocol followed by the session participants; we omit their syntax and refer the interested reader to [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF] for the details. Conditional processes and parallel composition are standard.

Queues and channels with role are generated by the operational semantics (see Table 2). A channel with role is a pair s[p] representing the runtime endpoint of session s used by participant p. As in [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF], we model TCP-like asynchronous communications (where the message order is preserved and send actions are non-blocking) with unbounded queues of messages in a session, denoted by h. A message in a queue can be a value message (q, Π, v), indicating that the value v was sent by participant q to the recipients in Π; a channel message (delegation) (q, p, s[p ]), indicating that q delegates to p the role of p on the session s (represented by the channel with role s[p ]); and a label message (q, Π, l) (similar to a value message). By and h • m we respectively denote the empty queue and the queue obtained by concatenating m to the queue h. With some abuse of notation we will also write m • h to denote the queue with head element m. By s : h we denote the queue h of the session s. In (νs)P all occurrences of s[p] and the queue name s are bound.

We write fs(P), fc(P) respectively for the sets of service names and channel names occurring free in P. We define fn(P) = fs(P) ∪ fc(P). A user process is a process which does not contain runtime syntax.

→ P | s : h • (p, Π, v) (e ↓ v) [SEND] s[p]! q, s [p ] .P | s : h → P | s : h • (p, q, s [p ]) [DELEG] s[p]⊕ Π, l .P | s : h → P | s : h • (p, Π, l) [SEL] s[p]?(q, x).P | s : (q, p, v) • h → P{v/x} | s : h [RCV]
s[p]?((q, y)).P | s : (q, p,

s [p ]) • h → P{s [p ]/y} | s : h [SRCV] s[p]&(q, {l i : P i } i∈I ) | s : (q, p, l k ) • h → P k | s : h (k ∈ I) [BRANCH]
Operational Semantics. The operational semantics is defined as the combination of reduction rules expressing actual computation steps and structural equivalence rules that rearrange terms so as to enable reductions. Structural equivalence is almost standard (and therefore omitted). The only peculiar rules allow rearranging the order of messages in a queue when the senders or the receivers are not the same and for splitting a message targeted to multiple recipients. Table 2 shows a selection of the relevant rules for the process reduction relation P → P . We briefly comment the rules in what follows.

Rule [INIT] describes the initiation of a new session involving n + 1 participants that synchronize over the service name a. Here we use ∏ n i=1 P i to denote

P 1 | • • • | P n .
The last participant a [n + 1](y).P n+1 , distinguished by the overbar on the service name, determines the number n + 1 of participants. After the initiation, the participants share a private session name s and the queue associated with s, which is initially empty. The variable y in each participant p is replaced by the corresponding channel with role s[p]. The output rules [SEND], [DELEG], and [SEL] respectively push values, channels and labels into the queue of the session s (in rule [SEND], the side condition e ↓ v denotes the evaluation of the expression e to the value v). The input rules [RCV], [SRCV] and [BRANCH] perform the corresponding complementary operations. Note that these operations check that the sender of the message matches the expected one so that the message is actually meant for the receiver. Reduction is closed under evaluation contexts, which are special terms with holes [ ] generated by the grammar below:

E ::= [ ] | P | (νa : G)E | (νs)E | (E | E )
We write E [P 1 , . . . , P n ] for E where the i-th (left-to-right) hole has been filled with P i .

The Communication Type System. The communication type system checks that processes use service names and channels according to the global types associated with them. It ensures that messages are exchanged in the right order and have the right types within sessions. The communication type system also guarantees progress within a single session, if this session is not interleaved with other sessions, but it cannot guarantee progress when multiple sessions are interleaved. We omit the specification of the communication type system because it is well understood (see [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF] for details). In fact all processes in this paper are (assumed to be) well typed with respect to the communication type system.

Progress. Informally, we intend that a process has the progress property if each session, once started, is guaranteed to satisfy all the requested interactions. A formal definition of the progress property is not straightforward and the definition in [START_REF] Bettini | Global Progress in Dynamically Interleaved Multiparty Sessions[END_REF] is unsatisfactory in presence of infinite computations. We explain the key ideas and problems separately.

A natural requirement for progress in the case of communication protocols is that an input process can always read a message in the expected queue and vice versa a message in a queue is always read by an input process. Hence, we must assure that any request of interaction on a session channel will always be satisfied. For instance, take the processes:

P 1 = a[1](y).b[1](z).y?(2, x).z! 2, x Q 1 = a [2](y). b [2](z).z?(1, x ).y! 1, x
The problem of P 1 | Q 1 is that it reduces to a process in which the output actions of both sessions are prefixed by input actions of the other session. Indeed,

P 1 | Q 1 reduces to (νs)(νs )(s[1]?(2, x).s [1]! 2, x | s [2]?(1, x ).s[2]! 1, x )
where the private sessions s and s respectively established for the a and b services have replaced the channel variables y and z in P 1 and Q 1 . This configuration is stuck because the two processes are blocked mutually waiting for a message from restricted channels. Instead, the process P 1 | Q 1 where:

Q 1 = a [2](y). b [2](z).y! 1, true .z?(1, x).0
has progress and reduces to 0.

Building on Kobayashi's definition of lock-freedom [START_REF] Kobayashi | A Type System for Lock-Free Processes[END_REF] and on the definition of communication safety of [START_REF] Deniélou | Dynamic Multirole Session Types[END_REF] we require that each input process will always be able to receive an appropriate message along some computation and that each message in a queue will always be received by an appropriate input process along some computation. However, we must also consider that an incomplete session (i.e., without all the required participants) on service a occurring in a process P can always be allowed to start by composing P with a process containing the missing participants for a. For this reason, we use catalyser processes to provide the missing participants to sessions and to make sure that rule [INIT] can always be applied, so that session accept and session request prefixes are never blocking. We omit here the precise definition of catalysers which requires a number of auxiliary definitions (see [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF] for the details). Intuitively, a catalyser is a parallel composition of processes where each process implements the behavior of a single participant. In particular, in a catalyser it is never the case that actions pertaining to different sessions are interleaved with each other in the same sequential thread. Therefore, catalysers cannot generate deadlocks.

The last notion we need before defining progress is a natural duality between input processes and message queues, which only takes into account top inputs in processes and leftmost messages in queues.

Definition 2.1 (Duality).

The duality between input processes and message queues is the least symmetric relation defined by: s[p]?(q, x).P s : (q, p, v) • h s[p]?((q, y)).P s : (q, p,

s [p ]) • h s[p]&(q, {l i : P i } i∈I ) s : (q, p, l k ) • h (k ∈ I)
We are now able to define progress as follows:

Definition 2.2 (Progress). A process P has the progress property if for all catalysers Q such that P | Q is well typed in the communication system, if

P | Q → * E [R],
where R is an input process or a non-empty message queue, then there are a catalyser Q , and

E , R such that E [R] | Q → * E [R, R ] and R R .

A Tutorial to Progress Inference

Service dependencies. The basic idea for preventing deadlocks is to forbid mutual dependencies between services. A dependency between two services originates when an input action pertaining to one of the services guards (hence potentially blocks) any action of the other service. A paradigmatic example of process without progress is P 1 | Q 1 that we have already examined in §2. Observe that in process P 1 we have an input action on service a that guards an output action on service b. This dependency can be recorded as the relation a ≺ b associated with process P 1 . In process Q 1 the situation is reversed, determining b ≺ a. If we take P 1 and Q 1 in isolation, then no circular dependency is detected. However, when considering P 1 | Q 1 , the relations associated with this composition result into the circular dependency a ≺ b ≺ a.

The idea of avoiding circular dependencies between services breaks apart as soon as service names are first-class entities that can be sent as messages. When this happens, the actual dependencies between services may dynamically change as the system evolves and it might happen that a system without circular dependencies turns into one with circular dependencies. To illustrate the issue, consider the processes

P 2 = c[1](t).t?(2, x).x[1](y).b[1](z).y?(2, x ).z! 2, x Q 2 = c [2](z).z! 1, a
and observe that Q 2 sends to P 2 the name of service a. The analysis of process P 2 may determine the relation x ≺ b, because there is an action pertaining to service x that blocks another action pertaining to service b. However, since x is a bound variable in P 2 , there is no obvious way to associate this dependency with P 2 . On the other hand, the analysis of process Q 2 yields no apparent dependencies for a. Overall, no dependency is inferred for P 2 | Q 2 , even though at runtime the system will reduce to a configuration that yields the relation a ≺ b. Then, if P 2 | Q 2 is composed with a process that yields the inverse dependency b ≺ a, a deadlock can occur. Indeed

P 2 | Q 2 | Q 1 reduces to P 1 | Q 1
which leads to a deadlock, as we have seen in §2.

The idea then is to identify a class of services which do not cause deadlocks even when they are involved into circular dependencies, and to allow a service name to be sent as a message only if it refers to a service in this class. A practically relevant class of services with this property is that of nested ones, which are characterized by the fact that they can only be blocked by actions pertaining to nested invocations of services that are themselves nested. As an example, consider the processes

P 3 = a [2](y).y?(1, x). a [2](z).z?(1, x ).z! 1, true .y! 1, false Q 3 = a[1](y).y! 2, false .a[1](z).z! 2, true .z?(2, x ).y?(2, x) R 3 = a[1](y).y! 2, false .a[1](z).y?(2, x).z! 2, true .z?(2, x )
and observe that P 3 represents the request of two nested invocations of service a. Observe also that in P 3 there is an input action on channel z that guards an output action on channel y and that both actions pertain to the service a. As a consequence, these dependencies result in the relation a ≺ a that denotes a circular dependency. However, P 3 has a peculiar structure in that all the actions related to the innermost invocation of a are completely nested within the ones related to the outermost invocation of a. More generally, there is no blocking action of the outermost invocation of a that is interleaved with actions of the innermost invocation of a. In fact, this interaction structure closely resembles an ordinary function call of a sequential programming language, where a caller function is suspended until the callee has terminated. The point is that if all request and accept operations concerning service a follow this pattern (i.e., they are not interleaved with blocking actions from other sessions), then the process P 3 cannot deadlock even if its structural analysis establishes the circular dependency a ≺ a. For example, also Q 3 gives rise to the same circular dependency, but it follows the same structure as P 3 and the composition P 3 | Q 3 is deadlock free. By contrast, in R 3 we notice that, after the innermost invocation of a has been accepted, there is an input action on y, which pertains to the outermost invocation, blocking the actions pertaining to the innermost one. Indeed, the composition P 3 | R 3 yields a deadlock.

Relative and Nested services. To promote P 3 (and Q 3 ) among the safe processes, we associate services with different features and we impose different constraints on the structure of services depending on the features they have. We say that a service that is never involved in circular dependencies with other services has the R (for Relative) feature. A service a where no action from other sessions can block the sessions initiated on a has the N (for Nested) feature. This is precisely the case of the innermost invocation of a in P 3 and Q 3 . But there is more: if the innermost session cannot deadlock, it becomes "unobservable" as far as the dependency analysis is concerned so we can say that also the outermost invocation of a in P 3 and Q 3 is not blocked by actions of other sessions. As a consequence, the outermost service a has the N feature as well.

The N feature may also be used for dealing with circular dependencies between different services. As an example, consider the processes

P 4 = a [2](y). b [2](z).z?(1, x).y?(1, x ) Q 4 = b [2](z). a [2](y).y?(1, x).z?(1, x )
representing two clients which, for unspecified reasons, request the two services a and b in different orders. If P 4 and Q 4 run within the same system, then they immediately yield the circular dependencies a ≺ b ≺ a. Still, if the processes implementing a and b (not shown here) are independent, in the sense that they do not rely on each other, then there is no danger of deadlock. The fundamental observation here is that neither service seems to have the N feature if considered in isolation: each service request is blocked by an action from the other service. However, if b is assumed to have the N feature, then a has the N feature also, and vice versa. In other words, the circular dependency a ≺ b ≺ a identifies a clique of services that is safe (i.e., deadlock-free) if every service in the clique has the N feature under the hypothesis that all the others do as well.

In general, the same service may have both the R and the N features at the same time. This is the case of a and b in P 4 and Q 4 above when each process is considered in isolation. However, note that the b service in P 1 has the R feature but not the N one, while neither a nor b has the R feature in P 4 | Q 4 . This observation is crucial for the inference algorithm because the fact that a service a does not have a particular feature may affect other services related to a by the dependency relation. In particular, if a ≺ b and b does not have the R feature (hence it has the N one), then a cannot have the R feature (and it must have the N one). Dually, if a does not have the N feature, then b cannot have the N feature.

Bounded services. The next usage pattern that we wish to consider concerns private services. Take for example the process

b[1](y).(νa : 1 → 2 : bool )( a [2](z).z?(1, x).y! 2, false )
where the a service has been restricted and is therefore inaccessible from the outside. Even if the a service has both the R and N features, the fact that it is restricted makes it observably equivalent to the idle process. This has severe consequences on the outer service b, because the output action on channel y cannot be executed. In essence, we devise a third feature B (for Bounded) associated with services that can be restricted and that prevents them to be followed by any communication action on free channels.

Wrap up. To summarize, when we analyze a system of interleaved multiparty sessions we associate services in the system with (a combination of) three features R, N, and B:

-A service has the R feature if it never generates circular dependencies with other services it is interleaved with. -A service has the N feature if it is never interleaved with blocking actions from other services not having the N feature. -Finally, a service has the B feature if it has the N feature and it is never followed by any action on free communication channels.

Overall there are eight feature combinations. One of these corresponds to the fact that a service has none of the features outlined above. In this case, the service will be rejected by our system as being ill typed. Furthermore, having the B feature implies having the N feature. Therefore, each well-typed service may be classified into one of five feature combinations. Note that, in the informal definitions above, "never" means both "for no occurrence of the service in the system" and "at any time during the evolution of the system". The inference algorithm has to find a trade off between flexibility (the number of systems for which progress can be guaranteed) and feasibility (the analysis is solely based on the initial state of the system). In fact, when discussing first-class service names we have already seen a case in which the algorithm is forced to act conservatively due to the lack of precise information about the runtime evolution of a system. The inference of the progress property performs an analysis on the structure of processes, keeping track of the dependencies between services and incrementally refining the features associated with services, making sure that each service has at least one of the features described above. Initially, each service has every feature. As the analysis proceeds bottom up on the structure of processes, features are removed from services that are found to be incompatible with them. In a nutshell, the most relevant refinement steps taken by the algorithm occur at the following events:

-As soon as a circular dependency is detected, all processes involved in the circularity (and those preceding them in the dependency relation) lose the R feature. -When a process of shape ã[p](y).P is encountered, where ã is either an accept action a or a request action a , a loses the N feature if it is not minimal in the dependency relation (meaning that it may be blocked by another session of a service not having the N feature). Also, a loses the B feature if P has free channels other than y. -When a process of shape y?(p, x).P is encountered, the dependencies are enriched with relations y ≺ z for every channel z that occurs free in P. The same happens for session receives and branching processes, since these are all blocking actions. -When a process of shape P | Q is encountered, the dependencies computed for P and those computed for Q are merged together, while the features for every service in the overall process are those in common between P and Q. Similar operations are performed when analyzing branching and conditional processes, where multiple processes come together. -When a process of shape y! p, a .P is encountered, the service a loses the R feature.

-Special measures must be taken when channels are communicated. These will be detailed shortly.

The next section is devoted to formalizing all the concepts and procedures outlined in this tutorial.

Progress Inference

In this section we introduce a deterministic, compositional type inference algorithm, defined via a set natural semantics rules, assuring that a given user process has the progress property. As we have anticipated in §3, the basic idea of the inference algorithm is to keep track of dependencies between services.

A service qualifier is either a service name a or a channel variable y; we write Λ = S ∪ V for the set of all service qualifiers; we let λ range over elements of Λ and L over subsets of Λ.

A dependency relation is a transitive relation D ⊆ Λ × Λ. We denote with λ ≺ λ the elements of Λ × Λ. The meaning of λ ≺ λ is, roughly, that an input action on the channel (or on the channel bound by service) λ can block a communication action on the channel (or on the channel bound by service) λ .

The inference algorithm makes use of some auxiliary operators for D that are introduced below:

-D ↓ λ def = {λ } ∪ {λ | λ ≺ λ ∈ D}
is the set of elements that are smaller than or equal to λ in D, namely the set of service qualifiers having an input action that can block a communication action on λ , plus λ itself.

-D ↑ λ def = {λ } ∪ {λ | λ ≺ λ ∈ D}
is the symmetric operation that determines the set of service qualifiers that may be blocked by an input action on λ , plus λ itself.

-D \ L def = {λ ≺ λ ∈ D | λ ∈ L ∧ λ ∈ L }
is the subset of D pertaining to all the service qualifiers not occurring in L .

Table 3. Inference algorithm for the interaction type system.

{INACT-I}

{BRANCH-I}

P i ⇒ D i ; R i ; N i ; B i (i∈I) D = (pre(y, i∈I fc(P i )) ∪ i∈I D i ) + y&(p, {l i : P i } i∈I ) ⇒ F(D, i∈I R i , i∈I N i , i∈I B i ) {PAR-I} P i ⇒ D i ; R i ; N i ; B i (i=1,2) D = (D 1 ∪ D 2 ) + P 1 | P 2 ⇒ F(D, R 1 ∩ R 2 , N 1 ∩ N 2 , B 1 ∩ B 2 ) {IF-I} P i ⇒ D i ; R i ; N i ; B i (i=1,2) D = (D 1 ∪ D 2 ) + if e then P 1 else P 2 ⇒ F(D, R 1 ∩ R 2 , N 1 ∩ N 2 , B 1 ∩ B 2 ) -D ∞ def = {λ | λ ≺ λ ∈ D} is the set of service qualifiers involved in circular depen- dencies in D.
We extend ↓ and ↑ to sets L of service qualifiers in the natural way. We also write D{a/y} for the relation obtained from D where every occurrence of y has been replaced by a and R + for the transitive closure of a generic relation R.

The inference rules prove judgments of the form P ⇒ D; R; N; B, where D is a dependency relation and R, N, and B are sets of service names. As a first approximation, we can think of the services in these sets as those that respectively have the R, N, and B feature. However, for services that are communicated in messages it is not easy to statically guarantee that they will not be involved in a circular dependency at runtime. Therefore, we conservatively remove communicated services from the R set even if they are not explicitly involved in circular dependencies.

A judgment P ⇒ D; R; N; B is well formed if:

1. If a service a has the R feature, then all the services following a in D have R feature. Also, no service involved in a circular dependency can have the R feature. This is formally expressed as

D ↑ R ⊆ R \ D ∞ ∪ V . 2.
If a service a has the N feature, then all service qualifiers preceding a in D must be services with the N feature. That is, D ↓ N ⊆ N. 3. The set of services having the B feature is included in those having the N feature.

That is, B ⊆ N. 4. All services occurring free in P have at least the R or the N feature. If some service in P has neither the R nor the N feature, then our inference algorithm does not guarantee the progress property for P. That is, fs(P) ⊆ R ∪ N.

In general, the inference rules add dependencies to the D relation and remove service names from the R, N, B sets when these services lose features. To be sure that the quadruple resulting from the application of an inference rule still satisfies the conditions (1-3) above, we define a function F that, given a quadruple D, R, N, B, computes a new one where services are removed from the sets R, N, B whenever they are found to be incompatible with the corresponding feature:

F(D, R, N, B) def = D; R ; N ; B ∩ N where R = {a ∈ R | D ↑ a ⊆ R \ D ∞ ∪ V } and N = {a ∈ N | D ↓ a ⊆ N}.
Table 3 defines the inference for the interaction type system. We implicitly assume that an inference rule can be applied only if the judgment in the conclusion is well formed. In the next paragraphs we describe each inference rule in detail.

{INACT-I} is by far the simplest inference rule, which yields no dependencies and poses no constraints on the features of services. In particular, D is / 0 and the R, N, and B components are the full set S of service names.

{INIT*-I} is used for typing accept and request operations on a known service name a (recall that we use ã for either a or a). The rule computes a new quadruple F(D{a/y} + , R, N, B \ {a | fc(P) \ {y} = / 0}) from the one obtained by typing the continuation process P, where D{a/y} + replaces the channel variable y with a in D so that all the dependencies already established for a are enriched with those computed for y. Also, a loses the B feature if P contains free channels other than y.

{INITV-I} is analogous to {INIT*-I}, but considers the case in which the session is initiated on an unknown service x. Because nothing is known on the service a that will replace x at runtime, the rule acts conservatively assuming that a has both the N and the B features. In particular, the continuation process P is required to have no free channel other than y (this is necessary if a has the B feature) and all services preceding y in D lose the R feature (this is necessary if a has the N feature but not the R one). Note that it is not possible to keep track, in D, of all the dependencies related to y as we did in {INIT*-I}. In fact, any dependency related to y in D is removed. This may prevent the inference algorithm from statically detecting circular dependencies for services that are communicated in messages. For this reason, we will require that all service names communicated by rule {SEND-I} must have the N feature (Example 4.2 shows that this is necessary for communicated services to prevent deadlocks). When a service name a is restricted in a process P, rule {NRES-I} checks that a has the B feature. Then, all dependencies related to a and a itself are removed from all the components of the quadruple in the conclusion of the rule.

Rules {SEND-I} and {SEL-I} do not change the dependency relation because send operations are non-blocking. In the case of {SEND-I}, however, we must check that if the message sent e is a service name, then it cannot have the R feature. The application of the F function makes sure that all the components of the quadruple remain consistent after this removal.

Rule {RCV-I} is used for typing value receptions. In this case, only the dependency relation is changed to record the fact that the input action on channel y may block subsequent actions on the free channels occurring in P. The function pre(y, fc(P)) creates the dependency relation that contains the pairs y ≺ z for all z ∈ fc(P). Note that no dependency is recorded between y and the free service names possibly occurring in P. This is because these services can always be unblocked by adding suitable catalysers (see Definition 2.2) provided that the communication occurring on y does not reach a deadlock.

Rule {BRANCH-I} is a natural generalization of rule {RCV-I} to a process with multiple branches. In this case, the dependencies inferred for each branch are merged together and services lose those features that are not present in every branch.

Rule {DELEG-I} is similar to {SEND-I} and {SEL-I} in that it deals with a nonblocking send operation. However, in this case the process is sending a channel variable z over channel y, meaning that an action blocking a communication on y may also block a communication on z, because z cannot be used by the receiver process until delegation happens. Consequently, the dependency relation is enriched with the y ≺ z dependency.

Rule {SRCV-I} is similar to {RCV-I}, except that it is used for typing the reception of a session channel. The rule is particularly restrictive because it is meant to prevent a dangerous phenomenon called self-delegation, which happens when one process ends up owning two (or more) endpoints of the same session. An example of this phenomenon is shown in the processes which is stuck. Remarkably, the process P 5 | Q 5 is typable in the communication type system hence it is the interaction type system that must detect the problem in this case. The premise D \ S ⊆ {y ≺ z} requires that the continuation process P 5 cannot perform any potentially blocking action on any channel other than y, and that if a potentially blocking action is performed on y then it must necessarily block a communication action on z. This restriction prevents self-delegation and, in general, suffices to guarantee progress. Note that P 5 is still allowed to open new sessions on other services.

{PAR-I} and {IF-I} conclude the inference system by suitably combining dependencies and features, similarly to what we have already seen for the {BRANCH-I} rule.

The algorithm is quadratic in the size of processes, being defined on their structure, if we use appropriate data structures to represent the dependency relation and the service sets, getting linear complexity for the evaluation of the required functions.

The algorithm is sound, namely: This theorem can be proved by showing that the inference algorithm is sound and complete with respect to the interaction type system defined in [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF].

We end with the application of the inference algorithm on two examples used earlier.

Example 4.1. Below are two executions of the inference algorithm on P 1 and Q 1 of §2.

For the sake of readability, we develop the inference bottom up assuming S = {a, b}. From the above table it turns out that both P 1 and Q 1 are well typed in isolation, in particular we have P 1 ⇒ {a ≺ b}; {a, b}; {a}; {a} and Q 1 ⇒ {b ≺ a}; {a, b}; {a, b}; {a} but the application of rule {PAR-I} fails since F(D, {a, b}, {a}, {a}) = (D, / 0, / 0, / 0) where D = {a ≺ b, b ≺ a} + , and the resulting judgment would not satisfy condition 4 of the definition of well formedness. In particular the circular dependency removes the R feature from both a and b and the N feature is removed from b in P 1 and then also from a in the composition

P 1 D R N B z! 2, x / 0 {a,
P 1 | Q 1 because of b ≺ a (see the definition of F).
Example 4.2. The inference algorithm is not always able to statically determine a violation of the R feature, therefore it is unsafe to leave service names that are sent as messages in the R set. Below is the result of the inference algorithm on the processes P 2 and Q 2 of §3 assuming S = {a, b, c}: Note that the dependency y ≺ b in P 2 is erased because it concerns an unknown service x that is bound in P 2 . This means that b is actually involved in dependencies a ≺ b for every service a that is sent to P 2 , which is precisely what Q 2 does. Indeed we have

P 2 | Q 2 ⇒ / 0; {b, c}; {a, c}; {a, c} but P 2 | Q 2 | Q 1 ,
where Q 1 is defined in Example 4.1, cannot be typed. In fact, adding c to the set of services we get immediately Q 1 ⇒ {b ≺ a}; {a, b, c}; {a, b, c}; {a, c} but rule {PAR-I} cannot be applied since F({b ≺ a}, {b, c}, {a, c}, {a, c}) = ({b ≺ a}, {b, c}, {c}, {c}) does not satisfy the condition 4 of the definition of well-formedness for service a. Indeed we have the reduction

P 2 | Q 2 | Q 1 → * P 1 | Q 1 which
leads to a deadlock, as we have seen in §3.

Related Work

Our notion of progress is strongly related to, and partly inspired from, the notion of lock-freedom in [START_REF] Kobayashi | A Type System for Lock-Free Processes[END_REF], where Kobayashi develops a type system to enforce it. Intuitively, a process is lock-free if, no matter how it reduces, every top-level prefix can be eventually consumed. In our case this roughly corresponds to the property that no process gets stuck on an input action and that every message in a queue can be received. Kobayashi's type system seems capable of a much more fine-grained analysis than our type system. However, despite the similarities between progress and lock-freedom, the two type systems are difficult to compare, because of several major differences in both processes and types. In addition to the fact that we consider progress modulo the availability of catalysers, our type system is given for an asynchronous language with a native notion of (multiparty) session, while Kobayashi's type system is defined for a basic variant of the synchronous, pure π-calculus. A natural way for comparing these analysis techniques would require compiling a session-based process into the pure π-calculus [START_REF] Dardha | Session types revisited[END_REF], and then using Kobayashi's type system for reasoning on progress of the original process in terms of lock-freedom of the one resulting from the compilation.

A strategy that is alternative to compiling/encoding session-based processes is to lift the technique underlying Kobayashi's type system to a session type system for reasoning directly on the progress properties of processes. Some preliminary experiments in this sense are reported in [START_REF] Padovani | From Lock Freedom to Progress Using Session Types[END_REF].

Most papers on service-oriented calculi only assure that clients are never stuck inside a single session [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF][START_REF] Dezani | Sessions and Session Types: an Overview[END_REF][START_REF] Deniélou | Dynamic Multirole Session Types[END_REF]. The first papers considering progress for interleaved sessions required the nesting of sessions in Java [START_REF] Dezani-Ciancaglini | Session Types for Object-Oriented Languages[END_REF][START_REF] Coppo | Asynchronous Session Types and Progress for Object-Oriented Languages[END_REF].

The papers more related to the present one are [START_REF] Dezani-Ciancaglini | On Progress for Structured Communications[END_REF] and [START_REF] Carbone | A graphical approach to progress for structured communication in web services[END_REF]. In both these papers there are constructions of processes providing missing participants, which are simpler than our catalysers since sessions are dyadic.

[2] proposes a sophisticated proof system which builds a well-founded ordering on events to enforce progress for processes of the Conversation Calculus [START_REF] Vieira | The Conversation Calculus: A Model of Service-Oriented Computation[END_REF], also in presence of dynamic join and leave of participants. Their progress is guaranteed under the assumption that all communications are matched with sufficient joiners.

Formal theories of contracts using multiparty interaction structures are studied in [START_REF] Castagna | Contracts for Mobile Processes[END_REF]. Contracts record the overall behaviour of a process, and typable processes themselves may not always satisfy properties such as progress: it is proved later by checking whether a whole contract satisfies a certain form. Proving properties with contracts requires an exploration of all possible interleaved or non-deterministic paths of a protocol.

Conclusions and Future Work

We have presented a sound and complete inference algorithm for the interaction type system defined in [START_REF] Coppo | Global Progress for Dynamically Interleaved Multiparty Sessions[END_REF] restricted to finite processes. This system guarantees progress of interleaved multiparty sessions with session delegation and service communication.

There is a number of extensions stemming from this work, we focus on two of them. First of all, it appears that the algorithm can be easily adapted to deal with recursive processes, although soundness and completeness of such extension remain to be formally established. Second, we plan to investigate how the approach can be applied to concrete programming languages. The point is that the inference algorithm (and the interaction type system as well) makes the fundamental assumption that a process can be examined in terms of the complete sequence of input/output operations it performs. In practice, programs are made of opaque structures (higher-order functions, methods, modules, etc.) and it is currently unclear whether such structures can be faithfully encoded as processes in our calculus, or if instead it is necessary to devise richer type constructs to describe them and to reason on global progress of systems in a modular way.

  0 ⇒ / 0; S ; S ; S {INIT*-I} P ⇒ D; R; N; B ã[p](y).P ⇒ F(D{a/y} + , R, N, B \ {a | fc(P) ⊆ {y}}) {INITV-I} P ⇒ D; R; N; B fc(P) ⊆ {y} x[p](y).P ⇒ F(D \ {y}, R \ (D ↓ y), N, B) {NRES-I} P ⇒ D; R; N; B a ∈ B (νa : G)P ⇒ D \ {a}; R \ {a}; N \ {a}; B \ {a} {SEND-I} P ⇒ D; R; N; B y! Π, e .P ⇒ F(D, R \ {e}, N, B) {RCV-I} P ⇒ D; R; N; B y?(q, x).P ⇒ (pre(y, fc(P)) ∪ D) + ; R; N; B {DELEG-I} P ⇒ D; R; N; B y! p, z .P ⇒ ({y ≺ z} ∪ D) + ; R; N; B {SRCV-I} P ⇒ D; R; N; B D \ S ⊆ {y ≺ z} y?((q, z)).P ⇒ D \ {z}; R; N; B {SEL-I} P ⇒ D; R; N; B y⊕ Π, l .P ⇒ D; R; N; B

P 5 =

 5 b[1](z).a[1](y).y! 2, z Q 5 = b [2](z). a [2](y).y?((1, x)).x?(2, w).z! 1, false which, when executed in parallel, open two sessions on services a and b. Then, P 5 sends the channel z related to the session on b over the channel y, which is related to the session on a. At this point, Q 5 owns both endpoints of the session on b and tries to use them in an order that causes a deadlock. Indeed, P 5 | Q 5 reduces to (νs)(s[1]?(2, w).s[2]! 1, false )

Theorem 4 . 1 .

 41 If P ⇒ D; R; N; B, then P has the progress property.

  ,c} {a,b,c} {a,b,c} {SEND-I} y?(2, x ) {y ≺ z} {a,b,c} {a,b,c} {a,b,c} {RCV-I} b[1](z) {y ≺ b} {a,b,c} {a,c} {a,c} {INIT*-I} x[1](y) / 0 {a,b,c} {a,c} {a,c} {INITV-I} t?(2, x) / 0 {a,b,c} {a,c} {a,c} {RCV-I} c[1](t) / 0 {a,b,c} {a,c} {a,c} {INIT*-I} Q 2 D R N B t! 1, a / 0 {b,c} {a,b,c} {a,b,c} {SEND-I} c [2](t) / 0 {b,c} {a,b,c} {a,b,c} {INIT*-I}

Table 2 .

 2 Reduction (selected rules).

	∏ n i=1 a[i](y).P i | a [n + 1](y).P n+1 → (νs)(∏ n i=1 P i {s[i]/y} | P n+1 {s[n + 1]/y} | s : ) [INIT]
	s[p]! Π, e .P | s : h

  b} {a,b} {a,b} {SEND-I} y?(2, x) {y ≺ z} {a,b} {a,b} {a,b} {RCV-I} b[1](z) {y ≺ b} {a,b} {a} {a} {INIT*-I} a[1](y) {a ≺ b} {a,b} {a} {a} {INIT*-I} ) {z ≺ y} {a,b} {a,b} {a,b} {RCV-I} b [2](z) {b ≺ y} {a,b} {a, b} {a} {INIT*-I} a [2](y) {b ≺ a} {a,b} {a,b} {a} {INIT*-I}

	Q 1	D	R	N	B
	y! 1, x	/ 0 {a,b} {a,b} {a,b} {SEND-I}
	z?(1, x

Acknowledgments. The authors are grateful to the reviewers for their useful comments and to Naoki Kobayashi for discussions on the notion of lock-freedom. This work was partially supported by EPSRC EP/G015635/1 and EP/K011715/1, NSF Ocean Observatories Initiative, MIUR Project CINA and Ateneo/CSP Project SALT.


David Margery
email: david.margery@inria.fr

David Guyon
email: david.guyon@irisa.fr

Anne-Cécile Orgerie
email: anne-cecile.orgerie@irisa.fr

Christine Morin
email: christine.morin@inria.fr

Gareth Francis
email: g.francis@epcc.ed.ac.uk

Charaka Palansuriya
email: c.palansuriya@epcc.ed.ac.uk

Kostas Kavoussanakis
email: kostas.kavoussanikis@epcc.ed.ac.uk

A CO2 emissions accounting framework with market-based incentives for Cloud infrastructures

Keywords: Cloud computing, Energy monitoring, Carbon emissions, CO2 accounting

CO2 emissions related to Cloud computing reach nowadays worrying levels, without any reduction in sight. Often, Cloud users, asking for virtual machines, are not aware of such emissions which concern the entire Cloud infrastructures and are thus difficult to split into the actual resources utilization, such as virtual machines. We propose a CO2 emissions accounting framework giving flexibility to the Cloud providers, predictability to the users and allocating all the carbon costs to the users. This paper shows the architecture of our accounting framework and ideas on how to practically implement it.

INTRODUCTION

Cloud computing's wide adoption leads to a rising increase of data center's electricity consumption. This major social issue will worsen with the explosion of connected devices and Internet of Things (IoT), asking for always more computing and storage capacity in the Cloud. In 2013, U.S. data centers consumed an estimated 91 billion kWh of electricity; this consumption is projected to increase to roughly 140 billion kilowatt-hours annually by 2020, the equivalent annual output of 50 power plants, costing American businesses $13 billion per year in electricity bills and causing the emission of nearly 150 million metric tons of carbon pollution annually (Natural Resources Defense Council, 2014).

This uncontrolled energy consumption of Cloud's data center causes increased greenhouse gas (GHG) emissions. This important consequence is mainly determined by the amount and sources of consumed energy [START_REF] Bosse | Introducing Greenhouse Emissions in Cost Optimization of Fault-Tolerant Data Center Design[END_REF]. Among GHG, carbon dioxide (CO 2 ) is the major one in quantity produced by human activities. Consequently, carbon taxes have been proposed in order to reduce CO 2 emissions and their negative effects on environment [START_REF] Nordhaus | Carbon Taxes to Move Toward Fiscal Sustainability[END_REF]. From an operational point of view, a carbon tax requires a monitoring and accounting infrastructure in order to fairly distribute CO 2 costs among the Cloud users. Even outside a carbon tax system, such an infrastructure can provide useful information to users about their real CO 2 emissions based on their utilization of the Cloud system, and therefore, it can raise their environmental awareness and incite them to adopt more sustainable practices.

To build a carbon tax system, it is required to precisely monitor the resource usage that can be attributed to each user (computing, storage, communication), and to account for the resource cost induced by the user's utilization, like the data center air conditioning cost for instance. While the live monitoring issue has already been addressed in literature [START_REF] Wajid | On Achieving Energy Efficiency and Reducing CO2 Footprint in Cloud Computing[END_REF], the accounting issue has received little attention.

The accounting problem consists in splitting the indirect costs between the Cloud users (such as air conditioning), and forecasting the direct costs for each user. Indeed, Cloud computing is using a payas-you-go model where users buy computing, storage and network resources in the form of virtual machines (VM). Cloud providers exhibit prices per virtual machine type, depending on the amount of virtual resources included in the virtual machine. Such a model involves an a priori cost which is known by the user upon purchase as opposed to an a posteriori cost based on a precise monitoring of the resources really used and thus, provided to the user at the end of its Cloud resources utilization. Such an accounting model has to be flexible enough for the Cloud providers to be attractive, and it should provide to the users a predictable cost. From an external third-party organization, the carbon tax accounting system needs to be certified: for a given period of time, all the carbon emissions of the data center must be equal to the overall carbon emissions charged to the users.

In this paper, we propose a CO 2 emissions accounting framework giving flexibility to the Cloud providers, predictability to the users and allocating all the carbon costs to the users. We provide the architecture of our accounting framework and ideas on how to practically implement it. We argue that instead of trying to keep the difference between predicted and real CO 2 emissions as low as possible at any time, an effective framework could consider this difference as a flexible capital to support an economical approach for users' energy-awareness.

The paper is organized as follows. Section 2 provides motivational examples and the context of this work. The related work is presented in Section 3. Our proposed architecture is described in Section 4. Section 5 discusses the advantages and drawbacks of our approach and provides ideas for implementing it in real Cloud infrastructures. Section 6 concludes this work.

CONTEXT AND MOTIVATION

2.1 From the Cloud user point of view Cloud users are renting virtual machines (VM) on a pay-as-you-go basis. The energy consumption of their virtual machine depends on the resource utilization (CPU, memory, disk, network) and on the infrastructure power management (cooling cost, resource allocation management, etc.) [START_REF] Kurpicz | How much does a VM cost? Energy-proportional Accounting in VM-based Environments[END_REF]. The CO 2 emissions depends on the energy consumption and on the electricity mix [START_REF] Wajid | On Achieving Energy Efficiency and Reducing CO2 Footprint in Cloud Computing[END_REF]. One could compute these costs at each time and divide them proportionally to the number of resources booked by each VM. However, it would mean that identical VMs running the same computation could have really different costs. Indeed, if a VM is alone on the infrastructure at a given time, then it would support the entire infrastructure cost, while this same VM during a busy period would account for a much lower cost. Such an accounting model, with high variations over the time, would provide great unpredictability to users, and is thus not desirable.

On the contrary, we argue for a shift of the prediction responsibility from the user to the provider. The Cloud provider gives a CO 2 cost for a VM upon its purchase. This cost depends on the VM size and can vary over time, but it cannot change for VMs already paid. So, the provider has to carefully monitor resource consumption, infrastructure costs and electricity mix to entirely attribute the CO 2 emissions to its users for a given period of time (a month for instance).

From the Cloud provider point of view

The Cloud provider is responsible for assigning all the CO 2 costs to the users over a long period (a month for instance). A third-party, like a governmental organization could be in charge of certifying the summary of provider's CO 2 accounts. The accounting model described above does not aim at being as accurate as possible. Indeed, the provider could compute the difference between invoiced and real costs at the end of each VM booking and it could directly pass on this difference to the next client. However, such a system does not give any flexibility to the provider. Instead, we argue for a flexible model, fixed by the provider itself, and following market opportunities. The provider is then responsible for dealing with the difference between invoiced and real costs. It fixes its own CO 2 cost model for its VMs, and it can choose not to make direct adjustments, but to use this difference as a capital to invest. For instance, this capital can be reinvested to reduce the cost of VMs when the electricity mix is better or when cooling costs are lower (at night for instance with free cooling). This capital with its associated cheap offers would constitute a market-based incentive to increase users' energy-awareness. This accounting framework also favors energy-aware behavior from the Cloud providers as they need to invoice all the CO 2 costs to the users. So, in order to be competitive, they need to have CO 2 costs as low as possible. It creates then a strong incentive to switch off unused servers or perform over-commitment on servers hosting VMs with low workload.

RELATED WORK

The carbon emissions of users' virtualized resources mainly depend on their power consumption. The power consumption attributed to a user is not equal to the total server power consumption when the user is not using all the server's resources. A finegrained monitoring of the power consumed by each VM on a server is necessary in order to be able to estimate their carbon emissions. Several VM power models have been proposed in literature with different implementations. They are usually based on counters (hardware or software) in order to monitor the resource usage. Their accuracy thus depends which resources are selected, how they are monitored and which formulas are used to estimate the VM power consumption from the monitoring data, such as linear regression [START_REF] Kim | Energy-Based Accounting and Scheduling of Virtual Machines in a Cloud System[END_REF] [START_REF] Wu | An Intelligent Power Consumption Model for Virtual Machines Under CPU-intensive Workload in Cloud Environment[END_REF], polynomial regression [START_REF] Xiao | Virtual Machine Power Measuring Technique with Bounded Error in Cloud Environments[END_REF], machine learning [START_REF] Yang | iMeter: An integrated VM power model based on performance profiling[END_REF] or tree regression based approach [START_REF] Gu | A Tree Regression-Based Approach for VM Power Metering[END_REF]. In these studies, estimation errors typically fluctuate from 2 to 5%.

Research studies start to include ecologicalrelated factors in their optimization algorithms. Bosse et al introduces GHG emissions into the system availability and cost optimization problem of faulttolerant IT services [START_REF] Bosse | Introducing Greenhouse Emissions in Cost Optimization of Fault-Tolerant Data Center Design[END_REF]. Experiments show that, for a slightly increased cost, a significant reduction in GHG emissions is possible. Similarly, Khosravi et al propose a VM placement algorithm taking into account Cloud sites' PUE and their carbon footprint [START_REF] Khosravi | Energy and Carbon-Efficient Placement of Virtual Machines in Distributed Cloud DataCenters[END_REF]. While maintaining the same level of QoS, their solution manages to reduce the power consumption and CO 2 emissions.

Workload predictions as well as green energy availability predictions bring an important contribution in reducing CO 2 emissions as it offers the ability to adapt system configurations in order to face future trends. Cloud resources usage can be predicted for a given Cloud by using Extreme Learning Machine algorithm on VM usage traces and user behavior (Ismaeel and Miri, 2016). Sharma et al present a prediction model for green energy availability [START_REF] Sharma | Cloudy Computing: Leveraging Weather Forecasts in Energy Harvesting Sensor Systems[END_REF]. The model is able to predict next day energy harvesting based on weather forecasts. They improved accuracy by 27% with machine learning techniques [START_REF] Sharma | Predicting Solar Generation from Weather Forecasts Using Machine Learning[END_REF].

The existing studies show the ability to monitor VMs power consumption, the inclusion of GHG emissions factor in algorithms and also the possibility to predict availability of green energy as well as Cloud users workload. However, to the best of our knowledge, no work is handling the difference between predictions and calculated estimations of effective CO 2 emissions. Enabling quotes would allow Cloud providers to bill the CO 2 emissions of a Cloud VM to the final user.

PROPOSED ARCHITECTURE

Figure 1 presents the high level architecture for enabling a provider to attribute CO 2 emissions to endusers. This system allows users to access information about resource usage (past and present), CO 2 emissions (estimated and attributed) for the VMs they run, and to quotes for CO 2 emissions that will be attributed to their future usage. Moreover, external services named Third Party Cloud Brokers can select platforms emitting the smallest amount of carbon between several Cloud providers to execute an application. In order to accurately predict the carbon emissions, the system needs to compute current and historical data. The current data is retrieved by communicating with the Infrastructure Monitoring Service and Third Party Information Services components. The historical data comes from the Database and Third Party Information Services. These components are presented in details below.

Infrastructure Monitoring Service

The Infrastructure Monitoring Service accesses the underlying hardware and software infrastructure which belongs to the Cloud provider. Thus, it knows the hardware data of each server: its energy efficiency, its availability and down times (planned and unexpected). As for the software infrastructure, it collects the amount of resources used by each VM. It is used to compute a cost per resource type as presented to the user.

Third Party Information Services

To increase the accuracy of the carbon emissions prediction, the model gathers information from external services. They can be of different types and sources. The electricity power grid service provides information about the current Carbon Intensity Factor (CIF). The CIF represents the amount of carbon emitted for a given quantity of electricity provided by the power grid. The value of CIF varies over time depending on the electricity's origin (renewable or not). Other information sources can be used depending on the electricity used. For instance, weather forecast services can help predicting the production of solar panels.

Application Programming Interface

The Application Programming Interface (API) gives clients access to resource usage metrics for their VMs. It also provides a quote system that informs the clients about the CO 2 emissions that will be attributed to their VMs. The quote system publishes the period for which the quote is valid, binding the Cloud provider to attribute CO 2 emissions according to that quote. This allows clients, who are in control of resource usage (i.e. they can deploy additional VMs), to predict CO 2 emissions that will be attributed to their usage, enabling them to make provisioning decisions based only on parameters under their control.

Database and Data Mining Information

The data from the Infrastructure Monitoring Service and Third Party Information Services is gathered and stored in the Database. The former stores static information such as the energy efficiency of servers as well as non-static information such as planned down time of servers. The Database also saves periodically information about the current CIF value and the other third party-related information.

The Data Mining Information provides the data needed by CO 2 Emission Predictor. It can give the variation trend of the CIF associated to a specific time period for instance.

CO 2 Emissions Predictor

In order to offer quotes, the provider must be able to forecast resource usage and energy provisioning. The forecast and quote calculations are based on a mix of current data and historical data patterns retrieved by mining data stored in the Database. For example, records such as the past variation trend of the CIF for a specific time period can have a significant impact on the accuracy of the prediction. Prediction accuracy can also be increased by including factors that have an effect on CO 2 emissions. Such factors can be seasonal changes or the prediction of green energy availability (wind energy, solar energy).

Internal information is as important as external information. The Infrastructure Monitoring Service component allows to figure out which servers are likely to be available to satisfy a request and their CO 2 footprint. Some servers may be less energy efficient and therefore have a greater carbon footprint. The past carbon emission attribution is gathered from the Database records. Users can ask for a collection of their historical carbon emissions for a specific time period. After data is retrieved from the Database, the collection is created and sent to the user through the API.

The prediction algorithm is left to Cloud providers' discretion as it is part of the market-based incentive. They can indeed choose to underestimate or to overestimate their CO 2 emissions predictions at some point in order to attract clients. The difference between the billed cost (depending on the predictions and policy of the Cloud provider at a given time) and the real cost is managed by the CO 2 Capital.

CO 2 Capital

At the infrastructure level, the provider can measure the total power consumption, and using external sources, the total CO 2 emissions attributable to its infrastructure. Comparing this latter value with the sum of CO 2 emissions attributed to users provides a way to measure the difference induced by the Cloud policy. These differences are accumulated over time in the CO 2 Capital. In order to keep this capital under an acceptable threshold, it can be taken into account by the prediction algorithm, or by a business policy (not described in the architecture) sitting between the API and the Predictor. Please note that this capital can be negative when estimation is too high and thus users are attributed more CO 2 emissions than attributable to the infrastructure.

Architecture Difficulties

The architecture presented in this paper relies on the capacity to get real-time information about the energy sources and their CO 2 intensity at the level of each Cloud infrastructure. While it is quite easy to get that information country-wide or to rely on contractual promises made by the energy provider, it might be difficult in practice to get that information in the general case. Indeed, some green energy accounted for in the country-wide energy mix will probably already have been sold as such.

A second issue with this architecture is that it does not include a mechanism to protect an infrastructure provider from users massively changing their behavior to adapt their workload to the current quote for CO 2 emissions. This in turn would impact the accuracy of the workload prediction component of the CO 2 Emission Predictor, always increasing the error made during prediction. Some form of user behavior modeling might be necessary to be able to keep predictions accurate, or some business model component to link quotes to clients using Service Level Agreements and base quotes not on periods but on expected resources usage.

Certification

The presented architecture exhibits good properties only if the CO 2 Capital stays very low. This is what ensures that globally all CO 2 emissions estimated for the infrastructure are passed on to users.

On the one hand, it seems relatively easy to accurately measure power consumption at the infrastructure level, using the same perimeter as in PUE calculations, and to certify that value. In the same vein, a certification authority could independently monitor power sources, and certify the CO 2 emissions that need to be attributed to users.

On the other hand, getting a certifiable view of all CO 2 emissions attributed to users is more complex. Some form of publicly auditable record of CO 2 emissions attributed to every client must be made available, raising confidentiality issues. Some form of block-chain usage might help here [START_REF] Swan | Blockchain: Blueprint for a new economy[END_REF].

The difference between the CO 2 emissions to attribute and those attributed to clients builds up over time in the CO 2 Capital. Further work is needed to understand the properties required for the CO 2 capital so as to limit side effects in the way CO 2 emissions are attributed.

At a global scale, our initial thoughts are that the CO 2 Capital must stay within a few percent of total CO 2 emissions over a year. Maybe a higher threshold should be required at the scale of a week, a month, etc. Another threshold could be set per client, so that eco-aware clients do not benefit from the presence of other users that don't care about CO 2 emissions. This would avoid shifting all CO 2 emissions to clients that do not report their carbon footprint, so as to offer unrealistic reports to eco-aware clients.

Quotes and Business logic

We have said very little until now about the contents of quotes, other than the fact that they give users the amount of attributed CO 2 per unit of usage of resources over a period of time in the future. We anticipate that providers might want to offer different quotes for different periods, different quotes for different VM sizes, or for different hardware zones or regions. The provider could even attempt to sell at a higher price usage of the part of energy he gets from renewable sources, in an attempt to partition its user base between clients for which environmental impact is important and others. As long as it can stay certified while doing this, it is possible, thus enabling a dynamic and competitive eco-system of eco-aware providers.

VM CO 2 emissions

As seen in the related work, the literature has focused on modeling the power consumption of a single VM. These models are seldom able to take into account the infrastructure costs of the VM, for example, the amount of unusable memory on the VM's host because of the effective size of the VM.

With the presented architecture, it only important to have an accurate enough VM power model so that the clients have little opportunity to change their behavior to beat the system to be attributed less CO 2 emissions than the system would do. It is important to note that there is no value for real CO 2 emissions. The difference does not lie between an objective value measured after the fact and the value attributed to a VM according to the quote given to the client by the provider. It lies between the value attributed to a VM and calculated using the power model at the VM level and the one using the power model at the infrastructure level. As the complete model takes into account the infrastructure contribution to power consumption, and that the quote system does not, there are optimization opportunities for clients.

Because the optimization opportunities come from infrastructure costs more than from inaccurate power modeling, the focus of an infrastructure provider should be to make its infrastructure energy proportional, rather than to provide accurate VM power modeling.

Passing the cost up to the end-user

We have discussed here how CO 2 emissions are attributed to VMs by the infrastructure provider. Because the VM user has the ability to predict CO 2 emissions as she knows in advance how they will be computed from resource usage counters, she has the ability to apply the same techniques to pass the costs up to the different users of her VMs. This can be applied recursively up to the end user, who is then empowered with information about the CO 2 emissions attributed to her usage of computing resources.

CONCLUSION

We present in this paper an architecture that allows users of a Cloud infrastructure to have predictable CO 2 emissions attributed to their usage while taking into account the difference between predictions and estimations of effective CO 2 emissions. If this difference is kept under a pre-defined threshold, it opens the way to an eco-system where infrastructure providers can be certified as providing reasonable CO 2 emissions certificates to users while at the same time giving predictability to users. This creates a fair playing field where infrastructure providers compete to attract eco-aware users in a way such that the complete infrastructure costs are taken into account. This should increase the adoption of green technologies in all aspects of datacenter provisioning and therefore, contribute to limiting the impact of IT on GHG.

Figure 1 :

 1 Figure 1: High level architecture of a CO 2 emissions accounting framework

DISCUSSIONIn this section, we discuss the pitfalls to avoid for implementing the proposed accounting framework.

ACKNOWLEDGEMENTS

This work has been supported by the ECO2Clouds project (http://eco2clouds.eu/) and was partially funded by the European Commission under grant agreement number 318048.