The Paths to Choreography Extraction

Abstract

Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their application. To attack this problem, previous work investigated choreography extraction, which automatically constructs a choreography that describes the behavior of a given set of programs or protocol specifications.

We propose a new extraction methodology that improves on the state of the art: we can deal with programs that are equipped with state and internal computation; time complexity is dramatically better; and we capture programs that work by exploiting asynchronous communication.

Montesi was supported by CRC (Choreographies for Reliable and efficient Communication software), grant DFF–4005-00304 from the Danish Council for Independent Research. Cruz-Filipe and Larsen were supported in part by the Danish Council for Independent Research, Natural Sciences, grant DFF-1323-00247.

1 Introduction

Choreographies are global descriptions of interactions among components. They have been used as a basis for different models and tools that aim at tackling the complexity of modern software, where separate units – such as processes, objects, and threads – interact to reach a common goal [3, 25].

Two lines of research are of particular interest. In choreography specifications, choreographies specify interaction protocols, e.g., multiparty session types [17]. In choreographic programming [20], choreographies are programs that define the behavior of concurrent algorithms [13] and/or distributed systems [5, 6, 14]. The key feature of these works is EndPoint Projection (EPP), a procedure that translates choreographies to correct endpoint behaviors in lower-level models. For choreography specifications, EPP generates the local specifications of each participant; these specifications can then be used for verification, to check whether some programs implement their role in the protocol correctly and will thus interact without problems at runtime [17]. In choreographic programming, instead, EPP generates correct-by-construction implementations in a model of executable code (program synthesis), typically given in terms of a process calculus [6].

EPP implements a top-down development methodology: developers first write choreographies and then use the output mechanically generated by EPP. However, there are scenarios where this methodology is not applicable; for example:

• Analysis or integration of legacy software: either code developed previously, or new code written in a technology without support for choreographies.

• Updates: endpoint programs generated by EPP can later be updated locally (e.g., for configuration or optimizations). Since the original choreography is not automatically updated, rerunning EPP loses these changes.

To attack these issues, previous work investigated a procedure to infer choreographies from arbitrary endpoint descriptions. We call this procedure choreography extraction. To the best of our knowledge, the current reference for extracting choreography specifications is [19], where graphical choreographies that represent protocol specifications are extracted from communicating automata [4]. Instead, the state of the art for extraction in choreographic programming is [7], where extraction takes terminating processes typed using a fragment of linear logic as input. We advance both lines of work in several aspects, described below.

1.1 Contributions

Extraction for synchronous systems. We define an extraction procedure that applies directly to both choreography specifications and choreographic programming, by working with representative models. We focus on the more difficult case of choreographic programming, and then show how our approach can be applied to other settings in Sect. 6. First we define an extraction algorithm for processes with synchronous communications (Sect. 4), which showcases the key elements of our construction: building a choreography corresponds to finding paths in a graph that represents the abstract execution of the input processes. Our extraction also helps in debugging: if extraction detects a potential deadlock, we pinpoint it with a special term ($\varvec{1}$). This is the first extraction procedure for choreographic programming that can deal with procedures and infinite behavior [7].

Asynchrony. We extend our development to asynchronous communication (Sect. 5). The key novelty is that we can extract a new class of behaviors where processes progress because of asynchronous communication. The simplest example of this class is a two-way exchange: a network of two processes where each process starts by sending a value to the other, and then consumes the received value. This network is deadlocked under a synchronous semantics, violating the state-of-the-art requirements for extraction [19]. Capturing these behaviors is challenging for two reasons: there is no choreography language capable of representing them; and the extraction algorithms presented so far require the behaviors of processes to be representable also under a synchronous interpretation. We overcome both limitations with a new choreography primitive for multiparty asynchronous exchange and a look-ahead mechanism for asynchronous actions in extraction.

Efficiency. We show that our extraction has exponential worst-case time complexity in both the synchronous and the asynchronous cases (Sects. 4 and 5, respectively), unlike the factorial case of [19], even though we can capture a new class of behaviors. In particular, we need only one phase of exponential complexity, while [19] uses multiple phases applied in sequence. The authors of [19] detail only the complexities of their first two phases: the first has exponential complexity (but in a quantity larger than ours), while the second has factorial complexity in a function exponential in the size of the input. Our better time complexity stems from the design of our process language, which does not allow non-deterministic receives from different channels, and careful algorithm crafting. Despite the restriction, we can still model interesting examples thanks to asynchronous exchange. In Sect. 5, we present a novel formulation of the alternating 2-bit protocol, which is given in [15] and used in [19] as a motivating example. Our formulation is simpler and does not require threads as in [19].

2 Related Work

Choreographic Programming. The state of the art for extraction in choreographic programming is [7], where synchronous processes with finite behavior are typed using the multiplicative-additive fragment of linear logic. Our approach is significantly more expressive, bringing support for recursion and asynchronous communication. Also, the proof theory in [7] requires that there are no cycles in the structure of connections among processes. We do not have this limitation.

Choreography Specifications. To the best of our knowledge, the state of the art for extracting choreography specifications is [19], which captures more behaviors than previous works with similar objectives [18, 22].

Extraction in [19] is more restrictive wrt. to asynchrony, requiring all process traces and choices to be represented in the synchronous transition system of the network. Thus, networks that are safe because of asynchronous communication are not extracted in [19]. Instead, our extraction can deal with programs that use multiparty asynchronous exchange, where multiple processes exchange values by exploiting asynchronous communication. As a consequence, we can extract the alternating 2-bit protocol implemented via asynchronous exchange in Sect. 5, which is deadlocked under a synchronous semantics and thus cannot be extracted in [19]. Our extraction is the first capturing systems that are not correctly approximated by synchronous semantics (cf. [2]). A precise characterization of the class of extractable systems is thus an interesting future direction.

