# Compiling Cooperative Task Management to Continuations

Keiko Nakata, Andri Saar

► To cite this version:

Keiko Nakata, Andri Saar. Compiling Cooperative Task Management to Continuations. 5th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2013, Tehran, Iran. pp.95-110, 10.1007/978-3-642-40213-5_7. hal-01514661

HAL Id: hal-01514661

https://inria.hal.science/hal-01514661

Submitted on 26 Apr 2017

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques 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.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Compiling cooperative task management to continuations

Keiko Nakata and Andri Saar

Institute of Cybernetics at Tallinn University of Technology
Akadeemia tee 21, 12618 Tallinn

**Abstract.** Although preemptive concurrency models are dominant for multi-threaded concurrency, they may be criticized for the complexity of reasoning because of the implicit context switches. The actor model and cooperative concurrency models have regained attention as they encapsulate the thread of control. In this paper, we formalize a continuation-based compilation of cooperative multitasking for a simple language and prove its correctness.

## 1 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 [2] 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 [8] and ABS [7] 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 type-safe communication mechanism and are a good match for object-oriented languages [4,3]. ABS generalizes the concurrency model of Creol by introducing concurrent object groups [10] as the unit of concurrency. The concurrency model of ABS can be split in two: in one layer, we have local, synchronous and shared-memory communication<fnref n="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

<footnote n="1">¹ In ABS, different tasks originating from the same object may communicate with each other via fields of the object.</footnote>
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 multi-tasking 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 [12,6], and is still considered as a viable technique [9,11,1]. 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.

## 2 Source language

$$ S ::= x := e \mid u := e \mid \text{skip} \mid S_1; S_2 \mid \text{if} e \ \text{then} \ S_1 \ \text{else} \ S_2 \mid \text{while} e \ \text{do} \ S \\ \mid \text{var} \ x = e \mid f(\bar{e}) \mid \text{await} \ e \mid \text{spawn} \ f \ \bar{e} \mid \text{return} $$

<caption>**Fig. 1.** Syntax of the source language</caption>

In Figure 1, we define the syntax for the source language. We use the overline notation to denote sequences, with $\epsilon$ denoting an empty sequence. It is the
The order of tasks in the task set is irrelevant: the parallel operator `||` is commutative and associative. Formally, we assume the following structural equivalence:

$$ \Theta \equiv \Theta \qquad \Theta \parallel \Theta' \equiv \Theta' \parallel \Theta \qquad \Theta \parallel (\Theta' \parallel \Theta'') \equiv (\Theta \parallel \Theta') \parallel \Theta'' $$

Transition rules in the semantics are in the form $env_F \vdash cfg \rightarrow 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\langle S, \Pi' \rangle$ where $S = x := e$ and $\Pi' = \rho; \Pi$. Note that the topmost element of the stack $\Pi$ 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 $\Pi'$ with the residual statement $S'_1$ to be run when resumed, then the entire statement $S_1; S_2$ suspends in $\langle e, S'_1; S_2, \Pi' \rangle$, where the residual statement now contains the second statement $S_2$ (S-SEQ-GRD). If $S_1$ terminates in $\Pi'$, then $S_2$ will run next in $\Pi'$ (S-SEQ-FIN). Otherwise, $S_1$ transfers to $S'_1$ with the stack $\Pi'$, 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 \bar{e}$ creates a new task $n'\langle true, S, [\bar{x} \mapsto \bar{v}] \rangle$ 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(\bar{e})$ evaluates the arguments $\bar{e}$ in the current state, pushes into the stack the local state $[\bar{x} \mapsto \bar{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:

$$ \begin{array}{l} f \mapsto u := 1 \\ \text{main} \mapsto u := 3; \text{spawn } f \epsilon; \text{await } u = 1; u := 2 \end{array} $$

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.
<figure><img src="image_2.png" /><figcaption>Fig. 2. Semantics of the source language</figcaption></figure>
<figure><img src="image_3.png" /><figcaption>Fig. 3. The full execution trace of the example program</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 4. Example of a derivation in the source language</figcaption></figure>

