Manish Gaur

S Arun-Kumar

On Efficiency Preorders

Theories of efficiency preorders and precongruences for concurrent systems have been described in various papers. We describe a procedure to implement two of these precongruences. Considering the extra information that is needed to be maintained while computing efficiency preorders, our procedure with a complexity O(n 3 m), compares favourably with that for deciding observational equivalence (O(n α m)). Further, the algorithm may be plugged in to existing model-checkers such as the Concurrency-Workbench of the New Century (CWB-NC) without any significant overheads of space or time.

Introduction

Research in process algebra has focused on the use of behavioural relations such as equivalences and refinement orderings as a basis for establishing system correctness. In the process algebraic framework, both specifications and implementations are defined in the same language; the intuition is that a specification describes the desired high level behaviour, while the implementation details the proposed means for achieving this behaviour. One then uses an appropriate equivalence or preorder to establish that an implementation behaves as defined in the specification. In the case of equivalence based reasoning, an implementation is correct if its behaviour is indistinguishable from that of its specification. Refinement (or Preorder) relations, on the other hand, typically embody a notion of comparison: an implementation conforms to (or refines) a specification if the behaviour of the former is "at least as good as" that stipulated by the specification. The benefits of such process algebraic approaches include the following:

-Users as well as testing and verification tools work within a single formalism for specification and implementation.

With support from Sun Microsystems Inc. USA

-The algebra provides explicit support for compositional specification and implementation, allowing the specification (implementation) of a system to be built up from the specification (implementation) of its components. -Specifications include information about what is disallowed as well as what is allowed.

Consequently, a number of different process algebras have been studied, and a variety of different equivalences and refinement relations capturing different aspects of behaviour have been developed. The simplest of these equivalences is the notion of bisimulation and there exist efficient algorithms and tools to implement various bisimulation-based preorders and equivalences. In general, algorithms for computing semantic equivalences and preorders usually consist of two steps. In the first step, the entire state space is generated and the second step then manipulates this space to determine whether an appropriate relation exists. Such algorithms are usually referred to as "global", as opposed to "onthe-fly" or "local" algorithms which work on a partially generated state space in an attempt to mitigate the state explosion problem in verification.

Refinements could come in several flavours. One of the earliest refinement relations ( [START_REF] Hennessy | Algebraic Theory of Processes[END_REF], [START_REF] Hoare | Communicating Sequential Processes[END_REF]) in the process algebra framework related refinement to the level of indeterminacy in the specification i.e. a more determinate process was considered a refinement of a less determinate one in terms of behaviour. Other notions of refinement such as action refinement yield various other preorders.

One such method is efficiency prebisimulation for processes ([4], [2], [3]). It is based on the simple idea of, essentially, counting the number of internal moves by a process. It has also been shown that it can be incorporated within the general frame work of bisimulation, to obtain a mathematically tractable preorder, which in common with the standard notions of bisimulation equivalence, is sensitive to the branching structure of processes.

Hence in the context of verification and development methodology it is more fruitful to regard these preorders as particular refinement relations. Due to the state explosion problem in verifying concurrent systems, it makes more sense to adopt a top-down methodology in both the development and verification of concurrent systems.

An alternative method to alleviate the state explosion problem is to use congruences and precongruences on the specification language as detailed below.

Consider a specification S 0 of a system. An initial refinement of this system would typically split the specification into (specifications of) subsystems S 1 , S 2 , . . . , S n combined in some fashion to obtain a first refinement

S 1 = o(S 1 , S 2 , . . . , S n )
where o is some appropriately defined combinator. Under a typical precongruence ≤ c as defined in ([4], [2], [3]) we would have S 1 ≤ c S 0 . The problem now reduces to obtaining refinements (S 1 1 , S 1 2 , . . ., S 1 n ) such that for each i,

1 ≤ i ≤ n, S 1 i ≤ c S i . It is then clear from the properties of ≤ c that S 2 = o(S 1 1 , . . . , S 1 n ) ≤ c o(S 1 , . . . , S n ) ≤ c S 0
Hence the problem of developing and verifying a large system to satisfy a specification S may be broken down to the problem of performing n smaller verification problems viz.

S 1 i ≤ c S i (1 ≤ i ≤ n).
The above verification methodology has the following advantages:

1. It closely follows the development methodology rather than postponing the problem of verification of a possible complex system to the end. 2. This methodology allows for the verification of the large system to be directly inferred from the verification of the smaller subsystems (without actually performing the verification).

A characteristic of process-oriented behavioural relations is that they are usually defined on labeled transition systems, which forms the semantic model of systems, rather than with respect to a particular syntax of process descriptions. This style of definition permits notions of equivalence and refinement to be applied to any algebra with a semantics given in terms of labeled transition systems. If in addition, these labeled transition systems are finite state, then the relation may be calculated in a purely mechanical manner: algorithms may then be developed for automatically checking that an implementation satisfies a specification.

In this paper we propose a method for computing efficiency prebisimulations for processes which are in fact bisimulation-based refinement relations called efficiency preorders. There exist very good algorithms [START_REF] Paige | Three partition refinement refinement algorithms[END_REF][START_REF] Kanellakis | Ccs expressions, finite state processes and three problem of equivalence[END_REF][START_REF] Groote | An efficient algorithm for branching bisimulation and stuttering equivalence[END_REF]] and tools such as [START_REF] Parrow | The concurrency workbench: A semantic based tool for the verification of the concurrent systems[END_REF] to construct strong and weak bisimulations on labeled transition systems. But little attention is given in computing the efficiency preorders. We believe that incorporating the feature of computation of efficiency preorder on a labeled transition system will add significant power to the verification tools like CWB-NC [START_REF] Parrow | The concurrency workbench: A semantic based tool for the verification of the concurrent systems[END_REF].

Theories of efficiency preorders (which combine both correctness and efficiency considerations into a single preorder) have been developed in various papers ( [2], [4], [3]). The largest precongruences contained in these preorders have also been characterized and axiomatized for finite CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF] processes. The notion of efficiency in these cases is abstract enough to be interpreted loosely as based on timing, communication or even energy consumed in a computation. Efficiency Preorder has been studied in modeling various distributed systems, where a notion of comparison is used reflect the fact one implementation is at least as good as another. Most recently the concept of efficiency preorder has been used in [START_REF] Gaur | Counting the cost in the picalculus (extended abstract)[END_REF] in context of an extension of asynchronous pi-calculus [START_REF] Milner | Communicating and mobile systems: The π-Calculus[END_REF].

Many equivalence and preorder checking problems on labelled transition systems may be reduced to the problem of constructing a strong bisimulation. In any labeled transition system of finite state processes if n is the total number of states and m the number of transitions then Paige and Tarjan [START_REF] Paige | Three partition refinement refinement algorithms[END_REF] gave an O(m log(n)) solution to the generalised partitioning problem on some relation E on states of FSPs. Kanellakis and Smolka studied the problem of equivalence checking of CCS expression and gave O(m log(n) + n) and O(n2 m log(n) + mn α ) time algorithms for strong bisimulation and weak bisimulation respectively [START_REF] Kanellakis | Ccs expressions, finite state processes and three problem of equivalence[END_REF].