To circumvent the limitation that asynchronous exchange is not supported, choreographies in [19] support local concurrency: processes can have internal threads. This opens up for an alternative formulation of the alternating 2-bit protocol, where the two participants use two threads each. However, these choreographies are harder to read. As an example, compare our choreography for the alternating 2-bit protocol in Sect. 5 to that obtained with the automata in [19] (given in [15], Protocol 7 in Example 2.1). Our formulation is a simple recursive procedure with two exchanges, whereas the control flow in [15] is rather intricate and uses three different operators (fork, join, and merge) at different places to compose two separate loops. In our opinion, our choreographies follow the principles of structured programming to a greater extent, and are simpler; also because coordination happens only through communication.

More interestingly than readability, local concurrency makes the complexity of extraction blow up factorially [19]: process threads are represented using non-determinism between different actions in communicating automata. Determining whether the non-deterministic behavior of these automata is extractable takes (super-)factorial time (factorial time in the size of a graph similar to our AES, cf. Definition 2)! Thus, asynchronous exchange supports a more efficient way of capturing an interesting class of behaviors. Nevertheless, we believe that developing efficient extractions of local concurrency may be useful future work.

3 Core Choreographies and Stateful Processes

We review the languages of Core Choreographies (CC) and Stateful Processes (SP), from [11], which respectively model choreographies and endpoint programs. We introduce labels in the reduction semantics for these calculi to formalize the link between choreographies and their process implementations as a bisimilarity.

Fig. 1.

Core Choreographies, Syntax.

Core Choreographies (CC). The syntax of CC is given in Fig. 1. A choreography C describes the behavior of a set of processes ($\mathsf {p}$, $\mathsf {q}$, ...) running concurrently. Each process has an internal memory cell storing a local value (the value of the process). Term $\varvec{0}$ is the terminated choreography (omitted in examples). Term $\eta ;C$ reads “the system executes $\eta$ and proceeds as C”. An interaction $\eta$ is either: a value communication $\mathsf {p}.e\;\texttt {->}\;\mathsf {q}$, where process $\mathsf {p}$ evaluates e and sends the result to process $\mathsf {q}$, which stores it in its memory cell, replacing its previous value; or a selection $\mathsf {p}\;\texttt {->}\;\mathsf {q} [l]$, where $\mathsf {p}$ selects l among the branches offered by $\mathsf {q}$. We abstract from the concrete language of expressions e, which models internal computation and is orthogonal to our development, assuming only that: expressions can contain values v and the placeholder $\mathtt {*}$, which refers to the value of the process evaluating them; and evaluating expressions always terminates and returns a value. In a conditional $\mathsf {if}\, \mathsf {p} \! \mathop {\texttt {=}}\limits ^{\texttt {<\!-}}\! \mathsf {q} \, \mathsf {then} \, C_1 \, \mathsf {else} \, C_2$, $\mathsf {p}$ checks if its value is equal to $\mathsf {q}$’s to decide whether the system proceeds as $C_1$ or $C_2$. Term $\mathsf {def} \, X = C_2 \, \mathsf {in} \, C_1$ defines a procedure X with body $C_2$, which can be called in $C_1$ and $C_2$ by using term X.

The semantics of CC is given in terms of labeled reductions ; the main reduction rules are given in Fig. 2. Reductions are also closed under context (procedure definitions) and under a structural precongruence $\preceq$, allowing procedure calls to be unfolded and non-interfering actions to be executed in any order. The most interesting rule for $\preceq$ is rule $\left\lfloor \text{ C }|\text{ Eta-Eta }\right\rceil$, which swaps communications between disjoint sets of processes (modeling concurrency). The total function $\sigma$ maps each process name to the value it stores. Labels $\lambda$ tell us which action has been performed, which helps stating our later results. In rule $\left\lfloor \text{ C }|\text{ Com }\right\rceil$, v is the value obtained by evaluating ($\downarrow$) the expression e, with $\mathtt {*}$ replaced by the value of the sender $\mathsf {p}$, $\sigma (\mathsf {p})$. In the reductum, $\sigma$ is updated such that the receiver $\mathsf {q}$ stores v. Rule $\left\lfloor \text{ C }|\text{ Sel }\right\rceil$ does not alter $\sigma$: selections model invoking a method/operation available at the receiver. Rules $\left\lfloor \text{ C }|\text{ Then }\right\rceil$ and $\left\lfloor \text{ C }|\text{ Else }\right\rceil$ (omitted) model conditionals in the standard way. Function $\mathsf {pn}(C)$ returns all the process names that appear in C, and $C \equiv C'$ means $C \preceq C'$ and $C' \preceq C$.

Fig. 2.

Core choreographies, semantics and structural precongruence (selected rules).

Example 1

We define a simple choreography for client authentication. We write $\mathsf {p}\;\texttt {->}\;\mathsf {c},\mathsf {s} [l]$ as a shortcut for $\mathsf {p}\;\texttt {->}\;\mathsf {c} [l]; \mathsf {p}\;\texttt {->}\;\mathsf {s} [l]$.

$$ \mathsf {def} \, X\! = \! \left( \mathsf {c}.pwd\;\texttt {->}\;\mathsf {a}; \mathsf {if}\, \mathsf {a} \! \mathop {\texttt {=}}\limits ^{\texttt {<\!-}}\! \mathsf {s} \, \mathsf {then} \, \left( \mathsf {a}\;\texttt {->}\;\mathsf {c},\mathsf {s} [ok]; \mathsf {s}.t\;\texttt {->}\;\mathsf {c}\right) \, \mathsf {else} \, \left( \mathsf {a}\;\texttt {->}\;\mathsf {c},\mathsf {s} [ko]; X\right) \right) \, \mathsf {in} \, X $$

