Cosimo Laneve
email: cosimo.laneve@unibo.it

Michael Lienhardt
email: michael.lienhardt@onera.fr

Ka I Pun
email: ka.i.pun@hvl.no

Guillermo Román-Díez
email: guillermo.roman@upm.es

Time analysis of actor programs ✩

Keywords:

This paper proposes a technique for estimating the computational time of programs in an actor model, which is intended to serve as a compiler target of a wide variety of actor-based programming languages. We define a compositional translation function returning cost equations, which are fed to an automatic off-the-shelf solver for obtaining the time bounds. Our approach is based on a new notion of synchronization sets, which captures possible difficult synchronization patterns between actors and helps make the analysis efficient and precise. The approach is proven to correctly over-approximate the worst computational time of an actor model of concurrent programs. Our technique is complemented by a prototype analyzer that returns upper bound of costs for the actor model.

Introduction

Time computation for programs running on mainstream architectures, for example, multicore, distributed systems or cloud, is intricate and demanding as the execution of a process may be indirectly delayed by other processes running on different machines due to synchronizations. The computational time of programs is particularly relevant in cloud architectures, where services are bound by so-called service-level agreements (SLAs), which regulate the costs in time and assign penalties for their infringements [START_REF] Buyya | Cloud computing and emerging IT platforms: vision, hype, and reality for delivering computing as the 5th utility[END_REF]. In particular, the service providers need guarantees that the services meet the SLA, for example in terms of the end-user response time, by deciding on a resource management policy, and by determining the appropriate number of virtual machine instances (or containers) and their parameter settings (e.g., their CPU speeds).

In this paper we propose a technique for estimating the computational time of programs in an actor model. This model is intended to serve as a compiler target of a wide variety of actor-based programming languages, such as object-oriented ones, including Java and C#, which are used in cloud architectures. Our technique aims at (and in fact, has been developed for) helping service providers to select resource management policies in a correct way, before actually deploying the service.

Several techniques have been proposed for analyzing the computational time of sequential programs. See for example [START_REF] Albert | Cost analysis of object-oriented bytecode programs[END_REF][START_REF] Brockschmidt | Alternating runtime and size complexity analysis of integer programs[END_REF][START_REF] Gulwani | Speed: precise and efficient static estimation of program computational complexity[END_REF][START_REF] Hoffmann | Multivariate amortized resource analysis[END_REF][START_REF] Wegbreit | Mechanical program analysis[END_REF] and Section 7. Our approach is similar to [START_REF] Morrisett | From system f to typed assembly language[END_REF], where a statically typed intermediate language has been defined in order to verify safety properties and certify code optimizations. Different from [START_REF] Morrisett | From system f to typed assembly language[END_REF], our language, called alt, short for actor language with time, is concurrent, and contains an operation defining the number of processing cycles required to be computed, called wait(n) (similar to the sleep(n) operation in Java). In order to analyze the computational time of alt, we define an algorithm that returns a set of cost equations that are adequate for a solver. We demonstrate that the solution of the cost equations over-approximates the computational time of the alt program in input. Given these results, estimating the computational time of a program in some programming languages amounts to defining a compilation into an alt program (and demonstrating its correctness).

The presented work builds upon a previous article by the authors [START_REF] Giachino | Time complexity of concurrent programs[END_REF], where it captures the actor models of actor-based programming languages in terms of behavioral types, and obtains the computational time of the corresponding program by feeding the cost equations produced by a translation function to a off-the-shelf solver, namely the CoFloCo solver [START_REF] Montoya | Resource analysis of complex programs with cost equations[END_REF].

However, this technique proposed in [START_REF] Giachino | Time complexity of concurrent programs[END_REF] has a very severe constraint: invocations were admitted only either on the same actor or on newly created ones, i.e., no invocation on parameters. For instance, according to this constraint, an invocation to a method inner(y, x), where the first parameter is the actor executing the method, cannot occur in the body of a method outer(x, y). The challenge is that, in this case, computing the cost of outer(x, y) requires to know whether there is a synchronization between actors x and y. In case there is, one has to consider that inner(y, x) might be delayed by other methods running on y, which might be independent from outer(x, y).

This paper focuses on overcoming this issue. We first compute synchronization sets of actors, which are actors that potentially might interfere with the executions of each other. We then compose the cost of an invocation with the cost of the callee in two ways: [START_REF] Albert | SACO: static analyzer for concurrent objects[END_REF] it is added, corresponding to sequential compositions, if the arguments of the invocation and those of the caller are in the same synchronization set; (2) it is the maximum value, corresponding to parallel composition, otherwise.

We then define a new translation function that takes the synchronization sets of an alt program into account and returns the corresponding set of cost equations.

The translation of alt programs into the solver input code [START_REF] Albert | Closed-form upper bounds in static cost analysis[END_REF][START_REF] Montoya | Resource analysis of complex programs with cost equations[END_REF] has been prototyped and can be experimented (see Section 6). This tool, together with the compiler we have defined in [START_REF] Giachino | Time complexity of concurrent programs[END_REF], allows us to automatically compute the cost of programs in ABS, a prototype language for programming the cloud [START_REF] Johnsen | ABS: a core language for abstract behavioral specification[END_REF] that is an extension of alt. Experimental results show that our technique is very precise when computing the cost of a number of typical distributed patterns, such as fork-join or map-reduce.

Paper overview. The alt language is defined in Section 2 and we discuss in Section 3 the issues in estimating the computational time. Section 4 explains the analysis of computational time by means of a translation function that returns cost equations, and Section 5 discusses the properties of the translation. In Section 6, we illustrate the conversion of the translation output to the adequate form for an off-the-shelf solver, present our prototype, together with the experimental results of our approach and a comparison with other tools. In Section 7, we discuss the related work and deliver concluding remarks in Section 8.

The language alt

In this section, we define the syntax and the semantics of alt and illustrate the language with some examples.

Syntax. We use several disjoint sets of names that, for convenience, we address taking different notations or identifiers: method names, ranged over by m, m , • • • ; actor names ranged over by x, y, • • • ; natural names u, w, a, b, • • • ; future names ranged over by f , g, h, • • • . The notations x and u denote a possibly empty sequence of actor and natural names, respectively; p ranges over sequences whose elements may be either actor or natural names. An alt program

m 1 (p 1 ) = s 1 , • • • , m n (p n ) = s n , main(x, u) = s
is a sequence of method definitions of the form m i (p i ) = s i . The last method is the main method, where x is the actor name executing the main body and u are natural names. Statements s and expressions e are defined by the following syntax: The syntax of alt statements is quite basic: 0 indicates a terminated statement; νx is the creation of a new actor x; ν f : m(e);s creates a new task of the method m that is associated to the future f ; the task starts in parallel with the continuation s. The term f performs the synchronization of the task associated to f . This may cause the (busy) waiting for the termination of the task. The statement wait(e n ), where e n is a natural expression, represents the advance of e time units. This is the only term in our model that consumes time (a.k.a. that generates a cost). Note that term e n in wait(e n ) contains constants and natural names, including the arithmetic binary operator + between them. These expressions are also known as Presburger arithmetics, which is a decidable fragment of Peano arithmetics containing only addition.

The restriction is necessary because the analysis in Section 4 cannot deal with generic expressions. Note that, in general, expressions e also include actor names (in the syntax of e, x also ranges over actor names), as in the method invocations.

Method definitions have the form m(p) = νz 1 ; • • • ;νz k ;s such that all actors can only be created in the beginning of the method. Additionally, the method definition m(p) = s binds names p to the body s. We assume that p has always a fixed pattern: p = x, y, u, namely p is a nonempty sequence where the first element is always an actor name indicating the callee of the method, y are actor names and u are natural names. We assume that actor names x, y do not clash with names z 1 , • • • , z k . Therefore, method invocations ν f : m(e) have the pattern x , y , e . We further assume that alt has a simple type system that verifies the type correctness of method applications. Statements νx;s and ν f : m(e);s link the names x and f in the continuations s. For the notion of bound name and the one of free name, we use the standard operations of alpha-conversion and substitution. It is also assumed that method names m 1 , • Consider method main which is executed by actor x. Note that this actor is automatically created when the main method starts to run. After creating two actors y and z at line 2, main invokes timer(y, a) and continues its execution. By binding this invocation to the future name f and synchronizing it immediately afterwards at line 4, it is possible to delay the execution of the caller actor x until the termination of timer(y, a). In this case, since y has been just created, it will immediately execute timer(y, a) and return (this is not true in general because y might have other tasks running).

Therefore, x will wait exactly a time units (effect of the instruction wait(n) at line 16) before continuing. The continuation spawns a task ν g: timer(z, b) at line 5 on actor z and waits for its termination, which, for the same reasons as before, will occur after b time units. Overall, the computational time of main is a + b. Observe that the time is the same when line 5 is replaced by ν g: timer(y, b), e.g., spawning the thread on y instead of z.

In the case of main , the two invocations to timer are performed one after the other, without any synchronization in between. Thus the two tasks are executed in parallel, and as they are both synchronized at lines 12 and 13, the computational time of main is max(a, b). Observe that if line 11 is replaced by ν g: timer(y, b), e.g., spawning the thread on y instead of z, the computational time becomes a + b. 2

Two features of alt ease our theoretical development: (i) alt actors are stateless and (ii) methods do not return values.

In fact, computing the cost of stateful actor programs requires a leap of the theory developed in this contribution because it is necessary to trace the state of the fields. Similarly, when methods return a value, it is necessary to estimate the value (is it an old actor or a new one? if it is a natural number, how large it is?) in order to have sensible cost computations.

Semantics. The semantics of alt is a transition system whose states are configurations cn that are defined as follows.

cn ::= act(x, p, q) | fut( f , val) | invoc(x, f , m, v) | cn cn val ::= ⊥ | p ::= s; f | f | 0 v ::= x | f | k q ::= ∅ | s; f | q q
The notation s; f represents the statement s where the tailing 0 is replaced by the future name f . We use p to range over s; f , f , and 0. A configuration cn is a nonempty set of actors, invocation messages and futures. The associative and commutative union operator on configurations is denoted by whitespace. An actor is written as act(x, p, q), where x is the identity of the actor, p is the active task, and q is a pool of either suspended or waiting tasks. An invocation message is denoted as invoc(x, f , m, v), where x is the callee, f the future to which the call is bound, m the method name, and v the set of parameter values of the call. Configurations also include futures, denoted as fut( f , val), where f is the future identity and val indicates whether f has already been computed, written as , otherwise ⊥.

The transition rules of alt are given in Fig. 1. We use an auxiliary function to bind invocations to the corresponding method bodies. Let m(x, z) = s be an alt method. Then bind( y, m, v) = s{ y, v / x, z } .

(Context) cn → cn cn cn → cn cn (New) z = fresh( ) act(x, νz;p, q) → act(x, p{ z / z }, q) act(z , 0, ∅) (Get-True) act(x, f ;p, q) fut( f , ) → act(x, p, q) fut( f , ) (Get-False) act(x, f ;p, q) fut( f , ⊥) → act(x, 0, q ∪ ( f ;p)) fut( f , ⊥) (Async-Call) [[e]] = v f = fresh( ) act(x, ν f : m(z, e);p, q) → act(x, p{ f / f }, q) invoc(z, f , m, v) fut( f , ⊥) (Bind-Fun) s = bind(x, m, v) act(x, p, q) invoc(x, f , m, v) → act(x, p, q ∪ s; f ) (Wait-0)
[[e]] = 0 act(x, wait(e);s, q) → act(x, s, q) We also use the function fresh( ) to return either a fresh actor name or a fresh future name. Finally, we use an evaluation function [ [•] ] of expressions e such that [ [x] ] = x, and [ [e] ] = v whenever e is a constant natural expression and v is its value;

(Activate) act(x, 0, q ∪ p) → act(x, p, q) (Return) act(x, f , q) fut( f , ⊥) → act(x, 0, q) fut( f , ) (Tick) strongstable t (cn) cn t → (cn, t)
[ [e] ] is undefined otherwise. The semantics of alt is almost standard. See, for example [START_REF] Laneve | Foundations of web transactions[END_REF], for a similar semantics for a dialect of pi-calculus with time. We discuss the most relevant rules in the following: actor creation, method invocation, method return and the wait(e) statement.