Here the smallest such α known is 2.376 [START_REF] Coppersmith | Matrix multiplication via arithmetic progression[END_REF]. We propose a method running in O(mn 3 ) time complexity for deciding efficiency preorders.

The organization of the paper is as follows: In section 2 we give the basic definitions of labeled transition systems and various equivalences and preorders relevant to our purpose and characterize them. In section 3 we describe a method for constructing efficiency preorder. It is a polynomial time algorithm whose complexity is no more than that of deciding weak bisimulation. Section 4 is the conclusion. It briefly compares the time complexty of our method with that of deciding weak bisimulation.

Basic definitions and Characterization

In this section we will define and characterize a general framework in which the labelled transition system (LTS) on processes will be used to present an algorithm for deciding efficiency prebisimulations.

Definition 1. A Finite State Process (FSP) is a 5-tuple K, p 0 , A, -→, X where -K is a finite set of states, -p 0 ∈ K is the start state, -A is a finite set of labels, --→⊆ K × A × K is the transition 1 relation, -X ⊆ K × {x}, where x ∈ A, is the extension relation 2 .
LTSs tell us what behaviour of process is. The next question now is: when should two behaviours be considered equal? That is, what does it mean that two processes are equivalent? Intuitively, two processes should be equivalent if they cannot be distinguished by interacting with them. It's easy to observe that LTSs resemble graphs and the standard equality on graphs is graph isomorphism. In [START_REF] Milner | A Calculus of Communicating Systems[END_REF][START_REF] Sangiorgi | Introduction to Bisimulation and Coinduction[END_REF] it has been shown that graph isomorphism is too strong as a behavioural equivalences for processes. It prevents us equating processes that should be considered equal.

Another important notion of equivalence is present by the automata theory in computer science. The notion of automata and LTS are very similar and two automata are considered equal if they accept same set of labels (actions) [START_REF] John | Intoduction to Automata Theory, Langauages and Computation[END_REF].

The analogous equivalence on processes is called trace equivalence. But the trace equivalence as behaviour equality for processes is also not acceptable [START_REF] Milner | A Calculus of Communicating Systems[END_REF]. In fact for process equivalence we need a loose equality than graph isomorphism but a tighter correspondence between transitions than trace equivalence. Intuitively when some transition is done by a process the other must be able to mimic it and the evolved process out of these transitions must in turn be able to do the same again. This idea of equality, known as bisimilarity has been extensively studied [START_REF] Milner | A Calculus of Communicating Systems[END_REF]5] in process algebra. We will formally define this in the following definition.

Definition 2. Let P = K, p 0 , A, -→, X be a FSP and let ρ and σ be binary relations on Σ. A binary relation R on K is a (ρ, σ)-induced bisimulation if pRq implies the following conditions hold, for all α, β ∈ Σ.

1. p -→ α p ⇒ ∃β, q : αρβ ∧ q -→ β q ∧ p Rq , and 2. q -→ β q ⇒ ∃α, p : ασβ ∧ p -→ α p ∧ p Rq . A (=, =)-induced bisimulation will sometimes be called a natural bisimulation on a finite-state process.

A FSP may be represented by a labeled directed graph whose nodes are states and whose arcs have labels from A. We will be particularly interested in the case where the the set of labels of a FSP is a finite set A of symbols called actions such that τ ∈ A is a distinguished action called the invisible action and V = A -{τ } is the set of visible actions.

Let A * denote the set of all finite sequences of actions (including the empty sequence ε). We write ŝ to denote the sequence obtained from s ∈ A * by deleting all occurrences of τ . If s contains no visible action then ŝ yields ε. Finally |s| denotes the length of the sequence s. We write s =t if ŝ = t.

For s, t ∈ A * and a ∈ A, the transitions p -→ s p and p =⇒ s p are defined by induction on the length of s as follows p -→ ε p for all p, p -→ s p for s = ta iff ∃p : p -→ t p -→ a p , p =⇒ ε p iff ∃m ≥ 0 : p -→ τ m p , p =⇒ a p iff ∃p , p : p =⇒ ε p -→ a p =⇒ ε p , and p =⇒ s p for s = ta iff ∃p : p =⇒ t p =⇒ a p . Let be the relation on A * generated by the inequations s s and τ s s, i.e. is closed under reflexivity, transitivity and substitution under catenation contexts. It is clear that ε τ , sτ s for all s and that is antisymmetric. Hence is a partial order on A * and s = t iff s t and t s. We will be particularly interested in the set of extended actions defined by EA = {u ∈ A * | |û| ≤ 1}, viz. the set of sequences which contain at most one visible action. It is easy to see that for any a ∈ V and v ∈ EA, a v implies v = a. Also τ i τ j iff i ≥ j.

Bisimulations can be regarded as one of the most important contributions of concurrency theory to computer science. Nowadays, bisimulation and coinductive techniques [START_REF] Sangiorgi | Introduction to Bisimulation and Coinduction[END_REF] developed from the idea of bisimulation are widely used.

Here we define two earliest discovered bisimulations called as strong and weak bisimualtion. Definition 3. A binary relation R on the states of a FSP K, p 0 , A, -→, X , is a strong bisimulation (also ∼-bisimulation) if pRq implies for every a ∈ A, 1. p -→ a p ⇒ ∃q : q -→ a q ∧ p Rq , and 2. q -→ a q ⇒ ∃p : p -→ a p ∧ p Rq . a weak bisimulation (also ≈-bisimulation) if pRq implies for every a ∈ A 1. p -→ a p ⇒ ∃q : q =⇒ â q ∧ p Rq and 2. q -→ a q ⇒ ∃p : p =⇒ â p ∧ p Rq . Some enhancements were proposed shortly after discovery of strong and weak bisimulation. The best known example is Milner's bisimulation up to bisimilarity technique [START_REF] Milner | Communication and Concurrency[END_REF], in which the closure of the bisimulation relation is achieved up to bisimilarity itself. The up to bisimilarity is basically achieved with the fact that ∼ is a transitive relation. A problem with up to bismilarity is that the it fails for weak bisimulation despite it being transitive [START_REF] Sangiorgi | Beyond bisimulation: The up-to techniques[END_REF][START_REF] Sangiorgi | The problem of weak bisimulation up-to[END_REF]. In its place, a number of variations have been proposed; for instance allowing only uses of strong bisimilarity with in the upto bisimilarity [START_REF] Milner | Communication and Concurrency[END_REF]. The most important variation, however, involves a relation called expansion [3,[START_REF] Sangiorgi | The problem of weak bisimulation up-to[END_REF]. Expansion is a preorder derived from weak bismilarity by, essentially, comparing the number of silent actions. The idea underlying expansion is roughly that if Q expands P , then P and Q are bisimilar, except that in mimicking P 's behaviour, Q cannot perform more τ transitions than P . We can think of P uses at least as many resources as Q. An interest of expansion derives from the fact that, in practice, most of weak bisimilarity are indeed instances of expansion. Expansion is preserved by all CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF] operators but sum, and has a complete proof system for finite terms based of a modification of the standard τ laws for CCS. Expansion is also a powerful auxiliary relation for up to techniques involving weak forms of behaviour equivalences. Now we define following two expansions called efficiency prebisimulation and elaboration. These expansions typically embody a notion of efficiency where one process is at least as efficient as the other provided they are behaviourally equivalent. Definition 4. A binary relation R on the states of a FSP K, p 0 , A, -→, X , is an efficiency prebisimulation (also -bisimulation) if pRq implies for every u, v ∈ EA, 1. p -→ u p ⇒ ∃v, q : u v ∧ q -→ v q ∧ p Rq , and 2. q -→ v q ⇒ ∃u, p : u v ∧ p -→ u p ∧ p Rq . an elaboration (also < ≈ -bisimulation) if pRq implies for every a ∈ A, 1. p -→ a p ⇒ ∃q : q =⇒ â q ∧ p Rq , and 2. q -→ a q ⇒ ∃p : p =⇒ a p ∧ p Rq . Definitions 3 and 4 are from [2,4]. The following proposition is a direct consequence of these definitions. In Proposition 5, strong bisimulation, weak bisimulation, efficiency prebisimulation and elaboration are expressed over a sequence of actions.