In this choreography, a client process $\mathsf {c}$ sends a password to an authentication process $\mathsf {a}$, which checks if the password matches that contained in the server-side process $\mathsf {s}$. If the password is correct, $\mathsf {a}$ notifies $\mathsf {c}$ and $\mathsf {s}$, and $\mathsf {s}$ sends an authentication token t to $\mathsf {c}$. Otherwise, $\mathsf {a}$ notifies $\mathsf {c}$ and $\mathsf {s}$ that authentication failed, and a new attempt is made (by recursively invoking X).   $\square$

Stateful Processes. The calculus SP models concurrent/distributed implementations. Thus, unlike in CC, actions are now distributed among processes.

Fig. 3.

Stateful processes, syntax.

The syntax of SP is given in Fig. 3. Networks N are parallel compositions of processes $\mathsf {p} \triangleright _{} B$, read “process $\mathsf {p}$ has behavior B”. An output term ${\mathsf {q}}!\langle e \rangle ;B$ sends the result of evaluating e to $\mathsf {q}$, and then proceeds as B. Outputs are meant to synchronize with input terms at the target process, i.e., $\mathsf {p}?;B$, which receives a value from $\mathsf {p}$ to be stored locally and then proceeds as B. Term ${\mathsf {q}}\oplus l;B$ sends the selection of the branch labeled l to $\mathsf {q}$. Branches are offered by the receiver with term ${\mathsf {p}} \& {\{ l_i : B_i\}_{i\in I}}$, which offers a choice among the labels $l_i$ to $\mathsf {p}$. When one of these labels is selected, the respective behavior $B_i$ is run. Term $\mathsf {if}\, \mathtt {*} \! \mathop {\texttt {=}}\limits ^{\texttt {<\!-}}\! \mathsf {q} \, \mathsf {then} \, B_1 \, \mathsf {else} \, B_2$ communicates with process $\mathsf {q}$ to check whether it stores the same value as the process running this behavior, in order to choose between the continuations $B_1$ and $B_2$. Terms $\mathsf {def} \, X = B_2 \, \mathsf {in} \, B_1$ and $X$ are procedure definition and call, respectively.

Fig. 4.

Stateful processes, semantics (selected rules).

The semantics of SP is given by labeled reductions , with labels $\lambda$ as in CC.¹ Figure 4 shows the key rules (see the appendix for the complete set). Two processes can synchronize when they refer to each other. In rule $\left\lfloor \text{ S }|\text{ Com }\right\rceil$, an output at $\mathsf {p}$ directed at $\mathsf {q}$ synchronizes with the dual input action at $\mathsf {q}$ – intention to receive from $\mathsf {p}$; in the reductum, $\mathsf {q}$’s value is updated. The reduction receives the same label as the equivalent communication term in CC. The other rules shown are similar. The omitted rules are standard, and close the semantics under parallel composition, structural precongruence, and procedure definitions.

Example 2

The following network implements the choreography in Example 1.

EndPoint Projection (EPP). As shown in [11], there exists a partial function $[\![\cdot ]\!]_{}:\text{ CC }\rightarrow \text{ SP }$, called EndPoint Projection (EPP), that produces correct implementations of choreographies. EPP produces a parallel composition of processes, one for each process name in the original choreography: $[\![C]\!]_{} = \prod _{\mathsf {p} \in \mathsf {pn}(C)} \mathsf {p} \triangleright _{} [\![C]\!]_{\mathsf {p}}$. The rules for computing $[\![C]\!]_{}$ project the local action performed by the process of interest. For example, $[\![\mathsf {p}.e\;\texttt {->}\;\mathsf {q}]\!]_{\mathsf {p}}={\mathsf {q}}!\langle e \rangle$ and $[\![\mathsf {p}.e\;\texttt {->}\;\mathsf {q}]\!]_{\mathsf {q}}=\mathsf {p}?$.

The network presented in Example 2 is exactly the EPP of the choreography in Example 1. Observe that the projection of the conditional in the original choreography for the processes $\mathsf {c}$ and $\mathsf {s}$ is a branching that supports all the possible choices made by process $\mathsf {a}$ in its projected conditional. Producing these branching terms is possible only if, whenever there is a conditional at a process ($\mathsf {a}$ in our example), all other processes receive a label that tells them which branch such a process has chosen. (In case the behaviors of the other processes are the same in both cases, producing branching terms is not necessary.) When this cannot be done for a choreography C, the EPP for C is undefined, and we say that C is unprojectable. Conversely, C is projectable if $[\![C]\!]_{}$ is defined.

In the remainder, we relate choreographies to network implementations via a strong labeled reduction bisimilarity $\sim$. Bisimilarity is defined as usual [24]: it is the union of all bisimulation relations $\mathcal R$, which in our case relate choreographies to networks. A relation $\mathcal R$ is one such bisimulation if whenever $C \mathcal R N$ we have that, for all $\sigma$: (i) implies for some $N'$ with $C'\mathcal R N'$; (ii) implies for some $C'$ with $C'\mathcal R N'$.

Theorem 1

(adapted from [11]). If C is projectable, then $C \sim [\![C]\!]_{}$.

4 Extraction from SP

The finite case. We first investigate finite SP, the fragment of SP without recursive definitions, which we use to discuss the intuition behind our extraction.

Definition 1

We define a rewriting relation $\leadsto$ on the language of CC extended with terms $(\![{N}]\!)$, where N is a network in finite SP, as the transitive closure of:

A network N in finite SP extracts to a choreography C if $(\![{N}]\!)\leadsto C$.

The last rule guarantees that every network is extractable. Extraction uses structural precongruence (namely, commutativity and associativity of parallel composition) to find matching actions. For finite SP, this is not a problem (the set of networks equivalent to a given one is finite), but it makes extraction nondeterministic, e.g., the network $\mathsf {p} \triangleright _{} {\mathsf {q}}!\langle e \rangle \, \varvec{|} \, \mathsf {q} \triangleright _{} \mathsf {p}? \, \varvec{|} \, \mathsf {r} \triangleright _{} {\mathsf {s}}!\langle e' \rangle \, \varvec{|} \, \mathsf {s} \triangleright _{} \mathsf {r}?$ extracts both to $\mathsf {p}.e\;\texttt {->}\;\mathsf {q};\mathsf {r}.e'\;\texttt {->}\;\mathsf {s}$ and $\mathsf {r}.e'\;\texttt {->}\;\mathsf {s};\mathsf {p}.e\;\texttt {->}\;\mathsf {q}$. These choreographies are equivalent by Rule $\left\lfloor \text{ C }|\text{ Eta-Eta }\right\rceil$ (Fig. 2). This holds in general, as stated below.

Lemma 1

If $(\![{N}]\!) \leadsto C_1$ and $(\![{N}]\!) \leadsto C_2$, then $C_1 \equiv C_2$.

There is one important design option to consider: what to do with actions that cannot be matched, i.e., processes that will deadlock. There are two alternatives: restrict extraction to lock-free networks (networks where all processes eventually progress, in the sense of [8]); or extract stuck processes to a new choreography term $\varvec{1}$, with the same semantics as $\varvec{0}$. We choose the latter option for debugging reasons. Specifically, practical applications of extraction may annotate $\varvec{1}$ with the code of the deadlocked processes, giving the programmer a chance to see exactly where the system is unsafe, and attempt at fixing it manually. Better yet: since the code to unlock deadlocked processes in process calculi can be efficiently synthesized [8], our method may be integrated with the technique in [8] to suggest an automatic system repair.

Remark 1

If $(\![{N}]\!) \leadsto C$ and C does not contain $\varvec{1}$, then N is lock-free. However, even if C contains $\varvec{1}$, N may still be lock-free: the code causing the deadlock may be dead code in a conditional branch that is never chosen during execution.

Extraction is sound: it yields a choreography that is bisimilar to the original network. Also, for finite SP, it behaves as an inverse of EPP.

Theorem 2

