# Procedural Choreographic Programming

Luís Cruz-Filipe, Fabrizio Montesi

► To cite this version:

Luís Cruz-Filipe, Fabrizio Montesi. Procedural Choreographic Programming. 37th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2017, Neuchâtel, Switzerland. pp.92-107, 10.1007/978-3-319-60225-7_7. hal-01658417

HAL Id: hal-01658417

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

Submitted on 7 Dec 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
Procedural Choreographic Programming

Luís Cruz-Filipe and Fabrizio Montesi

University of Southern Denmark {lcf, fmontesi}@imada.sdu.dk

**Abstract.** Choreographic Programming is an emerging paradigm for correct-by-construction concurrent programming. However, its applicability is limited by the current lack of support for reusable procedures. We propose Procedural Choreographies (PC), a choreographic language model with full procedural abstraction. PC includes unbounded process creation and name mobility, yielding a powerful framework for writing correct concurrent algorithms that can be compiled into a process calculus. This increased expressivity requires a typing discipline to ensure that processes are properly connected when enacting procedures.

# 1 Introduction

Choreographic Programming [20] is a paradigm for programming concurrent software that is deadlock-free by construction, by using an “Alice and Bob” notation to syntactically prevent mismatched I/O communications in programs (called choreographies) and using an EndPoint Projection to synthesise correct process implementations [2,4,24]. Choreographies are found in standards [1,26], languages [6,14,23,25], and specification models [2,4,17]. They are widely used as a design tool in communication-based software [1,23,25,26], since they describe interactions unambiguously and thus help ensure correctness [19].

Driven by these benefits, research on applicability of choreographic programming has recently gained in breadth, ranging from service programming [2,4] to runtime adaptation [11]. We focus on another important aspect: modular programming. Writing procedures that can be arbitrarily instantiated and composed into larger programs is still unsupported. The absence of full procedural abstraction disallows the creation of libraries that can be reused as “black boxes”.

*Example 1.* We discuss a parallel version of merge sort, written as a choreography. Although this is a toy example, it cannot be written in any previous model for choreographic programming. We present more realistic and involved examples in the remainder. We make the standard assumption that we have concurrent processes with local storage and computational capabilities. In this example, each process stores a list and can use the following local functions: `split1` and `split2`, respectively returning the first or the second half of a list; `is_small`, which tests if a list has at most one element; and `merge`, which combines two sorted lists into one. The following (choreographic) procedure, `MS`, implements merge sort on the list stored at its parameter process $p$.<fnref n="1" />

<footnote n="1">¹ In this work, we use a monospaced font for readability of our concrete examples, and other fonts for distinguishing syntactic categories in our formal arguments as usual.</footnote>
MS(p) = if p.is_small then 0
else p start q1,q2; p.split1 -> q1; p.split2 -> q2;
MS<q1>; MS<q2>; q1.* -> p; q2.* -> p.merge

Procedure MS starts by checking whether the list at process p is small, in which case it does not need to be sorted (0 denotes termination); otherwise, p starts two other processes q1 and q2 (p start q1,q2), to which it respectively sends the first and the second half of the list (p.split1 -> q1 and p.split2 -> q2). The procedure is recursively reapplied to q1 and q2, which independently (concurrently) proceed to ordering their respective sub-lists. When this is done, MS stores the first ordered half from q1 to p (q1.* -> p, where * retrieves the data stored in q1) and merges it with the ordered sub-list from q2 (q2.* -> p.merge).

Procedure MS in Example 1 cannot be written in current choreography models, because it uses two unsupported features: *general recursion*, allowing procedure calls to be followed by arbitrary code; and *parametric procedures*, which can be reused with different processes (as in `MS<q1>` and `MS<q2>`).

We present Procedural Choreographies (PC), a model for choreographic programming that captures these features (§ 2). PC has a simple syntax, but its semantics is expressive enough to infer safe out-of-order executions of choreographic procedures – for example, in `MS<q1>`; `MS<q2>`, the two calls can be run in parallel because they involve separate processes and are thus non-interfering.

We also illustrate the expressivity of PC with a more involved parallel downloader, showing how our semantics infers parallel executions in a complex scenario of concurrent data streams. This example makes use of additional features: mobility of process names (networks with connections that evolve at runtime) and propagation of choices among processes.

The interplay between name mobility and procedure composition requires careful handling, because of potential dangling process references. We prevent such errors using a decidable typing discipline (§ 3) that supports type inference.

PC includes an EndPoint Projection (EPP) that synthesises correct concurrent implementations in terms of a process calculus (§ 4). This process calculus is an abstraction of systems where processes refer to one another's locations or identifiers (e.g., MPI [22] or the Internet Protocol).

Full definitions, proofs, and further extensions are given in [9]. Additional examples can be found in [8] (which is based on a pre-print of this article).

## 2 Procedural Choreographies (PC)

*Syntax.* The syntax of PC is displayed in Figure 1. A procedural choreography is a pair ⟨$\mathcal{D}$, $C$⟩, where $C$ is a choreography and $\mathcal{D}$ is a set of procedure definitions. Process names ($p, q, r, ...$), identify processes that execute concurrently. Each process is equipped with a memory cell that stores a single value of a fixed type. Specifically, we consider a fixed set $\mathcal{T}$ of datatypes (numbers, lists, etc.); each process $p$ stores only values of type $T_p \in \mathcal{T}$. Statements in a choreography can either be communication actions ($\eta$) or compound instructions ($I$), both of which
$$
\begin{align*}
C ::= & \eta; C \mid I; C \mid \mathbf{0} & \eta ::= \mathbf{p.e} \rightarrow \mathbf{q.f} \mid \mathbf{p} \rightarrow \mathbf{q}[l] \mid \mathbf{p.start} \mathbf{q}^T \mid \mathbf{p} : \mathbf{q} \leftarrow \mathbf{r} \\
\mathcal{D} ::= & X(\tilde{\mathbf{q}}^T) = C, \mathcal{D} \mid \emptyset & I ::= \mathbf{if} \ \mathbf{p.e} \ \mathbf{then} \ C_1 \ \mathbf{else} \ C_2 \ | X(\tilde{\mathbf{p}}) \mid \mathbf{0}
\end{align*}
$$