Actor creation is handled by rule New, which extends the configuration with act(z , 0, ∅) where z is a fresh actor identifier. In alt, method invocations are asynchronous: rule Async-Call creates a new invocation predicate invoc(z, f , m, v) and a new unresolved future predicate fut( f , ⊥), which is associated to the invocation with a fresh future identifier f . The invocation predicate will then be bound to the corresponding callee actor as one of the tasks in the task pool (cf. rule Bind-Fun). When a method terminates, rule Return sets the value of the corresponding future f to . Note that f is added to the end of the method body in rule Bind-Fun. In our model, wait(e) is the unique operation that consumes time; that is, time does not advance as long as a wait(e) statement is prefixed by some active task. For the trivial case where e = 0 (see rule Wait-0), the statement is simply discarded. On the contrary, when a configuration cn reaches a stable state, that is, no other transition is possible apart from those evaluating the wait(e) statements, time advances until an actor with a non-wait(e) statement can proceed. To formalize this semantics, we first introduce the notion of stability as follows:

Definition 2.1. Let t > 0. A configuration cn is t-stable, written as stable t (cn), if every actor in cn matches one of the following forms:

1. act(x, wait(e);s; f , q) with [ [e] ] ≥ t, 2. act(x, 0, q) and i. either q = ∅, ii. or, for every s ∈ q, s = f ;p and fut( f , ⊥) ∈ cn.

A configuration cn is strongly t-stable, written as strongstable t (cn), if it is t-stable and there exists an actor act(x, wait(e);s, q) with [ [e] ] = t.

Note that t-stable (and consequently, strongly t-stable) configurations cannot progress anymore because every actor is stuck either on a wait(•)-statement or on an unresolved future.

We then define a function to update a configuration cn with respect to a time value t.

(cn, t) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎩ act(x, wait(k);s, q) (cn , t) if cn = act(x, wait(e);s, q) cn and k = [[e]] -t act(x, 0, q) (cn , t)
if cn = act(x, 0, q) cn cn otherwise.

Together with the rule Tick in Fig. 1, we define the time progress of a configuration.

The initial configuration of a program whose main method is main(x, u) = s and with invocation main(z, k) is

act(z, s{ k / u }; f start , ∅)
where f start is the future identifier for the main body. As usual, → * is the reflexive and transitive closure of → and

t ⇒ is → * t →→ * . A computation is cn t 1 ⇒ • • • t n
⇒ cn , that is, cn is a configuration reachable from cn with either transitions → or t ⇒. When the time labels of transitions are not relevant we also write cn ⇒ * cn .

Definition 2.2. The computational time of cn

t 1 ⇒ • • • t n ⇒ cn is t 1 + • • • + t n .
The computational time of a configuration cn, written time(cn), is the maximum computational time of computations starting at cn. The computational time of an alt program is the computational time of its initial configuration.

Example 2.2. Consider the following method main 1 : This method creates a new actor y at line 2 and spawns two tasks on it at lines 4 and 6, respectively, where the two tasks will execute in parallel with main 1 . Their terminations are synchronized at lines 8 and 9 by means of g and f . Note that main 1 takes its natural number arguments as the input parameter of the wait(•)-operations at lines 5 and 7, while the one at line 3 uses a constant k 0 . Thus, the computational time of main 1 depends on the concrete values of a and b. The other wait(•)-statements in the example are executed with some constants k 0 , k 1 and k 2 . 2

1 main 1 (x, a, b) = 2 ν y; 3 wait(k 0 ); 4 ν f : m 1 (y);
Our semantics does not exclude behaviors of methods that perform infinite actions without consuming time (preventing rule Tick to apply), such as foo(x) = ν f : foo(x); f . This kind of behaviors are well-known in the literature (cf. Zeno behaviors, see [START_REF] Laneve | Foundations of web transactions[END_REF]) and they may be easily excluded from our analysis by constraining recursive invocations to be prefixed by a wait(e)-statement, where e is a not-zero natural. A similar paradoxical behavior is gee(x) = ν y;ν f : gee(y); f that spawns the new task on a new actor, thereby creating an unbounded number of actors.

We finally remark that the composite effect of Activate and Get-False might produce infinite computations that do not make progress, and no time is passing (an actor can repeatedly activate a blocked task and then suspend it again). However, assuming fairness in computations (an enabled task will eventually be executed), it is possible to demonstrate that these behaviors are not possible in alt.

The challenges of cost computation for alt programs

Computing the time of alt programs is challenging. In this section, we illustrate the difficulties by discussing four examples. These difficulties range from determining the tasks that cannot execute in parallel -therefore the cost of each of these tasks must be added together -, to understanding the tasks that are executed in parallel -thus, the maximum value of the cost of the tasks is selected -or to analyzing the whole spectrum of scheduling policies because they might also affect the computational time. Computation 1 represents an execution where a > k 1 , which leads to the execution of m 2 on actor y starts after the termination of m 1 . In this case, the executions of wait(b) and m 2 run in parallel. Thus, the cost of this computation is k 0 + a + max(b, k 2 ) (the expression c 1 in the figure reflects the case where b ≥ k 2 ). Computation 2 and Computation 3 describe computations where a < k 1 . This leads to delaying m 2 until the execution of m 1 finishes. In Computation 2, since a + b < k 1 + k 2 , actor x has to wait for the termination of m 2 . On the contrary, in Computation 3, m 2 returns before actor x finishes the execution of wait(b). Finally, Computation 4 illustrates an execution where both x and y have to wait either for a method to terminate and return or for executing a new task.

As our analysis aims at finding a sound approximation of time needed for any computation of the program, the cost of main 1 is over-approximated by the expression

c main 1 = k 0 + max(a, k 1 ) + max(b, k 2 )
For Computation 1, Computation 2 and Computation 4, c main 1 captures precisely the execution time. Note that the subexpression k 0 + max(a, k 1 ) determines the starting time of m 2 on actor y. However, k 0 + max(a, k 1 ) is an over-approximation of the starting time of the statement wait(b) at line 7 of main 1 , ending up in a non-precise result for Computation 3 as

c main 1 > c 3 . 2
Another challenging issue to cope with is when a task is delayed due to an unresolved future (see rule Get-false). In this situation, the carrier actor may start the execution of the pending tasks and may reschedule the initial task after the termination of the other ones.

Example 3.2. Consider following method main 2 , which is similar to main 1 in Example 2.2, except that m 2 is invoked on the callee actor x. The computations on the right show two possible executions of main 2 , depending on the values of a and b.

In Computation 1, the synchronization g at line 8 happens before m 1 terminates. In this case, the cost of executing m 2 does not contribute to the overall cost c 1 . On the contrary, in Computation 2, the cost of executing m 1 does not contribute to the overall cost c 2 . The reason is that the values of a and b in this computation are larger than Computation 1, which consequently results in longer time for executing wait(a), wait(b) and m 2 (i.e., wait(k 2 )) on actor x than m 1 on actor y. The expression

c main 2 = k 0 + max(a + b + k 2 , k 1 )
captures the worst case computational time of main 2 , which over-approximates c 1 and c 2 . 2

A more complex scenario can be illustrated by having two actors x and y spawning tasks on a third actor z. In this case, the execution of tasks on x and y may delay the starting time of those spawned on z. As a consequence, it may lead to the postponement of the synchronizations on x and y. Determining the delays of synchronizations is crucial, as discussed in the following example.

Example 3.3. Consider the following method main 3 that creates two actors y and z at line 2, then invokes m 3 on y at line 4 and m 1 on z at line 6. The actor z is given as a parameter in the invocation of m 3 (line 4) and becomes the carrier of m 2 (line 18). In Computation 1, the cost is the sum of the costs of the wait(•) statements in main 3 . This cost does not include the cost of any task executed on y and z as they are running in parallel with main 3 without any delay.

Computation 2 combines the costs from actors x and z but not from y because a > k 2 + k 3 . Observe that the time needed to start m 1 is determined by the expression k 0 + a; observe also that wait(k 3 ) and wait(k 2 ) execute sequentially although they run on different actors (y and z). Note that, wait(b) and wait(k 1 ) are executed in parallel on x and z, and since k 1 > b, the maximum cost is expressed as

c 2 = k 0 + a + k 1 .
In Computation 3, we assume a < k 3 such that the execution of m 1 on z starts before the invocation of m 2 on z. Thus, the execution of m 2 is delayed until m 1 has finished. The cost of Computation 3 is calculated by the expression

c 3 = k 0 + a + k 1 + k 2 .
Computation 4 highlights a possible dependency among tasks executed on actors y and z. The cost expression for this

case is c 4 = k 0 + k 3 + k 2 + k 1 ,
describing a sum to which all three actors contribute (k 0 on x, k 3 on y and k 2 + k 1 on z). The reason is that a > k 3 where the statement wait(k 3 ) on y (line 17) directly determines the starting time of m 2 on z, and which in this case delays the execution of m 1 on z as a consequence.

One remarkable difference between Computation 2 and Computation 4 is the time taken before starting m 1 on actor z. In Computation 2, the cost k 0 + k 3 is smaller than k 0 + a, causing that m 2 is executed before m 1 on z. When there are two actors whose tasks could be dependent on each other, their costs must be considered as if the tasks are executed sequentially, that is, their costs are summed up. Thus, the relation between the tasks executed on y and on z must be considered in order to over-approximate all possible computations of main 3 . Considering all possible values of a and b, the cost expression that over-approximates the cost of executing main 3 is

c main 3 = k 0 + max(a, k 2 + k 3 ) + max(b, k 1 )
Observe that c main 3 precisely approximates the overall cost of Computation 2 and Computation 4. However, to safely approximate the latest starting time of m 1 in case a > k 3 , the subexpression max(a, k 2 + k 3 ) returns k 2 + k 3 . Thus, we have that c main 3 > c 3 , indicating that this expression is over-approximating the cost of Computation 3. Similarly, Computation 1 is also over-approximated by c 3 as it captures that the starting time of m 1 is k 0 + k 2 + k 3 , when its starting time is k 0 + a. 2

This last example suggests that, when a method invocation has several actors as arguments, the pools of pending tasks of these actors can have implicit and possibly complex dependencies, i.e., each of them may in principle affect the task pools of the others by delaying the execution of the tasks therein. We say that these actors belong to the same synchronization set. It is crucial to note that this synchronization relation is transitive. For instance, if x and y belong to the same synchronization set at a program point and if a new synchronization relation between y and z is established by a subsequent invocation, then actors x, y and z belong to the same synchronization set as well.

The final example illustrates how the scheduling might also affect the computational time of the alt programs.

Example 3.4. The following example shows the method main 4 that spawns three tasks in actor y in parallelm 1 , m 2 and m 3 -that will be in the pool of pending tasks of y. In turn, m 3 spawns m 4 in a newly created actor z.

We have also highlighted two possible computations of main 4 . Computation 1 illustrates an execution where task m 2 is scheduled before m 3 . Therefore, the execution of m 4 , spawned by m 3 , is executed when m 2 is finished. This scheduling leads to the computational time c 1 that adds the cost of all methods. Additionally, note that different scheduling orders in y affect the execution of m 4 in z. On the contrary, in Computation 2 the execution of m 3 is scheduled before m 2 . In this case, after executing wait(k 3 ) at line 16, m 4 is spawned and its return is synchronized at line 18. Note that, as m 2 is in the pool of pending tasks of y, it will be executed in parallel with m 4 . The computational time of Computation 2 will be smaller:

c 2 = k 0 + k 1 + k 3 + max(k 2 , k 4 ).
For this program, the expression that over-approximates the cost of executing main 4 needs to sum up the cost of all methods:

c main 4 = k 0 + k 1 + k 2 + k 3 + k 4
Since our technique is sound (see Section 5 for details), i.e., it returns an over-approximation for every possible computational time, it takes into account every scheduling order when multiple tasks can be pending in the same pool. 2

The analysis of alt programs

This section defines the translation of an alt program into a cost program, i.e., a set of cost equations m(u) = exp, where m is a (cost) function symbol and exp is an expression that may contain (cost) function applications of the form:

exp ::= k | u | exp + exp | m(e) | max(exp, exp)
In particular, cost expressions are additions of the following type of elements: natural numbers k, natural names u, m(e) which refers to the cost of executing method m, but only considering the natural expressions in e; or max(exp, exp ), which returns the maximum between two cost expressions exp and exp .

Given an alt program P, the analysis iterates independently over each method definition m(x, y, u) = s in P and translates it into a cost equation of the form m(u) = exp, where m corresponds to the method name m and exp encodes a cost function which corresponds to an upper bound of the time executing m, with respect to the numerical parameters u. As hinted in our examples, the analysis performs this translation by studying the task pool of every actor involved in the method's execution, identifying an upper bound for the ending time of each of its tasks, which in turn give raise to an upper bound to the computational time of the method itself.