Let N be in finite SP. If $(\![{N}]\!)\leadsto C$, then $C\sim N$. Furthermore, if $N = [\![C']\!]_{}$ for some $C'$, then $(\![{N}]\!) \leadsto C'$.

As we show later, the second part of this theorem does not hold in the presence of recursive definitions.

We now restate extraction in terms of a particular graph, which is the hallmark of our development: when we add recursion to SP, we can no longer define extraction as a set of rewriting rules. We first introduce a new abstract semantics for networks, , defined as in Fig. 4 except for the rules for value communication and conditionals, which are replaced by those in Fig. 5 (we omit the obvious rule $\left\lfloor \text{ S }|\text{ Else }\right\rceil$). In particular, conditionals are now nondeterministic. Labels $\alpha$ are like $\lambda$ but may now contain expressions (see the new rule $\left\lfloor \text{ S }|\text{ Com }\right\rceil$); in all other rules, $\lambda$ is replaced by $\alpha$. We write for .

Fig. 5.

Stateful Processes, Abstract Semantics (selected rules).

Definition 2

Given a network N, the Abstract Execution Space (AES) of N is the directed graph obtained by considering all possible abstract reduction paths from N. Its vertices are all the networks $N'$ such that , and there is an edge between two vertices $N_1$ and $N_2$ labeled $\alpha$ if .

A Symbolic Execution Graph (SEG) for N is a subgraph of its AES that contains N and such that each vertex $N'\not \preceq \varvec{0}$ has either one outgoing edge labeled by an $\eta$ or two outgoing edges labeled $\mathsf {p} \! \mathop {\texttt {=}}\limits ^{\texttt {<\!-}}\! \mathsf {q}:\mathsf {then}$ and $\mathsf {p} \! \mathop {\texttt {=}}\limits ^{\texttt {<\!-}}\! \mathsf {q}:\mathsf {else}$.

Intuitively, the AES of N represents all possible evolutions of N (each evolution is a path in this graph). A SEG fixes the order of execution of actions, but still abstracts from the state (and thus considers both branches of conditionals). For networks in finite SP, these graphs are finite.

Given a network N, there is a one-to-one correspondence between SEGs for N and choreographies C such that $(\![{N}]\!)\leadsto C$. Indeed, given a SEG we can extract a choreography as follows. We start from the initial vertex, labeled N. If there is an outgoing edge with label $\eta$ to $N'$, we add $\eta$ to the choreography and continue from $N'$. If there are two outgoing edges with labels $\mathsf {p} \! \mathop {\texttt {=}}\limits ^{\texttt {<\!-}}\! \mathsf {q}:\mathsf {then}$ and $\mathsf {p} \! \mathop {\texttt {=}}\limits ^{\texttt {<\!-}}\! \mathsf {q}:\mathsf {else}$ to $N_1$ and $N_2$, respectively, we extract a conditional whose branches are the choreographies extracted by continuing exploration from $N_1$ and $N_2$, respectively. When we reach a leaf, we extract $\varvec{0}$ or $\varvec{1}$, according to whether its label is equivalent to $\varvec{0}$ or not. Conversely, we can build a SEG from a particular rewriting of $(\![{N}]\!)$ by following the choreography actions one at a time.

Treating recursive definitions. We now extend extraction to networks with recursive definitions, using SEGs. We need to be careful with the definition of the AES, since including all possible (abstract) executions now may make it infinite (due to recursion unfolding), and thus extraction may not terminate. To avoid this, we only allow recursive definitions to be unfolded (once) if they occur at the head of a process involved in a reduction. With this restriction, we can define the AES and SEGs for a network as in the finite case. These graphs may now contain cycles: a network may evolve into the same term after a few reductions.

Example 3

Consider the following network.

$$ \begin{aligned}&\mathsf {p} \triangleright _{} {}\mathsf {def} \, X = {\mathsf {q}}!\langle \mathtt {*} \rangle ;{\mathsf {q}} \& \{{\textsc {l}:{\mathsf {q}}!\langle \mathtt {*} \rangle ;X,\textsc {r}:\varvec{0}}\} \, \mathsf {in} \, {\mathsf {q}}!\langle \mathtt {*} \rangle ;X \\ \, \varvec{|} \,&\mathsf {q} \triangleright _{} {}\mathsf {def} \, Y = \mathsf {p}?;\mathsf {p}?;\mathsf {if}\, \mathtt {*} \! \mathop {\texttt {=}}\limits ^{\texttt {<\!-}}\! \mathsf {r} \, \mathsf {then} \, {\mathsf {p}}\oplus \textsc {l};Y \, \mathsf {else} \, {\mathsf {p}}\oplus \textsc {r};\varvec{0} \, \mathsf {in} \, Y \, \varvec{|} \, \mathsf {r} \triangleright _{} {}\mathsf {def} \, Z = {\mathsf {q}}!\langle \mathtt {*} \rangle ;Z \, \mathsf {in} \, Z \end{aligned}$$

This network generates the AES in Fig. 6, which is also its SEG.   $\square$

Fig. 6.

The AES and SEG for the network in Example 3.

The key insight is that the definitions of recursive procedures are extracted from the loops in the SEG, rather than from the recursive definitions in the source network. This construction typically yields mutually recursive definitions, motivating a small change to CC that does not add expressivity: we replace the constructor $\mathsf {def} \, X = C_2 \, \mathsf {in} \, C_1$ by top-level procedure definitions, in the style of [12]. A choreography now becomes a pair $\langle \mathcal D,C\rangle$, where $\mathcal D=\{X_i=C_i\}$ and all procedure calls in either C or the $C_i$ are to some $X_i$ defined in D.

Definition 3

The choreography extracted from a SEG is defined as follows. We annotate each node that has more than one incoming edge with a unique procedure identifier. Then, for every node annotated with an identifier, say X, we replace each of its incoming edges with an edge to a new leaf node that contains a special term X (so now the node annotated with X has no incoming edges). This eliminates all loops in the SEG, allowing us to reuse the extraction procedure for the non-recursive case to extract the desired pair $\langle \mathcal D,C\rangle$. We get C by extraction starting from the initial network. Then, for each node that we annotated with an X, we extract a choreographic procedure X in $\mathcal D$ that has as body the choreography extracted from the graph that starts from that annotated node. Any new leaf node containing a special term X is extracted as a procedure call X.

Example 4

Consider the SEG in Fig. 3. To extract a choreography, we annotate the topmost node with a procedure identifier X and replace the incoming edge to that node with an edge to a new leaf X. We thus extract X to be

$$ {\mathsf {p}.\mathtt {*}}{\mathsf {q}};\mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q};\mathsf {if}\, \mathsf {q} \! \mathop {\texttt {=}}\limits ^{\texttt {<\!-}}\! \mathsf {r} \, \mathsf {then} \, \mathsf {q}\;\texttt {->}\;\mathsf {p} [\textsc {l}];X \, \mathsf {else} \, \mathsf {q}\;\texttt {->}\;\mathsf {p} [\textsc {r}];\varvec{1} $$

and the extracted choreography itself is simply X. The body of X is not projectable (the branches for $\mathsf {r}$ are not mergeable, cf. [11]), but it faithfully describes the behavior of the original network.   $\square$

The procedure in Definition 3 always terminates, but sometimes it yields choreographies that starve some processes. As an example, the network

$$\begin{aligned}&\mathsf {p} \triangleright _{} {}\mathsf {def} \, X = {\mathsf {q}}!\langle \mathtt {*} \rangle ;X \, \mathsf {in} \, X \ \, \varvec{|} \, \ \mathsf {q} \triangleright _{} {}\mathsf {def} \, Y = \mathsf {p}?;Y \, \mathsf {in} \, Y \\ \, \varvec{|} \,&\mathsf {r} \triangleright _{} {}\mathsf {def} \, Z = {\mathsf {s}}!\langle \mathtt {*} \rangle ;Z \, \mathsf {in} \, Z \ \, \varvec{|} \, \ \mathsf {s} \triangleright _{} {}\mathsf {def} \, W = \mathsf {r}?;W \, \mathsf {in} \, W \nonumber \end{aligned}$$

(1)

has two SEGs, which extract to the choreographies $\mathsf {def} \, X = \mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q};X \, \mathsf {in} \, X$ and $\mathsf {def} \, X = \mathsf {r}.\mathtt {*}\;\texttt {->}\;\mathsf {s};X \, \mathsf {in} \, X$, none of which captures all the behaviors of N.

To avoid this problem, we change the definitions of AES and SEGs slightly. We annotate all procedure calls in networks with either $\circ$ or $\bullet$. The node in the AES corresponding to the initial network has all procedure calls annotated with $\circ$. There is an edge from N to $N'$ with label $\alpha$ if and the procedure calls in $N'$ are annotated as follows.