1. Every strong bisimulation is an efficiency prebisimulation. 2. Every efficiency prebisimulation is an elaboration. 3. Every elaboration is a weak bisimulation. 4. For ∈ {∼, , < ≈ , ≈}, the largest -bisimulation, denoted , is a preorder. 5. For ∈ {∼, , < ≈ , ≈}, p q iff there exists a -bisimulation containing (p, q). 6. The largest ∼-and ≈-bisimulations, are equivalence relations.

The following simple examples in CCS syntax [START_REF] Milner | A Calculus of Communicating Systems[END_REF] give some idea of the distinctions between the relations discussed above. For CCS operators none of the relations , < ≈ , ≈, preserves summation. It is therefore necessary to consider the largest (pre)congruence contained in (and denoted c ) in order to be able to use refinement effectively.

Example 7. Let a be a visible action. Then 1. a.τ.0 < ≈ c a.0 but the converse does not hold.

2. a.0 + a.τ.0 c a.0 but the converse does not hold. =. Also for any a ∈ V and v ∈ EA, a . v implies v = a, and τ i . τ j iff i ≥ j. Further, . is coarser than (i.e. u v implies u . v but not the converse). We are now ready with the following lemma which is used in the characterization of Theorem 10. Lemma 8. Let R be a binary relation on the states of a FSP and pRq. The following are equivalent.

What we have described is essentially a "global" preorder checking method [START_REF] Cleaveland | Equivalence and preorder checking for finitestate system[END_REF] which may be smoothly integrated into a tool which implements natural bisimulation.

Our algorithm for efficiency prebisimulation reduces the given problem in O(n 3 m) time to another problem for which the solution is known and some extra processing whose time complexity is absorbed in the total time complexity of the reduction step. We compare the time complexity of the described method for efficiency prebisimulation, O(n 3 m+n 2 mlog(n)+n 2 m), with that of the weak bisimulation algorithm [START_REF] Kanellakis | Ccs expressions, finite state processes and three problem of equivalence[END_REF], which is O(n α m + n 2 mlog(n)), 2 < α ≤ 3. For weak bisimulation, the transitive closure of a directed graph having n nodes is computed in O(n α ) time using boolean matrix multiplication for which very elegant algorithms [START_REF] Coppersmith | Matrix multiplication via arithmetic progression[END_REF] are available. However, in the case of efficiency prebisimulation we are interested not just in finding transitive closure but in the number of τ moves padding each visible action, as well. Therefore it requires a time of O(n 3 ) to compute both transitive closure as well as the total number of invisible moves.

The entire computation of efficiency prebisimulation and elaboration is done in two steps, where the first step is to reduce the FSP P to another FSP P † and the second step is to compute the natural bisimulation relation in P † while comparing pairs of elements.

Rather than verifying a complete system specification against a complete implementation, congruence and precongruence properties may be usefully employed to split up a problem into several smaller individual sub-problems. Verification may then be carried out on the sub-problems.

In the case of CCS, the following result proved in [2] may be used to compute the precongruence relations for CCS processes. Proposition 14. For ∈ { , < ≈ , ≈}, p c q, iff for some visible action α not occurring in p or q, p + α q + α. p c q may be determined by using a special action that is not available to the user in the system specification language but is internal to the model checker.

There may exist other methods for tackling state explosion that may be worth exploring. One such is the use of the extension in FSPs as a naming device that abstracts away from complex internal structure and names structurally or behaviourally equal components by the same name. Thus far extensions were used only to distinguish deadlock/termination from other states. But the use of names in extensions may facilitate factoring out parts of systems and thus produce a collection of smaller graphs on which global algorithms may be run locally to check equivalences, congruences, preorders and precongruences.

we write p -→ α q to denote p, α, q ∈-→.

The extension relation has been kept for completeness and will not be used in the paper except to be referred in the conclusion.

We then have the following characterization of the two prebisimulations which will be used to present the algorithm to decide them in next section.

Theorem 10. (Characterization).

-The following are equivalent for any binary relation R on the states of a FSP. 1. R is an efficiency prebisimulation. 2. pRq implies for all u, v ∈ EA, p -→ u p ⇒ ∃v, q : u . v ∧ q -→ v q ∧ p Rq and q -→ v q ⇒ ∃u, p : u . v ∧ p -→ u p ∧ p Rq . 3. pRq implies for all s, t ∈ A * , p -→ s p ⇒ ∃q , t : s . t ∧ q -→ t q ∧ p Rq and q -→ t q ⇒ ∃p , s : s . t ∧ p -→ s p ∧ p Rq . and so are the following.

1. R is an elaboration.

2. pRq implies for all u, v ∈ EA, p -→ u p ⇒ ∃v, q : u =v ∧ q -→ v q ∧ p Rq and q -→ v q ⇒ ∃u, p : u . v ∧ p -→ u p ∧ p Rq . 3. pRq implies for all s, t ∈ A * , p -→ s p ⇒ ∃q , t : s =t ∧ q -→ t q ∧ p Rq and q -→ t q ⇒ ∃p , s : s . t ∧ p -→ s p ∧ p Rq .

The above characterization shows that the nature of efficiency prebisimulations remains unchanged even when the preorder is weakened to . . This fact provides us a convenient handle on which to base our algorithm.

Corollary 11. A binary relation R on the states of a FSP K, p 0 , EA, -→, X , is an efficiency prebisimulation iff it is a ( . , . )-induced bisimulation an elaboration iff it is a ( =, . )-induced bisimulation.

The Algorithm

For finite state processes with n the number of states and m the number of transitions Paige and Tarjan [START_REF] Paige | Three partition refinement refinement algorithms[END_REF] gave an O(mlog 2 (n)) solution to a generalised partitioning problem. Kanellakis and Smolka studied the problem of checking equivalences of CCS expressions and gave O(mlog 2 (n)+n) and O(n 2 mlog 2 (n)+mn α ) (where 2 < α ≤ 3) algorithms for strong and weak bisimulation respectively. In this section we present a method for computing prebisimulations.