In order to manage the complexity of studying task pools and the different scheduling possibilities as described in Section 3, our analysis uses two major structures, synchronization schema and accumulated costs. The synchronization schema of a method gives the synchronization set of every actor involved in that method's body. As described in Example 3.3, actors in the same synchronization set interact outside the scope of the analyzed method, which means that the ending time of a task in one actor's task pool depends somehow on the task pools and its scheduling orders of other actors in the same synchronization set. The analysis over-approximates this implicit dependency by considering the pools of all these actors as if they were one unique pool. An accumulated costs is an abstraction of a task pool used to get a good upper bound for the ending time of a computation. The main difficulty in identifying such an upper bound is to determine the starting time of a computation, which depends on the state of the task pool itself and on the time at which the corresponding method call was performed.

Synchronization schema

A synchronization set, ranged over by A, B, • • • , is a set of actor names whose tasks have implicit dependencies, that is, the tasks of these actors may reciprocally affect the task pools of the other actors in the same set by means of method invocations and synchronizations. A synchronization schema, ranged over by S, S , • • • , is a collection of pairwise disjoint synchronization sets. The synchronization schema of a method m is thus a partition of the actors used in that method into synchronization sets and is constructed as follows.

Definition 4.1 (Synchronization schema function).

Let S be a synchronization schema and s be a statement. Let

sschem(S, s) = ⎧ ⎨ ⎩ S ⊕ {y , z} if s = ν f : m(y , z, e) sschem(sschem(S, s ), s ) if s = s ;s S otherwise where S ⊕ A = ⎧ ⎨ ⎩ A if S = ∅ (S ⊕ A) ∪ A if S = S ∪ A and A ∩ A = ∅ S ⊕ (A ∪ A) if S = S ∪ A and A ∩ A = ∅
Let be an alt method definition. The synchronization schema S m , where m(x, y, u) = νz 1 ; • • • ;νz k ;s, is the set S m = sschem({{x, y}}, s). The term S(x) denotes the synchronization set, which contains x, in the synchronization schema S.

The function S ⊕ A merges a schema S with a synchronization set A. If none of the actors in A belongs to a set in S, the operation reduces to a simple set union. For example, let S={{x, y}, {z, w}}. Then S ⊕ {x, v} is equal to ({{x, y}} ⊕ {x, v}) ∪ {{z, w}}, which equals {{x, y, v}, {z, w}}. It is worth to observe that the same result follows by swapping {x, y} and {z, w} (because elements of S are disjoint). In fact {{z, w}} ⊕ ({x, y} ∪ {x, v}) = {{x, y, v}, {z, w}}.

The synchronization schema sschem(S, ν f : m(y, z)) = {{x, y, z, w}} indicates that all the actors are in the same synchronization set. On the contrary, sschem(S, ν f : m(x, v)) = {{x, y, v}, {z, w}}, because actors x, v do not belong to {z, w}.

We also compute S main , where main(x, a, b) = ν y;ν z;ν w;s main is the main method in Fig. 2. This schema is equal to {{x}, {y, z}, {w}}, that is the task pools of actors y and z may affect each other due to the invocation at line 8, whereas the task pools of x and w are independent from the rest. Observe that, as the body of m 3 does not contain actor creation statements, its synchronization schema is a singleton set that containing only its parameters, e.g., S m 3 = {{y, z}}.

Accumulated costs

In order to define (an over-approximation of) the time advancements of tasks in a same pool -e.g. in a same synchronization set -we use an extension of the syntax of exp, called accumulated cost and noted ε, which is defined as follows:

ε ::= exp | ε • m(e), exp | ε exp .
The term exp defines the starting time of a task invoked in an actor that does not belong to the same synchronization set of the carrier. Let this carrier be x in the discussion below and consider an actor y that resides in a different synchronization set than that of x. The term ε • m(e), exp represents the starting time of a method invoked on actor y. For example, when x invokes a method m on y using ν f : m(y, z, e), the accumulated cost of the synchronization set of y is ε • m(e), 0 , where ε is the cost up to that point. Time advancements in the task of the carrier x (e.g., with wait(e )), which affect the starting time of subsequent method invocations on y, is expressed by adding e to exp; namely, ε • m (e), exp becomes ε • m (e), exp + e , which means that the starting time of the next method invocation on the synchronization set of y is after the time expressed by ε plus the maximum between m (e) and exp + e . The term ε exp expresses the time advancement in the carrier x when a method running on an actor y in a different synchronization set is synchronized. In this case the time advances by the maximum between the current time exp of x and the time of y, represented by ε.

Following the semantics described above, we can define the function [ [ε] ] that computes the time corresponding to ε, i.e., the (over-approximation of) starting time of the next task in the synchronization set whose cost is ε:

[[exp]] = exp [[ε • m(e), exp ]] = [[ε]] + max(m(e), exp) [[ε exp]] = max([[ε]], exp) Example 4.1.
The following expressions ε i indicate the accumulated costs in actor y for some interesting program points of method main 1 in Example 2.2:

3: wait(k 0 ); ε 3 = 0 4: ν f : m 1 (y); ε 4 = k 0 • m 1 (), 0 5: wait(a); ε 5 = k 0 • m 1 (), a 6: ν g: m 2 (y); ε 6 = k 0 • m 1 (), a • m 2 (), 0 7: wait(b); ε 7 = k 0 • m 1 (), a • m 2 (), b
Note that each task creation in y includes a new tuple in the accumulated cost: m 1 (), 0 in ε 4 and m 2 (), 0 in ε 6 . Note also that time advancements local in the carrier, i.e., actor x in Example 2.2, update the last tuple in the accumulated cost with the corresponding expression: a in ε 5 and b in ε 7 .

Next, consider the expression

ε 7 = k 0 • m 1 (), a • m 2 (), b .
Because of the synchronization g at line 8 of main 1 we obtain the following cost expression:

[[ε 7 ]] = k 0 + max(m 1 (), a) + max(m 2 , b)
that over-approximates the worst possible time when g is synchronized. We observe that k 0 is the computational time when m 1 is invoked, max(m 1 (), a) expresses that m 1 and wait(a) can be executed in parallel (analogously for max(m 2 (), b)) and k 0 + max(m 1 (), a) corresponds to the worst possible starting time of m 2 . It is worth to notice that [ [ε 7 ] ] returns the cost expression c main 1 computed in Example 3.1. 2

The translation function

We have seen how the accumulated costs and their corresponding cost expressions can be computed for a given synchronization set. Interestingly, each synchronization set has its own accumulated cost, thus, for our analysis it is fundamental to keep the accumulated costs separate in order to get precise results. In the following section we define a translate function that computes the cost of a method considering all possible synchronization sets and synchronizations performed on it.

The translation of an alt method m consists of two steps: first (i) the synchronization schema S m is computed, following the technique described Section 4.1, then (ii) the body of method m is analyzed, by parsing each of its statements in order.

The analysis (ii) records the accumulated costs of synchronization sets in translation environments, ranged over by , ,

• • • . Translation environments are maps of the form S m (x) → ε, which relate the different synchronization sets to their corresponding accumulated costs. The auxiliary operators and + are used as follows:

( exp)(S) = (S) exp ( + exp)(S) = ε • m(e), exp' + exp (exp 1 + exp) • • • (exp n + exp) with (S) = ε • m(e), exp exp 1 • • • exp n
Given a synchronization schema S, the translation function, written as translate S (I, , x, l, t, s), takes the following six arguments:

translate S (I, , x, l, t, μ) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (1) (I, + e, l, t + e) when μ = wait(e) (2) (I[ f → S(x)], , l + m(e), t)
when μ = ν f : m(y, z, e) and y ∈ S(x)

(3) (I[ f → S(y)], [S(y) → ε • m(e), 0 ], l, t) when μ = ν f : m(y, z, e) and y / ∈ S(x) ε = (S(y)) if S(y) ∈ dom( ) t otherwise (4) (I \ F , + l, 0, t + l) when μ = f and x ∈ I( f )
where i. I is a map from future names to synchronization sets, ii.

F = { f | I( f ) = S(x)} (5) (I \ F , ( t ) \ I( f ), 0, t ) when μ = f and x / ∈ I( f ) where F = { f | I( f ) = S(x) or I( f ) = I( f )} and t = max(t + l, [[ (I( f ))]]) (6) (I \ F , + l, 0, t + l) when μ = f and f / ∈ dom(I) where F = { f | I( f ) = S(x)}
is a translation environment, iii. x is the name of the carrier, i.e., the actor on which s is executing, iv. l is a cost expression that over-approximates the cost of the methods invoked on actors belonging to the same synchronization set where the carrier x resides and not yet synchronized, v. t is a cost expression that over-approximates the current computational cost, which is the computational time accumulated from the beginning of the method execution, and vi. s is a sequence of statements, representing wait(e), ν f : m(e), or f that must be translated.

and returns a tuple consisting of the four elements:

i. an updated map I , ii. an updated translation environment , iii. an updated the cost of methods running on actors in the same synchronization set as the carrier, and iv. an expression of the updated current computational cost.

The function is defined on statements as follows translate S (I, , x, l, t, 0) = (I, , l, t)

translate S (I, , x, l, t, μ;s) = translate S (I , , x, l , t , s) where translate S (I, , x, l, t, μ) = (I , , l , t )

where translate S (I, , x, l, t, μ) is detailed in Fig. 3. Note that, the difficult case of the translation function is when the statement is a task synchronization f , which is covered by cases (4), ( 5) and ( 6). In the following, we discuss the six cases of Fig. 3 in detail.

Case (1):

When s is a wait(e) statement, the translate function adds the cost e to the current cost t, which is also reflected on the environment by updating the accumulated cost of the method invocations on each synchronization set in .

Cases (2) and (3):

When s is a method invocation on actor y, there are two subcases, depending on whether y is in the same synchronization set of carrier x (Case (2)) or not (Case (3)). In Case (2), the cost of the invocation is added to l and the updated I binds the corresponding future f to S(x). In Case (3), we add the binding from f to S(y) to the map I and update the translation environment by appending the cost of invoking m to the accumulated cost to which S(y) maps. Note that, method invocations only includes the natural expressions used for invoking m, that is, it includes m(e).

Case (4): This is the first sub-case of task synchronization which captures the situation where the synchronization is performed on a method whose callee belongs to S(x). Since it is non-deterministic when the task being synchronized will actually be scheduled, we add the sum of the costs of all the tasks running on actors in S(x), which is stored in l, to the current time t (worst case) at this synchronization point. The translate function then resets l to 0, and removes from I all the corresponding futures since the corresponding costs have been already considered.