<caption>Fig. 1. Procedural Choreographies, Syntax.</caption>

can have continuations. Term **0** is the terminated choreography, which we often omit in examples. We call all terms but **0**; *C program terms*, or simply programs, since these form the syntax intended for developers to use for writing programs. Term **0**; *C* is necessary only for the technical definition of the semantics, to capture termination of procedure calls with continuations, and can appear only at runtime. It is thus called a *runtime term*.

Processes communicate through direct references (names) to each other.<fnref n="2" />
In a value communication p.e -> q.f, process p sends the result of evaluating expression e (replacing the placeholder * at runtime with the data in its memory) to q. When q receives the value from p, it applies to it the (total) function f and stores the result. The definition of f may also access the contents of q's memory.

In a selection term p -> q[l], p communicates to q its choice of label l, which is a constant. This term is intended to propagate information on which internal choice has been made by a process to another (see Remark 2 below).

In term p start q^T, process p spawns the new process q, which stores data of type T. Process name q is bound in the continuation C of p start q^T; C.

Process spawning introduces the need for name mobility. In real-world sys-
tems, after execution of p start q<sup>T</sup>, p is the only process that knows q's name. Any
other process wanting to communicate with q must therefore be first informed
of its existence. This is achieved with the introduction term p: q &lt;=&gt; r, read “p
introduces q and r” (with p, q and r distinct). As its double-arrow syntax sug-
gests, this action represents two communications – one where p sends q's name
to r, and another where p sends r's name to q. This is made explicit in § 4.

In a conditional term if p.e then C₁ else C₂, process p evaluates e to choose between the possible continuations C₁ and C₂.

The set $\mathcal{D}$ contains global procedures. Term $X(\tilde{\mathbf{q}}^T) = C_X$ defines a procedure $X$ with body $C_X$, which can be used anywhere in $\langle \mathcal{D}, C \rangle$ – in particular, inside $C_X$. The names $\tilde{\mathbf{q}}$ are bound to $C_X$, and they are exactly the free process names in $C_X$. Each procedure can be defined at most once in $\mathcal{D}$. Term $X(\tilde{\mathbf{p}})$ calls (invokes) procedure $X$ by passing $\tilde{\mathbf{p}}$ as parameters. Procedure calls inside definitions must be guarded, i.e., they can only occur after some other action.

We assume the Barendregt convention and work up to α-equivalence in chore-
ographies, renaming bound variables as needed when expanding procedure calls.

*Example 2.* Recall procedure *MS* from our merge sort example in the Introduction (Example 1). If we annotate the parameter *p* and the started processes *q*₁ and *q*₂ with a type, e.g., **List(T)** for some *T* (the type of lists containing elements

<footnote n="2">² PC thus easily applies to settings based on actors, objects, or ranks (e.g., MPI).</footnote>
of type T), then MS is a valid procedure definition in PC, as long as we allow two straightforward syntactic conventions: (i) p start q^T stands for the sequence p start q_1^T; ... ; p start q_n^T; (ii) a communication of the form p.e -> q stands for p.e -> q.id, where id is the identity function: it sets the content of q to the value received from p. We adopt these conventions also in the remainder.

**Remark 1 (Design choices).** We comment on two of our design choices.