A direct consequence of Theorem 10 is that the extended actions τ i aτ j and τ m aτ n are indistinguishable whenever i + j = m + n. It suffices therefore to consider the set EA = {(V ∪ {ε}) × N} (where N is the set of naturals) as representing the set of extended actions. For any a, m ∈ EA , we define p =⇒ a m p to mean ∃i, j : i + j = m ∧ p -→ τ i aτ j p and reserve the notation p =⇒ a p to mean ∃m : p =⇒ a m p . Consider the FSP P = K, p 0 , A, -→, X and the underlying directed graph G = K, -→ τ represented by a function λ :

For any path π = (p 1 , . . . , p k ) in G we define the length of the path π as len(π) = k-1 j=1 λ(p j , p j+1 ). Let Q k i,j be the set of paths from vertex p i to p j with all intermediate vertices in the set {p 1 , . . . , p k }. Let len k i,j = min π∈Q k i,j len(π). It follows that

We may use dynamic programming [START_REF] Cleveland | Introduction to Algorithms[END_REF]1] to solve the recurrence (1) for all values of i, j and k. If λ is represented by an n × n adjacency matrix, then the solution to recurrence (1) yields a n × n-matrix M τ * , where |K| = n.

For each α ∈ V ∪ {ε}, let M α be an n × n matrix of ordered pairs, whose first component is a boolean value and the second component is a natural number. Then we have

For each a ∈ V we may then compute the matrix ∆ a as follows. ∆ a (i, l) = M ε (i, j).M a (j, k).M ε (k, l), where (b, x).(c, y) = (b ∧ c, x + y). Let ∆ * a be the matrix containing only the first components of ∆ a .

It is easy to see that

Given an FSP P = K, p 0 , A, -→, X , we may therefore construct the FSP P † = K, p 0 , EA , ∆ † , X by the above procedure. By simply ignoring the second component in each element of the matrix ∆ † we obtain also the FSP P * = K, p 0 , V ∪ {ε}, ∆ * , X . For α = a, m , β = b, n ∈ ∆ † , let α ≤ . β if and only if a = b and m ≤ n. Further let α =β if and only if a = b. Then Proposition 12. Let P = K, p 0 , A, -→, X be a FSP and let P † and P * be the FSPs obtained by from P by the above procedure. Then for any states p, q ∈ K, 1. p ∼ q in P iff there exists a natural bisimulation R on the states of P † with pRq. 2. p q in P iff there exists a (≤ . , ≤ . )-induced bisimulation R on the states of P † with pRq.

p <

≈ q in P iff there exists a ( =, ≤ . )-induced bisimulation R on the states of P † with pRq. 4. p ≈ q in P iff there exists a natural bisimulation R on the states of P * with pRq.

Proof. Directly follows from the construction of the transition relation ∆ † . Note that comparison under . involves comparing second components, whenever the transitions exist under ∆ † . By ignoring the second component in each element of ∆ † , we may compare two elements in ∆ † under =.

Theorem 13. Let p, q be states of a FSP and assume that the FSP to which these states belong have a total of n states and m transitions. Then both the relations and < ≈ may be decided in O(mn 3 ) time.

Proof. The correctness follows from proposition 12. As for the time complexity, equation (1) requires O(n 3 ) time to solve. Since there may be at most m distinct actions, the computation of ∆ † would require O(mn 3 ) time (here O(n 3 ) is the matrix multiplication time). We also know that a natural bisimulation may be computed in O(mn 2 log(n)) time since the size of ∆ † is O(mn 2 ). And finally the comparison of all tuples for deciding both efficiency prebisimulation and elaboration will not take more than O(mn 2 ) time. Therefore the total time complexity for the algorithm is O(mn 3 + n 2 mlog(n) + mn 2 ) = O(mn 3 ).


Keiko Nakata

Andri Saar

Compiling Cooperative Task Management to Continuations

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

In a preemptive concurrency model, threads may be suspended and activated at any time. While preemptive models are dominant for multi-threaded concurrency, they may be criticized for the complexity of reasoning because of the implicit context switches. The programmer often has to resort to low-level synchronization primitives, such as locks, to prevent unwanted context switches. Programs written in such a way tend to be error-prone and are not scalable. The actor model [START_REF] Agha | Actors: a model of concurrent computation in distributed systems[END_REF] addresses this issue. Actors encapsulate the thread of control and communicate with each other by sending messages. They are also able to call blocking operations such as sleep, await and receive, reminiscent of cooperative multi-tasking. Erlang and Scala actors support actor-based concurrency models.

Creol [START_REF] Johnsen | Creol: A type-safe object-oriented model for distributed concurrent systems[END_REF] and ABS [START_REF] Johnsen | ABS: a core language for abstract behavioral specification[END_REF] combine a message-passing concurrency model and a cooperative concurrency model. In Creol, each object encapsulates a thread of control and objects communicate with each other using asynchronous method calls. Asynchronous method calls, instead of messages-passing, provide a typesafe communication mechanism and are a good match for object-oriented languages [START_REF] Caromel | Asynchronous and deterministic objects[END_REF][START_REF] De Boer | A complete guide to the future[END_REF]. ABS generalizes the concurrency model of Creol by introducing concurrent object groups [START_REF] Schäfer | JCoBox: generalizing active objects to concurrent components[END_REF] as the unit of concurrency. The concurrency model of ABS can be split in two: in one layer, we have local, synchronous and sharedmemory communication 1 in one concurrent object group (COG) and on the second layer we have asynchronous message-based concurrency between different concurrent object groups as in Creol. The behavior of one COG is based on the cooperative multitasking of external method invocations and internal method activations, with concrete scheduling points where a different task may get scheduled. Between different COGs only asynchronous method calls may be used; different COGs have no shared object heap. The order of execution of asynchronous method calls is not specified. The result of an asynchronous call is a future; callers may decide at run-time when to synchronize with the reply from a call. Asynchronous calls may be seen as triggers that spawn new method activations (or tasks) within objects. Every object has a set of tasks that are to be executed (originating from method calls). Among these, at most one task of all the objects belonging to one COG is active; others are suspended and awaiting execution. The concurrency models of Creol and ABS are designed to be suitable in the distributed setting, where one COG executes on its own (virtual) processor in a single node and different COGs may be executed on different nodes in the network.

In this paper, we are interested in the compilation of cooperative multitasking into continuations, motivated to execute a cooperative multi-tasking model on the JVM platform, which employs a preemptive model. The basic idea of using continuations to manage the control behavior of the computation has been known from 80's [START_REF] Wand | Continuation-based multiprocessing[END_REF][START_REF] Haynes | Continuations and coroutines[END_REF], and is still considered as a viable technique [START_REF] Karmani | Actor frameworks for the JVM platform: a comparative analysis[END_REF][START_REF] Srinivasan | Kilim: Isolation-typed actors for Java[END_REF][START_REF] Adya | Cooperative task management without manual stack management[END_REF]. This is particularly so, if the programming language supports first-class continuations, as in the case of Scala, and hence one can obviate manual stack management. The contribution of the paper is a correctness proof of such a compilation scheme. Namely, we create a simplified source language, by extending the While language with (synchronous) procedure calls and operations for cooperative multi-tasking (i.e., blocking operations and creation of new tasks) and define a compilation function from the source language into the target language, which extends While with continuation operations-the target language is sequential. We then prove that the compilation preserves the operational behavior from the source language to the target language.