• If executing $\alpha$ does not require unfolding procedure calls, then all calls in $N'$ are annotated as in N.

• If executing $\alpha$ requires unfolding procedure calls, then we annotate all the calls in $N'$ introduced by these unfoldings with $\bullet$. If $N'$ now has all procedure calls annotated with $\bullet$, we change all annotations to $\circ$.

We then require loops in a SEG to contain a node where every procedure call is annotated with $\circ$. This ensures that every procedure call is unfolded at least once before returning to the same node. This holds even if $\mathsf {p} \triangleright _{} X$ unfolds to a behavior that calls different procedures, but not X: in order to return to the same node, the newly invoked procedures themselves need to be unfolded.

Example 5

The annotated AES for the network (1) is:

This AES now has the following two SEGs:

Observe that the self-loops are discarded because they do not go through a node with all $\circ$ annotations. From these SEGs, we can extract two definitions for X:

$$ \mathsf {def} \, X = \mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q};\mathsf {r}.\mathtt {*}\;\texttt {->}\;\mathsf {s};X \, \mathsf {in} \, X \qquad \text{ and } \qquad \mathsf {def} \, X = \mathsf {r}.\mathtt {*}\;\texttt {->}\;\mathsf {s};\mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q};X \, \mathsf {in} \, X $$

Both of these definitions correctly capture all behaviors of the network.   $\square$

A similar situation may occur if there are processes with finite behavior (no procedure calls): the network

$$ \mathsf {p} \triangleright _{} \mathsf {def} \, X = {\mathsf {q}}!\langle \mathtt {*} \rangle ;X \, \mathsf {in} \, X \ \, \varvec{|} \, \ \mathsf {q} \triangleright _{} \mathsf {def} \, Y = \mathsf {p}?;Y \, \mathsf {in} \, Y \ \, \varvec{|} \, \ \mathsf {r} \triangleright _{} {\mathsf {s}}!\langle \mathtt {*} \rangle \ \, \varvec{|} \, \ \mathsf {s} \triangleright _{} \mathsf {r}? $$

can be extracted to the choreography X, with $X=\mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q};X$, where $\mathsf {r}$ and $\mathsf {s}$ never communicate. Hence, we require that if a node in a SEG has more than one incoming edge (it is a “loop” node) and contains processes with finite behavior, then these processes must be deadlocked (being finite, this is trivially verifiable). This ensures that if finite processes are able to reduce, they cannot be in a loop.

Definition 4

A SEG for a network N is valid if all its loops:

• pass through a node where all recursive calls are marked with $\circ$;

• start in a node where all processes with finite behavior are deadlocked.

A network N extracts to a choreography C if C can be constructed (as in Definition 3) from a valid SEG for N.

Validity implies, however, that there are some non-deadlocked networks that are not extractable, such as

$$ \mathsf {p} \triangleright _{} \mathsf {def} \, X = {\mathsf {q}}!\langle \mathtt {*} \rangle ;X \, \mathsf {in} \, X \, \varvec{|} \, \mathsf {q} \triangleright _{} \mathsf {def} \, Y = \mathsf {p}?;Y \, \mathsf {in} \, Y \, \varvec{|} \, \mathsf {r} \triangleright _{} \mathsf {def} \, Z = \mathsf {p}?;Z \, \mathsf {in} \, Z $$

for which there is no valid SEG. This is to be expected, since deadlock-freedom is undecidable in SP. We can generalize this observation as a necessary condition for extraction to be defined, in the following theorem.

Theorem 3

If the AES for a network N does not contain nodes from which a process is always deadlocked, then N is extractable.

Lemma 1 and the first part of Theorem 2 still hold for extraction in SP with recursion, but the second part of Theorem 2 does not: in general, the projection of a choreography is extracted to a choreography with different procedures, since extraction ignores the actual definitions in the source network.

Theorem 4

If C is a choreography extracted from a network N, then $N\sim C$.

We conclude this section with some complexity theoretical considerations.

Lemma 2

The annotated AES for a network of size n has at most $e^{\frac{2n}{e}}$ vertices.

Theorem 5

Extraction from a network of size n terminates in time $O(n e^{\frac{2n}{e}})$.

As discussed earlier, this time complexity is a dramatic improvement over earlier, comparable work. However, in practice, we may be able to perform even better. Algorithmically, all the required work stems from traversals of the AES, so any reduction in its (explored) size will lead to proportional runtime improvements. Thus, instead of first computing the entire AES and then a valid SEG, we can compute the relevant parts of the AES lazily as we need them, so parts of the AES that are never explored while computing a valid SEG are never generated.

5 Asynchrony

We now discuss an asynchronous semantics for SP, with which we can express new safe behaviors. Most notably, SP can now express asynchronous exchange (Example 6). We also show a novel choreography primitive that successfully captures this pattern, which cannot be described in previous works on choreographic programming, and extend our algorithm to extract it from networks.

Asynchronous SP. Asynchronous communication can be added to SP using standard techniques for process calculi. In the semantics of networks, we add a FIFO queue for each pair of processes. Communications now synchronize with these queues: send actions append a message in the queue of the receiver, and receive actions remove the first message from the queue of the receiver (see [12] for a formalization in an extension of SP).

Example 6