3 : ∅, ∅, 0, t 3 [ t 3 = k 0 ] (1) 4 : { f → {x}}, ∅, m 1 , t 4 [ t 4 = t 3 ] (2) 5 : { f → {x}, g → {y, z}}, {{y, z} → t 4 • m 3 , 0 }, m 1 , t 5 [ t 5 = t 4 ] (3) 6 : { f → {x}, g → {y, z}}, {{y, z} → t 4 • m 3 , a }, m 1 , t 6 [ t 6 = t 5 + a ] (1) 7 : { f → {x}, g → {y, z}, h → {w}}, {{y, z} → t 4 • m 3 , a , {w} → t 6 • m 4 , 0 }, m 1 , t 7 [ t 7 = t 6 ] (3) 8 : { f → {x}, g → {y, z}, h → {w}, i → {y, z}}, {{y, z} → t 4 • m 3 , a • m 2 , 0 , {w} → t 6 • m 4 , 0 }, m 1 , t 8 [ t 8 = t 7 ] (3

Case (5):

The second sub-case describes the synchronization that is performed on a task whose callee, say y, does not belong to S(x). As actors x and y reside in different synchronization sets, the invocation on y is executed in parallel with the carrier x. Thus, the overall cost is computed as the maximum between the total cost of all pending invocations on the actors in S(x) to which carrier x belongs, captured by the local cost l, and the cost of all invocations on actors in S(y), denoted by [ [ (S(y))] ]. Since at this point we have considered the worst scheduling, that is, we have already counted the cost of all methods spawned on the actors in S(y) and S(x) so far, we remove from the environment all invocations on the actors in S(y), as well as all the futures associated to S(y) and S(x) from I .

Case (6):

In this case, the future f does not belong to I , which implies that the cost of the invocation has been already computed. Nevertheless, it is possible that other methods have been invoked after this computation. Therefore, the actual termination of the invocation corresponding to f may happen after the completion of all the invocations. In order to take this into account, we need to add the cost of those tasks whose callee belongs to S(x), which has been accumulated in l, in a similar way as we have done in Case (4).

We observe that the resulting translation environment n is always empty because every method invocation is always synchronized within the method body. For the same reason, l n is always equal to 0. The following example is used to discuss in detail some relevant aspects of translate.

Example 4.2. Fig. 4 illustrates the application of translate function to main in Fig. 2. The leftmost column states the line of code i of main and we let I i , i , l i , t i refer to the corresponding argument of the function at line i. The second column contains the output tuple of translate function, while the third specifies the calculation of the current cost t i . The rightmost column indicates the case (c i ) of translate function that we have applied. For the sake of clarity, as method calls do not contain numeric parameters, we use m for the cost expression m(_). Note that translate takes the synchronization schema S main = {{x}, {y, z}, {w}} that has been computed in Section 4.1 as input.

At lines 3, 6 and 10, the cost expression t i increases by summing the previous cost expression and the cost of wait(•)-statements at each of these lines (case (1)). A local invocation (case (2)) to m 1 is added to l 4 at line 4 and its corresponding future variable is added to I 4 = { f → {x}}. Lines 5, 7 and 8 contain method invocations on actors not belonging to the carrier's synchronization set, which correspond to case (3) of the translate function. For instance, at line 5 we have the first method invocation on an actor in the synchronization set {y, z}. We then add the bindings g → {y, z} to I 5 and {y, z} → t 4 • m 3 , 0 to 5 , where t 4 corresponds to the accumulated costs of methods invoked on the carrier's synchronization set so far, and the time distance to the subsequent method invocation on the same synchronization is 0. Observe that it is possible to compute the cost of pending invocations (on the actors of a synchronization set) by combining information in I and . In particular, I returns the synchronization set of the carrier of a future, returns the cost of the pending invocations on actors of that set.

The invocation of m 4 on actor w works analogously, where the associated synchronization set is {w}. As the call to m 2 at line 8 is invoked on z and S(y) = {y, z}, we update 8 by appending the pair m 2 , 0 to ({y, z}), obtaining 8 ({y, z}) = t 4 • m 3 , a • m 2 , 0 . This accumulated cost expresses that the actors in {y, z} have (i) two pending calls to be synchronized, namely m 3 and m 2 ; (ii) the time distance between these calls is a; and (iii) the first invocation on this synchronization set {y, z} is performed at time t 4 . Observe that the time distance a between m 3 and m 2 is set at line 6 by applying case (1) of translate function.

There are four synchronizations in this example, namely, i at line 9, h at line 11, and f , g at line 12. Since 8 ({y, z}) = t 4 • m 3 , a • m 2 , 0 , the synchronization i may have to wait for the termination of the calls to both m 2 and m 3 . The function translate applies case (5) at line 9, which gives t 9 as the maximum between (i) the cost local to the carrier, that is, t 8 + m 1 , where m 1 corresponds to the cost expression of m 1 that is invoked on the carrier's synchronization set, which is pending to be synchronized and (ii) the expression t 4 + max(m 3 , a) + max(m 2 , 0), which consists of three parts: (a) t 4 that is the starting time of the first call to an actor in I(g) = {y, z}, (b) the maximum between the cost of m 3 and the distance a between the invocations of m 3 and m 2 , and (c) the time needed to compute m 2 . Observe that {y, z} is removed from 9 , as the cost of the invocations on these two actors have already been calculated. Similarly, I(i) and I(g) are removed from I 9 . Consequently, the synchronizations f and g at line 12 do not affect the cost expression. Observe also that t 9 is kept in parallel with the synchronization set {w} in the translation environment, which allow us to calculate the correct costs of synchronizations in subsequent steps.

The application of case (1) at line 10 increases the cost local to the carrier to t 10 = t 9 +b, and updates 10 by adding b to the time distance in the pair m 4 , b and to the parallel cost t 9 . The synchronization h at line 11 amounts to the maximal value of three elements: (a) t 10 which is the local cost before the synchronization; (b) the cost expression t 6 + max(m 4 , b), which is the sum of the first invocation on an actor in {w} and the cost of method m 4 ; and (c) the cost t 9 + b which is parallel to the method m 4 . Finally, the application of function translate at line 12 does not produce any effect. Thus, the cost of the main method in Fig. 2, t main is the cost expressed by t 12 , that is:

t main = max(k 0 + a + max(b, k 4 ), max(k 0 + max(a, k 3 + k 4 ) + k 2 , a + k 0 + k 1 ) + b) 2

Properties of the translation

The correctness of our system relies on the property that the computational time never increases during transitions. Therefore, the cost of the program in the initial configuration over-approximates the actual cost of every computation.

Cost programs

The cost of a program is computed by solving a number of equations. Let a cost program be an equation system of the form

m 1 (u 1 ) = exp 1 . . . m h (u h ) = exp h main(u) = exp
where m i are function names, u i natural formal parameters, and exp i and exp are cost expressions. The solution of the above cost program is the closed-form upper bound for the equation main(u), which is a function expressed in terms of its input parameters.

Definition 5.1 (Cost of P).

Let

P = m 1 (x 1 , y 1 , u 1 ) = νz 1 ;s 1 , • • • , m h (x h , x h , u h ) = νz h ;s h , main(x, u) = νz;s be an alt program. For every 1 ≤ i ≤ h, let 1. S m i = sschem({{x i , y i }}, s i ), 2. m i (u i ) = t i , where translate S m i (∅, ∅, x i , 0, 0, s i ) = (I i , i , l i , t i ),
3. S = sschem({∅}, s) and translate S (∅, ∅, x, 0, 0, s) = (I, , l main , t main ).

Let also eq(P) be the cost program

(m 1 (u 1 ) = t 1 , • • • , m h (u h ) = t h , main(u) = t main )
A cost solution of eq(P), named U (P), is the closed-form solution of the equation main(u) in eq(P).

For each method we produce cost equations which matches the cost of the method to the cost of its last statement,

m h (u h ) = t h .
Analogously, we produce one extra equation for the cost of the main method main(u) and its close-form solution over-approximates the computational time of an alt program.

Main result

The correctness of our analysis follows by the statement below.

Theorem 5.1 (Correctness). Let P be an alt program, whose initial configuration is cn, and U (P) be the closed-form solution of eq(P). If cn ⇒ * cn , then time(cn ) ≤ U (P).

( 1) eq(m_pp(u),e,[m_pp-1(u))]),[]) (2), [START_REF] Albert | Cost analysis of object-oriented bytecode programs[END_REF] eq(m_pp(u),0,[m_pp-1(u))]),[]) (4), [START_REF] Brockschmidt | Alternating runtime and size complexity analysis of integer programs[END_REF] eq(m_pp(u),numexp(l),[calls(l),m_pp-1(u)]),[]) [START_REF] Blazy | Formal verification of loop bound estimation for WCET analysis[END_REF] eq(m_pp(u),0,[maxeq(pp, t + l, [

[ (I( f ))]])]),[])

Fig. 5. PUBS cost equations production.

The proof of Theorem 5.1 is presented in the Appendix. It relies on (i) the extension of the function translate to runtime configurations, on (ii) defining the cost of a computation cn ⇒ * cn , noted time(cn ⇒ * cn ) to be the sum of the labels of transitions, and on (iii) verifying that if U (P) is a solution of translate(cn) and cn ⇒ * cn then U (P)time(cn ⇒ * cn ) is a solution of translate(cn ).

As regards the extension in (i), we need to enhance the notion of synchronization set in order to refer to the current state of the objects. In this way, it is possible to define the cost equations of futures that have been already created (the corresponding task is either enqueued in a task pool, or running, or terminated). Overall, this enhancement requires the demonstration of a number of properties (see Lemma A.3, A.4, and A.5). In particular, Lemma A.5 shows that synchronization sets are stable over time. Namely, two different synchronization sets will never get merged during the execution. This is clearly very important as objects of two different synchronization sets are considered to execute in parallel in our analysis, while objects within the same synchronization set are considered to execute sequentially.

As regards (iii), we reason by induction on the length of cn ⇒ * cn and we are reduced to two basic cases, according to the type of the last transition in cn ⇒ * cn :

1. either cn → cn ; assuming that U is a solution of translate(cn ), then it is also a solution of translate(cn ), see Lemma A.15; 2. or cn t → cn ; assuming that U is a solution of translate(cn ), then Ut is also a solution of translate(cn ), see Lemma A.14.

The proof is complex because we have to deal with a lot of technical details, such as managing the synchronous sets at runtime and extracting the time difference in the cost equations when cn t → cn (which is not easy when costs are stored in ).

It is important to observe that Theorem 5.1 is demonstrated using the (theoretical) solution of cost equations in [START_REF] Albert | Closed-form upper bounds in static cost analysis[END_REF]. This allows us to circumvent possible errors in implementations of the theory, such as CoFloCo [START_REF] Montoya | Resource analysis of complex programs with cost equations[END_REF] or PUBS [START_REF] Albert | Closed-form upper bounds in static cost analysis[END_REF]. As a byproduct of Theorem 5.1, we obtain the correctness of our technique, modulo the correctness of the solver.

The prototype

The analysis technique proposed in this paper has been prototyped using [START_REF] Albert | SACO: static analyzer for concurrent objects[END_REF]. In this section, we are going to discuss a number of technical details about converting cost equations in Section 4 to an adequate format for PUBS [START_REF] Albert | Closed-form upper bounds in static cost analysis[END_REF], which is an equation solver. We also present a preliminary evaluation of our prototype by discussing a number of examples and compare our analysis with the parallel cost analysis in [START_REF] Albert | Parallel cost analysis[END_REF].

The conversion of cost equations

The translate function returns a set of equations that need to be adapted before inputting them in PUBS. In particular, the equations used by this tool have the form eq(name,cost,calls,size), where name is the equation name, cost the value produced by this equation, calls a list of equations called from name and size the size relations needed to compute the closed form of the upper bound (see [START_REF] Albert | Closed-form upper bounds in static cost analysis[END_REF] for details). The reason why an adaptation is needed is that in one equation, PUBS add the cost of the expression cost plus the cost of all calls in calls, thus, using only one equation we cannot express the cost of max(m 1 , m 2 ), because the cost of methods m 1 and m 2 will be summed if we include m 1 and m 2 in calls. A maximum can be derived by generating two different equations with the same name, so that, as PUBS computes the worst cost, it applies the maximum between the two equations.

Let us explain how equations are generated by using the recursive execution of translate. Observe that, as it is detailed in Section 4.3, function translate is applied recursively to all statements in a method. Note also that the cost of each program can be expressed with respect to the cost of the previous program point with expressions like t + e, where t corresponds to the time computed for the previous program point. This can be seen in Example 4.2 where the cost produced by the application of translate to each statement can be expressed in terms of the cost produced by the previous executions with expressions like t 6 = t 5 + a (see the right of Fig. 4). Then, for each program point, by means of the application of translate, we produce one cost equation capturing how the time advances, that is, how t is modified in the different cases of Fig. 1. Fig. 5 illustrates how the execution translate S (I, , x, l, t, pp:μ), where pp corresponds to the program point of instruction μ, produces its corresponding equation for the different cases of Fig. 3 applied to method m. We use m_pp to refer to the new equation produced at program point i of method m, which captures the cost at this point, that is t i eq(main(A,B),0,[main_12(A,B)],[]).

eq(main_2(A,B),0,[],[]). eq(main_3(A,B),c(k0),[main_2(A,B)],[]). eq(main_4(A,B),0,[main_3(A,B)],[]). eq(main_5(A,B),0,[main_4(A,B)],[]). eq(main_6(A,B),nat(A),[main_5(A,B)],[])

. eq(main_7(A,B),0,[main_6(A,B)],[]). eq(main_8(A,B),0,[main_7(A,B)],[]). eq(main_9(A,B),0,[main_9_max(A,B)],[]). eq(main_9_max(A,B),0,[main_8(A,B),m1(A)],[]). eq(main_9_max(A,B),0,[main_4(A,B),main_9_1_max(A,B), main_9_2_max(A,B)],[]). in Fig. 4. We also use m_pp-1 for the equation of the preceding program point. For case [START_REF] Albert | SACO: static analyzer for concurrent objects[END_REF] the equation adds the cost expression e with the cost of the previous program point m_pp-1. Cases (2) and (3) only adds the cost of the previous program point. Cases [START_REF] Albert | Parallel cost analysis[END_REF] and [START_REF] Brockschmidt | Alternating runtime and size complexity analysis of integer programs[END_REF] adds the cost of l, which might contain natural expressions, like constants or natural names, or can contain calls to other methods or to previous program point equations. We define two functions to handle these two cases: numexp(e), which returns the addition of the natural expressions in e; and calls(e), which returns a sequence of all non-natural expressions in e. Thus, numexp(l) are added to the cost expression of the equation, and calls to other equations, captured by calls(l), are added to the calls of the equation, including also the cost of the previous program point m_pp-1(u). The following example illustrates the production of the equations according to the application of translate function shown in Fig. 4. Example 6.1. Fig. 6 outputs the equations corresponding to translate function shown in Fig. 4. The solver uses nat(e) to refer to max(e, 0) and to avoid negative input values (see equations main_6 and main_10), and c(k) for constant values (see equations main_3, m1, m2, m3 and m4). Note that the cost expressions are composed step by step by referencing the previous cost equation in the calls of a cost equation, as it is shown in all cost equations. New cost is added according to case (1) e.g., main_3, which sums the cost of main_2 and c(k0), or main_6, which sums the cost of main_5 and nat(A). For instance, expressions like t 6 = t 5 + a are captured by the equation