The remainder of the paper is organized as follows. We define the source language and its operational semantics in the next section, and the target language and its operational semantics in Section 3. In Section 4, we present the compilation function from the source language to the target language and, in Section 5 we prove its correctness. We conclude in Section 6. In Figure 1, we define the syntax for the source language. We use the overline notation to denote sequences, with denoting an empty sequence. It is the While language extended with (local) variable definitions, var x = e, procedure calls f (e), the await statement await e, creation of a new task spawn f e, and the return statement return. For simplicity, we syntactically distinguish local variable assignment x := e and global variable assignment u := e. The statement var x = e defines a (task) local variable x and initializes it with the value of e. The statement f (e) invokes the procedure f with arguments e, to be executed within the same task. The procedure does not return the result to the caller, but may store the result in a global variable. The statement await e suspends the execution of the current task, which can be resumed when the guard expression e evaluates to true. The statement spawn f e spawns a new task, which executes the body of f with arguments e. (Hence, in contrast to procedure calls, which are synchronous, spawn f e is like an asynchronous procedure call executed in a new task.) The return statement is a runtime construct, not appearing in the source program, and will be explained later.

Source language

We assume disjoint supplies of local variables (ranged over by x), global variables (ranged over by u), and procedure names (ranged over by f ). We assume a set of (pure) expressions, whose elements are ranged over by e. We assume the set of values to be the integers, non-zero integers counting as truth and zero as falsity. The metavariable v ranges over values. We have two kinds of stateslocal states and global states. A local state, ranged over by ρ, maps local variables to values; a global state, ranged over by σ, maps global variables to values. We denotes by ∅ an empty mapping, whose domain is empty. Communication between different tasks is achieved via global variables. For simplicity, we assume a fixed set of global variables. The notation ρ[x → v] denotes the update of ρ with v at x, when x is in the domain of ρ. If x is not in the domain, it denotes a mapping extension. The notation σ[u → v] denotes similar. We assume given an evaluation function e (ρ,σ) , which evaluates e in the local state ρ and the global state σ. We write (ρ, σ) |= e and (ρ, σ) |= e to denote that e is true, resp. false with respect to ρ and σ. A stack Π is a non-empty list of local states, whose elements are separated by semicolons. A stack grows leftward, i.e., the leftmost element is the topmost element.

A program P consists of a procedure environment env F which maps procedure names to pairs of a formal argument list and a statement, and a global state which maps global variables to their initial values. The entry point of the program will be the procedure named main.

We define the operational semantics of the source language as a transition system on configurations, in the style of structural operational semantics. A configuration cfg consists of an active task identifier n, a global variable mapping σ and a set of tasks Θ. A task has an identifier and may be in one of the three forms: a triple e, S, Π , representing a task that is awaiting to be scheduled, where e is the guard expression, S the statement and Π its stack; or, a pair S, Π , representing the currently active task; or, a singleton Π , representing a terminated task.

Configuration cfg

::= n, σ Θ Task sets Θ ::= n e, S, Π | n S, Π | n Π | Θ Θ
The order of tasks in the task set is irrelevant: the parallel operator is commutative and associative. Formally, we assume the following structural equivalence:

Θ ≡ Θ Θ Θ ≡ Θ Θ Θ (Θ Θ ) ≡ (Θ Θ ) Θ
Transition rules in the semantics are in the form env F cfg → cfg , shown in Figure 2. The first two rules (S-Cong and S-Equiv) deal with congruence and structural equivalence. The rules for assignment, skip, if-then-else and while are self-explanatory. For instance, in the rule S-Assign-Local, the task is of the form n S, Π where S = x := e and Π = ρ; Π. Note that the topmost element of the stack Π is the current local state. The rules for sequential composition may deserve some explanation. If the first statement S 1 suspends guarded by e in the stack Π with the residual statement S 1 to be run when resumed, then the entire statement S 1 ; S 2 suspends in e, S 1 ; S 2 , Π , where the residual statement now contains the second statement S 2 (S-Seq-Grd). If S 1 terminates in Π , then S 2 will run next in Π (S-Seq-Fin). Otherwise, S 1 transfers to S 1 with the stack Π , so that S 1 ; S 2 transfers to S 1 ; S 2 with the same stack (S-Seq-Step). The await statement immediately suspends (S-Await) the currently active task, enabling us to switch to some other task in accordance to the scheduling rules. An example of the await statement (and the scheduling rules) at work can be found in the example in Figure 3. The statement spawn f e creates a new task n true, S, [x → v] with n a fresh identifier (S-Spawn). The caller task continues to be active. The newly created task is suspended, guarded by true, and may get scheduled at scheduling points by the scheduling rules (see below). Procedure invocation f (e) evaluates the arguments e in the current state, pushes into the stack the local state [x → v], mapping the formal parameters to the actual arguments, and transfers to S; return, where S is the body of f (S-Call). The return statement pops the topmost element from the stack (S-Return). The local variable definition var x = e extends the current local state with the newly defined variable and initializes it with the value of e (S-Var).

The last three rules deal with scheduling. If the current active task has terminated, then a new task whose guard evaluates to true is chosen to be active (S-Sched-Fin). When the active task suspends, a scheduling point is reached. The rule (S-Sched-Same) considers the case in which the same task is scheduled; the rule (S-Sched-Other) considers the case in which a different task is scheduled.

As an example, we will look at a program containing one global variable u with the initial value 0 and the following procedures:

f → u := 1 main → u := 3; spawn f ; await u = 1; u := 2
A detailed step, showing the full derivation, can be seen in Figure 4. A full execution trace, showing all intermediate configurations, is shown in Figure 3.

env F n, σ Θ → n , σ Θ env F n, σ Θ Θ → n , σ Θ Θ S-Cong Θ ≡ Θ env F n, σ Θ → n , σ Θ Θ ≡ Θ env F n, σ Θ → n , σ Θ S-Equiv x ∈ dom ρ env F n, σ n x := e, ρ; Π → n, σ n ρ[x → e (ρ,σ) ]; Π S-Assign-Local u ∈ dom σ env F n, σ n u := e, Π → n, σ[u → e (ρ,σ) ] n Π S-Assign-Global env F n, σ n S1, Π → n , σ n e, S 1 , Π Θ env F n, σ n S1; S2, Π → n , σ n e, S 1 ; S2, Π Θ S-Seq-Grd env F n, σ n S1, Π → n , σ n Π Θ env F n, σ n S1; S2, Π → n , σ n S2, Π Θ S-Seq-Fin env F n, σ n S1, Π → n , σ n S 1 , Π Θ env F n, σ n S1; S2, Π → n , σ n S 1 ; S2, Π Θ S-Seq-Step (ρ, σ) |= e env F n, σ n if e then S1 else S2, ρ; Π → n, σ n S1, ρ; Π S-If-True (ρ, σ) |= e env F n, σ n if e then S1 else S2, ρ; Π → n, σ n S2, ρ; Π S-If-False (ρ, σ) |= e env F n
env F f = (x, S) v = e (ρ,σ) n is fresh env F n, σ n spawn f e, ρ; Π → n, σ n ρ; Π n true, S, [x → v] S-Spawn env F n, σ n await e, Π → n, σ n e, skip, Π S-Await x ∈ dom ρ env F n, σ n var x = e, ρ; Π → n, σ n ρ[x → e (ρ,σ) ]; Π S-Var env F f = (x, S) v = e (ρ,σ) env F n, σ n f (e), ρ; Π → n, σ n S; return, [x → v]; ρ; Π S-Call env F n, σ n return, ρ; Π → n, σ n Π S-Return (ρ, σ) |= e env F n, σ n Π n e,
:= 2, ∅ → main, [u → 3] main spawn f ; await u = 1; u := 2, ∅ → main, [u → 3] main await u = 1; u := 2, ∅ f true, u := 1, ∅ → main, [u → 3] main u = 1, skip; u := 2, ∅ f true, u := 1, ∅ → f, [u → 3] main u = 1, skip; u := 2, ∅ f u := 1, ∅ → f, [u → 1] main u = 1, skip; u := 2, ∅ f ∅ → main, [u → 1] main skip; u := 2, ∅ f ∅ → main, [u → 1] main u := 2, ∅ f ∅ → main, [u → 2] main ∅ f ∅ Fig. 3.
The full execution trace of the example program 3 Target language