The network $\mathsf {p} \triangleright _{} {\mathsf {q}}!\langle \mathtt {*} \rangle ;\mathsf {q}? \ \, \varvec{|} \, \ \mathsf {q} \triangleright _{} {\mathsf {p}}!\langle \mathtt {*} \rangle ;\mathsf {p}?$ exemplifies the pattern of asynchronous exchange. This network is deadlocked in synchronous SP, but runs without errors in asynchronous SP: both $\mathsf {p}$ and $\mathsf {q}$ can send their respective values, becoming ready to receive each other’s messages. This behavior is not representable in any previous work on choreographies (including CC from Sect. 3), since all choreographies presented so far can only describe processes that are not deadlocked under a synchronous semantics (see [12] for a formal argument).   $\square$

The multicom. The situation in Example 6 is prototypical of programs that are safe only in an asynchronous setting: a group of processes wants to send messages to a group of receivers, with circular dependencies among communications.

We deal with this situation by means of a new choreography action, which we call a multicom. Syntactically, a multicom is a list of communication actions with distinct receivers, which we write $(\tilde{\eta })$. In the unary case, we obtain the usual communications and selections; by removing these from the syntax of CC and adding the multicom, we obtain a more expressive calculus with fewer primitives. The semantics of multicom is given by the following rule, which generalizes (and replaces) both $\left\lfloor \text{ C }|\text{ Com }\right\rceil$ and $\left\lfloor \text{ C }|\text{ Sel }\right\rceil$.

Structural precongruence rules for the multicom are motivated by its intuitive semantics: actions inside a multicom can be permuted as long as the senders differ, and sequential multicoms can be merged as long as they do not share receivers and there are no sequential constraints between them (i.e., none of the receivers in the first multicom is a sender in the second one).

From these rules we can derive all instances of $\left\lfloor \text{ C }|\text{ Eta-Eta }\right\rceil$, e.g.:

$$ \mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q};\mathsf {r}.\mathtt {*}\;\texttt {->}\;\mathsf {s} \equiv \left( \begin{array}c \mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q}\\ \mathsf {r}.\mathtt {*}\;\texttt {->}\;\mathsf {s} \end{array}\right) \equiv \left( \begin{array}c \mathsf {r}.\mathtt {*}\;\texttt {->}\;\mathsf {s}\\ \mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q} \end{array}\right) \equiv \mathsf {r}.\mathtt {*}\;\texttt {->}\;\mathsf {s};\mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q} $$

The problematic program in Example 6 can now be written as $\left( \begin{array}c \mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q}\\ \mathsf {q}.\mathtt {*}\;\texttt {->}\;\mathsf {p} \end{array}\right)$.

Structural precongruence rules for multicom also allow us to define a normal form for choreographies, where no multicom can be split in smaller multicoms.

Extraction. In order to extract choreographies containing multicoms, we alter the definition of the AES for a process network by allowing multicoms as labels for the edges. These can be computed using the following iterative algorithm.

• 1. For a process $\mathsf {p}$ with behavior ${\mathsf {q}}!\langle e \rangle ;B$ (or ${\mathsf {q}}\oplus l;B$), set $\mathsf {actions}=\emptyset$ and $\mathsf {waiting}=\{\mathsf {p}.e\;\texttt {->}\;\mathsf {q}\}$ (resp. $\mathsf {waiting}=\{\mathsf {p}\;\texttt {->}\;\mathsf {q} [l]\}$).

• 2. While $\mathsf {waiting}\ne \emptyset$:

  • (a) Move an action $\eta$ from $\mathsf {waiting}$ to $\mathsf {actions}$. Assume $\eta$ is of the form $\mathsf {r}.e\;\texttt {->}\;\mathsf {s}$ (the case for label selection is similar).

  • (b) If the behavior of $\mathsf {s}$ is of the form $a_1;\ldots ;a_k;\mathsf {r}?;B$ where each $a_i$ is either the sending of a value or a label selection, then: for each $a_i$, if the corresponding choreography action is not in $\mathsf {actions}$, add it to $\mathsf {waiting}$.

• 3. Return $\mathsf {actions}$.

This algorithm may fail (the behavior of $\mathsf {s}$ in step 2(b) is not of the required form), in which case the action initially chosen cannot be unblocked by a multicom.

Example 7

Consider the network from Example 6. Starting with action ${\mathsf {q}}!\langle \mathtt {*} \rangle$ at process $\mathsf {p}$, we initialize $\mathsf {actions}=\emptyset$ and $\mathsf {waiting}=\{\mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q}\}$. We pick the action $\mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q}$ from $\mathsf {waiting}$ and move it to $\mathsf {actions}$. The behavior of $\mathsf {q}$ is ${\mathsf {p}}!\langle \mathtt {*} \rangle ;\mathsf {p}?$, which is of the form described in step 2(b); the choreography action corresponding to ${\mathsf {p}}!\langle \mathtt {*} \rangle$ is $\mathsf {q}.\mathtt {*}\;\texttt {->}\;\mathsf {p}$, so we add this action to $\mathsf {waiting}$, obtaining $\mathsf {actions}=\{\mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q}\}$ and $\mathsf {waiting}=\{\mathsf {q}.\mathtt {*}\;\texttt {->}\;\mathsf {p}\}$. Now we consider the action $\mathsf {q}.\mathtt {*}\;\texttt {->}\;\mathsf {p}$, which we move from $\mathsf {waiting}$ to $\mathsf {action}$, and look at $\mathsf {p}$’s behavior, which is ${\mathsf {q}}!\langle \mathtt {*} \rangle ;\mathsf {q}?$. The choreography action corresponding to ${\mathsf {q}}!\langle \mathtt {*} \rangle$ is $\mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q}$, which is already in $\mathsf {actions}$, so we do not change $\mathsf {waiting}$. The set $\mathsf {waiting}$ is now empty, and the algorithm terminates, returning $\left( \begin{array}c \mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q}\\ \mathsf {q}.\mathtt {*}\;\texttt {->}\;\mathsf {p} \end{array}\right)$. We would obtain the equivalent $\left( \begin{array}c \mathsf {q}.\mathtt {*}\;\texttt {->}\;\mathsf {p}\\ \mathsf {p}.\mathtt {*}\;\texttt {->}\;\mathsf {q} \end{array}\right)$ by starting with the send action at $\mathsf {q}$.   $\square$