eq(main_9_1_max(A,B),0,[m3(A)],[]). eq(main_9_1_max(A,B),nat(A),[],[]). eq(main_9_2_max(A,B),0,[m2(A)],[]). eq(main_9_2_max(A,B),0,[],[]). eq(main_10(A,B),nat(B),[main_9(A,B)],[]). eq(main_11(A,B),0,[main_11_max(A,B)],[]). eq(main_11_max(A,B),0,[main_10(A,B)],[]). eq(main_11_max(A,B),0,[main_6(A,B),main_11_1_max(A,B)],[]). eq(main_11_max(A,B),nat(B),[main_9(A,B)],[]). eq(main_11_1_max(A,B),0,[m4(A)],[]). eq(main_11_1_max(A,B),nat(B),[],[]). eq(main_12(A,B),0,[main_11(A,B)],[]). eq(m1(A),c(k1),[],[]). eq(m2(A),c(k2),[],[]). eq(m3(A),c(k3),[m4(A)],[]). eq(m4(A),c(k4),[],[]).

eq(main_6(A,B),nat(A),[main_5(A,B)],[]) . 2

The computation of the accumulated costs in case [START_REF] Blazy | Formal verification of loop bound estimation for WCET analysis[END_REF], which include max expressions, requires a specific treatment. To deal with expressions of the form max(exp 1 , . . . , exp n ), we produce n equations of the forms maxeq(u) = exp 1 ; . . . ; maxeq(u) = exp n . max expressions are processed by the function maxeq(id, exp eq(m_id_max(u),natexp(exp 1 ),[calls(exp 1 ),maxexp(exp 1 )],[])

. . .

eq(m_id_max(u),natexp(exp n ),[calls(exp n ),maxexp(exp n )],[])

As before, in the equations we distinguish the cost corresponding to natural values and the cost associated to calls. In addition, we use maxexp(exp) to separate the cost associated to other max expressions that could be found in the accumulated cost. For each max expression, we use to maxeq function with a fresh identifier for processing other possible max expressions found within the expressions and apply it recursively.

Example 6.2. For instance, let us produce the equations for the cost expression

t 9 = max(t 8 + m 1 , t 4 + max(m 3 , a) + max(m 2 , 0))
at line 9 in Fig. 4 is captured by the two main_9_max equations in Fig. 6, which respectively includes the cost main_8 + m1, and the cost of main_4 + main_9_1_max + main_9_2_max. Analogously, main_9_1_max and main_9_2_max corresponds to the maximums max(m 3 , a) and max(m 2 , 0), respectively. Similarly, three equations main_11_max are needed to compute max expression of t 11 at line 11 in Fig. 4. By solving the equations shown in Fig. 6 with PUBS, we get the expression:

max([nat( A) + c(k 0 ) + max([nat(B), c(k 4 )]), nat(B) + max([c(k 0 ) + max([nat( A), c(k 3 ) + c(k 4 )]) + c(k 2 ), nat( A) + c(k 0 ) + c(k 1 )])])
which reflects the cost expression t main computed in Fig. 4 and captures the overall cost of main in Example 4.2. 2

Another point to remark is that PUBS is able to detect non-terminating programs caused by direct or indirect recursions, indicating the solution of the equations is unbounded.

Experimental evaluation

The prototype can be experimented online. 1 To deliver preliminary assessments, we have written our programs in a language that is an extension of alt -the ABS language [START_REF] Johnsen | ABS: a core language for abstract behavioral specification[END_REF], where only the features presents in alt are used. The experiments, whose source codes are available in the tool web site, model a number of typical concurrent and distributed scenarios:

NWorkers(t1,t2,lt) models the standard fork-join pattern where multiple workers execute in parallel on different actors parts of a larger task, represented by wait(t1) and wait(t2), respectively, and the carrier spends lt time units in parallel to the workers. NWorkersMultiWorks(t1,t2,t3,t4) models a similar scenario but spawning four tasks per worker, with durations t1, t2, t3, t4 and synchronizes all of them at the end of the main method. NWorkersPartSync(t1,t2,lt) models a fork-join pattern with two workers, but the launcher spends lt time units, between the synchronizations; NWorkersDelayed(t1,t2,t3,t4,lt) also models a fork-join pattern with two workers that execute four tasks with durations t1, t2, t3, t4. In this model, the launcher spends lt time units between spawning the second and the third task. ProdCons(pt,ct) models a producer-consumer scenario where the production and the consumption might occur in parallel, taking pt and ct time units for producing and consuming, respectively.

MapReduce(mt1,mt2,lt1,rt1,rt2,lt2) models the map-reduce algorithm where the map tasks, which take mt1 or mt2, are spawned on multiple workers in parallel. When all map tasks are finished, after lt1 time units for modeling the map result processing, the reduce tasks, which take rt1 or rt2, are spawned on the workers. Then after the synchronizations, the main methods spends lt2 time units to process the results. MapReduceSubWorkers(mt,rt,sm1,sm2,sr1,sr2) models the map-reduce algorithm where the workers share the task, taking times mt for map and rt for reduce, and launch subtasks with times sm1, sm2 for map and sr1, sr2 for reduce to other sub-workers.

We have executed the above codes on an Intel Core i7-7500U CPU @ 2.70 GHz with 64 Gb of RAM, running Debian 9.3. Table 7 summarizes the upper bounds obtained by means of our prototype. For the sake of clarity, we have simplified the expressions that are redundant, and we have replaced in the table nat(e) by e. For instance, the expression returned for NWorkers, namely max([nat(t2),nat(lt),nat(t1),nat(lt)]), is written as max([t2,lt,t1]).

The results of Table 7 show that the computational time of our analysis is quite short: less than 5 ms for all the programs. The number of equations might be high for big programs, as it can be seen in MapReduce or in MapReduceSubWorkers. Even so, the time required to solve them is higher but is still rather short. This number of equations can be reduced by producing only one equation for those sequence of instructions that do not modify the time, reducing the time taken in solving them.

Regarding to the precision of our analysis, the results highlight that we do not lose precision in fork-join patterns. In fact, in this case, we properly identify those parts that can execute in parallel and use the max to capture the parallelism. For instance, in NWorkers and NWorkersMultiWorks, our tool identifies the parts running in parallel and calculates the cost as the maximum cost needed among the workers, independent from the number of workers executing simultaneously (in this programs we have four different workers). Similarly, as highlighted by the programs MapReduce and MapReduceSubWorkers, our tool identifies that map and reduce tasks might execute in parallel before their synchronization. In this case, their costs are added only once to the total cost inside the two maximum expressions max(mt2,mt1) and max(rt2,rt1).

Tools comparison

In the following, we compare the results obtained by our approach and by the analysis described in [START_REF] Albert | Parallel cost analysis[END_REF].

The analysis of [START_REF] Albert | Parallel cost analysis[END_REF] uses a language -the ABS language [START_REF] Johnsen | ABS: a core language for abstract behavioral specification[END_REF] -that is actually a superset of alt. In particular, in order to solve the syntactic mismatches, we had to modify the wait(e)-statement into loops with e iterations so as to model the time progress. Additionally, we ignore the constant times output by [START_REF] Albert | Parallel cost analysis[END_REF] as they are not considered by our time analysis.

The table illustrates the results obtained by applying our time analysis and the analysis of [START_REF] Albert | Parallel cost analysis[END_REF] to the alt programs in Examples 3.1, 3.2 and 3.3.

Prog. Time Analysis Analysis of [4]

main 1 k 0 +max(a,k 1 )+max(b,k 2 ) max(k 0 +a+b,k 0 +k 1 +k 2 +a) main 2 k 0 +max(a+b+k 2 ,k 1 ) k 0 +max(k 1 +k 2 ,a+b+k 2 ) main 3 k 0 +max(a,k 2 +k 3 )+max(b,k 1 ) k 0 +max(k 0 +a+b,k 0 +k 1 +k 2 +k 3 ,k 0 +a+k 1 +k 2 )
To explain this point, we need to recall the technique of [START_REF] Albert | Parallel cost analysis[END_REF], which uses block-level cost-centers to compute the cost expression of the sequential parts of the program. A distributed flow graph of the program is then generated to express tasks that might be executed in parallel and their flow relations. The distributed flow graph is used to find all the paths that start from the initial node and end in any possible final node. The cost expressions of every path are computed accordingly and the overall cost, called the parallel cost of the program, is simply the maximum of the costs. The critical point of the technique in [START_REF] Albert | Parallel cost analysis[END_REF] is that, in order to take into account every possible scheduler's choice, the distributed flow graph collects edges that connect the beginning and the end of those methods that might be simultaneously in the pool of pending tasks. These edges introduce cycles in the graph; hence, the collection also includes those paths where parallel methods are sequentialized. This results in a loss of precision.

The reader may notice that the results obtained in some scenarios by our time analysis are more precise than [START_REF] Albert | Parallel cost analysis[END_REF] for the studied programs. For instance, this precision loss in [START_REF] Albert | Parallel cost analysis[END_REF] is shown in main 1 , where the cost of a and k 1 are not considered to happen in parallel. Similarly, in main 2 , where the costs k 1 and k 2 are summed; or in main 3 , where k 2 should not be added to the expression k 0 +a+k 1 +k 2 . As the values of the upper bound depend on the input values, cost expressions cannot be directly compared. In order to compare the results obtained by both tools, we evaluate the upper bound for all possible combinations of the input arguments, including constant values, ranging each of them between [1-100] and compare the results obtained with both tools. The following table summarizes the results obtained by showing the percentage of evaluations where our approach is more precise (% w ), less precise (% l ) or equally precise (% e ) with respect to the technique in [START_REF] Albert | Parallel cost analysis[END_REF]: The results of the evaluations show that our technique obtains better results than [START_REF] Albert | Parallel cost analysis[END_REF] for programs for main 1 and main 2 , and for main 3 we get better results for 34% of the evaluations and worse for the same number of evaluations.

Program (% w ) (% l ) (% e )
Regarding the benchmarks of Fig. 7, the analysis of [START_REF] Albert | Parallel cost analysis[END_REF] gives results similar to our tool, except for NWorkersDelayed. In fact, this program is the only one spends some time between two invocations on the same actor. For this program, the upper bound expression obtained by [START_REF] Albert | Parallel cost analysis[END_REF] is lt+t1+t2+t3+t4, which sequentialize the cost of all the methods. On the contrary, our tool is able to detect that lt and t2 are costs of two parallel methods. Thus, our analysis does not sequentialized these two costs, but returns their maximal value, which in turn produces the expression t1+max(lt,t2)+t3+t4.

Related work

Static time analysis techniques for concurrent programs follow two main approaches: those based on type-and-effect systems and those based on abstract interpretation.

Type-and-effect systems [START_REF] Giachino | Time complexity of concurrent programs[END_REF] (i) collect constraints on type and resource variables and (ii) solve these constraints by means of an off-the-shelf solver [START_REF] Albert | Closed-form upper bounds in static cost analysis[END_REF][START_REF] Montoya | Resource analysis of complex programs with cost equations[END_REF]. Recent work has applied type-based amortized analysis for deriving upper bounds of parallel first-order functional programs [START_REF] Hoffmann | Automatic static cost analysis for parallel programs[END_REF]. This work differs from our approach in the concurrency model, as they do not handle references to actors in the programs and there is no distinction between blocking and non-blocking synchronization.

In this paper we do not perform constraint collection on type and resources. This is because alt is intended to be a behavioral type language; therefore, we directly use alt to define a (compositional) analysis that returns cost equations.

The main difference with respect to the analysis of [START_REF] Giachino | Time complexity of concurrent programs[END_REF] is that now we are able to compute the cost of functions that contain invocations on arguments, namely on actors that are already alive before the function invocations. An approach similar to our one has been proposed in [START_REF] Morrisett | From system f to typed assembly language[END_REF] for verifying safety properties of sequential languages.

Abstract interpretation techniques addressing domains carrying quantitative information, such as resource consumption, have been proposed in the literature -see references in [START_REF] Trinder | Resource analyses for parallel and distributed coordination[END_REF]. Consequently, several well-developed automatic solvers for cost analysis already exist. These solvers either use finite domains or use expedients (widening or narrowing functions) to guarantee the termination of the fix-point generation. For this reason, solvers often return inaccurate answers when fed with systems that are finite but not statically bounded. Among the others, [START_REF] Albert | Parallel cost analysis[END_REF] defines a technique based on abstract interpretation that targets a language with a similar concurrency model as presented in this paper. We have discussed the technique of [START_REF] Albert | Parallel cost analysis[END_REF] in Section 6, where we have also analyzed the differences with our technique. We recall that our technique returns more precise costs for programs that spawn several invocations without synchronization on the same synchronization set. In particular, [START_REF] Albert | Parallel cost analysis[END_REF] manifests a sensible loss of precision when cycles appear in the distributed flow graph, as all nodes in the cycle will be part of the path that leads to the maximum upper bound. We also observe that, since the technique in [START_REF] Albert | Parallel cost analysis[END_REF] is not compositional, it does not require any management of synchronization sets, which entangles a lot our technique.

Conclusions

This paper presents a technique for computing the time of concurrent programs. We have defined alt, an actor calculus that is intended to be a compilation target for concurrent languages featuring actor creation, task invocation and synchronization. In particular, alt features an explicit cost annotation that defines the number of machine cycles required before executing the continuation, which abstracts away the actual computation activities of the program. The computational time is then measured by introducing the notion of (strong) t-stability (cf. Definition 2.1), which represents the ticking of time and expresses that no control activity is possible up to t time units. In order to relate actors that might potentially delay executions of other actors, we introduce the notion of synchronization sets. Then, we define a translate function that uses synchronization sets to compute a cost equation function for each method definition. We have also proven that our approach is sound with respect to the actual computational time (cf. Theorem 5.1). The analysis has been prototyped and experimented, which shows that our approach produces accurate over-approximation.

Overall, our technique allows one to estimate the computational time of the source program by computing the cost of the target actor program. The aim is to use our technique in a cloud computing setting because alt terms might be considered as abstract descriptions of services and the estimation of the computational time may be used for enforcing the compliance with the service level agreement contract. In this context, the cost expressions in wait(•)-statement, might be defined by means of a worst-case execution time analysis [START_REF] Blazy | Formal verification of loop bound estimation for WCET analysis[END_REF]. Future lines of work must consider the possibility of obtaining more precise information about synchronization sets of actors. In this paper, these sets are computed for method bodies by simply accumulating information, despite of the fact that two actors, in a stage of the computation may affect each other, while in another stage they are independent. In fact, a more appropriate notion would have been that of sequence of synchronization sets. While such improvement will end up in more precise results of the cost analysis, it is not clear how much more complex the theoretical developments will become. Perhaps a manageable extension will be a notion in between the synchronization sets and the sequences of such sets.

In this paper, the cost of a method includes that of the asynchronous invocations in its body because every invocation is synchronized. This constraint does not permit to trigger methods such as drivers, daemons, etc. without waiting for their termination. In order to take care of costs of unsynchronized methods, one should use continuations and compose costs according to the synchronization set they correspond. We will address this extension in a future work.

Appendix A

We introduce this appendix with some helpful notation related to the cost equation of an alt program, and with few algebraic notation on graphs and equivalence relations that will be helpful to define synchronization schema for runtime configurations.

Definition A.1. In this appendix, to simplify future notations, we extend the notion of cost expression with future names, to be able to refer to the cost of currently running processes. We also extend the max operator to take a variable number of parameters (with the standard semantics), and thus have the following syntax definition:

exp ::= k | u | f | exp + exp | m(e) | max(exp)
Additionally, we extend the syntax of accumulated costs as follows, to allow to count the cost of running process as well as functions yet to be executed:

ε ::= exp | ε • m(e), exp | ε • f , exp | ε exp .
The parameters S, I , , x, l, t and s of the translate function are consistent iff: S is an equivalence relation on a set including all free actor names in s and x; all free future names in s are in dom(I); all the synchronization sets in im(I) are in S;2 and all the synchronization sets in im(I), minus S(x), are in dom( ).

Suppose given consistent parameters S, I , , x, l, t and s. We write T S (I, , x, l, t, s) the cost of the translation of s:

translate S (I, , x, l, t, s) = (I , , l , t ) ⇔ T S (I, , x, l, t, s) = t Definition A.2. Suppose given any two cost expressions exp 1 and exp 2 . We write exp 1 ≤ exp 2 iff for all substitution with fv(exp 1 ) ∪ fv(exp 2 ) ⊆ dom( ) and im( ) ⊆ [0..∞], we have (exp 1 ) ≤ (exp 2 ).

The following definition is a small adaptation of Definition 5.1 where the cost of the main statement of the program, instead of being by itself, is mapped to a name f start . That way, a cost program becomes a simple set of equations, that is easier to manipulate in the proofs (see Lemma A.13).

Definition A.3. Suppose given a set of functions

FD = m 1 (x 1 ) = s 1 , • • • , m n (x n ) = s n .
The cost program eq of an alt program P = (FD, s main ) is defined as follows:

eq(P) def = [ f start → T sschem({ {start} },s main ) (∅, ∅, start, 0, 0, s main )] ∪ i [m i (x i ) → translate(m i (x i ) = s i )]
A cost solution of an alt program P is a solution for the equation eq(P).

Finally, the following definition introduces some notations on graphs and relations. They will be useful in the next section, where we define the notion of synchronization schema on runtime configurations. Definition A.4. Given a set V and a relation R on V , we write R eq(V ) the transitive, reflexive and symmetric closure of R in V . Note that we will write R eq when the set V is clear from the context. Given a set V and an equivalence relation R on V , we write R the partition of V raised by R. Given a graph G = (V , E) and an equivalence relation R on V , we write

G/ * R the graph G = (V , E ) such that: V def = R E def = {(A, A ) | A = A ∈ R, ∃x ∈ A, y ∈ A , (x, y) ∈ E}
In the rest of the appendix, we write: parents(G, x) for the set of the parent nodes of x in G, i.e., parents(G, x) def = {y | (y, x) ∈ E}; paths(G) for the set of non-empty paths p in the directed graph G; start(p) for the start node of the path p; end(p) for the end node of the path p; and nodes(p) for the set of nodes traversed by the path p.

A.1. Runtime analysis

In this section, we extend the translation function of Fig. 3 to the runtime terms of alt. This extension maps all tasks in the runtime to a cost equation encoding an upper bound of its finishing time. In order to do so, we need to define the different parameters of the translate function. First of all, let us introduce the necessary notations: Definition A.5. Suppose given a runtime configuration cn. We write x ∈ cn iff there exists p, q and cn such that cn = act(x, p, q) cn . If cn = act(x, p, q) cn , we write cn(x) for the configuration act(x, p, q). If cn = act(x, p, q) cn , we write (x : f ) ∈ cn iff there exists s; f ∈ p q or if cn = invoc(x, f , m, v) cn ; we write f → f ∈ cn iff there exists s; f ∈ p q and f is a statement in s; and we write f → x ∈ cn iff there exists s; f ∈ p q such that x is free in s or if there exists f such that f → f ∈ cn and (x : f ) ∈ cn. Finally, we write roots(cn) for the set of root futures of cn, i.e., roots(cn) = { f | f , f → f ∈ cn}; and A(cn) for a set of actor names A, which extracts from cn all actors named in A, with their futures fut( f , val) and invocation messages invoc(x, f , m, v).

Synchronization schema The first parameter, the synchronization schema, has a central role in the cost computation, as it captures the actors that may reciprocally affect the queues of each other by means of function invocations and synchronizations. Without such information, the cost computation cannot capture all the tasks that could occur in an actor's process queue, and thus would be erroneous. At static time, such schemas are computed using the parameters of method calls. However, at runtime, this information is missing as running code does not refer back to their originating method and parameters. The way we can recreate information captured by a synchronization schema at runtime is to follow the point-to relation between objects. We recall the point-to relation between object in the following definition:

Definition A.6. The point-to relation of a runtime configuration cn, noted point-to(cn), is a directed graph (V , E) where

V def = {x, f | (x : f ) ∈ cn}; E def = {(x, f ) | (x : f ) ∈ cn} ∪ {( f , x) | f → x ∈ cn}.
With this, we can construct the synchronization schema of a runtime configuration. Following Definition 4.1, synchronization sets actually capture a notion slightly more subtle than simply affecting each other's queue. Firstly, synchronization sets do not include the obvious parent-son object relation, as this would be a too restrictive approximation that would consider any concurrent computation as put in sequence. Secondly, synchronization sets put in relation not only objects that may influence each other, but also objects that refer to influencing objects: the synchronization set somehow consider the transitive closure of the point-to relation. Finally, we also need to include in the synchronization sets the dependencies that might be created by future method calls. These considerations lead to the following definition of the synchronization sets for runtime configuration: Definition A.7. Give a runtime configuration cn and a graph G = (V , E) where the vertexes are sets of object and futures names in cn, we define the relation I on V as follows:

v I v ⇔ x ∈ v, f ∈ v , (x : f ) ∈ cn
This relation I is used to identify an object with its processes in the point-to relation.

Given a graph G = (V , E), we define the relations P and L on V as follows:

x P y ⇔ {y} parents(G, x)

x L y ⇔ ∃p ∈ paths(G), start(p) = end(p) ∧ {x, y} ∈ nodes(p)
The relation P corresponds to the fact that an object x with more than one parent y must be in the same synchronization set; the relation L corresponds to the fact that objects in a dependency loop are in the same synchronization set.

The synchronization graph of a runtime configuration cn, written G cn is defined as follows: The synchronization schema of a runtime configuration cn, written S cn is the set of vertices of G cn . Note that, by construction, S cn is a partition of the object names in cn. Hence, we can use the same notation as in Section 4 by writing S cn (x) for the set A ∈ S cn containing x. Future localization The parameter I is the simplest to define, now that we have a precise definition of synchronization schema. Indeed, this parameter simply maps the futures living in the configuration to its actor's synchronization set. Given a runtime configuration cn, we define:

I cn def = [ f → S cn (x) | x ∈ cn, f ∈ cn(x)] translate S (I, cn) = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (1) ∅ when cn = ε (2.1) ∅ when cn = fut( f , ⊥) (2.2) { f → 0} when cn = fut( f , ) (3)
p ∈p,q translate S (I, x, p ) when cn = act(x, p, q)

(4) { f → m(x, v)} when cn = invoc(x, f , m, v)

Translation environments

The translate function has a last important parameter: the environment giving the accumulated cost of every running synchronization set. At runtime, waiting statements are not only bound to numerical expression or method calls, but partially to executed processes identified by futures. This motivates the expression extension we gave in the introduction of the appendix. During the static time analysis, and also in the runtime analysis, contains an entry for all synchronization sets that have a non-empty process queue. Hence, this parameter is relevant only when translating a process, and collects data about the futures and synchronization sets related to the analyzed process.

The translation function We present in Fig. 8 the translation function of runtime configurations into mappings from future names to cost equations. Note that when translating a specific process, we need to use a local future localizations I , which takes into account objects that are not created yet, and to create the corresponding translation environment . This is done with the following function:

[S, I] x s def = (S , I , , l) with ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ S = sschem(S, s) I = [ f → A | f ∈ dom(I), I( f ) ⊂ A, A ∈ S ] = [A → I( f )=A, f ∈fv(s) f , 0 | A ∈ I (fv(s)) ∧ x / ∈ A] l = f ∈I -1 (S(x)) f free in s f Definition A.8. Suppose given a set of functions FD = m 1 (x 1 ) = s 1 , • • • , m n (x n ) = s n .
The cost configuration eq of a runtime configuration cn based on the functions FD, written eq(cn, FD), is defined as follows:

eq(cn, FD)

def = translate S cn (I cn , cn , cn) ∪ i [m i (x i ) → translate(m i (x i ) = s i )]
A cost solution of a runtime configuration cn based on the functions FD, is a solution for the cost configuration eq(cn, FD).

The following two lemmas give some properties about the image of a cost equation, so we will be able to manipulate them in the rest of the proofs. The first lemma states that a cost equation maps functions and futures to expressions exp x .

Lemma A.1. Consider a consistent set of parameters S, I, , x, l, t and s. Then, T S (I, , x, l, t, s) is a cost expression. Consider additionally a runtime configuration cn and a set of functions FD. Then, the image of eq(cn, FD) is a set of cost expressions exp.

Proof. Inspecting the rules in Fig. 3, it is clear that t in (I, , l , t ) = translate S (I, , x, l, et, s) is a cost expression. Consequently, by Definition A.1, T S (I, , x, l, t, s) is a cost expression as well. Additionally, it is easy, looking at the rules in Fig. 8, and by Definition A.8, to see that the image of eq(cn, FD) are all constructed from T S (I, , x, l, 0, s) where l is a sum over futures. Hence, the image of eq(cn, FD) is a set of cost expressions exp (a sum of future is a valid cost expression). 2 Lemma A.2. A cost expression exp is always equal to some max(exp 1 , . . . , exp n ) where none of the exp i contain a max operator.

Proof. This property is a consequence of the following equations that can move all the max functions in e to the top level: max(exp 1 , . . . , exp n ) + exp = max(exp 1 + exp, . . . , exp n + exp) max(max(exp), exp ) = max(exp, exp ) 2

In the rest of this appendix, we will always consider cost expressions exp to be equivalent modulo the previous equalities that allow to move the max function around.

A.2. Upper bound correction

In this section, we prove that the cost we computed is a correct upper bound for the execution time of the program.

A.2.1. Properties of the runtime configuration's graph structure

The three following lemmas illustrate the fact that our definition of synchronization sets abstracts within synchronization sets all the complex artifacts of the point-to relation between objects, and exposes only a simple structure that we can analyze. Lemma A.3 states that the point-to relation between synchronization sets is a forest. Lemma A.4 shows that links in the point-to relation between objects of different synchronization sets have all different sources and targets. And Lemma A.5 shows that our notion of synchronization set is stable over time, in the sense that two different synchronization sets will never get merged during the runtime configuration's execution. This last lemma is very important as objects of two different synchronization sets are considered to execute in parallel in our analysis, while objects within the same synchronization set are considered to execute sequentially. Hence while splitting a synchronization set reduces the computed cost of the program (as objects considered to execute sequentially are now considered to execute in parallel), merge synchronization set increases it and could likely mean that our analysis did not compute the right cost before the merger.

Lemma A.3. The synchronization graph of a runtime configuration cn is a forest.

Proof. This is a direct consequence of merging in the same equivalence classes the nodes that break acyclicity in the point-to graph. 2 Lemma A.4. Suppose given a runtime configuration cn, (x : f ) ∈ cn, (x : f ) ∈ cn and y ∈ cn such that f → y ∈ cn, f → y ∈ cn and S cn (x) = S cn (y). Then, x = x and f = f . Proof. This is a direct consequence of the construction of the synchronization graph, where we quotient the point-to graph of cn by H , putting every actor accessible from different processes in the same equivalence class. 2 Lemma A.5. Given a runtime configuration cn and a process p = s; f such that cn = act(x, p , q) cn with p ∈ p q. Then, for all A 1 = A 2 ∈ S cn , there exists A

1 = A 2 ∈ sschem(S cn , s) with A 1 ⊂ A 1 and A 2 ⊂ A 2 .
Proof. This is directly proven by induction on s, and by the fact that S cn is constructed by taking into account the dependency between actors in p. 2

Finally, the following definition and lemma show that the synchronization dependencies between processes have a simple tree structure. This property is important as when a process f synchronizes with a process f , our analysis counts the cost of f within f . Hence, if the dependencies between process was a more general graph and several processes could synchronize with f , then its cost would be counted several times. Definition A.9. The process graph of a runtime configuration cn is a graph (

V , E) such that V = { f | f ∈ cn(x), x ∈ cn} and E = {( f , f ) | f , f ∈ V ∧ f → f ∈ cn}.
Lemma A.6. The process graph G of a runtime configuration cn is a tree.

Proof. By induction on the reduction steps to reach cn from an initial configuration. Note that only the Async-Call reduction rule creates a link between futures; moreover, it creates this link to a fresh future name, so it is not possible to create loop. Hence, the process graph is a forest. Finally, because all futures must be synchronized, it is not possible to break a link towards a running process. Therefore, all nodes in the process graph are reachable. Thus, the process graph is a tree. 2

A.2.2. Properties of runtime evolution

The following Lemma simply states that the only part of I and relevant for the computation of the cost of a statement s is the one about the future on which s will synchronize. This lemma is useful, as it states that if two processes f and f have no dependencies between each other, then executing f will not change the cost of f . Lemma A.7. Suppose given S, I 1 , I 2 , , x, l, t, s such that: the sets of parameters S, I i , , x, l, t and s are consistent, for 1 ≤ i ≤ 2; and for all f free in s, we have f ∈ dom(I 1 ) ∩ dom(I 2 ) and I 1 ( f ) = I 2 ( f ). Then, we have T S (I 1 , , x, l, t, s) = T S (I 2 , , x, l, t, s) Proof. This is directly proven by induction on s, by remarking that all futures that are accessed in I i (with 1 ≤ i ≤ 2) are the ones free in s (rules (4) and (5) of Fig. 3). 2

The following lemma states two of the core properties of our analysis, and is used in all the rest of this appendix. First, this lemma discusses the structure of the cost expression generated by our analysis. Looking at the rules (3), ( 4), (5) of Fig. 3, and using Lemma A.2, we can see that the cost of every synchronization set in has two parts: one that captures all the costs related to the execution of the analyzed statement (or local cost); and one that only refers to the cost of synchronization set's processes, plus the initial time ε of rule (3) (or external cost). More precisely, for every synchronization sets A ∈ dom( ), we have [ [ (A)] ] = max(exp A 1 , exp A 2 ) where exp A 1 is the first part of the cost, and exp A 2 is its second part. Consequently, with rules (4) and ( 5) of Fig. 3, we can remark that the computed cost equation has the same structure.

Second, this lemma illustrates how changing the starting moment of the analyzed statement is integrated in its cost. Consider a moment t 1 preceding by k units of time the moment t 2 : as time advance is triggered by the program waiting, these two moments can be described as costs, following the structure we just discussed. Hence, t 1 can be written as max(exp 1 , exp 2 ) where exp 1 is the local cost and exp 2 the external cost, while t 2 can be written as max(exp 1 + k, exp 2 ) (time passes locally). The cost expression in the translation environment follows the same pattern. Starting from these initial times, the lemma shows that if the statement s start at time t 2 instead of t 1 , its computed cost will have the same shape, but its local cost will have k additional units of time.

Lemma A.8. Suppose given S, I, 1 , 2 , x, exp 1 , exp 2 , l, s and k with: S, I, i , x, t i and l are coherent parameters for 1 ≤ i ≤ 2 where t 1 = max(exp 1 , exp 2 ) and t 2 = max(exp 1 + k, exp 2 ); dom( 1 ) = dom( 2 ); and for all A ∈ dom( 1 ), there exists exp A 1 and exp

A 2 such that [ [ 2 (A)] ] = max(exp A 1 + k, exp A 2 ) where [ [ 1 (A)] ] = max(exp A 1 , exp A 2 ). We then have T S (I, 2 , x, l, t 2 , s) = max(k + exp r 1 , exp r 2 ) with ⎧ ⎨ ⎩ T S (I, 1 , x, l, t 1 , s) = max(exp r 1 , exp r 2 ) exp r 1 = max(exp 1 + exp 1 , max A∈dom( ) (exp A 1 + exp A 1 )) for some exp 1 and exp A 1 exp r 2 = max(exp 2 + exp 2 , max A∈dom( ) (exp A 2 + exp A 2 )
) for some exp 2 and exp A 2 Proof. We prove this result by induction on s:

(i) Case s = 0. By construction, the lemma holds: I , 1 and 2 are empty in this case (all the futures must be synchronized at the end of a method), e = 0 (for the same reason), and

T S (∅, ∅, x, 0, t 2 , 0) = t 2 T S (∅, ∅, x, 0, t 1 , 0) = t 1
(ii) Case s = νx;s . By construction, we have that

T S (I, 2 , x, l, t 2 , s) = T S (I, 2 , x, l, t 2 , s ) T S (I, 1 , x, l, t 1 , s) = T S (I, 1 , x, l, t 1 , s )
Hence, with the induction hypothesis, we conclude the case.

(iii) Case s = ν f : m(y, z, e);s with y ∈ S(x). By rule (2) of Fig. (v) Case s = f ;s with x ∈ I( f ). By rule (4) of Fig. 3, we have that T S (I, 2 , x, l, t 2 , s) = T S (I, ( 2 + l), x, 0, t 2 + l, s ) T S (I, 1 , x, l, t 1 , s) = T S (I, ( 1 + l), x, 0, t 1 + l, s )

By construction, it is straightforward to see that dom( 2 + l) = dom( 1 + l) and that for all A ∈ dom( 1 + l), we have

[[( 1 + l)( A)]] = max(exp A 1 + l, exp A 2 + l) [[( 2 + l)( A)]] = max(k + exp A 1 + l, exp A 2 + l)
Hence, with the induction hypothesis we conclude the case. It is straightforward to see that the following equalities hold: exp 3 = max(k + max(exp 1 + l, exp I( f ) 1 ), max(exp 2 + l, exp I( f ) 2 )) exp 4 = max(max(exp 1 + l, exp I( f ) 1 ), max(exp 2 + l, exp I( f ) 2 ))

Additionally, we have that dom( Hence, with the induction hypothesis, we conclude the case.

(vii) Case s = wait(e);s . By rule (1) of Fig. 3, we have that T S (I, 2 , x, l, t 2 , s) = T S (I, 1 + e, x, l, t 2 + e, s ) T S (I, 1 , x, l, t 1 , s) = T S (I, 1 + e, x, l, t 1 + e, s )

We can first remark that t 2 + e = max(k + exp 1 + e, exp 2 + e) and t 1 + e = max(exp 1 + e, exp 2 + e). By construction, it is straightforward to see that dom( 2 + e) = dom( 1 + e). We then have Proof. Let eq 1 be the cost configuration of cn and eq 2 the cost configuration of cn : we remark that dom(eq 1 ) = dom(eq 2 ), and we first prove by induction on cn that for all f ∈ dom(eq 1 ), we either have that:

[[( 1 + e)( A)]] = max(exp A

eq 1 ( f ) = max(t + e 1 , max A∈dom( ) ( (A) + e A ))

with eq 2 ( f ) = max(e 1 , max A∈dom( ) ( (A) + e A ))

or eq 1 ( f ) = eq 2 ( f ) = f ∈F f + e for some e and with F = { f | f → f ∈ cn} = ∅. If the configuration is empty, then its cost configuration is empty and the result trivially holds. Now let us consider that cn is not empty. By the definition of cn t → cn, triggered by the rule (Tick), cn is strongly t-stable (see Definition 2.1). Let us consider f ∈ dom( ), we have three cases:

• Case cn = act(x, wait(e);s; f , q) cn . By Definition 2.1, we have cn = act(x, wait(k);s; f , q) (cn , t) with k = [ [e] ]t.

By Lemma A.9, we have that eq 1 ( f ) = max(t + e 1 , max A∈dom( ) ( (A) + e A )) with eq 2 ( f ) = max(e 1 , max A∈dom( ) ( (A) + e A )). • Case cn = act(x, f ;s; f , q) cn with I cn ( f ) = I cn ( f ). By Definition 2.1, we have cn = act(x, f ;s; f , q) (cn , t), which implies that eq 1 ( f ) = eq 2 ( f ). Using Lemma A.8, it is straightforward to see that eq 2 ( f ) = f ∈F f + e for some e, with F = { f | I cn ( f ) = I cn ( f ), f → f ∈ cn} and f ∈ F . • Case cn = act(x, f ;s; f , q) cn with I cn ( f ) = I cn ( f ). By Definition 2.1, we have cn = act(x, f ;s; f , q) (cn , t), which implies that eq 1 ( f ) = eq 2 ( f ). Using Lemma A.8, it is straightforward to see that eq 2 ( f ) = f ∈F f + e for some e, with F = { f | I cn ( f ) = I cn ( f ), f → f ∈ cn} and f ∈ F .

Using Lemma A.6, we have that the process graph G of cn is a tree, and so we can construct the solution inductively, starting from the leaves of G. 2

Lemma A.15 (Upper Bound Stability 3/3). Suppose given a configuration cn such that there exists cn with cn → cn . Suppose moreover given a solution of the cost configuration of cn. Then, there exists a solution of the cost configuration of cn such that for all f ∈ dom( ), we have ( f ) ≤ ( f ).

Proof. Let us consider the cost configuration eq 1 of cn and eq 2 of cn . We prove that for all f ∈ dom(eq 1 ), we have eq 2 ( f ) ≤ eq 1 ( f ), which thus proves the result. We construct our demonstration by case distinction on the reduction rule, modulo the rule Context.

• Case New. It is straightforward to see that, with the definition of S cn , that eq 1 = eq 2 . Hence, the result holds for the case.

• Case Get-True. We have that cn = act(x, f 1 ;p, q) cn , with p = s; f . We can first remark that for all (x : f ) ∈ cn such that f = f , we have that eq 1 ( f ) = eq 2 ( f ). Moreover, from the construction of the future localization, we have that f 1 / ∈ dom(I cn ). Hence, using the rule (6) of Fig. 3, we have that eq 1 ( f ) = eq 2 ( f ). • Case Get-False. It is easy in this case to see that eq 1 = eq 2 , which gives us the result.

• Case Async-Call. We have that cn = act(x, ν f 1 : m(z, e);p, q) cn , with p = s; f . Let f 2 be the fresh future name created in this rule. We now have two sub-cases.

Let first consider that S cn (z) = S cn (x). By construction, we have cn (S cn (z)) = cn (S cn (z)), as f 2 is free in p. Moreover, considering the rule (7) of Fig. 8, for all f ∈ dom(eq 1 ) \ { f 2 }, we have eq 1 ( f ) = eq 2 ( f ). Now, by rule (4) of Fig. 8, we have that eq 2 ( f 2 ) = m(z, e), and eq 1 ( f ) = eq 2 ( f ){ m(z, e) / f 2 }. By stating that = [ f 2 → (m(z, e))], we have that (eq 1 ( f )) = (eq 2 ( f )), which concludes this sub-case. Second, consider that S cn (z) = S cn (x). By Lemma A.4, we have that f is the only future name such that f → z ∈ cn. Hence, by construction, we have that for all f ∈ (dom(eq 1 )) \ { f }, we have eq 1 ( f ) = eq 2 ( f ). Now, by rule (4) of Fig. 8, we have that eq 2 ( f 2 ) = m(z, e), and eq 1 ( f ) = eq 2 ( f ){ m(z, e) / f 2 }. By stating that = [ f 2 → (m(z, e))], we have that (eq 1 ( f )) = (eq 2 ( f )), which concludes this sub-case.

• Case Bind-Fun. Here, we have that eq 1 ( f ) = m(x, v), and eq 2 ( f ) = e where eq 1 (m(x, v)) = e. Thus, we conclude the case.

• Case Wait-0. It is easy in this case to see that eq 1 = eq 2 , which gives us the result.

• Case Activate. It is easy in this case to see that eq 1 = eq 2 , which gives us the result. • Case Return. We have that cn = act(x, f , q) cn . By construction, we have that eq 1 ( f ) = 0 = eq 2 ( f ) (by rule (2.2) of Fig. 8). By Lemma A.6, either: i) f = f start , and so we have the result, as eq 2 ( f ) = 0 for all f ∈ dom(eq 2 ); or ii) there exists exactly one f such that f → f ∈ cn. By construction, for all f ∈ dom(I cn ) \ f , we have eq 1 ( f ) = eq 2 ( f ). Finally, by Lemma A.12, we have that eq 1 ( f ) ≥ eq 2 ( f ), which concludes the case. 2

s

  ::= 0 | νx;s | ν f : m(e);s | f ;s | wait(e n );s e ::= e n | x e n ::= k | u | e n + e n (k are natural constants)

Fig. 1 .

 1 Fig. 1. Transition rules.

Example 3 . 1 .

 31 The method main 1 in Example 2.2 invokes m 1 and m 2 on an actor that is different from the caller. The following graphical representations illustrate four different computations that are obtained by choosing different values of a and b. Rectangles in dark gray represent the largest segment of time that are used for computing the maximal cost of the computations, which are denoted by the names c 1 , c 2 , c 3 and c 4 , respectively.

1 main 3 2 ν y; νz; 3 wait(k 0 ); 4 ν

 3234 (x, a, b) = f : m 3 (y, z);

12 13 m 2

 122 (x) = 14 wait(k 2 );

15 16 m 3

 153 (x, y) = 17 wait(k 3 ); 18 νh: m 2 (y); 19 h ; The figure below shows four different computations of main 3 that correspond to various values of a, b, k 1 , k 2 and k 3 .

1 3 wait(k 0 ); 4 ν

 34 main(x, a, b) = 2 ν y; νz; ν w; f : m 1 (x); 5 ν g: m 3 (y, z);

Fig. 2 .

 2 Fig. 2. Running example of a alt program.

Fig. 3 .

 3 Fig. 3. The translation of alt statements.

Fig. 6 .

 6 Fig. 6. Equations from the translate function Fig. 4.

Fig. 7 .

 7 Fig. 7. Experimental results (times in ms).

=*

  ({flat(S) | S ∈ V }, {(flat(S), flat(S )) | (S, S ) ∈ E}) where (V , E) = point-to(cn)/ ) = N∈M O ∈N O ∩ {x | x ∈ cn}