The introduction action (*p*: *q*<->*r*) requires a three-way synchronization, essentially performing two communications. The alternative development of PC with asymmetric introduction (an action *p*: *q*->*r* whereby *p* sends *q*'s name to *r*, but not conversely) would be very similar. Since in our examples we always perform introductions in pairs, the current choice makes the presentation easier.

The restriction that each process stores only one value of a fixed type is, in practice, a minor constraint. As shown in Example 2, types can be tuples or lists, which mimics storing several values. Also, a process can create new processes with different types – so we can encode changing the type of *p* by having *p* create a new process *p'* and then continuing the choreography with *p'* instead of *p*.

**Remark 2 (Label Selection).** We motivate the need for selections (*p* -> *q*[*l*]). Consider the choreography if *p*.coinflip then (*p*.* -> *r*) else (*r*.* -> *p*). Here, *p* flips a coin to decide whether to send a value to *r* or to receive a value from *r*. Since processes run independently and share no data, only *p* knows which branch of the conditional will be executed; but this information is essential for *r* to decide on its behaviour. To propagate *p*'s decision to *r*, we use selections:

$$ \text{if } p.\text{coinflip then } (p \to r[L]; p.* \to r) \text{ else } (p \to r[R]; r.* \to p) $$

Now *r* receives a label reflecting *p*'s choice, and can use it to decide what to do.

Selections are needed only for compilation (see § 4): the first choreography above is not projectable, whereas the second one is. They can be inferred, and thus could be removed from the user syntax, but it is useful to be able to specify them manually (see Remark 4). See also Example 5 at the end of this section.

*Semantics.* We define a reduction semantics $\to_{\mathcal{D}}$ for PC, parameterised over $\mathcal{D}$ (Figure 2, top). Given a choreography $C$, we model the state of its processes with a state function $\sigma$, with domain $pn(C)$, where $\sigma(p)$ denotes the value stored in $p$. We assume that each type $T \in \mathbb{T}$ has a special value $\perp_T$, representing an uninitialised process state. We also use a connection graph $G$, keeping track of which processes know each other. In the rules, $p \leftarrow_G q$ denotes that $G$ contains an edge between $p$ and $q$, and $G \cup \{p \leftrightarrow q\}$ denotes the graph obtained from $G$ by adding an edge between $p$ and $q$ (if missing).

Executing a communication action *p*.e -> *q*.f in rule $\lfloor C|Com \rfloor$ requires that: *p* and *q* are connected in *G*; *e* is well typed; and the type of *e* matches that expected by the function *f* at the receiver. The last two conditions are encapsulated in the notation *e* $\downarrow$ *v*, read “*e* evaluates to *v*”. Choreographies can thus deadlock (be unable to reduce) because of errors in the programming of communications; this issue is addressed by our typing discipline in § 3.
<figure><img src="image_2.png" /><figcaption>**Fig. 2.** Procedural Choreographies, Semantics and Structural Precongruence (selected rules).</figcaption></figure>

Rule $[C|Sel]$ defines selection as a no-op for choreographies (see Remark 2).

Rule $[C|Start]$ models the creation of a process. In the reductum, the starter and started processes are connected and can thus communicate with each other. This rule also extends the domain of the state function $\sigma$ accordingly. Rule $[C|Tell]$ captures name mobility, creating a connection between two processes $q$ and $r$ when they are introduced by a process $p$ connected to both.

Rule $[C|Cond]$ uses the auxiliary operator $\ $$ to obtain a reductum in the syntax of PC regardless of the forms of the branches $C_1$ and $C_2$ and the continuation $C$. The operator $\ $$ is defined by $\eta \ $$ C = \eta; C$, $I \ $$ C = I; C$ and $(C_1; C_2) \ $$ C = C_1; (C_2 \ $$ C)$. It extends the scope of bound names: any name $p$ bound in $C$ has its scope extended also to $C'$. This scope extension is capture-avoiding, as the Barendregt convention guarantees that $p$ is not used in $C'$.

Rule $[C|Struct]$ uses structural precongruence $\leq_{\mathcal{D}}$. The main rules defining $\leq_{\mathcal{D}}$ are given in Figure 2 (bottom). We write $C \equiv_{\mathcal{D}} C'$ when $C \leq_{\mathcal{D}} C'$ and $C' \leq_{\mathcal{D}} C$, $pn(C)$ for the set of process names (free or bound) in a choreography $C$, and $A\#B$ when two sets $A$ and $B$ are disjoint. These rules formalise the notion of parallelism in PC, recalling out-of-order execution. Rule $[C|Eta-Eta]$ permutes two communications performed by processes that are all distinct, modelling that
processes run independently of one another. For example, `p.* -> q`; `r.* -> s` $\equiv_{\mathcal{D}}$
`r.* -> s`; `p.* -> q` because these two communications are non-interfering, but
`p.* -> q`; `q.* -> s` $\not\equiv_{\mathcal{D}}$ `q.* -> s`; `p.* -> q`: since the second communication
causally depends on the first (both involve `q`).

This reasoning is extended to instructions in rule $[C|I-I]$; in particular, procedure calls that share no arguments can be swapped. This is sound, as a procedure can only refer to processes that are either passed as arguments or started inside its body, and the latter cannot be leaked to the original call site. Thus, any actions obtained by unfolding the first procedure call involve different processes than those obtained by unfolding the second one. As the example below shows, calls to the same procedure can be exchanged, since X and Y need not be distinct. Omitted rules include moving actions inside or outside both branches of a conditional, or switching independent nested conditionals. Rule $[C|Unfold]$ unfolds a procedure call, again using the $\%$ operator defined above.

**Example 3.** In our merge sort example, structural precongruence $\leq_{\mathcal{D}}$ allows the recursive calls `MS<q₁>` and `MS<q₂>` to be exchanged. Furthermore, after the calls are unfolded, their code can be interleaved in any way.

This example exhibits map-reduce behaviour: each new process receives its input, runs independently from all others, and then sends its result to its creator.

**Example 4.** In a more refined example of implicit parallelism, we swap communications from procedure calls that share process names. Consider the procedure

```c
auth(c,a,r,1) = c.creds -> a.rCreds;
               a chk -> r.res; a.log -> l.app
```

Client `c` sends its credentials to an authentication server `a`, which stores the result of authentication in `r` and appends a log of this operation at process `l`. In the choreography `auth<c,a1,r1,1>`; `auth<c,a2,r2,1>`, a client `c` authenticates at two different authentication servers `a1` and `a2`. After unfolding the two calls, rule $[C|Eta-Eta]$ yields the following interleaving:

```c
c.creds -> a1.rCreds; c.creds -> a2.rCreds;
a2 chk -> r2.res; a1 chk -> r1.res;
a1.log -> l.app; a2.log -> l.app
```

Thus, the two authentications proceed in parallel. Observe that the logging operations cannot be swapped, since they use the same logging process `l`.

**Example 5.** A more sophisticated example involves modularly composing different procedures that take multiple parameters. Here, we write a choreography where a client `c` downloads a collection of files from a server `s`. Files are downloaded in parallel via streaming, by having the client and the server each create subprocesses to handle the transfer of each file. Thus, the client can request and start downloading each file without waiting for previous downloads to finish.

```python
par_download(c,s) = if c.more
    then c -> s [more]; c start c'; s start s';
    s: c <-> s'; c.top -> s'; pop<c>;
```
```
c: c' <-> s'; download<c',s'>;
    par_download<c,s>; c'.file -> c.store
else c -> s [end]
```

At the start of `par_download`, the client `c` checks whether it wants to download more files and informs the server `s` of the result via a label selection. In the affirmative case, the client and the server start two subprocesses, `c'` and `s'` respectively, and the server introduces `c` to `s'` (`s`: `c` <-> `s'`). The client `c` sends to `s'` the name of the file to download (`c.top -> s'`) and removes it from its collection, using procedure `pop` (omitted), afterwards introducing its own subprocess `c'` to `s'`. The file download is handled by `c'` and `s'` (using procedure `download`), while `c` and `s` continue operating (`par_download<c,s>`). Finally, `c'` waits until `c` is ready to store the downloaded file.

Procedure `download` has a similar structure. It implements a stream where a file is sequentially transferred in chunks from a process `s` to another process `c`.

```python
download(c,s) = if s.more
    then s -> c [more]; s.next -> c.app; pop
; download<c,s>
else s -> c [end]
```

The implementation of `par_download` exploits implicit parallelism considerably. All calls to `download` are made with disjoint sets of parameters (processes), and can thus be fully parallelised: many instances of `download` run at the same time, each one implementing a (sequential) stream. Due to our semantics, we effectively end up executing many streaming behaviours in parallel.

We can even compose `par_download` with `auth`, such that we execute the parallel download only if the client can successfully authenticate with an authentication server `a`. Below, we use the shortcut $p \rightarrow \tilde{q}[l]$ for $p \rightarrow q_1[l]; \dots; p \rightarrow q_n[l]$.

```python
auth<c,a,r,l>; if r.ok then r -> c,s[ok]; par_download<c,s>
else r -> c,s[ko]
```

## 3 Typability and Deadlock-Freedom

We give a typing discipline for PC, to check that (a) the types of functions and processes are respected by communications and (b) processes that need to communicate are first properly introduced (or connected). Regarding (b), two processes created independently can communicate only after they receive the names of each other. For instance, in Example 5, the execution of `download<c',s'>` would get stuck if `c'` and `s'` were not properly introduced in `par_download`, since our semantics requires them to be connected.

Typing judgements have the form $\Gamma; G \vdash C \triangleright G'$, read "C is well-typed according to $\Gamma$, and running C with a connection graph that contains G yields a connection graph that includes G'". Typing environments $\Gamma$ are used to track the types of processes and procedures; they are defined as: $\Gamma ::= \emptyset | \Gamma, p : T | \Gamma, X : G \triangleright G'$. A typing $p : T$ states that process `p` stores values of type `T`, and a typing $X : G \triangleright G'$ records the effect of the body of `X` on graph `G`.
<figure><img src="image_3.png" /><figcaption>Fig. 3. Procedural Choreographies, Typing Rules.</figcaption></figure>

The rules for deriving typing judgements are given in Figure 3. We assume standard typing judgements for functions and expressions, and write * : T ⊢<T e : T and * : T₁ ⊢<T f : T₂ → T₃ meaning, respectively “e has type T assuming that * has type T” and “f has type T₂ → T₃ assuming that * has type T₁”. Verifying that communications respect the expected types is straightforward, using the connection graph G to track which processes have been introduced to each other. In rule [T|Start], we implicitly use the fact that q does not occur in G (again using the Barendregt convention). The final graph G' is only used in procedure calls (rule [T|Call]). Other rules leave it unchanged.

To type a procedural choreography, we need to type its set of procedure definitions $\mathcal{D}$. We write $\Gamma \vdash \mathcal{D}$ if: for each $X(\tilde{q}^T) = C_X \in \mathcal{D}$, there is exactly one typing $X(\tilde{q}^T) : G_X \vdash G'_X \in \Gamma$, and this typing is such that $\Gamma, \tilde{q} : T, G_X \vdash C_X \vdash G'_X$. We say that $\Gamma \vdash (\tilde{\mathcal{D}}, C)$ if $\Gamma, \tilde{\mathcal{D}}; G_C \vdash C, G'$ for some $\tilde{\mathcal{D}}$ such that $\Gamma_{\tilde{\mathcal{D}}} \vdash \mathcal{D}$ and some $G'$, where $G_C$ is the full graph whose nodes are the free process names in $C$. The choice of $G_C$ is motivated by observing that (i) all top-level processes should know each other and (ii) eventual connections between processes not occuring in $C$ do not affect its typability.

Well-typed choreographies either terminate or diverge.<fnref n="3" />

<footnote n="3">³ Since we are interested in communications, we assume evaluation of functions and expressions to terminate on values with the right types (see § 5, Faults).</footnote>
**Theorem 1 (Deadlock freedom/Subject reduction).** Let $\langle \mathcal{D}, C \rangle$ be a procedural choreography. If $\Gamma \vdash \mathcal{D}$ and $\Gamma'; G_1 \vdash C \triangleright G'_1$ for some $\Gamma$, $G_1$ and $G'_1$, then either: (i) $C \preceq_{\mathcal{D}} 0$; or, (ii) for every $\sigma$, there exist $G_2, C'$ and $\sigma'$ such that $G_1, C, \sigma \to_{\mathcal{D}} G_2, C', \sigma'$ and $\Gamma'$; $G_2 \vdash C' \triangleright G'_2$ for some $\Gamma' \supseteq \Gamma$ and $G'_2$.

Checking that $\Gamma \vdash \langle \mathcal{D}, C \rangle$ is not trivial, as it requires "guessing" $\Gamma_{\mathcal{D}}$. However, this set can be computed from $\langle \mathcal{D}, C \rangle$.

**Theorem 2.** Given $\Gamma$, $\mathcal{D}$ and $C$, $\Gamma \vdash \langle \mathcal{D}, C \rangle$ is decidable.

The key idea behind the proof of Theorem 2 is that type-checking may require expanding recursive definitions, but their parameters only need to be instantiated with process names from a finite set. A similar idea yields type inference for PC.

**Theorem 3.** There is an algorithm that, given any $\langle \mathcal{D}, C \rangle$, outputs: (i) a set $\Gamma$ such that $\Gamma \vdash \langle \mathcal{D}, C \rangle$, if such a $\Gamma$ exists; or (ii) NO, if no such $\Gamma$ exists.

**Theorem 4.** The types of arguments in procedure definitions and the types of freshly created processes can be inferred automatically.

*Remark 3 (Inferring introductions).* These results allow us to omit type annotations in choreographies, if the types of functions and expressions at processes are given (in $\vdash_{\mathbb{T}}$). Thus, programmers can write choreographies as in our examples.

The same reasoning can be used to infer missing introductions ($p: q \leftrightarrow r$) in a choreography automatically, thus lifting the programmer also from having to think about connections. However, while the types inferred for a choreography do not affect its behaviour, the placement of introductions does. In particular, when invoking procedures one is faced with the choice of adding the necessary introductions inside the procedure definition (weakening the conditions for its invocation) or in the code calling it (making the procedure body more efficient).

*Example 6.* Consider a procedure $X(p, q, r) = p.* \to q; p: q \leftrightarrow r; q.* \to r$, whose invocation requires only that $p$ is connected to $q$ and $r$. If we invoke $X$ twice with the same parameters, as in $X\langle p, q, r \rangle; X\langle p, q, r \rangle$, we end up performing the same introduction $p: q \leftrightarrow r$ twice. We could avoid this duplication by rewriting $X$ as $X(p, q, r) = p.* \to q; q.* \to r$ and then performing the introduction only once before invoking the procedure $- p: q \leftrightarrow r; X\langle p, q, r \rangle; X\langle p, q, r \rangle$. However, this makes invoking $X$ more complicated, and deciding which variant is best depends heavily on the context.

# 4 Synthesising Process Implementations

We now present our EndPoint Projection (EPP), which compiles a choreography to a concurrent implementation represented in terms of a process calculus.

## 4.1 Procedural Processes (PP)

We introduce our target process model, Procedural Processes (PP).
$B ::= q!e; B \mid p?f; B \mid q!!r; B \mid p?r; B \mid q \oplus l; B \mid p\&\{l_i : B_i\}_{i \in I}; B$
$| \mathbf{0} \mid \mathbf{start} \ q^T \triangleright B_2; B_1 \mid \text{if } e \text{ then } B_1 \text{ else } B_2; B \mid X \langle \bar{p} \rangle; B \mid \mathbf{0}; B$
$\mathcal{B} ::= X(\bar{q}) = B, \mathcal{B} \mid \emptyset \quad N, M ::= p \triangleright_v B \mid (N|M) \mid \mathbf{0}$

$$
\frac{u = (f[w/*])(e[v/*])}{p \triangleright_v q!e; B_1 \mid q \triangleright_w p?f; B_2 \rightarrow \mathcal{B} \ p \triangleright_v B_1 \mid q \triangleright_u B_2} [P|\text{Com}]
$$
$$
\frac{j \in I}{p \triangleright_v q \oplus l_j; B \mid q \triangleright_w p \& \{l_i : B_i\}_{i \in I} \rightarrow \mathcal{B} \ p \triangleright_v B \mid q \triangleright_w B_j} [P|\text{Sel}]
$$
$$
\frac{q' \text{ fresh}}{p \triangleright_v (\mathbf{start} \ q^T \triangleright B_2); B_1 \rightarrow \mathcal{B} \ p \triangleright_v B_1[q'/q] \mid q' \triangleright_{\perp T} B_2} [P|\text{Start}]
$$
$$
\frac{p \triangleright_v q!!r; B_1 \mid q \triangleright_w p?r; B_2 \mid r \triangleright_u p?q; B_3 \rightarrow \mathcal{B} \ p \triangleright_v B_1 \mid q \triangleright_w B_2 \mid r \triangleright_u B_3} [P|\text{Tell}]
$$

<caption>**Fig. 4.** Procedural Processes, Syntax and Semantics (selected rules).</caption>

*Syntax.* The syntax of PP is given in Figure 4 (top). A term $p \triangleright_v B$ is a process, where $p$ is its name, $v$ is its value, and $B$ is its behaviour. Networks, ranged over by $N, M$, are parallel compositions of processes, where $\mathbf{0}$ is the inactive network. Finally, $\langle \mathcal{B}, N \rangle$ is a procedural network, where $\mathcal{B}$ defines the procedures that the processes in $N$ may invoke. Values, expressions and functions are as in PC.

A process executing a send term $q!e; B$ sends the evaluation of expression $e$
to $q$, and proceeds as $B$. Term $p?f; B$ is the dual receiving action: the process
executing it receives a value from $p$, combines it with its value as specified by $f$,
and then proceeds as $B$. Term $q!!r$ sends process name $r$ to $q$ and process name $q$
to $r$, making $q$ and $r$ “aware” of each other. The dual action is $p?r$, which receives
a process name from $p$ that replaces the bound variable $r$ in the continuation.
Term $q \oplus l; B$ sends the selection of a label $l$ to process $q$. Selections are received
by the branching term $p\&\{l_i : B_i\}_{i \in I}$, which can receive a selection for any of
the labels $l_i$ and proceed as $B_i$. Branching terms must offer at least one branch.
Term $\mathbf{start} \ q \triangleright B_2; B_1$ starts a new process (with a fresh name) executing $B_2$, and
proceeds in parallel as $B_1$. Conditionals, procedure calls, and termination are
standard. Term $\mathbf{start} \ q \triangleright B_2; B_1$ binds $q$ in $B_1$, and $p?r; B$ binds $r$ in $B$.

*Semantics.* The main rules defining the reduction relation $\rightarrow_{\mathcal{B}}$ for PP are shown in Figure 4 (bottom). As in PC, they are parameterised on the set of behavioural procedures $\mathcal{B}$. Rule $[P|\text{Com}]$ models value communication: a process $p$ executing a send action towards a process $q$ can synchronise with a receive-from-$p$ action at $q$; in the reductum, $f$ is used to update the memory of $q$ by combining its contents with the value sent by $p$. The placeholder $*$ is replaced with the current value of $p$ in $e$ (resp. $q$ in $f$). Rule $[P|\text{Sel}]$ is standard selection [15], where the sender process selects one of the branches offered by the receiver.
Rule [P|Tell] establishes a three-way synchronisation, allowing a process to introduce two others. Since the received names are bound at the receivers, we use α-conversion to make the receivers agree on each other's name, as in session types [15]. (Differently from PC, we do not assume the Barendregt convention here, in line with the tradition of process calculi.) Rule [P|Start] requires the name of the created process to be globally fresh.

All other rules are standard. Relation $\rightarrow_{\mathcal{B}}$ is closed under a structural congruence $\preceq_{\mathcal{B}}$, which supports associativity and commutativity of parallel ($|$), standard garbage collection of 0, and unfolding of procedure calls.

*Example 7.* We show a process implementation of the merge sort choreography in Example 1 from § 1. All processes are annotated with type **List**(T) (omitted); id is the identity function (Example 2).

$$MS_p(p) = \begin{cases} \text{if } is\_small \text{ then } 0 \\ \text{else } \begin{array}{l} \text{start } q_1 \triangleright (p?id; MS_p<q_1>; p!*); \\ \text{start } q_2 \triangleright (p?id; MS_p<q_2>; p!*); \\ q_1!split_1; q_2!split_2; q_1?id; q_2?merge \end{array} \end{cases}$$

In the next section, we show that our EPP generates this process implementation automatically from the choreography in Example 1.

## 4.2 EndPoint Projection (EPP)

We now show how to compile programs in PC to processes in PP.

*Behaviour Projection.* We start by defining how to project the behaviour of a single process p, a partial function denoted $[C]_p$. The rules defining behaviour projection are given in Figure 5. Each choreography term is projected to the local action of the process that we are projecting. For example, a communication term p.e $\rightarrow$ q.f projects a send action for the sender p, a receive action for the receiver q, or skips to the continuation otherwise. The rules for projecting a selection or an introduction (name mobility) are similar.

The rule for projecting a conditional uses the partial merging operator $\sqcup$: $B \sqcup B'$ is isomorphic to B and $B'$ up to branching, where the branches of B or $B'$ with distinct labels are also included. The interesting rule defining merge is:

$$(p\&\{l_i : B_i\}_{i \in I}; B) \sqcup (p\&\{l_j : B'_j\}_{j \in J}; B') = \\ p\&\{(l_k : (B_k \sqcup B'_k))_{k \in I \cap J} \cup \{l_i : B_i\}_{i \in I \setminus J} \cup \{l_j : B'_j\}_{j \in J \setminus I}\}; (B \sqcup B')$$

The idea of merging comes from [2]. Here, we extend it to general recursion, parametric procedures, and process starts. Merging allows the process that decides a conditional to inform other processes of its choice later on, using selections. It is found repeatedly in most choreography models [2,7,17].

Building on behaviour projection, we define how to project the set $\mathcal{D}$ of procedure definitions. We need to consider two main aspects. The first is that, at runtime, the choreography may invoke a procedure X multiple times, but
$$ [[\mathbf{p}.e \to \mathbf{q}.f; C]]_r = \begin{cases} q!e; [C]_r & \text{if } r = \mathbf{p} \\ p?f; [C]_r & \text{if } r = \mathbf{q} \\ [C]_r & \text{o.w.} \end{cases} \quad [[\mathbf{p} \to q[l]; C]]_r = \begin{cases} q \oplus l; [C]_r & \text{if } r = \mathbf{p} \\ p \& \{l : [C]_r\} & \text{if } r = \mathbf{q} \\ [C]_r & \text{o.w.} \end{cases} $$

$$ [[\mathbf{p}: q \leftarrow \to r; C]]_s = \begin{cases} q!!r; [C]_s & \text{if } s = \mathbf{p} \\ p?r; [C]_s & \text{if } s = \mathbf{q} \\ p?q; [C]_s & \text{if } s = \mathbf{r} \\ [C]_s & \text{o.w.} \end{cases} \quad [[X \langle \tilde{p} \rangle; C]]_r = \begin{cases} X_r \langle \tilde{p} \rangle; [C]_r & \text{if } r = \mathbf{p}_i \\ [C]_r & \text{o.w.} \end{cases} \quad [[0]]_r = \mathbf{0} \quad [[0; C]]_r = [C]_r $$

$$ [[\text{if } \mathbf{p}.e \text{ then } C_1 \text{ else } C_2; C]]_r = \begin{cases} \text{if } e \text{ then } [C_1]_r \text{ else } [C_2]_r; [C]_r & \text{if } r = \mathbf{p} \\ ([C_1]_r \sqcup [C_2]_r); [C]_r & \text{o.w.} \end{cases} $$

$$ [[\mathbf{p} \text{ start } q^T; C]]_r = \begin{cases} \text{start } q \triangleright [C]_q; [C]_r & \text{if } r = \mathbf{p} \\ [C]_r & \text{o.w.} \end{cases} $$

<caption>**Fig. 5.** Procedural Choreographies, Behaviour Projection.</caption>

potentially passing a process r at different argument positions each time. This means that r may be called to play different “roles” in the implementation of the procedure. For this reason, we project the behaviour of each possible process parameter p as the local procedure $X_p$. The second aspect is: depending on the role that r is called to play by the choreography, it needs to know the names of the other processes that it is supposed to communicate with in the choreographic procedure. We deal with this by simply passing all arguments (some of which may be unknown to the process invoking the procedure). This is not a problem: for typable choreographies, typing ensures that those parameters are not actually used in the projected procedure (so they act as “dummies”). We do this for clarity, since it yields a simpler formulation of EPP. In practice, we can annotate the EPP by analysing which parameters of each recursive definition are actually used in each of its projections, and instantiating only those.

We thus define $[[\mathcal{D}]] = \bigcup \{ [[X(\tilde{q}^T) = C] | X(\tilde{q}^T) = C \in \mathcal{D}] \text{ where, for } \tilde{q}^T = q_1^{T_1}, \dots, q_n^{T_n}, \text{ we set } [[X(\tilde{q}^T) = C]] = \{ X_{q_1}(\tilde{q}) = [C]_{q_1}, \dots, X_{q_n}(\tilde{q}) = [C]_{q_n} \}.$

**Definition 1 (EPP).** Given a procedural choreography $\langle \mathcal{D}, C \rangle$ and a state $\sigma$, the EPP $[[\mathcal{D}, C, \sigma]]$ is the parallel composition of the processes in C with all definitions from $\mathcal{D}$: $[[\mathcal{D}, C, \sigma]] = \langle [[\mathcal{D}]], [[C, \sigma]] \rangle = \langle [[\mathcal{D}]], \prod_{p \in \mathbf{pn}(C)} p \triangleright_{\sigma(p)} [C]_p \rangle$ where $[[C, \sigma]]$, the EPP of C wrt state $\sigma$, is independent of $\mathcal{D}$.

Since the $\sigma$s are total, if $[[C, \sigma]]$ is defined for some $\sigma$, then $[[C, \sigma')]$ is defined also for all other $\sigma'$. When $[[C, \sigma]] = N$ is defined for any $\sigma$, we say that C is projectable and that N is the projection of C, $\sigma$. The same holds for $[[\mathcal{D}, C, \sigma]]$.

**Example 8.** The EPP of the choreography in Example 1 is given in Example 7.
*Example 9.* For an example involving merging and introductions, we project the procedure `par_download` (Example 5) for process s, omitting type annotations.

```hml
par_download_s(c,s) = c&{
  more: start s'▷(s?c; c?id; c?c'; download_s<c',s'>);
  c!!s'; par_download_s<c,s>
end: 0
}
```

Observe that we invoke procedure `download_s`, since `s'` occurs in the position of `download`'s formal argument `s`.

*Properties.* EPP guarantees correctness by construction: the code synthesised from a choreography follows it precisely.

**Theorem 5 (EPP Theorem).** If $\langle \mathcal{D}, C \rangle$ is projectable, $\Gamma \vdash \mathcal{D}$, and $\Gamma; G \vdash C \triangleright G^*$, then, for all $\sigma$: if $G, C, \sigma \to_{\mathcal{D}} G', C', \sigma'$, then $[[C, \sigma]] \to_{[\mathcal{D}]} [[C', \sigma']]$ (completeness); and if $[[C, \sigma]] \to_{[\mathcal{D}]} N$, then $G, C, \sigma \to_{\mathcal{D}} G', C', \sigma'$ for some $G'$, $C'$ and $\sigma'$ such that $[[C', \sigma']] \prec N$ (soundness).

Above, the *pruning relation* $\prec$ from [2] eliminates branches introduced by the merging operator $\sqcup$ when they are not needed anymore to follow the originating choreography ($N \succ N'$ stands for $N' \prec N$). Pruning does not alter reductions, since the eliminated branches are never selected [2]. Combining Theorem 5 with Theorem 1 we get that the projections of typable PC terms never deadlock.

**Corollary 1 (Deadlock-freedom by construction).** Let $N = [[C, \sigma]]$ for some $C$ and $\sigma$, and assume that $\Gamma; G \vdash C \triangleright G'$ for some $\Gamma$ such that $\Gamma \vdash \mathcal{D}$ and some $G$ and $G'$. Then, either: (i) $N \preceq_{[\mathcal{D}]} \mathbf{0}$ ($N$ has terminated); or (ii) there exists $N'$ such that $N \to_{[\mathcal{D}]} N'$ ($N$ can reduce).

*Remark 4 (Amendment).* A choreography can only be unprojectable because of unmergeable subterms, and thus can be made projectable by adding label selections. This can be formalised in an amendment algorithm, similar to [10,18]. For example, the first (unprojectable) choreography in Remark 2 can be amended to the projectable choreography presented at the end of the same remark.

The same argument as in Remark 3 applies: amendment allows us to disregard label selections, but placing them manually can be useful. For example, suppose $p$ makes a choice that affects $q$ and $r$. If $q$ has to perform a slower computation as a result, then it makes sense for $p$ to notify $q$ first.

# 5 Related Work and Discussion

*Choreographic Programming.* Our examples cannot be written in previous models for choreographic programming, which lack full procedural abstraction. In state-of-the-art models [2,4], procedures cannot have continuations, there can only be a limited number of protocols running at any time (modulo dangling asynchronous actions), and the process names used in a procedure are statically determined. In PC, all these limitations are lifted.
Differently from PC, name mobility in choreographies is typically done using channel delegation [4], which is less powerful: a process that introduces two other processes requires a new channel to communicate with them thenceforth.

Some choreography models include explicit parallel composition, $C | C'$ Most behaviours of $C | C'$ are already captured in PC, for example $X\langle p, q \rangle | Y\langle r, s \rangle$ is equivalent to $X\langle p, q \rangle; Y\langle r, s \rangle$ in PC (cf. Example 3) – see [4] for a deeper discussion. If a parallel operator is desired, PC can be easily extended (cf. [2]).

In [21], choreographies can be integrated with existing process code by means of a type system, which we could easily integrate in PC.

***Asynchrony.*** Asynchronous communication in choreographic programming was addressed in [4] using an ad-hoc transition rule. Adding asynchrony to PC is straightforward (see the technical report [9]).

***Multiparty Session Types (MPST).*** In MPST [16], global types are choreographic specifications of single protocols, used for verifying the code of manually-written implementations in process models. Global types are similar to a simplified fragment of PC, obtained (among others) by replacing expressions and functions with constants (representing types), removing process creation (the processes are fixed), and restricting recursion to parameterless tail recursion.

MPST leaves protocol composition to the implementors of processes, which can result in deadlocks, unlike in PC. We illustrate this key difference using our syntax; we view a protocol in MPST as a (simplification of a) procedure in PC. Consider the protocols $X(r,s) = r.e \rightarrow s.f$ and $Y(r',s') = r'.e' \rightarrow s'.f'$, and their instantiations $X\langle p, q \rangle$ and $Y\langle q, p \rangle$. In MPST, a valid composition (in PP) is $p \succ_v q?f'; q!e | q \succ_v p?f; p!e'$. This network is obviously deadlocked, but MPST does not detect it because the interleaving of the two protocols is not checked. In PC, we can only obtain correct implementations, because compositions are defined at the level of choreographies, e.g., $X\langle p, q \rangle; Y\langle q, p \rangle$ or $Y\langle q, p \rangle; X\langle p, q \rangle$.

Deadlock-freedom for compositions in MPST can be obtained by restricting connections among processes participating in different protocols to form a tree [3,5]. In PC, connections can form an arbitrary graph. Another technique for MPST is to use pre-orders [7], but this is also not as expressive as PC (see [9]).

MPST can be extended to protocols where the number of participants is fixed only at runtime [27], or can grow during execution [13]. These results use ad-hoc primitives and “middleware” terms in the process model, e.g., for tracking the number of participants in a session [13], which are not needed in PC. MPST can be nested [12], partially recalling our parametric procedures. Differently from PC, nested procedures in MPST are invoked by a coordinator (requiring extra communications), and compositions of such nested types can deadlock.

***Sessions and Mobility.*** Recent theories based on session types [2,4,5,7,16] assume that all pairs of processes in a session have a private full-duplex channel to communicate. Thus, processes in a protocol must have a complete connection graph. PC can be used to reason about different kinds of network topologies.
Another important aspect of sessions is that each new protocol execution requires the creation of a new session, whereas procedure calls in PC reuse available connections – allowing for more efficient implementations. Our parallel下载器 example uses this feature (Example 5).

The standard results of communication safety found in session-typed calculi can be derived from our EPP Theorem (Theorem 5), as discussed in [4].

*Faults*. We have abstracted from faults and divergence of internal computations: in PC, we assume that all internal computations terminate successfully. If we relax these conditions, deadlock-freedom can still be achieved simply by using timeouts and propagating faults through communications.

*Acknowledgements*. We thank the anonymous reviewers for their useful comments. This work was supported by the CRC project, grant no. DFF-4005-00304 from the Danish Council for Independent Research, and by the Open Data Framework project at the University of Southern Denmark.

## References

1. Business Process Model and Notation. http://www.omg.org/spec/BPMN/2.0/.

2. M. Carbone, K. Honda, and N. Yoshida. Structured communication-centered programming for web services. *ACM Trans. Program. Lang. Syst.*, 34(2):8, 2012.

3. M. Carbone, S. Lindley, F. Montesi, C. Schürmann, and P. Wadler. Coherence generalises duality: A logical explanation of multiparty session types. In *CONCUR*, volume 59 of *LIPIcs*, pages 33:1–33:15. Schloss Dagstuhl, 2016.

4. M. Carbone and F. Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In *POPL*, pages 263–274. ACM, 2013.

5. M. Carbone, F. Montesi, C. Schürmann, and N. Yoshida. Multiparty session types as coherence proofs. *Acta Informatica*, 2017.

6. Chor. Programming Language. http://www.chor-lang.org/.

7. M. Coppo, M. Dezani-Ciancaglini, N. Yoshida, and L. Padovani. Global progress for dynamically interleaved multiparty sessions. *Mathematical Structures in Computer Science*, 26(2):238–302, 2016.

8. L. Cruz-Filipe and F. Montesi. Choreographies in practice. In *FORTE*, volume 9688 of LNCS, pages 114–123. Springer, 2016.

9. L. Cruz-Filipe and F. Montesi. A language for the declarative composition of concurrent protocols. CoRR, abs/1602.03729, 2016.

10. L. Cruz-Filipe and F. Montesi. A core model for choreographic programming. In *FACS 2016*, volume 10231 of LNCS. Springer, 2017. Accepted for publication.

11. M. Dalla Preda, M. Gabbrielli, S. Giallorenzo, I. Lanese, and J. Mauro. Dynamic choreographies. In *COORDINATION*, LNCS, pages 67–82. Springer, 2015.

12. R. Demangeon and K. Honda. Nested protocols in session types. In *CONCUR*, pages 272–286, 2012.

13. P.-M. Deniélou and N. Yoshida. Dynamic multirole session types. In *POPL*, pages 435–446. ACM, 2011.

14. K. Honda, A. Mukhamedov, G. Brown, T.-C. Chen, and N. Yoshida. Scribbling interactions with a formal foundation. In *ICDCIT*, pages 55–75. Springer, 2011.
15. K. Honda, V. Vasconcelos, and M. Kubo. Language primitives and type disciplines for structured communication-based programming. In *ESOP*, volume 1381 of LNCS, pages 122–138. Springer, 1998.

16. K. Honda, N. Yoshida, and M. Carbone. Multiparty Asynchronous Session Types. *J. ACM*, 63(1):9, 2016.

17. I. Lanese, C. Guidi, F. Montesi, and G. Zavattaro. Bridging the gap between interaction- and process-oriented choreographies. In *SEFM*, pages 323–332, 2008.

18. I. Lanese, F. Montesi, and G. Zavattaro. Amending choreographies. In *WWV*, pages 34–48, 2013.

19. S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. *ACM SIGARCH Computer Architecture News*, 36(1):329–339, 2008.

20. F. Montesi. *Choreographic Programming*. Ph.D. Thesis, IT University of Copenhagen, 2013. http://fabriziomontesi.com/files/choreographic_programming.pdf.

21. F. Montesi and N. Yoshida. Compositional choreographies. In *CONCUR*, volume 8052 of LNCS, pages 425–439. Springer, 2013.

22. MPI Forum. *MPI: A Message-Passing Interface Standard*. High-Performance Computing Center Stuttgart, 2015. Version 3.1.

23. PI4SOA. http://www pi4soa org, 2008.

24. Z. Qiu, X. Zhao, C. Cai, and H. Yang. Towards the theoretical foundation of choreography. In *WWW*, pages 973–982. ACM, 2007.

25. Savara. JBoss Community. http://www jboss org/savara/.

26. W3C WS-CDL Working Group. Web services choreography description language version 1.0. http://www.w3.org/TR/2004/WD-ws-cdl-10-20040427/, 2004.

27. N. Yoshida, P.-M. Deniélou, A. Bejleri, and R. Hu. Parameterised multiparty session types. In *FOSSACS*, volume 6014 of LNCS, pages 128–145. Springer, 2010.