env F main, [u → 3] main await u = 1, ∅ → main, [u → 3] main u = 1, skip, ∅ S-Await env F main, [u → 3] main await u = 1; u := 2, ∅ → main, [u → 3] main u = 1, skip; u := 2, ∅ S-Seq-Grd env F main, [u → 3] main await u = 1; u := 2, ∅ f true, u := 1, ∅ → main, [u → 3] main u = 1, skip; u := 2, ∅ f true, u := 1, ∅ S-Cong
We proceed to the target language. In Figure 5, we present the syntax of the target language. Expressions of the target language contain, besides pure expressions, continuations [S, Π], which are pairs of a statement S and a stack Π, and support for guarded (multi)sets: collections which contain pairs of an expression and a value. The expression stored with each element is called a guard expression, and is evaluated when we query the set: only elements whose guard expressions hold may be returned. There are five expressions in the language to work with guarded sets: an empty set ∅, checking whether a set is empty (isEmpty e s ), adding an element (add e s e g e), fetching an element (get e s ) and removing an element (del e s e).

Similar to the source language, for the target language we extend While with local variable definitions and procedure calls. We also add delimited control operators, shift k {S}, reset {S}, invoke k [START_REF] Danvy | Abstracting control[END_REF]. The statement shift k {S} captures the rest of the computation, or continuation, up to the closest surrounding reset {}, binds it to k, and proceeds to execute S. In shift k {S}, k is a binding occurrence, whose scope is S. Hence, the statement reset {S} delimits the captured continuation. The statement invoke k invokes, or jumps into, the continuation bound to the variable k. The statement R {S}, where R is a new constant, is a runtime construct to be explained later.

The target language is sequential and, unlike the source language, it contains no explicit support for parallelism. Instead, we provide building blocks -contin- uations and guarded sets -that are used to switch between tasks and implement an explicit scheduler in Section 4.

We assume given an evaluation function e (Π,σ) for pure expressions, which evaluates e with respect to the stack Π (the evaluation only looks at the current local state, which is the topmost element of Π) and the global state σ. In Figure 6, the evaluation function is extended to operations for guarded sets.

We define an operational semantics for the target language as a reduction semantics over configurations, using evaluation contexts. A configuration S, Π, σ is a triple of a statement S, a stack Π and a global state σ.

Evaluation contexts E are statements with a hole, specifying where the next reduction may occur. They are defined by

E ::= [] | E; S | R {E}
We denote by E[S] the statement obtained by placing S in the hole of E.

We define basic reduction rules in Figure 6. reset {S} inserts a marker † into the stack, just below the current state, and reduces to R {S} to continue the execution of S (T-Reset). We use a marker to delimit the portion of the stack captured by shift and to align the stack when exiting from R {}. The runtime construct R {} is used to record that the marker has been set. shift k {S} captures the rest of the execution up to and including the closest surrounding R {} together with the corresponding portion of the stack, binds it to a fresh variable k in the local state, and continues with the statement S obtained by substituting k by k in S (T-Shift). The surrounding R {} is kept intact. F is an evaluation context that does not intersect R {}, formally,

F ::= [] | F ; S
Note that shift k {S} captures the stack up to and including the topmost †, which has been inserted by the closest surrounding reset. Once the body of R {} terminates, i.e., reduces to skip, then we remove the R {} and pop the stack until the topmost †, but leaving the state just above † in the stack (T-R). invoke k invokes the continuation bound to k (T-Invoke). Namely, if k is bound to [S, Π ] in the local or global state, then the statement reduces to S; return and the stack Π is pushed into the current stack. S must be necessarily of the form R {S }, where S does not contain R, and Π contains exactly one † at the bottom. When exiting from the R {}, the state immediately above † in Π will add es eg e (Π,σ) = es (Π,σ) ∪ (eg, e (Π,σ) ) get es (Π,σ) = v when ∃eg∃v. (eg, v) ∈ es (Π,σ) ∧ eg (Π,σ) = true del es e (Π,σ) = es (Π,σ) \(eg, e (Π,σ) ) when ∃eg. (eg, e (Π,σ) ) ∈ es (Π,σ)

isEmpty es (Π,σ) = true if es (Π,σ) = ∅ false otherwise env F reset {S}, ρ; Π, σ → R {S}, ρ †; Π, σ T-Reset Π does not contain † k fresh S is obtained from S by replacing k with k env F R {F [shift k {S}]}, ρ; Π †; Π , σ → R {S }, ρ[k → [R {F [skip]}, ρ; Π †]]; Π †; Π , σ T-Shift Π does not contain † env F R {skip}, Π; ρ †; Π , σ → skip, ρ; Π , σ T-R k (Π,σ) = [S, Π ] env F invoke k, Π, σ → S; return, Π ; Π, σ T-Invoke env F skip; S, Π, σ → S, Π, σ T-Skip env F f = (x, S) v = e (Π,σ) env F f (e), Π, σ → S; return, [x → v]; Π, σ T-Call
→ R {u := k }; invoke u, [k → [R {skip; u := 0}, ∅ †]] †, [u → 0; u → 1] → R {skip}; invoke u, [k → [R {skip; u := 0}, ∅ †]] †, [u → [R {skip; u := 0}, ∅ †]; u → 1] → invoke u, [k → [R {skip; u := 0}, ∅ †]], [u → [R {skip; u := 0}, ∅ †]; u → 1] → R {skip; u := 0}; return, ∅ †; [k → [R {skip; u := 0}, ∅ †]], [u → [R {skip; u := 0}, ∅ †]; u → 1] → R {u := 0}; return, ∅ †; [k → [R {skip; u := 0}, ∅ †]], [u → [R {skip; u := 0}, ∅ †]; u → 1] → R {skip}; return, ∅ †; [k → [R {skip; u := 0}, ∅ †]], [u → [R {skip; u := 0}, ∅ †]; u → 0] → return, ∅; [k → [R {skip; u := 0}, ∅ †]], [u → [R {skip; u := 0}, ∅ †]; u → 0] → skip, [k → [R {skip; u := 0}, ∅ †]], [u → [R {skip; u := 0}, ∅ †]; u → 0]
Fig. 7. Capturing and invoking a continuation be left in the stack, which is popped by the trailing return. An example of how to capture and invoke a continuation is shown in Figure 7. In the example, we assume that the variables u and u are global. Procedure call f (e) reduces to S; return where S is the body of the procedure f , and pushes a local state [x → v], binding procedure's formal arguments to actual arguments, into the stack (T-Call). The trailing return ensures that, once the execution of S; return terminates, the stack is aligned to the original Π. return pops the topmost element from the stack (T-Return). The remaining rules are self-explanatory.