( 5 )when p = 0 ( 7 )( 8 )Fig. 8 .

 50788 Fig. 8. The translation of alt runtime terms.

( 2 = 1 =

 21 vi) Case s = f ;s with x / ∈ I( f ). Let S = I( f ). By rule (5) of Fig.3, we have thatT S (I, 2 , x, l, t 2 , s) = T S (I \ F , f 2 , x, 0, exp 3 , s ) T S (I, 1 , x, l, t 1 , s) = T S (I \ F , f 1 , x, 0, exp 4 , s ) with F = { f | I( f ) = S(x) or I( f ) = I( f )} and exp 3 = max(t 2 + l, [[ 2 (I( f ))]]), exp 4 = max(t 1 + l, [[ 1 (I( f ))]]) f ( 2 exp 3 ) \ I( f ), f ( 1 exp 4 ) \ I( f )

f 2 )

 2 = dom( f 1 ), and let us consider A ∈ dom( f 1 ), we then have[[ f 2 (A)]] = max(k + max(exp A 1 , exp 1 + l, exp I( f ) 1 ), max(exp A 2 , exp 2 + l, exp I( f ) 2 )) [[ f 1 (A)]] = max(max(exp A 1 , exp 1 + l, exp I( f ) 1 ), max(exp A 2 , exp 2 + l, exp I( f ) 2 ))

  • • , m n in program declarations are pairwise different.

	Example 2.1. To illustrate alt, consider the program:
	1 main(x, a, b) =
	2	ν y; νz;