## 3 Target language

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, \Pi]$, 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 $\emptyset$, 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 [5]`. 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-
<figure><img src="image_5.png" /><figcaption>Fig. 5. Syntax of the target language</figcaption></figure>

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 cur-
rent 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 | \mathbb{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
<figure><img src="image_6.png" /><figcaption>Fig. 6. Semantics of the target language</figcaption></figure>
<figure><img src="image_7.png" /><figcaption>Fig. 7. Capturing and invoking a continuation</figcaption></figure>

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

$$ \frac{\text{env}_F \vdash \langle S, \Pi, \sigma \rangle \rightarrow \langle S', \Pi', \sigma' \rangle}{\text{env}_F \vdash \langle E[S], \Pi, \sigma \rangle \rightarrow \langle E[S'], \Pi', \sigma' \rangle} $$

stating that the configuration $\langle S, \Pi, \sigma \rangle$ standard reduces to $\langle S', \Pi', \sigma' \rangle$ 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 $\text{env}_F \vdash \langle S_0, \Pi, \sigma \rangle \rightarrow \langle S'_0, \Pi', \sigma' \rangle$. The standard reduction is deterministic.

# 4 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.
<figure><img src="image_8.png" /><figcaption>Fig. 8. Compilation of source programs</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Fig. 9. Scheduler</figcaption></figure>

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 $\Theta$ 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.
$$
\begin{align*}
& [n, \sigma \triangleright n \langle \Pi \rangle \parallel \Theta] = \langle \mathit{Sched}, \emptyset, \sigma[T \mapsto [\Theta]]_2 \rangle \\
& [n, \sigma \triangleright n \langle e, S, \Pi \rangle \parallel \Theta] = \langle \mathit{Sched}, \emptyset, \sigma[T \mapsto [\Theta]]_2 \cup [n \langle e, S, \rho \rangle]_2 \rangle \\
& [n, \sigma \triangleright n \langle S, \Pi \rangle \parallel \Theta] = \langle \mathbb{R} \{[S]\}; \mathit{return}\rangle; \mathit{Sched}, \Pi \dagger; \emptyset \dagger, \sigma[T \mapsto [\Theta]]_2 \rangle \\
& [\Theta \parallel \Theta']_2 = [\Theta]_2 \cup [\Theta']_2 \\
& [n \langle e, S, \Pi \rangle]_2 = \{(\llbracket e \rrbracket, [\mathbb{R} \{\mathit{skip}\}; [S]]\}, \Pi \dagger]\} \\
& [n \langle \Pi \rangle]_2 = \emptyset
\end{align*}
$$

<caption>Fig. 10. Compilation of configurations</caption>

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<sub>F</sub> will get translated into two different procedures for synchronous and asynchronous calls, as follows:

$$
\begin{align*}
f_S &\mapsto [S] \\
f_A &\mapsto \mathit{reset} \{ \mathit{shift} \ k \ \{ T := \mathit{add} \ T \ \mathit{true} \ k \} ; [S] \}
\end{align*}
$$

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**<sub>A</sub> and **main**<sub>S</sub>. In the target language, we must invoke the scheduler, and thus we use a different entry point:

$$
T := \emptyset; \mathrm{main}_A(); \mathrm{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.

5 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: [[·]]<sub>2</sub>, which
$$ \frac{\rho x = [S, \Pi']}{\text{env}_F \vdash (\text{invoke } x, \rho; \Pi, \sigma) \rightarrow (S; \text{return}, \Pi'; \rho \setminus x; \Pi, \sigma)} \text{T-InvokeOnce} $$

<caption>**Fig. 11.** Alternative rule for invoke</caption>

generates a task set from $\Theta$, and $\llbracket \cdot \rrbracket$, which generates a configuration in the target semantics.

Every suspended task in the task set $\Theta$ 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 $\mathbb{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 $\mathbb{R}\{\}$ blocks and the stack $\Pi$ 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 := \llbracket \cdot \rrbracket \mid K; S $$

**Lemma 1.**

$$ \llbracket K[S] \rrbracket = \llbracket K \rrbracket [\llbracket S \rrbracket] $$

*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.
```
[[main, [u ↦ 0] ▷ main<await u = 1; u := 2, 0> || f<true, u := 1, 0>]]
= ⟨R {R {shift k {T := add T (u = 1) k}; skip; u := 2}; return}; Sched, 0†; 0†,
[u ↦ 0; T ↦ {⟨true, [R {skip; u := 1}, 0†]}>]
[[main, [u ↦ 0] ▷ main<u = 1, skip; u := 2, 0> || f<true, u := 1, 0>]]
= ⟨Sched, 0, [u ↦ 0; T ↦ {⟨u = 1, [R {skip; skip; u := 2}, 0†]⟩, (true, [R {skip; u := 1}, 0†])}⟩
```

<caption>**Fig. 12.** Example of compiling a configuration</caption>

```
⟨R {R {shift k {T := add T (u = 1) k}; skip; u := 2}; return}; Sched, 0†; 0†,
[u ↦ 0; T ↦ {⟨true, [R {skip; u := 1}, 0†]}>]
 ↦ ⟨R {R {T := add T (u = 1) k'}; return}; Sched, [k' ↦ [R {skip; skip; u := 2}, 0†]]†; 0†,
[u ↦ 0; T ↦ {⟨true, [R {skip; u := 1}, 0†]}>]
 ↦ ⟨R {skip}; return}; Sched, [k' ↦ [R {skip; skip; u := 2}, 0†]]†; 0†,
[u ↦ 0; T ↦ {⟨true, [R {skip; u := 1}, 0†]⟩, (u = 1, [R {skip; skip; u := 2}, 0†])}]
 ↦ ⟨R {return}; Sched, [k' ↦ [R {skip; skip; u := 2}, 0†]]; 0†,
[u ↦ 0; T ↦ {⟨true, [R {skip; u := 1}, 0†]⟩, (u = 1, [R {skip; skip; u := 2}, 0†])}]
 ↦ ⟨R {skip}; Sched, 0†,
[u ↦ 0; T ↦ {⟨true, [R {skip; u := 1}, 0†]⟩, (u = 1, [R {skip; skip; u := 2}, 0†])}]
 ↦ ⟨Sched, 0, [u ↦ 0; T ↦ {⟨true, [R {skip; u := 1}, 0†]⟩, (u = 1, [R {skip; skip; u := 2}, 0†])}]
```

<caption>**Fig. 13.** Reduction of the compiled configuration</caption>

**Theorem 1.** For all configurations `cfg_S` and `cfg'_S` such that

$$ \text{env}_F \vdash \text{cfg}_S \rightarrow \text{cfg}'_S $$

holds, then the following must also hold:

$$ [[\text{env}_F]] \vdash [[\text{cfg}_S]] \mapsto^+ [[\text{cfg}'_S]] $$

*Proof.* By induction over the derivation, analyzing the step taken. The possible steps have one of the following forms:

- Case

$$ \text{env}_F \vdash n, \sigma \triangleright n\langle S, \Pi \rangle \parallel \Theta \rightarrow n', \sigma' \triangleright n\langle \Pi' \rangle \parallel \Theta' $$

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.

$$ \frac{\text{env}_F f = (\bar{x}, S) \quad \bar{v} = [[\bar{e}]]_{(\rho, \sigma)} \quad n' \text{ is fresh}}{\text{env}_F \vdash n, \sigma \triangleright n\langle \text{spawn } f \bar{e}, \rho; \Pi \rangle \rightarrow n, \sigma \triangleright n\langle \rho; \Pi \rangle \parallel n'\langle \text{true}, S, [\bar{x} \mapsto \bar{v}] \rangle} $$

In this case, the source and target configurations are compiled to:

$$ \llbracket \text{cfg}_S \rrbracket = \langle \text{R} \{ \text{f}_A(\bar{e}) \}; \text{return} \rangle; \text{Sched}, \rho; \Pi; 0^\dagger, \sigma [T \mapsto \llbracket \Theta \rrbracket_2] \rangle \\ \llbracket \text{cfg}'_S \rrbracket = \langle \text{Sched}, 0, \sigma [T \mapsto \llbracket \Theta \rrbracket_2 \cup \{ (\text{true}, [\text{R} \{\text{skip}; \llbracket S \rrbracket\}], [\bar{x} \mapsto \bar{v}]^\dagger]) \} \rangle $$
Let the bottommost element of $\Pi$ be $\rho'$, where $\rho = \rho'$ if $\Pi$ is empty. The compiled source configuration will reduce as follows:

$$
\begin{align*}
& [[\text{env}_F]] \vdash \langle \mathbf{R} \{ \mathbf{R} \{ f_A(\bar{e}) \}; \text{return} \}; \text{Sched}, \rho; \Pi \dagger; \emptyset \dagger, \sigma [T \mapsto [[\Theta]]_2] \rangle \\
& \quad \mapsto \langle \mathbf{R} \{ \mathbf{R} \{ \text{reset} \{ \text{shift } k \{ T := \text{add } T \text{ true } k \} ; [[S]] \}; \text{return} \}; \text{return} \}; \text{Sched}, \\
& \qquad [\bar{x} \mapsto \bar{v}]; \rho; \Pi \dagger; \emptyset \dagger, \sigma [T \mapsto [[\Theta]]_2] \rangle \\
& \quad \mapsto \langle \mathbf{R} \{ \mathbf{R} \{ \text{shift } k \{ T := \text{add } T \text{ true } k \} ; [[S]] \}; \text{return} \}; \text{return} \}; \text{Sched}, \\
& \qquad [\bar{x} \mapsto \bar{v}] \dagger; \rho; \Pi \dagger; \emptyset \dagger, \sigma [T \mapsto [[\Theta]]_2] \rangle \\
& \quad \mapsto \langle \mathbf{R} \{ \mathbf{R} \{ \mathbf{R} \{ \text{skip} \}; \text{return} \}; \text{return} \}; \text{Sched}, [\bar{x} \mapsto \bar{v}] \dagger \dagger; \rho; \Pi \dagger; \emptyset \dagger, \\
& \qquad \sigma [T \mapsto [[\Theta]]_2 \cup \{ (\text{true}, [\mathbf{R} \{ \text{skip} ; [[S]] \}], [\bar{x} \mapsto \bar{v}] \dagger]) \} \rangle \\
& \quad \mapsto \langle \mathbf{R} \{ \mathbf{R} \{ \text{return} \}; \text{return} \}; \text{Sched}, [\bar{x} \mapsto \bar{v}, k \mapsto [\mathbf{R} \{ \text{skip} ; [[S]] \}], [\bar{x} \mapsto \bar{v}] \dagger; \rho; \Pi \dagger; \emptyset \dagger, \\
& \qquad \sigma [T \mapsto [[\Theta]]_2 \cup \{ (\text{true}, [\mathbf{R} \{ \text{skip} ; [[S]] \}], [\bar{x} \mapsto \bar{v}] \dagger]) \} \rangle \\
& \quad \mapsto \langle \mathbf{R} \{ \mathbf{R} \{ \text{skip} \}; \text{return} \}; \text{Sched}, \rho; \Pi \dagger; \emptyset \dagger, \sigma [T \mapsto [[\Theta]]_2 \cup \{ (\text{true}, [\mathbf{R} \{ \text{skip} ; [[S]] \}], [\bar{x} \mapsto \bar{v}] \dagger]) \} \rangle \\
& \quad \mapsto \langle \mathbf{R} \{ \text{return} \}; \text{Sched}, \rho'; \emptyset \dagger, \sigma [T \mapsto [[\Theta]]_2 \cup \{ (\text{true}, [\mathbf{R} \{ \text{skip} ; [[S]] \}], [\bar{x} \mapsto \bar{v}] \dagger]) \} \rangle \\
& \quad \mapsto \langle \mathbf{R} \{ \mathbf{R} \{ \text{skip} \}; \text{Sched}, \emptyset \dagger, \sigma [T \mapsto [[\Theta]]_2 \cup \{ (\text{true}, [\mathbf{R} \{ \text{skip} ; [[S]] \}], [\bar{x} \mapsto \bar{v}] \dagger]) \} \rangle \\
& \quad \mapsto \langle \text{Sched}, \emptyset, \sigma [T \mapsto [[\Theta]]_2 \cup \{ (\text{true}, [\mathbf{R} \{ \text{skip} ; [[S]] \}], [\bar{x} \mapsto \bar{v}] \dagger]) \} \rangle
\end{align*}
$$

The configuration we obtain from evaluation is exactly equal to the compiled configuration, thus for this case our claim holds.

– Case

$$
\text{env}_F \vdash n, \sigma \triangleright n \langle S, \Pi \rangle \parallel \Theta \rightarrow n', \sigma' \triangleright n \langle e, S', \Pi' \rangle \parallel \Theta'
$$

There are only two possible rules: S-SEQ-GRD and S-AWAIT. In both cases, it must be that $\sigma = \sigma'$, $\Pi = \Pi'$, $\Theta \equiv \Theta'$ 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:

$$
\begin{align*}
[[cfg_S]] &= \langle \mathbf{R} \{ \mathbf{R} \{ [[K]] [[await e]] \}; \text{return} \}; \text{Sched}, \Pi \dagger; \emptyset \dagger, \sigma [T \mapsto [[\Theta]]_2] \rangle \\
&= \langle \mathbf{R} \{ \mathbf{R} \{ [[K]] \text{shift } k \{ T := \text{add } T \text{ [e]} k \}; \text{skip} \} \}; \text{return} \}; \text{Sched}, \Pi \dagger; \emptyset \dagger, \sigma [T \mapsto [[\Theta]]_2] \rangle \\
[[cfg_S')] &= \langle \text{Sched}, \emptyset, \sigma [T \mapsto [[\Theta]]_2 \cup \{ ([e], \mathbf{R} \{ [[K]] [skip] \}, \Pi \dagger) \} \rangle
\end{align*}
$$

An example of this reduction can be seen in Figure 13.

– Case

$$
\mathrm{env}_F \vdash n, \sigma \triangleright n \langle S, \Pi \rangle \parallel \Theta \rightarrow n', \sigma' \triangleright n \langle S', \Pi' \rangle \parallel \Theta'
$$

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 that

$$
[[\text{env}_F]] \vdash [[n, \sigma \triangleright n \langle S_0, \Pi \rangle] \parallel \Theta] \rightarrow [[n', \sigma' \triangleright n \langle S'_0, \Pi' \rangle] \parallel \Theta']
$$

As by the definition of the compilation function $[[S]] = [[S_0]]$; $[[S_1]]$ and $[[S')] = [[S'_0]]$; $[[S'_1]]$, we obtain the needed result:

$$
[[\text{env}_F]] \vdash [[n, \sigma \triangleright n \langle S_0; S_1, \Pi \rangle] \parallel \Theta] \rightarrow [[n', \sigma' \triangleright n \langle S'_0; S_1, \Pi' \rangle] \parallel \Theta']
$$
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:

$$ \text{env}_F \vdash n, \sigma \triangleright n \langle \Pi' \rangle \parallel n' \langle e, S, \Pi \rangle \parallel \Theta \rightarrow n', \sigma \triangleright n \langle \Pi' \rangle \parallel n' \langle S, \Pi \rangle \parallel \Theta $$

$$ \text{env}_F \vdash n, \sigma \triangleright n \langle e', S', \Pi' \rangle \parallel n' \langle e, S, \Pi \rangle \parallel \Theta \rightarrow n', \sigma \triangleright n \langle e', S', \Pi' \rangle \parallel n' \langle S, \Pi \rangle \parallel \Theta $$

$$ \text{env}_F \vdash n, \sigma \triangleright n \langle e, S, \Pi \rangle \parallel \Theta \rightarrow n, \sigma \triangleright n \langle S, \Pi \rangle \parallel \Theta $$

These three patterns match each of the scheduling rules. We will look only at the first one.

$$ \frac{(\rho, \sigma) \models e}{\text{env}_F \vdash n, \sigma \triangleright n \langle \Pi' \rangle \parallel n' \langle e, S, \rho; \Pi \rangle \rightarrow n', \sigma \triangleright n' \langle S, \rho; \Pi \rangle \parallel n \langle \Pi' \rangle} \quad \text{S-SCHED-FIN} $$

$$ \llbracket \text{cfg}_S \rrbracket = \langle \text{Sched}, \emptyset, \sigma[T \mapsto \{([e], [R \{\text{skip}; [S]\}], \rho; \Pi^\dagger)]\}] \rangle $$

$$ \llbracket \text{cfg}'_S \rrbracket = \langle \mathbb{R} \{\llbracket S \rrbracket\}; \text{return}; \text{Sched}, \rho; \Pi^\dagger; \emptyset^\dagger, \sigma[T \mapsto \emptyset] \rangle $$

The initial configuration will reduce as (with some of the steps omitted):

$$ \llbracket \text{env}_F \rrbracket \vdash \langle \text{while} \; (\neg \text{empty} T) \; \text{do} \; \text{reset} \; \{ k := \text{get} T; T := \text{del} T k; \text{invoke} k \}, \emptyset, \sigma[T \mapsto \{([e], [R \{\text{skip}; [S]\}], \rho; \Pi^\dagger)]\}] \rangle $$

$$ \rightarrow \langle \text{reset} \{ k := \text{get} T; T := \text{del} T k; \text{invoke} k \}; \text{Sched}, \emptyset, \sigma[T \mapsto \{([e], [R \{\text{skip}; [S]\}], \rho; \Pi^\dagger)]\}] \rangle $$

$$ \rightarrow \langle \mathbb{R} \{ k := \text{get} T; T := \text{del} T k; \text{invoke} k \}; \text{Sched}, \emptyset^\dagger, \sigma[T \mapsto \{([e], [\text{skip}; \mathbb{R} \{\llbracket S \rrbracket], \rho; \Pi^\dagger])\}] \rangle $$

$$ \rightarrow^* \langle \mathbb{R} \{ \text{invoke} k \}; \text{Sched}, [k \mapsto [\mathbb{R} \{ \text{skip}; [S] \}], \rho; \Pi^\dagger]^\dagger \mid \sigma[T \mapsto \emptyset] \rangle $$

$$ \rightarrow \langle \mathbb{R} \{ \mathbb{R} \{ \text{skip}; [S] \}; \text{return} \}; \text{Sched}, \rho; \Pi^\dagger; \emptyset^\dagger, \sigma[T \mapsto \emptyset] \rangle $$

$$ \rightarrow \langle \mathbb{R} \{ \llbracket S \rrbracket \}; \text{return} \}; \text{Sched}, \rho; \Pi^\dagger; \emptyset^\dagger, \sigma[T \mapsto \emptyset] \rangle $$

# 6 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.

*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.
References

1. Adya, A., Howell, J., Theimer, M., Bolosky, W.J., Douceur, J.R.: Cooperative task management without manual stack management. In: ATEC '02: Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference. pp. 289–302. USENIX (2002)

2. Agha, G.: Actors: a model of concurrent computation in distributed systems. MIT Press (1986)

3. de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: ESOP'07 Proceedings of the 16th European conference on Programming. LNCS, vol. 4421, pp. 316–330. Springer (2007)

4. Caromel, D., Henrio, L., Serpette, B.P.: Asynchronous and deterministic objects. ACM SIGPLAN Notices - POPL'04 39(1), 123–134 (2004)

5. Danvy, O., Filinski, A.: Abstracting control. In: LFP '90: Proceedings of the 1990 ACM conference on LISP and functional programming. pp. 151–160. ACM (1990)

6. Haynes, C.T., Friedman, D.P., Wand, M.: Continuations and coroutines. In: LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional programming. pp. 293–298. ACM (1984)

7. Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: FMCO'10 Proceedings of the 9th international conference on Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 142–164. Springer (2012)

8. Johnsen, E.B., Owe, O., Yu, I.C.: Creol: A type-safe object-oriented model for distributed concurrent systems. Theoretical Computer Science 365(1-2), 23–66 (2006)

9. Karmani, R.K., Shali, A., Agha, G.: Actor frameworks for the JVM platform: a comparative analysis. In: PPPJ '09: Proceedings of the 7th International Conference on Principles and Practice of Programming in Java. pp. 11–20. ACM (2009)

10. Schäfer, J., Poetzsch-Heffter, A.: JCoBox: generalizing active objects to concurrent components. In: ECOOP'10: Proceedings of the 24th European conference on Object-oriented programming. LNCS, vol. 6183, pp. 275–299. Springer (2010)

11. Srinivasan, S., Mycroft, A.: Kilim: Isolation-typed actors for Java. In: ECOOP '08: Proceedings of the 22nd European conference on Object-Oriented Programming. LNCS, vol. 5142, pp. 104–128. Springer (2008)

12. Wand, M.: Continuation-based multiprocessing. In: LFP '80: Proceedings of the 1980 ACM conference on LISP and functional programming. pp. 19–28. ACM (1980)