Given the basic reduction rules, we now define a standard reduction, denoted by →, by env F S, Π, σ → S , Π , σ

env F E[S], Π, σ → E[S ], Π , σ
stating that the configuration S, Π, σ standard reduces to S , Π , σ if there exist an evaluation context E and statement S 0 and S 0 such that S = E[S 0 ] and S = E[S 0 ] and env F S 0 , Π, σ → S 0 , Π , σ . The standard reduction is deterministic.

Compilation

When compiling a program P into the target language, we compile expressions and statements according to the scheme shown in Figure 8. Expressions are translated into the target language as-is, and statements that have a corresponding equivalent in the target language are also translated in a straightforward manner. The two statements that have no direct correspondence in the target language are await and spawn. We look at how these statements are translated and how they interact with the scheduler later. The central idea of the compilation scheme is to use continuations to handle the suspension of tasks, and have an explicit scheduler (for brevity, in the examples we use Sched to denote the scheduler), shown in Figure 9. The control will pass to the scheduler every time a task either suspends or finishes, and the scheduler will pick up a new task to execute. During runtime, we also use a global variable T , which we assume not to be used by the program to be compiled. The global variable T stores the task set, corresponding to Θ in the source semantics, that contains all the tasks in the system. The tasks are stored as continuations with guard expressions.

The scheduler loops until the task set is empty (all tasks have terminated), in each iteration picking a continuation from T where the guard expression evaluates to true, removing it from T and then invoking the continuation using invoke k. The body of the scheduler is wrapped in a reset, guaranteeing that when a task suspends, the capture will be limited to the end of the current task. After the execution is completed -either by suspension or by just finishing the work -the control comes back to the scheduler.

Suspension (await e in the source language) is compiled to a shift statement. When evaluating the statement, the original computation until the end of the enclosing R {} will be captured and stored in the continuation k, and the original program is replaced with the body of the shift. The enclosing R {} guarantees that we capture only the statements up until the end of the current task, thus providing a facility to proceed with the execution of the task later.

n, σ n Π Θ = Sched , ∅, σ[T → Θ 2] n, σ n e, S, Π Θ = Sched , ∅, σ[T → Θ 2 ∪ n e, S, ρ 2] n, σ n S, Π Θ = R {R { S }; return}; Sched , Π †; ∅ †, σ[T → Θ 2] Θ Θ 2 = Θ 2 ∪ Θ 2 n e, S, Π 2 = {( e , [R {skip; S }, Π †])} n Π 2 = ∅ Fig. 10. Compilation of configurations
The body of the shift statement simply takes the captured continuation, k, and adds it to the global task set, with the appropriate guard expression. After adding the continuation to the task set, the control passes back to the scheduler. Procedures in env F will get translated into two different procedures for synchronous and asynchronous calls, as follows:

f S → S f A → reset {shift k {T := add T true k}; S }
When making an asynchronous call, the body of the procedure will be immediately captured in a continuation, added to the global task set, and the control passes back to the invoker via the usual synchronous call mechanism.

The entry point of a program in the source language, main, is a regular procedure and will get translated according to the usual rules into two procedures, main A and main S . In the target language, we must invoke the scheduler, and thus we use a different entry point:

T := ∅; main A (); Sched
After initializing the task set to be empty, the first statement will add an asynchronous call to the original entry point of the program, and passes control to the scheduler. As there is only one task in the task set -the task that will invoke the original entry point -the scheduler will immediately proceed with that.

Correctness

In this section, we prove that our compilation scheme is correct in the sense that it preserves the operational behavior from the source program into the (compiled) target program. Specifically, we prove that reductions in the source language are simulated by corresponding reductions in the target language. To do so, we extend the compilation scheme to configurations in Figure 10.

The compilation scheme for configurations follows the idea of the compilation scheme detailed in Section 4. We have two compilation functions: • 2 , which Every suspended task in the task set Θ is compiled to a pair consisting of the compiled guard expression and a continuation that has been constructed from the original statement and stack. The statement is wrapped in a R {} block and we prepend a skip statement, just as it would happen when a continuation is captured in the target language.

If the active task is finished or is suspended (but no new task has been scheduled yet), the generated configuration will immediately contain the scheduler. If the task has suspended, the task is compiled according to the previously described scheme and appended to T . Active tasks are wrapped in two R {} blocks and the stack Π is concatenated on top of the local state of the scheduler.

When the scheduler invokes a continuation k, the continuation will stay in the local state of the scheduler until control comes back to the scheduler. This is unnecessary, as the value is never used after it has been invoked; furthermore, the variable is immediately assigned a new value after control passes back to the scheduler. Thus, as an optimization, we may switch to an alternative reduction rule for invoke k, which only allows a continuation to be used once, T-InvokeOnce, shown in Figure 11. Although the behavior of the program is equivalent under both versions, using the one-shot version also allows us to state the correctness theorem in a more concise and straightforward manner, as the local state of the scheduler will always be empty when we are currently executing some task. In the proof, we assume this rule to be used instead of the original T-Invoke rule.

The following lemma states that the compilation of statements is compositional with respect to evaluation contexts, where evaluation contexts for the source language are defined inductively by

K := [] | K; S Lemma 1. K[S] = K S
Proof. By induction on the structure of K.

The correctness theorem below states that a one-step reduction in the source language is simulated by multiple-step reductions in the target language.

As an example, in Figure 12 we show the compiled form for both the initial and final configurations shown for the step in Figure 4 and in Figure 13, we show how to reach the compiled equivalent of the configuration in multiple steps in the target semantics. -

[u → 0; T → {(true, [R {skip; u := 1}, ∅ †])}] → R {R {skip}; return}; Sched, [k → [R {skip; skip; u := 2}, ∅ †]] †; ∅ †, [u → 0; T → {(true, [R {skip; u := 1}, ∅ †]), (u = 1, [R {skip; skip; u := 2}, ∅ †])}] → R {return}; Sched, [k → [R {skip; skip; u := 2}, ∅ †]]; ∅ †, [u → 0; T → {(true, [R {skip; u := 1}, ∅ †]), (u = 1, [R {skip; skip; u := 2}, ∅ †])}] → R {skip}; Sched, ∅ †, [u → 0; T → {(true, [R {skip; u := 1}, ∅ †]), (u = 1, [R {skip; skip; u := 2}, ∅ †])}] → Sched, ∅, [u → 0; T → {(true, [R {skip; u := 1}, ∅ †]), (u = 1, [R {skip; skip; u := 2}, ∅ †])}]
Case env F n, σ n S, Π Θ → n , σ n Π Θ
Rules matching this pattern are S-Assign-Local, S-Assign-Global, S-While-False, S-Spawn, S-Return, S-Var. As a representative example, we will look at S-Spawn in detail.