3 ν f : timer(y, a); 4 f ; 5 ν g: timer(z, b); 6 g ; 8 main (x, a, b) = 9 ν y; νz; 10 ν f : timer(y, a); 11 ν g: timer(z, b); 12 f ; 13 g ; 15 timer(x, n) = 16 wait(n);

) 9

 9 : {h → {w}}, {{w} → (t 6 • m 4 , 0 t 9 )}, 0, t 9 [ t 9 = max t 8 + m 1 , t 4 + max(m 3 , a) + max(m 2 , 0) ] (5) 10 : {h → {w}}, {{w} → (t 6 • m 4 , b t 9 + b)}, 0, t 10 [ t 10 = t 9 + b ] (1) 11 : ∅, ∅, 0, t 11 [ t 11 = max t 10 , t 6 + max(m 4 , b), t 9 + b ] (5) 12 : ∅, ∅, 0, t 12 [ t 12 = t 11 ] (6)

Fig. 4. Application of the translate function to main of Fig. 2. Every line l has pattern l :

(I i , i , l i , t i ) [t i ] (c i ), where [t i ] is the calculation of t i and (c i )

is the translate function case applied.

  Let S = S(y). By rule (3) of Fig.3, we have thatT S (I, 2 , x, l, t 2 , s) = T S (I[ f → S], f 2 , x, l, t 2 , s ) T S (I, 1 , x, l, t 1 , s) = T S (I[ f → S], f 1 , x, l, t 1 , s ) with f 2 = 2 [S → ε 2 • m(e), 0 ], f 1 = 1 [S → ε 1 • m(e), 0 ] and ε 2 = 2 (S), ε 1 = 1 (S) if S ∈ dom( 1 ) ε 2 = t 2 , ε 1 = t 1 else It is easy to see that dom( = max(k + exp S 1 , exp S 2 ), [[ = max(exp S 1 , exp S 2 ) if S ∈ dom( 1 ) [[ f 2 (S)]] = max(k + exp 1 , exp 2 ), [[ f 1 (S)]] = max(exp 1 , exp 2 )else Hence, with the induction hypothesis, we conclude the case.

		f 2 ) = dom(	f 1 ) and that
	[[	f 2 (S)]]

3, we have that

T S (I, 2 , x, l, t 2 , s) = T S (I[ f → S(x)], 2 , x, l + m(e), t 2 , s ) T S (I, 1 , x, l, t 1 , s) = T S (I[ f → S(x)], 1 , x, l + m(e), t 1 , s )

Hence, with the induction hypothesis, we conclude the case.

(iv) Case s = ν f : m(y, z, e);s with y / ∈ S(x). f 1 (S)]]

  1 + e, exp A 2 + e) [[( 2 + e)( A)]] = max(k + exp A 1 + e, exp A 2 + e)Hence, with the induction hypothesis, we conclude the case. 2 Lemma A.9. Suppose given S, I, , x, e, s, t and t with: S, I, , x, e, 0 and s are coherent parameters; for all A ∈ dom( ), we have(A) = 0 • exp A Lemma A.14 (Upper Bound Stability 2/3). Suppose given a runtime configuration cn such that there exists cn with cn t → cn . Suppose moreover given a solution of the cost configuration of cn. Then, there exists a solution of the cost configuration of cn such that for all f ∈ dom( ), we have ( f ) + t ≤ ( f ).