Example 8

As a more sophisticated example, we show how our new choreographies with multicom can model the alternating 2-bit protocol. Here, Alice alternates between sending a 0 and a 1 to Bob; in turn, Bob sends an acknowledgment for every bit he receives, and Alice waits for the acknowledgment before sending another copy of the same bit. Since we are in an asynchronous semantics, we only consider the time when the messages arrive. With this in mind, we can write this protocol as the following network.

$$\begin{aligned} \mathsf {a} \triangleright _{} {}&\mathsf {def} \, X = (\mathsf {b}?;{\mathsf {b}}!\langle 0 \rangle ;\mathsf {b}?;{\mathsf {b}}!\langle 1 \rangle ;X) \, \mathsf {in} \, ({\mathsf {b}}!\langle 0 \rangle ;{\mathsf {b}}!\langle 1 \rangle ;X) \\ \, \varvec{|} \, \ \mathsf {b} \triangleright _{} {}&\mathsf {def} \, Y = (\mathsf {a}?;{\mathsf {a}}!\langle \mathsf {ack}_0 \rangle ;\mathsf {a}?;{\mathsf {a}}!\langle \mathsf {ack}_1 \rangle ;Y) \, \mathsf {in} \, Y \end{aligned}$$

This implementation imposes exactly the dependencies dictated by the protocol. For example, Alice can receive Bob’s acknowledgment to the first 0 before or after Bob receives the first 1. This network extracts to the choreography

$$ {\mathsf {a}.0\;\texttt {->}\;\mathsf {b};X} \qquad \text{ where }\qquad X = \left( \begin{array}c \mathsf {a}.1\;\texttt {->}\;\mathsf {b}\\ \mathsf {b}.\mathsf {ack}_0\;\texttt {->}\;\mathsf {a} \end{array}\right) ; \left( \begin{array}c \mathsf {a}.0\;\texttt {->}\;\mathsf {b}\\ \mathsf {b}.\mathsf {ack}_1\;\texttt {->}\;\mathsf {a} \end{array}\right) ; X $$

which is a simple and elegant representation of the alternating 2-bit protocol.   $\square$

Extraction for asynchronous SP is still sound, but behavioral equivalence is now an expansion [1, 24], as each communication now takes two steps in asynchronous SP. Its complexity is also no larger than for the synchronous case. The algorithm computing the multicom takes linear time in the size of the multicom produced. Via a one-time preprocessing of the network, we can assume direct references from communication terms in one process to the process it directs its communication at, and from there to the current state of that process. Other than the above, all constant steps in the algorithm can be seen as an extension of the multicom. Since adding a communication to a multicom removes a potential node in the AES (as we are combining communications), the worst-case time complexity is no worse than in the synchronous case. In practice, this complexity actually gets better when larger multicoms are created, since building these is a much cheaper local operation than exploring graphs that would be larger in terms of nodes as well as edges without the multicoms.

6 Extensions and Applications

We discuss some straightforward modifications of our extraction to cover other scenarios occurring in the literature.

More expressive communications and processes. In real-world contexts, the values stored and communicated by processes are typed, and the receiver process can also specify how to treat incoming messages [12]. This means that communication actions now have the form $\mathsf {p}.e\;\texttt {->}\;\mathsf {q}.f$, where f is the function consuming the received message, and systems may deadlock because of typing errors. Our construction applies without changes to this scenario.

Some works allow processes to store several values, used via variables [5, 6]. Again, dealing with this situation does not require any changes to our algorithm.

Local conditionals. Many choreography models allow for a local conditional construct, i.e., $\mathsf {if}\, \mathsf {p}.e \, \mathsf {then} \, C_1 \, \mathsf {else} \, C_2$ [6, 14, 21]. Dealing with this construct is simple: the $\mathsf {if}$ and $\mathsf {then}$ transitions now can occur whenever a process has a conditional as top action, since they no longer require synchronization with other processes.

Choreography Specifications. So far, we have considered choreographies that describe concrete implementations, i.e., processes are equipped with storage and local computational capabilities. However, choreographies have also been advocated for the specification of communication protocols. Most notably, multiparty session types use choreographies to define types used in the verification of process calculi [17]. While there are multiple variants of multiparty session types, the one so far most used in practice is almost identical to a simplification of SP. In this variant, each pair of participants has a dedicated channel, and communication actions refer directly to the intended sender/recipient as in SP (see, e.g., the theory of [6, 9, 10, 21] and the practical implementations in [16, 20, 23]). To obtain multiparty session types from SP (and CC), we just need to: remove the capability of storing values at processes; replace message values with constants (representing types, which could also be extended to subtyping in the straightforward way); and make conditionals nondeterministic (since in types we abstract from the precise values and expression used by the evaluator). These modifications do not require any significant change to our approach, since our AES already abstracts from data and thus our treatment of the conditional is already nondeterministic. For reference, we can simply treat the standard construct for an internal choice at a process $\mathsf {p}$ – $C_1\oplus _{\mathsf {p}} C_2$ – as syntactic sugar for a local conditional like $\mathsf {if}\, \mathsf {p}.\mathsf {coinflip} \, \mathsf {then} \, C_1 \, \mathsf {else} \, C_2$.