env F f = (x, S) v = e (ρ,σ) n is fresh env F n, σ n spawn f e, ρ; Π → n, σ n ρ; Π n true, S, [x → v]
In this case, the source and target configurations are compiled to:

cfg S = R {R {f A (e)}; return}; Sched, ρ; Π †; ∅ †, σ[T → Θ 2 ] cfg S = Sched, ∅, σ[T → Θ 2 ∪ {(true, [R {skip; S }, [x → v] †])}]
Let the bottommost element of Π be ρ , where ρ = ρ if Π is empty. The compiled source configuration will reduce as follows:

env F R {R {f A (e)}; return}; Sched, ρ; Π †; ∅ †, σ[T → Θ 2] → R {R {reset {shift k {T := add T true k}; S }; return}; return}; Sched, [x → v]; ρ; Π †; ∅ †, σ[T → Θ 2 ] → R {R {R {shift k {T := add T true k}; S }; return}; return}; Sched, [x → v] †; ρ; Π †; ∅ †, σ[T → Θ 2 ] → R {R {R {T := add T true k}; return}; return}; Sched, [x → v, k → [R {skip; S }, [x → v] †] †; ρ; Π †; ∅ †, σ[T → Θ 2 ] → R {R {R {skip}; return}; return}; Sched, [x → v, k → [R {skip; S }, [x → v] †] †; ρ; Π †; ∅ †, σ[T → Θ 2 ∪ {(true, [R {skip; S }, [x → v] †])}] → R {R {return}; return}; Sched, [x → v, k → [R {skip; S }, [x → v] †]; ρ; Π †; ∅ †, σ[T → Θ 2 ∪ {(true, [R {skip; S }, [x → v] †])}] → R {R {skip}; return}; Sched, ρ; Π †; ∅ †, σ[T → Θ 2 ∪ {(true, [R {skip; S }, [x → v] †])}] → R {return}; Sched, ρ ; ∅ †, σ[T → Θ 2 ∪ {(true, [R {skip; S }, [x → v] †])}] → R {skip}; Sched, ∅ †, σ[T → Θ 2 ∪ {(true, [R {skip; S }, [x → v] †])}] → Sched, ∅, σ[T → Θ 2 ∪ {(true, [R {skip; S }, [x → v] †])}]
The configuration we obtain from evaluation is exactly equal to the compiled configuration, thus for this case our claim holds. These three patterns match each of the scheduling rules. We will look only at the first one. The initial configuration will reduce as (with some of the steps omitted):

Conclusion

In this paper, we formalized a compilation scheme for cooperative multi-tasking into delimited continuations. For the source language, we extend While with procedure calls and operations for blocking and creation of new tasks. The target language extends While with shift/reset-the target language is sequential. We then proved that the compilation scheme is correct: reductions in the source language are simulated by corresponding reductions in the target language. We have implemented this compilation scheme in our compiler from ABS to Scala. The compiler covers a much richer language than our source language, including object-oriented features, and employs the experimental continuations plugin for Scala. The compiler is integrated into the wider ABS Tool Suite, available at http://tools.hats-project.eu/. We are currently formalizing the results of the paper in the proof assistant Agda.

SFig. 1 .

 1 Fig. 1. Syntax of the source language

  , σ n while e do S, ρ; Π → n, σ n S; while e do S, ρ; Π S-While-True (ρ, σ) |= e env F n, σ n while e do S, ρ; Π → n, σ n ρ; Π S-While-False env F n, σ n skip, Π → n, σ n Π S-Skip

Fig. 2 .

 2 Fig. 2. Semantics of the source language

Fig. 4 .

 4 Fig. 4. Example of a derivation in the source language

Fig. 5 .

 5 Fig. 5. Syntax of the target language

Fig. 6 .

 6 Fig. 6. Semantics of the target language

Fig. 8 .

 8 Fig. 8. Compilation of source programs

Fig. 11 .

 11 Fig. 11. Alternative rule for invoke

Fig. 12 .

 12 Fig. 12. Example of compiling a configuration

Fig. 13 .Theorem 1 .

 131 Fig. 13. Reduction of the compiled configuration

  -Case env F n, σ n S, Π Θ → n , σ n e,S , Π ΘThere are only two possible rules: S-Seq-Grd and S-Await. In both cases, it must be that σ = σ , Π = Π , Θ ≡ Θ and there exists some K such that S = K[await e] and S = K[skip]. Therefore, taking into account Lemma 1, the source and target configurations are compiled to:cfg S = R {R { K [ await e ]}; return}; Sched, Π †; ∅ †, σ[T → Θ 2] = R {R { K [shift k {T := add T e k}; skip]}; return}; Sched, Π †; ∅ †, σ[T → Θ 2] cfg S = Sched, ∅, σ[T → Θ 2 ∪ {( e , R { K [skip]}, Π †)}An example of this reduction can be seen in Figure13.-Case env F n, σ n S, Π Θ → n , σ n S , Π ΘRules matching this pattern are S-Seq-Fin, S-Seq-Step, S-If-True, S-If-False, S-While-True, S-Call. In the case of S-Seq-Step, we know that S = S 0 ; S 1 and S = S 0 ; S 1 . By induction hypothesis, we get thatenv F n, σ n S 0 , Π Θ → n , σ n S 0 , Π ΘAs by the definition of the compilation function S = S 0 ; S 1 and S = S 0 ; S 1 , we obtain the needed result:env F n, σ n S 0 ; S 1 , Π Θ → n , σ n S 0 ; S 1 , Π ΘFor S-Seq-Fin, we know that S = S 0 ; S 1 and S = S 1 . Then the case follows by analyzing the step taken to reduce S 0 . The other cases are straightforward. -One of the following three:

(

  ρ, σ) |= e env F n, σ n Π n e, S, ρ; Π → n , σ n S, ρ; Π n Π S-Sched-Fin cfg S = Sched, ∅, σ[T → {( e , [R {skip; S }, ρ; Π †])}] cfg S = R {R { S }; return}; Sched, ρ; Π †; ∅ †, σ[T → ∅]

  env F while (¬isEmpty T ) do reset {k := get T ;T := del T k; invoke k}, ∅, σ[T → {( e , [R {skip; S }, ρ; Π †])}] → reset {k := get T ; T := del T k; invoke k}; Sched, ∅, σ[T → {( e , [R {skip; S }, ρ; Π †])}] → R {k := get T ; T := del T k; invoke k}; Sched, ∅ †, σ[T → {( e , [skip; R { S }, ρ; Π †])}] → * R {invoke k}; Sched, [k → [R {skip; S }, ρ; Π †]] †, σ[T → ∅] → R{R {skip; S }; return}; Sched, ρ; Π †; ∅ †, σ[T → ∅] → R {R { S }; return}; Sched, ρ; Π †; ∅ †, σ[T → ∅]

In ABS, different tasks originating from the same object may communicate with each other via fields of the object.

Acknowledgments This research was supported by the EU FP7 ICT project no. 231620 (HATS), the Estonian Centre of Excellence in Computer Science, EXCS, financed mainly by the European Regional Development Fund, ERDF, the Estonian Ministry of Education and Research target-financed research theme no. 0140007s12, and the Estonian Science Foundation grant no. 9398.