x , 0 ; and 0 < t ≤ t. We then have T S (I, , x, exp x , 0, wait(t);s) = max(t + exp

1

x , max A∈dom( ) ( (A)

+ exp A x ))

with max(exp 1

x , max A∈dom( ) ( (A) + exp A x )) = T S (I, , x, exp x , 0, wait(tt );s)

http://costa .ls .fi .upm .es /timeanalysis.

We note im(I) the image of I , i.e., im(I) = {I( f ) | f ∈ dom(I)}.

Theorem A. 16 (Correction). Given an alt program P, and a solution of the cost equation of P, we have that ( f start ) is an upper bound of the execution time of P.

Proof. By induction on the reduction time of P, using the three previous lemma. 2

supported by Comunidad de Madrid as part of the program S2018/TCS-4339 (BLOQUES-CM) co-funded by EIE Funds of the European Union, by the Spanish MINECO project TIN2015-69175-C4-2-R and the SIRIUS Centre for Scalable Data Access (http://www.sirius -labs .no).

Proof. By rule [START_REF] Buyya | Cloud computing and emerging IT platforms: vision, hype, and reality for delivering computing as the 5th utility[END_REF] of Fig. 3, we have that T S (I, , x, exp x , 0, wait(t);s) = T S (I, + t, x, exp x , t, s) T S (I, , x, exp x , 0, wait(tt );s) = T S (I, + (tt ), x, exp x , (tt ), s)

Hence, this lemma is a direct consequence of Lemma A.8. 2 Lemma A.10. Suppose given S, I, , x, e, f and s with: S, I, , x, 0 e, and s are coherent parameters; for all A ∈ dom( ), we have (A) = 0 • e A , 0 ; and I( f ) = S(x). We then have T S (I, , x, e, 0, f ;s) = max(e + e , max A∈dom( ) ( (A)

with max(e , max A∈dom( ) ( (A) + e A )) = T S (I, , x, e, 0, s)

Proof. By rules ( 4) and [START_REF] Buyya | Cloud computing and emerging IT platforms: vision, hype, and reality for delivering computing as the 5th utility[END_REF] of Fig. 3, we have that T S (I, , x, e, 0, f ;s) = T S (I, + e, x, 0, e, s)

This result is thus a direct consequence of Lemma A.8. 2

Lemma A.11. Suppose given S, I, , x, e, f and s with: S, I, , x, e, 0 and s are coherent parameters; for all A ∈ dom( ), we have (A) = 0 • e A , 0 ; and I( f ) = S(x). We then have

with max(e , max A∈dom( ) ( (A)

. By rule (5) of Fig. 3, we have that

The result can thus be proven in a similar way to Lemma A.8. 2

Lemma A.12. Suppose given S, I, , x, exp x , f and s with: S, I, , x, e, 0 and s are coherent parameters; for all A ∈ dom( ), we have (A) = 0 • e A , 0 ; and f ∈ dom(I). We then have T S (I, , x, e, 0, f ;s) ≥ T S (I \ { f }, , x, e, 0, f ;s)

Proof. This is directly proven by induction on s, by remarking that (I( f )) is a simple expression. 2

A.2.3. Main results

Lemma A.13 (Upper Bound Stability 1/3). Suppose given a cost solution of the cost program generated from an alt

Then is also a cost solution of the runtime configuration cn def = act(start, s main ; f start , ∅).

Proof. Let us consider the cost program eq 1 of the program P, and the cost configuration eq 2 of the runtime configuration cn. By construction, eq 1 and eq 2 are identical, except maybe for the entry f start : we indeed have:

Remark that cn \ S cn (start) = ∅, by Lemma A.7, we thus have that translate sschem(S cn ,s main ) (I cn , cn \ S cn (start), start, 0, 0, s main ) = translate sschem({ {start} },s main ) (∅, ∅, start, 0, 0, s main ) which proves the result. 2