Dieses Kapitel vertieft die Herausforderungen bei der Implementierung verteilter Systeme, insbesondere das Problem der Kommunikationsblockaden zwischen Nachrichtenweiterleitungsprozessen. Es führt choreografische Programmierung als Top-Down-Methode ein, um die Implementierung verteilter Systeme zu vereinfachen, indem globale Programme definiert werden, die das kollektive Verhalten aller Prozesse festlegen. Das Kapitel stellt dann einen neuartigen Ansatz vor, der First-Person-Choreografie genannt wird und die Erzählperspektive von der Third-Person-Perspektive auf die First-Person-Perspektive der Prozesse verlagert. Diese Verschiebung trägt entscheidend zur Unterstützung der Prozess-Parametrizität bei und ermöglicht die dynamische Bestimmung der Anzahl der Prozesse zur Laufzeit. Das Kapitel führt auch Continuation-Passing-Kommunikation ein, ein neues choreografisches Primitiv, das dynamische Projektion ermöglicht und gleichzeitig statische Schriftlichkeit aufrechterhält. Die Umsetzung dieses Ansatzes wird durch das 1CPLT-Projekt demonstriert, das eine Prototypsprache und Werkzeuge umfasst, die in VS Code integriert sind. Das Kapitel zeigt detaillierte Beispiele verteilter Systeme wie das M-out-of-N-System, den Chang-Roberts-Algorithmus für die Wahl des Parteivorsitzenden und den Echo-Algorithmus für Wellen, was die Aussagekraft und praktische Anwendbarkeit des neuen Ansatzes verdeutlicht. Die theoretischen Grundlagen werden in Isabelle / HOL formalisiert, um die Solidität und Richtigkeit der Methode zu gewährleisten. Das Kapitel schließt mit einer Diskussion über verwandte Arbeit und zukünftige Richtungen, wobei das Potenzial der choreographischen Programmierung in der ersten Person hervorgehoben wird, um die Beschränkungen bestehender choreografischer Programmiersprachen und der Typisierung von Sitzungen durch mehrere Parteien anzusprechen.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Choreographic programming (CP) is a method to implement distributed systems that ensures communication deadlock freedom by design. To use CP, though, the number of processes and the network among them must be known statically. Often, that information is known only dynamically. Thus, existing CP languages cannot be used to implement process-parametric distributed systems.
This paper introduces first-person choreographic programming (1CP) to support the implementation of process-parametric distributed systems while also ensuring communication deadlock freedom. We present both a design of 1CP (new calculus, formalised in Isabelle/HOL) and an implementation (new language and tooling, integrated in VS Code).
1 Introduction
1.1 Background: Choreographic Programming
Implementing distributed systems is hard. One of the challenges is to “prove”—broadly construed—the absence of communication deadlocks among message-passing processes. A communication deadlock is a form of misbehaviour that arises when all processes get stuck in cyclic communication dependencies.
Fig. 1:
Choreographic programming
Choreographic programming [3, 5, 39] is a top–down method to make the implementation of distributed systems easier. Fig. 1a visualises the idea:
1.
First, construct a global programG (“choreography”). A global program defines the behaviour of all n processes in the distributed system, collectively.
Anzeige
Example 1
The TwoBuyer distributed system consists of processes Buyer1 (
), Buyer2 (
), and Seller (
). As introduced by Honda et al. [30]: “Buyer1 and Buyer2 wish to buy an expensive book from Seller by combining their money. Buyer1 sends the title of the book to Seller, Seller sends to both Buyer1 and Buyer2 its quote, Buyer1 tells Buyer2 how much she can pay, and Buyer2 either accepts the quote or rejects the quote by notifying Seller.”
The following global program defines the behaviour of Buyer1, Buyer2, and Seller, collectively (excerpt):
Global program \(p.E {{\rightarrowtriangle }}q.y\) defines a communication of (the value of) expression E, from the process named p, to the process named q, into variable y. Global programs
and \(G_1 {{;}}G_2\) define conditional choice, at the process named p, and sequencing. We write \(p.E {{\rightarrowtriangle }}[q_1 \ldots , q_n].y\) as a shorthand for \(p.E {{\rightarrowtriangle }}q_1.y {{;}}\ldots {{;}}p.E {{\rightarrowtriangle }}q_n.y\). \(\square \)
2.
Next, statically decompose the global program into local programs\(L_1, L_2,\ldots , L_n\), by compilingG separately for each of the n processes. A local program defines the behaviour of one process, individually.
Example 2
The following local programs, compiled from \(G^\text {TwoBuyer}\), define the behaviour of Buyer1, Buyer2, and Seller, individually (excerpts):
Local programs
and \(p \text {?}y\) define a send to the process named q and a receive from the process named p. \(\square \)
3.
Last, dynamically (re)compose the local programs as processes into a distributed system by running them together, in parallel.
The main result of choreographic programming is that, if the compilation of G succeeds for each process, then the run of \(L_1, L_2,\ldots , L_n\) is free of communication deadlocks. That is, we enjoy communication deadlock freedom by design.
Early work on choreographic programming is due to Carbone et al. [3, 4] and Carbone–Montesi [5]; substantial progress has been made since. For instance, Montesi and Yoshida developed a theory of compositional choreographic programming [40]; Carbone et al. studied connections with linear logic [2, 6, 7]; Dalla Preda et al. combined choreographic programming with dynamic adaptation [45‐47]; Cruz-Filipe et al. presented a technique to extract global programs from local programs [14]; Giallorenzo et al. studied a correspondence with multitier languages [26]. Furthermore, theoretical results are supported in practice by several tools, including Chor [5], Choral [25, 26], and HasChor [50].
Anzeige
1.2 Open Problem: Process-Parametric Distributed Systems
Central to the compilation of global programs is the concept of static projection. Formally, static projection is a function \(\mathbin {{\upharpoonright }}\) that consumes a global program G and a name p as input, and that produces a local program \(G \mathbin {{\upharpoonright }}p\) as output.
Essentially, to decompose global program G into local programs, the compiler statically projects G onto each name that occurs in G. In this way, the number of names that occur in G at compile-time fully determines the number of processes that occur in the distributed system at run-time. In many distributed systems, though, the number of processes that occur at run-time is known only dynamically, not statically. Such distributed systems cannot be implemented using existing choreographic programming languages.
Example 3
An AnyBuyer distributed system consists of processes Buyer1 (
), Buyer2 (
), ..., Buyern (
), and Seller (
). It generalises the TwoBuyer distributed system from two buyers to any number. Each buyer contributes a fraction of the quote; Buyern decides to accept/reject. The following global programs define the behaviour of all processes, collectively, for \(n \in \{3, 4\}\) (excerpts):
Each buyer has its own variables \(\texttt {x}\), \(\texttt {y}\), and \(\texttt {f}\) (initialised when the run begins).
Thus, for each n, a separate global program needs to be written: no existing choreographic programming language supports parametrisation in n. However, n is typically known only dynamically. As a result, realistically, AnyBuyer cannot be implemented using choreographic programming. \(\square \)
Generally, existing choreographic programming languages require not only the number of processes to be known statically (always one per name), but also the network among them (always fully connected). These constraints seriously limit the applicability of choreographic programming. Thus, the open problem addressed in this paper is how to support process-parametric distributed systems, in which such information is known only dynamically. Related work suggests that this is difficult: in multiparty session typing (MPST) [30], in which static projection is used to decompose global types into local types, extensions for process parametricity lose decidability [51], soundness [41], or expressiveness [8].
1.3 This Paper
Whereas the decomposition of global types in MPST must happen statically (i.e., local types are used at compile-time), the decomposition of global programs in choreographic programming may—in principle—happen dynamically (i.e., local programs are used only at run-time). That is, in contrast to MPST, there is no fundamental reason in choreographic programming to insist on static projection. This insight paves the way to a completely different approach to choreographic programming based on dynamic projection. Exploring this approach is the aim of this paper. To summarise the contributions:
What: A novel approach, called first-person choreographic programming
How: A new choreographic primitive, called continuation-passing communication, that enables dynamic projection (at run-time) of choreographies that are still statically well-typed (at compile-time)
Why: To implement process-parametric distributed systems using choreographic programming, including communication deadlock freedom by design
Concretely, we present both a design of first-person choreographic programming (new calculus, formalised in Isabelle/HOL) and an implementation (new language and tooling, integrated in VS Code). Sect. 2 presents an overview. Sect. 3 presents the design. Sect. 4 presents the implementation (including type checking and interpretation; without code generation). The paper is concluded in Sect. 5.
2 Overview
2.1 Design: A Tour of First-Person Choreographic Programming
In existing choreographic programming languages, global programs are written from the third-person point-of-view of the programmer. For instance,
means “a communication from Alice to Bob” from the programmer’s point-of-view. At heart, the key novelty of this paper is to shift the narrative perspective in global programs to the first-person points-of-view of the processes. For instance,
means “a communication from me to Bob” from Alice’s point-of-view. This shift in perspective is instrumental for us to support process-parametricity.
We call the existing approach third-person choreographic programming (3CP) and our new approach first-person choreographic programming (1CP). Fig. 1b visualises the idea. We clarify it below and introduce our calculus along the way.
1.
First, construct global programs \(G_1, G_2, \ldots , G_m\). Like in 3CP, each global program in 1CP defines the behaviour of all processes, collectively. However:
In 3CP, a single global program reflects multiple points-of-view, each taken by one process.
In 1CP, in contrast, multiple global programs each reflect a single point-of-view, taken by one-or-more processes (process parametricity).
Example 4
To clarify the terminology and difference between 3CP and 1CP:
In 3CP, TwoBuyer consists of three processes (Buyer1, Buyer2, Seller), and three points-of-view (Buyer1, Buyer2, Seller; we overload the process names when the correspondence is one-to-one), reflected by \(G^\text {TwoBuyer}\).
In 1CP, AnyBuyer consists of \(n{+}1\) processes (Buyer1, ..., Buyern, Seller), but three points-of-view (Buyer1, Buyer\({\ge }2\), Seller), reflected by three global programs. Thus, a single point-of-view (Buyer\({\ge }2\)) is taken by more than one process (Buyer2, ..., Buyern). We note that Buyer1 has a different point-of-view than Buyeri, for any \(i \ge 2\), as Buyer1 is initially active (sends a message), whereas Buyeri is initially reactive (awaits a message). In our calculus, the following global programs reflect this:
Global program \({\textbf {skip}}\) defines a no-op. Thus,
and
define the absence of initial behaviour. \(\square \)
In more detail, each global program is written in terms of continuation-passing communications and choreographic procedures.
Example 5
To demonstrate continuation-passing communications, in our calculus, the following global program reflects the point-of-view of Buyer1:
Global program \(E {\rightarrowtriangle }q.y {\triangleright }G\) defines a continuation-passing communication
of (the value of) expression E, from an implicitactive process,
to the explicitreactive process named q, into variable y,
followed by the asynchronous execution, by q, of global program G, written from q’s point-of-view.
Thus, as the first active process, Buyer1 passes \(\texttt {"foo"}\) and a continuation—written from Seller’s point-of-view—to Seller. When Seller receives, as the next active process, it passes \(\texttt {quote(title)}\) and a continuation to Buyer1.
When Buyer1 receives, as one of the now-active processes, it passes \(\texttt {x / f}\) and a continuation to \(\texttt {neigh}\) (a reference to Buyer2). When Buyer2 receives, it calls choreographic procedure \(\texttt {contrib}\).
In parallel, Seller—still active—passes \(\texttt {quote(title)}\) and a continuation to each \(\texttt {neigh}\) in \(\texttt {neighs}\) (a list of references to Buyer2, ..., Buyern).
This example demonstrates that, due to the asynchronous execution of continuations, multiple processes can become active in parallel. \(\square \)
Intuitively, each occurrence of “\({\triangleright }\)” signifies a lexical context switch in which the previous active process passes a message and a continuation to the next active process.1 In this way, continuation passing is a form of process-driven dynamic projection: the processes at run-time tell each other how to behave (from their first-person points-of-view), instead of a choreographic programming tool at compile-time (from its third-person point-of-view).
Example 6
To demonstrate choreographic procedures, in our calculus, the following choreographic libraries map choreographic procedure names to bodies, for each of the three points-of-view in AnyBuyer:
Thus, Buyer1 and Seller do not have choreographic procedures, while Buyeri, for any \(i \ge 2\), has \(\texttt {contrib}\). The following global program defines its body:
Thus, each time Buyericalls\(\texttt {contrib}\), it checks if \(\texttt {x}\) (quote) and \(\texttt {y}\) (contribution up to Buyer\(i{-}1\)) are already set; \(\texttt {0}\) indicates unset. If so, and if \(\texttt {last}\) (flag to indicate whether or not Buyeri is the n-th buyer) is true, then Buyeri decides to accept/reject the quote; otherwise, using \(\texttt {f}\) (denominator of the fraction that Buyeri can contribute), Buyeri passes \(\texttt {x / f + y}\) (total contribution up to Buyeri) and a continuation to \(\texttt {neigh}\) (reference to Buyer\(i{+}1\)).
Putting the pieces in this example and in Exmp. 5 together, Buyeri calls \(\texttt {contrib}\) twice: once in a continuation passed to it by Seller (and the incoming message sets \(\texttt {x}\)), and once in a continuation passed to it by Buyer\(i{-}1\) (and the incoming message sets \(\texttt {y}\)), but in any order (due to asynchrony). \(\square \)
2.
Next, at compile-time, statically analyse each global program, including the bodies of choreographic procedures, by means of type checking. Our main result (Thm. 1) is that if each global program is well-typed, then any properly initialised run of those global programs is free of communication deadlocks. Proper initialisation means that the initial values of variables are well-typed; this involves a lightweight check right at the beginning of a run. Thus, just as third-person choreographic programming, first-person choreographic programming guarantees communication deadlock freedom by design.
Example 7
Intuitively, to ensure that none of the processes in AnyBuyer get stuck, they must have the following variables and choreographic procedures:
Seller: \(\texttt {title}\) (string) and \(\texttt {neighs}\) (list of process references).
In our calculus, the following data/choreographic type environments capture these assumptions, for each of the three points-of-view:
Using these environments, we can statically prove that
,
,
, and \(G_{\texttt {contrib}}^\text {AnyBuyer}\) (all defined in previous examples) are well-typed; we do not need to know n to make this judgment. Thus, any properly initialised run—for any n—is free of communication deadlocks.
We note that the typing rules do not guarantee functional correctness. For instance, if both Buyer2 and Buyer3 have a reference to Buyer4 in \(\texttt {neigh}\), then the system is deadlock-free (well-typed) but functionally incorrect. \(\square \)
3.
Last, at run-time, dynamically create a configuration for each process, and compose those configurations into a distributed systems by running them together, in parallel. If the point-of-view of a process is p, then its initial configuration is of the shape \((\varPhi , \varPsi , G)\), where:
\(\varPhi \) defines the initial values of the variables of the process;
\(\varPsi \) defines the choreographic library from point-of-view p;
G defines the behaviour of all processes, collectively, from point-of-view p.
Thus, all processes that have the same point-of-view, have the same choreographic library and the same global program in their initial configurations.
To be able to reference different processes that have the same point-of-view, we use indexed names of the shape \(p\)\(\texttt {[}\)\(i\)\(\texttt {]}\), where p is a point-of-view, and i is an index. We write just p as a shorthand for \(p\)\(\texttt {[0]}\).
Example 8
The following configurations initialise AnyBuyer for \(n = 4\):
Each \(\varPhi _{p\texttt {[}i\texttt {]}}\) is well-typed in \(\varGamma _p^\text {AnyBuyer}\); this is a near-trivial check. \(\square \)
Example 9
To demonstrate a run, we show the first few reductions of the configurations of Buyer1 and Seller in our calculus. First, the following configurations are initial:
Next, Buyer1 passes \(\texttt {"foo"}\) and a continuation to Seller:
Global program \(x {:=}E\) defines the assignment of (the value of) E, to variable x. Thus, as part of the communication from Buyer1 to Seller, the assignment of the incoming message and the execution of the continuation are explicitly scheduled to be executed by Seller, using sequencing.
Next, Seller executes the assignment. Let
:
Next, Seller passes the value of \(\texttt {quote(title)}\) (i.e., this expression is eagerly evaluated at Seller instead of lazily at Buyer1) and a continuation to Buyer1. Let
in
):
Next, Buyer1 executes the assignment or, in parallel, Seller asynchronously executes \(G_2\). And so on. \(\square \)
2.2 Implementation: 1CPLT by Example
About To explore how to possibly transfer the calculus from theory to practice, we initiated the 1CPLT project. It consists of a prototype language, along with proof-of-concept tooling (including modern editor support), to apply first-person choreographic programming “for real”. It is built as an extension to VS Code.2
1CPLT includes a parser (implements the syntax of the calculus), a type checker (static semantics), and an interpreter (dynamic semantics). The examples below demonstrate 1CPLT implementations of basic distributed systems that are not supported by existing choreographic programming languages.
M-out-of-N First, we demonstrate the structure of the 1CPLT language.
Example 10
An M-out-of-N distributed system consists of processes Producer1, ..., Producern, and Consumer. A self-reference is communicated from each producer to the consumer, unordered. The first m references received by the consumer, from any subset of producers, are stored; the last \(n{-}m\) references are lost. The consumer tells each producer whether or not its reference was stored. There are two points-of-view: that of any producer and that of the consumer.
Fig. 2:
M-out-of-N in 1CPLT
Fig. 2a shows a 1CPLT implementation of M-out-of-N.
Lines 1–14 contain two \(\texttt {global}\) blocks, each of which pertains to one point-of-view. In general, each \(\texttt {global}\) block defines:
the name of a point-of-view (e.g., \(\texttt {Prod}\));
the variables of any process that has that point-of-view (e.g., \(\texttt {ok}\));
a distinguished choreographic procedure \(\texttt {main}\) whose body is the initial global program of any process that has that point-of-view (when \(\texttt {main}\) is absent, the initial global program is assumed to be \({\textbf {skip}}\));
additional choreographic procedures (none in this example) that constitute the choreographic library of any process that has that point-of-view.
Lines 16–19 contain four \(\texttt {process}\) statements: each line defines an initial configuration of a process in terms of the name of its point-of-view (e.g., \(\texttt {Prod}\)), its index (e.g., \(\texttt {1}\); when absent, it is assumed to be \(\texttt {0}\)), and its initial values of variables.
A key point is that only\(\texttt {global}\)blocks are needed for static type checking, while\(\texttt {process}\)statements are needed only for dynamic execution.
We note that the consumer also uses each received reference \(\texttt {p}\) to reply. \(\square \)
Next, we demonstrate two forms of modern editor support offered by 1CPLT to improve the first-person choreographic programming experience.
Example 11
Fig. 2 shows that 1CPLT leverages two special features of VS Code:
Inlay hints provide the programmer contextual information about the code, displayed in grey font wherever relevant. In 1CPLT, inlay hints inform the programmer about which process is active by prefixing code fragments with process references, in the style of third-person choreographic programming. For instance, “\(\texttt {self.}\)” on line 4 and “\(\texttt {Cons.}\)” on lines 6, 8–9, and 11, are inlay hints: they are not part of the code fragments but inserted by 1CPLT ’s inlay hint generator. Inlay hints are intended to improve code comprehension.
Code lenses allow the programmer to trigger contextual actions, displayed as clickable text between lines of code (e.g., lines 16–19). In 1CPLT, “Simulate ...” uses the 1CPLT interpreter to run a simulation either of the full distributed system or of one particular process. \(\square \)
Last, we demonstrate 1CPLT implementations with errors.
Example 12
Fig. 2b and Fig. 2c show examples of bugs caught by 1CPLT:
In Fig. 2b, an unexpected message is passed from the consumer to a producer.
In Fig. 2c, a continuation with an unexpected choreographic procedure call is passed from the consumer to a producer.
In both cases, the consumer burdens a producer with input that it cannot handle, which causes that producer to fail. The 1CPLT type checker, which implements the typing rules of the calculus, detects this. \(\square \)
Even when m and n are fixed, most existing choreographic programming languages cannot be used to implement M-out-of-N. This is because these languages have limited support for non-determinism, which is crucial in M-out-of-N. That is, even when m and n are known statically, the order in which the consumer receives from the producers—and how to reply—is known only dynamically, which is problematic. In contrast, the event-driven nature of this paper’s approach supports non-deterministic receives. Another notable exception is the recent work by Plyukhin et al. [43], which offers special support for out-of-order execution.
Chang–Roberts In the remainder of this section, we further demonstrate the expressiveness of 1CPLT (and, in turn, of the new calculus) by considering two classical distributed algorithms. First, we consider a distributed algorithm for leader election. This is the problem of computing a unique leader among the processes in a distributed system. The Chang–Roberts algorithm solves the problem for non-anonymous processes in a directed ring network [11].
Fig. 3:
Chang–Roberts
Example 13
A Chang–Roberts distributed system consists of processes Node1, ..., Noden. Each node has a unique numeric identifier. The nodes elect the node with the greatest identifier among them as the leader. There is only one point-of-view: that of any node.
Fig. 3a shows a 1CPLT implementation of Chang–Roberts. As there is only one point-of-view, there is only one \(\texttt {global}\) block. Each node has four variables: a reference to its neighbour (\(\texttt {neigh}\)), its own identifier (\(\texttt {x}\)), the greatest identifier it has received so far (\(\texttt {y}\)), and a flag to indicate whether or not it is elected (\(\texttt {z}\)).
First, as defined by choreographic procedure \(\texttt {main}\), the identifier of each node is passed to that node’s neighbour (i.e., each node is initially active). Next, as defined by choreographic procedure \(\texttt {forward}\), if the neighbour’s own identifier is less than the incoming identifier, then the neighbour forwards the incoming identifier to the neighbour’s neighbour. And so on. In this way, only the greatest identifier is forwarded by all nodes and makes a full pass along the ring. When a node receives its own identifier, it declares itself the leader. \(\square \)
Next, we demonstrate that the network among the processes can be initialised at run-time, through the process references in their states.
Example 14
Fig. 3a and Fig. 3c show, on lines 15–17, definitions of two alternative sets of initial configurations for three nodes: a clockwise-directed ring and an anticlockwise-directed ring. That is, statically, it is known that each node has a neighbour, but only dynamically, it is known which one. \(\square \)
Even when the number of nodes and the neighbours of all nodes were fixed, but not the identifiers,3 existing choreographic programming languages cannot be used to implement Chang–Roberts. This is because the total number of communications during a run (message complexity) depends on the assignment of identifiers to nodes (key property of Chang–Roberts). For instance, if the identifiers happen to be assigned in ascending order in the direction of the ring, then \(2{\cdot }n-1\) communications are needed. In contrast, if the identifiers happen to be assigned in descending order, then
communications are needed. Existing choreographic programming language require at least \(n^2\) communications.
Echo Next, we consider a distributed algorithm for waves. This is the problem of scattering/gathering information to/from all processes. The Echo algorithm solves the problem for undirected networks of any topology [49].
Fig. 4:
Echo
Example 15
An Echo distributed system consists of processes Node1, ..., Noden. One of the nodes acts as the initiator that triggers the wave. Each node except the initiator goes through the following steps:
1.
Receive a message from any neighbour; it becomes the node’s parent.
2.
Send a message to each non-parent neighbour.
3.
Receive a message back from each non-parent neighbour.
4.
Send a message to the parent.
The initiator skips steps 1 and 4, while it sends/receives a message to/from all neighbours in steps 2 and 3. When step 3 of the initiator ends, it is guaranteed that each node has participated (and has been given the opportunity to scatter/gather information accordingly). Because the initiator and the non-initiators are very similar, we consider there to be only one point-of-view: that of any node. In general, there is some flexibility in determining the granularity at which points-of-view are identified for a given distributed system; this is a design decision.
Fig. 4a shows a 1CPLT implementation of Echo. Each node has five variables: a flag to indicate “initiator-hood” (\(\texttt {init}\)), a constant list of references to all neighbours (\(\texttt {neighs}\)), a list of references to all neighbours from which it has received (\(\texttt {senders}\)), a reference to the parent neighbour (\(\texttt {parent}\)), and a reference to the latest neighbour from which it has received (\(\texttt {sender}\)).
First, as defined by choreographic procedure \(\texttt {main}\), each node checks if it is the initiator (i.e., each node is initially active, but only one of them triggers the wave). Next, as defined by choreographic procedure \(\texttt {roll}\), the initiator sends a message and a continuation to each neighbour (i.e., \(\texttt {parent}\) has \(\texttt {self}\) as dummy initial value, which is not in \(\texttt {neighs}\)). Next, as defined by choreographic procedure \(\texttt {recv}\), each neighbour of the initiator:
updates \(\texttt {senders}\);
if it is the first receive, then it sets its parent and calls \(\texttt {roll}\) to send a message and a continuation to each neighbour (executed asynchronously by them);
if it is the last receive, then it sends a message and a continuation back to its parent. \(\square \)
Example 16
Fig. 4c and Fig. 4d show definitions of two alternative sets of initial configurations for four nodes, each of which has a different topology. The figure highlights that we need to write and statically analyse only one (collection of) global program(s) that can subsequently be initialised for any network. \(\square \)
3 Design: Calculus of First-Person Choreographies
3.1 Organisation of the Section
Having introduced the main ingredients of the new calculus in Sect. 2.1, we present the details in this section. In three separate subsections, we define the syntax of the calculus (Sect. 3.2), its static semantics (Sect. 3.3), and its dynamic semantics (Sect. 3.4). Our presentation in these sections is layered: the first layer concerns “data to communicate”, while on top of that, the second layer concerns “choreographies to communicate data”. A final subsection states our main result (Sect. 3.5): communication deadlock freedom by design. All definitions, as well as the main result, are formalised in Isabelle/HOL; see also the artifact [35].
3.2 Syntax
Data We define the following syntax for data:
Let \(\mathbb {X} = \{\texttt {x}, \texttt {y}, \texttt {z}, \ldots \}\) denote the set of variables, ranged over by x, y, z.
Let \(\mathbb {P}\) denote the set of point-of-view names, ranged over by p, q, r.
Let \(\mathbb {T}\) denote the set of data types, ranged over by T:
We note that many more data types may be available, but this is orthogonal to the contributions of this paper, so they are omitted here.
Let \(\mathbb {V}\) denote the set of values, ranged over by V:
Value \(p\)\(\texttt {[}V_\textrm{Nat}\texttt {]}\)—an “indexed point-of-view name”—defines a process reference. Value \(\texttt {[}V_1,...,V_n\texttt {]}\texttt {<}T\texttt {>}\) defines a list of length n with elements of data type T.
Let \(\mathbb {E}\) denote the set of expressions, ranged over by E:
Let \(\mathbb {X} \rightharpoonup \mathbb {V}\) denote the set of process states (partial functions from variables to values), ranged over by \(\varPhi \).
Choreographies We define the following syntax for choreographies:
Let \(\mathbb {K}\) denote the set of choreographic procedure names, ranged over by k.
Let \(\mathbb {C} = \{Chor\texttt {<}p\texttt {>}\mid p \in \mathbb {P}\}\) denote the set of choreographic types.
Let \(\mathbb {G}\) denote the set of global programs, ranged over by G:
Global program k defines a call of choreographic procedure k. Global program skip defines a no-op. Global program \(x {:=}E\) defines an assignment of (the value of) E, to variable x. Global program \(E_1 {\rightarrowtriangle }E_2.y {\triangleright }G\) defines a continuation-passing communication of (the value of) \(E_1\), to (the value of) \(E_2\)—“from an implicit active process to the explicit reactive process”—into variable y, followed by the asynchronous execution of G. Thus, \(E_1\) is evaluated to the value to communicate, while \(E_2\) is evaluated to (a reference to) the process to communicate with. Global programs \(G_1 {{;}}G_2\),
, and
define sequencing, conditional choice, and conditional iteration. In Exmp. 5, we also used the following syntactic sugar:
Here, \(\texttt {\_iter}_T\) is a variable that contains a list of data type T.
Let \(\mathbb {K} \rightharpoonup \mathbb {G}\) denote the set of choreographic libraries (partial functions from choreographic procedure names to global programs), ranged over by \(\varPsi \).
3.3 Static Semantics
Fig. 5:
Static semantics of data (excerpt)
Data Let \(\mathbb {X} \rightharpoonup \mathbb {T}\) denote the set of all data type environments (partial functions from variables to data types), ranged over by \(\varGamma \). Let
denote the well-typedness of E by T in \(\varGamma \), and \(\varPhi \) by \(\varGamma \). It is the relation induced by the rules in Fig. 5:
Rules [\({\vdash }\)-Var], [\({\vdash }\)-True], and [\({\vdash }\)-Neg] are standard [42].
Rule [\({\vdash }\)-Ref] states that an indexed point-of-view name
(process reference) is well-typed by
. Shortly, this judgment will allow us to make assumptions about the presence/absence of variables and choreographic procedures in the configurations of any process
that has point-of-view p.
Rule [\({\vdash }\)-State] states that a process state is well-typed when it has a well-typed value for each variable in the data type environment.
Fig. 6:
Static semantics of choreographies
Choreographies Let \(\mathbb {K} \rightharpoonup \mathbb {C}\) denote the set of choreographic type environments (partial functions from choreographic procedure names to choreographic types), ranged over by \(\varDelta \). If R is a set of point-of-view names, then let
denote the well-typedness of G by
, and \(\varPsi \) by \(\varDelta \), in families of environments
and
. It is the relation induced by the rules in Fig. 6:
Rule [\({\vdash }\)-Call] states that a choreographic procedure call is well-typed when that procedure exists and is well-typed.
Rule [\({\vdash }\)-NoOp] states that a no-op is well-typed.
Rule [\({\vdash }\)-Asgn] states that an assignment is well-typed from point-of-view p when the variable and the expression are well-typed by the same type in the data type environment of p.
Rule [\({\vdash }\)-Comm] states that a continuation-passing communication is well-typed from point-of-view p (input of the rule, algorithmically) when:
the type of the expression from point-of-view p (first premise), and the type of the variable from point-of-view q (third premise), are the same;
the receiver has point-of-view q (second premise);
the continuation is well-typed from point-of-view q (fourth premise).
This rule is the reason why families of data/choreographic type environments are needed in the judgments instead of individual environments: as we “cascade” along continuation-passing communications, at each next level, different environments are needed than at the previous level.
Rules [\({\vdash }\)-Seq], [\({\vdash }\)-If], and [\({\vdash }\)-While] are straightforward.
Rule [\({\vdash }\)-Lib] states that a choreographic library is well-typed when it has a well-typed global program for each name in the library.
We note that checking well-typedness is decidable and, in fact, linear in the size of the global program (because the typing rules are syntax-directed).
3.4 Dynamic Semantics
Fig. 7:
Dynamic semantics of data (excerpt)
Data Let \(\varPhi \llbracket E\rrbracket \) denote the evaluation of E in \(\varPhi \). It is the smallest function induced by the equations in Fig. 7. We note that the function is only partially defined. For instance, \(\emptyset \llbracket \texttt {x}\rrbracket \) and \(\varPhi \llbracket \texttt {!123}\rrbracket \) are undefined. Undefinedness is potentially problematic: it causes processes to get stuck, which in turn causes communication deadlocks among processes. However, using the static semantics of the previous section, undefinedness at run-time is detected at compile-time.
Choreographies Let \(\mathbb {A}\) denote the set of actions (labels), ranged over by A:
Actions
and
define a send and a receive of global program G from process
to process
. In this paper, G is of the form \(y {:=}V {{;}}G'\), where V and \(G'\) are a message and a continuation. Action \(\uptau \) defines an internal action.
Fig. 8:
Dynamic semantics of choreographies (part 1)
Let \((\varPhi , \varPsi , G) { \mathrel {{\downarrow }}}\) and
denote the termination of configuration \((\varPhi , \varPsi , G)\) and the reduction of source configuration \((\varPhi , \varPsi , G)\) to target configuration \((\varPhi ', \varPsi ', G')\) through action A. They are the relations induced by the rules in Fig. 8:
Rule [\({\downarrow }\)-NoOp] states that a no-op can terminate.
Rule [\({\downarrow }\)-Seq] states that sequencing can terminate when the operands can.
Rule [\({\rightarrow }\)-Call] states that a call can reduce to the body of the corresponding choreographic procedure through an internal action.
Rule [\({\rightarrow }\)-Asgn] states that an assignment can reduce to a no-op through an internal action, while the state in the configuration is updated accordingly.
Rule [\({\rightarrow }\)-Send] states that a continuation-passing communication can reduce to a no-op through a send. The outgoing global program contains the message and the continuation. In this way, continuation-passing is a form of process-driven dynamic projection: the sender at run-time tells the receiver how to behave (from its first-person point-of-view), instead of a choreographic programming tool at compile-time (from its third-person point-of-view).
Rule [\({\rightarrow }\)-Recv states that any global program can reduce through a receive. The first operand of the resulting sequence is the original global program; the second operand is the incoming global program, which contains a message and a continuation. In this way, the incoming global program is explicitly scheduled to be run, but only when all existing work is done. Thus, scheduling is non-preemptive, reminiscent of event-driven programming.
We note that there is a difference between: (1) the “physical receive” that takes the message/continuation off-network (happens when rule [\({\rightarrow }\)-Recv] is applied, and \(G_2\) is appended to \(G_1\)); (2) the “logical receive” that actually processes the message/continuation (happens when the reduction of \(G_1\) is finished, and the reduction of \(G_2\) is started). Because of this decoupling, no explicit receive operations need to be defined in global programs: they happen implicitly, at any time, induced by the dynamic semantics (in practice, the run-time system takes care of this). This is reminiscent of: (1) buffering a message in a local event queue; (2) taking that message out of the event queue in a later iteration of the event loop to process it.
Rules [\({\rightarrow }\)-Seq1] and [\({\rightarrow }\)-Seq2] are standard in the dynamic semantics of imperative languages [1] and process algebra [22], except that receives are excluded. Thus, receives happen only at the top-level and cannot preempt.
Rules [\({\rightarrow }\)-If1], [\({\rightarrow }\)-If2], [\({\rightarrow }\)-While1], and [\({\rightarrow }\)-While2] are standard in the dynamic semantics of imperative languages [1] and process algebra [22].
We note that choreographic procedures enhance expressiveness relative to conditional iteration: not every recursive call can be simulated with while. The difference is that each iteration of while must start at the same process (the active process in the loop’s enclosing scope), while each recursive call may start at a different process (the active process in the call site’s enclosing scope).
Fig. 9:
Dynamic semantics of choreographies (part 2)
If \(\varPi \) is a set of indexed point-of-view names, ranged over by \(\pi \), then let
denote the termination and reduction of families of configurations. That is, each configuration models a process, while the family models the distributed system. Formally, \({\downarrow }\) and \({\rightarrow }\) are the relations induced by the rules in Fig. 9:
Rule [\({\downarrow }\)-Sys] states that a family can terminate when each of its configurations can terminate. This rule is standard in the dynamic semantics of parallel composition in process algebra [22].
Rule [\({\rightarrow }\)-Sys1] states that a family can reduce when one of its configurations can reduce through an internal action. This rule models independent evolution of processes in the absence of communication dependencies.
Rule [\({\rightarrow }\)-Sys2] states that a family can reduce when one of its configurations can reduce through a send, while another configuration can reduce through a corresponding receive. This rule models communication between processes. We note that the send and the physical receive are synchronous (as usual in choreographic programming), but the logical receive is asynchronous.
Rule [\({\rightarrow }\)-Sys3] states that a family can reduce when one of its configurations can reduce through a self-communication (first a send, next the receive, by one process). This allows a process to schedule work for itself for a later time. We note that the (self-)send and the physical (self-)receive are, like in rule [\({\rightarrow }\)-Sys2], effectively synchronous (i.e., the two reductions in the premise result in a single reduction in the conclusion), but they need to be ordered.
3.5 Main Result: Communication Deadlock Freedom by Design
Soundness The following theorem states our main result. To formulate it, let
denote an initial family of configurations, where:
\(\varPi \) denotes a set of indexed point-of-view names (process references);
\(\varPhi _{p\texttt {[}i\texttt {]}}\) denotes an initial state for each \(p\texttt {[}i\texttt {]} \in \varPi \);
\(\varPsi _p\) and \(G_p\) denote a choreographic library and an initial global program for each point-of-view \(p \in \{p\mid p\texttt {[}i\texttt {]} \in \varPi \}\) (i.e., processes of the same point-of-view, have the same choreographic library and initial global program).
Now, the initial family of configurations either reduces finitely many times and terminates, or it reduces infinitely many times (i.e., it never gets stuck, so we enjoy communication deadlock freedom), when the following conditions are met:
1.
Each choreographic library \(\varPsi _p\) is well-typed. This is a static check.
2.
Each initial global program \(G_p\) is well-typed. This is a static check.
3.
Each initial state \(\varPhi _{p\texttt {[}i\texttt {]}}\) is well-typed. This is a lightweight dynamic check, part of initialisation (input validation).
4.
The family of configurations is closed: if a process is referenced in a configuration, then it must have a configuration in the family. This is a lightweight dynamic check, part of initialisation (network validation). In the theorem below, let
denote the set of process references that occur in any configuration of the family.
Intuitively, the static checks ensure that, if the initial configurations are proper, then a process never passes a continuation to another process that cannot run to completion: well-typedness guarantees that expected variables of expected types, as well as expected choreographic procedures, actually exist. Complementarily, the lightweight dynamic checks ensure that the initial configurations are proper.
Dynamically:\({\mathrel {{\vdash }}\varPhi _{p\texttt {[}i\texttt {]}} \mathrel {{:}}\varGamma _p}\) for each \(p\texttt {[}i\texttt {]} \in \varPi \)
4.
Dynamically:
If
, then either \(C' { \mathrel {{\downarrow }}}\), or
, for some \(C''\).
We formalised all the definitions of this section in Isabelle/HOL and mechanised the proof of this theorem and all auxiliary lemmas. The following outline summarises the main steps and structure. See the Isabelle/HOL code for details. Extending this result to livelock is left for future work.
Proof
(outline). The proof of Thm. 1 is split into two parts: progress and preservation. Progress states that if the four assumption hold for a family, then that family can either terminate or reduce. Preservation states that if the four assumptions hold for a source family, and if that source family reduces to a target family, then the four assumptions also hold for the target family. Thus, if the four assumptions hold for the initial family, then by applying progress and preservation inductively, we obtain the main result in Thm. 1. The proofs of progress and preservation use several forms of induction (on the structure of the terms; on the derivation of the judgments), nested inside each other through lemmas. \(\square \)
Expressiveness Expressiveness of choreographic programming calculi can be measured along (at least) two relevant dimensions:
Computability: Which classes of functional behaviour can be expressed?
Message complexity: How many messages are needed and in which patterns?
Regarding computability, it has been shown that a simple core calculus of choreographies is Turing-complete (e.g., [16]). That calculus can be trivially embedded in ours. Regarding message complexity, none of the existing choreographic programming languages we know of supports all realisable regular message patterns (i.e., message patterns that can be specified with a regular expression over synchronous communications; e.g., M-out-of-N for any concrete m and n). In contrast, in addition to supporting parametricity, we conjecture that our approach also supports all realisable regular message patterns.
4 Implementation: 1CPLT
4.1 From Theory to Practice
The calculus presented in the previous section is expressive, but it(s notation) is unwieldy to use directly to implement distributed systems. With the development of 1CPLT, demonstrated in Sect. 2.2, we set out to explore how to possibly transfer the calculus from theory to practice, in a way that intuitively and concisely hides its complexities; see also the artifact [35].
Fig. 10:
Correspondence between 1CPLT and the calculus
Fig. 10 demonstrates the correspondence between the concrete syntax of 1CPLT and the ingredients of the calculus. Inspired by classes in object-oriented programming, the idea is to combine, for each point-of-view, the declarations of variables and the definitions of choreographic procedures in the same “unit” (\(\texttt {global}\) block), using a special choreographic procedure (\(\texttt {main}\)) to define the initial global program. This is all the information needed for static type checking. For simulation purposes, the creation of configurations is expressed separately (\(\texttt {process}\) statements) by defining the initial values of variables for each process.
4.2 Technical Details
General 1CPLT is implemented in Rascal [38], a meta-programming environment geared towards implementing programming languages. Among other features, the Rascal language has core support to write context-free grammars (for defining concrete syntax), algebraic data types (for defining abstract syntax), and advanced pattern matching on grammar rules and ADT constructors. Together with standard programming abstractions, these features aim to simplify the implementation of parsers, type checkers, interpreters, and code generators.
Parsing The parser consumes a .1cp file as input and produces as output:
for each point-of-view: abstract syntax trees for a data type environment, a choreographic type environment, and a choreographic library (\(\texttt {global}\) block);
for each process: abstract syntax trees for an initial state (\(\texttt {process}\) stmnt).
The parser proceeds in two steps:
1.
First, it transforms the input file into a concrete syntax tree using the 1CPLT grammar. For instance, the following production rules in the 1CPLT grammar define the concrete syntax of assignments and communications (simplified to save space; see the artifact for the full version):
2.
Next, the parser transforms the concrete syntax tree into an abstract version using algebraic data types. For instance, the following constructors define the abstract syntax of assignments and continuation-passing communications (simplified to save space; see the artifact for the full version):
We note that each constructor has an optional argument
(declared on line 1), which associates each value of a constructor with a particular location in the input file (
is a core data type in Rascal for locations). This is essential for the type checker to generate properly located error messages.
Type checking The type checker consumes abstract syntax trees as input and produces a list of error messages as output; the list is empty if, and only if, the input is well-typed. Essentially, the type checker implements the typing rules in the static semantics of the calculus. For instance, the following code type-checks
constructors (simplified to save space; see the artifact for the full version):
For reference and comparison, typing rule [\({\vdash }\)-Asgn] ( Fig. 6) is reproduced below.
Lines 1–3 define a general ADT for choreographic type environments. Line 5 declares the arguments to type-check
constructors, each of which corresponds with a variable in the conclusion of the typing rule:
with p,
with
and
,
with x, and
with e;
is just a shorthand for
.
Line 6 checks if
exists in the data type environment of
; if not, an error message is generated. The second argument of constructor
is the location in the input file where the error message should be displayed. Line 7 recursively calls function
to collect all error messages that result from type-checking data expression
(E) against data type
(
) in data environment
(
). This is expressed using Rascal’s notation for list comprehension:
constructs a list such that each
satisfies the conjunction of
, ... Operator
splices a list into another list.
The functions to type-check the other constructors are defined similarly.
Interpretation The interpreter consumes abstract syntax trees as input (initial states and choreographic libraries) and produces a simulation as output. Essentially, the interpreter implements the reduction rules of the dynamic semantics of the calculus. For instance, the following code reduces
constructors (simplified to save space; see the artifact for the full version):
Line 1 declares that function
consumes a source configuration as input (i.e., the arguments are directly destructured using pattern matching). Line 2 defines that function
produces a target configuration as output by updating the value of
in
, in accordance with rule [\({\rightarrow }\)-Asgn] (Fig. 8).
The functions to reduce the other constructors are defined similarly.
Before each simulation, it is also checked whether or not each initial process state is well-typed, as well as closedness (points 3–4 of Thm. 1).
Code generation (outlook) We aim to extend 1CPLT with a code generator to be able to deploy 1CPLT implementations on real networks.
The most interesting aspect of such a code generator is that it should “compile away” continuation-passing: while continuation-passing is instrumental in our approach as a programming abstraction, physically passing around code-to-be-executed tends to be problematic in terms of security, privacy, and performance. Instead, we envisage a static transformation in which: (a) for each continuation, a choreographic procedure is introduced with a random label; (b) instead of passing the continuation, only the random label is passed.
5 Conclusion
5.1 Related Work
Process-parametric MPST Close to the work in this paper, in terms of starting point and aim, are several extensions of multiparty session typing (MPST) [30] to support process-parametricity. First, Deniélou et al. [51] designed a dependently typed calculus to support process-parametricity, but the resulting typing relation is undecidable and was never implemented. Next, taking the opposite approach, Ng and Yoshida [41] implemented an extension of the Scribble tools for MPST [31, 32], called Pabble, to support process-parametricity, but it was never formalised and does not provide type-soundness guarantees. Last, Castro et al. [8] presented a calculus (all static analysis decidable) and a tool (formalised by the calculus) to support process-parametricity, but the expressiveness is limited (many distributed systems remain unsupported, including those in Sect. 2.2), while the static analysis algorithm is of exponential complexity. Thus, there is tension between decidability, soundness, and expressiveness.4 However, by developing process-driven dynamic projection through continuation-passing communications (which diverges considerably from classical static MPST), our approach in this paper manages to combine these properties.
Dynamic projection Shen et al. [50] developed a choreographic programming library in Haskell, called HasChor, that uses dynamic projection to be able to build their library on top of the freer monad [37]. In this way, dynamic projection is primarily an implementation mechanism in HasChor. HasChor does not support process-parametricity, and it has not been formalised yet.
In MPST, dynamic projection has been studied by Hamers et al. [27, 34] in the form of a run-time verification framework based on global types, called Discourje. Discourje also supports process-parametricity, but it imposes run-time overhead, as all analysis happens dynamically. In contrast, the analysis in this paper happens almost completely statically.
Behavioural-typed actors/mailboxes The event-driven nature of our approach to choreographic programming is reminiscent of programming methods based on event loops/queues and asynchronous execution of event handlers. Closest in this area is the work on behavioural typing of actors and mailboxes by Fowler et al. [23, 24], De’Liguoro and Padovani [21], and Scalas et al. [48].
More fundamentally, we speculate that a deeper connection may be uncovered between actors/mailboxes and the approach in this paper. Our initial observation is that a mailbox-based runtime for 1CPLT (in combination with code generation; end of Sect. 4.2) would align perfectly with the dynamic semantics of our calculus—much more so than a (point-to-point) channel-based runtime would. This leads us to hypothesise that mailbox-based actors are to first-person choreographies what (point-to-point) channel-based processes are to third-person choreographies. That is, the following table would be completed:
Proof mechanisation In recent years, mechanisation of choreographic programming theory has received considerable attention, including the work of Cruz-Felipe et al. [15, 17‐20], Hirsch and Garg [29], and Pahjola et al. [44]. Similar initiatives for behavioural typing include the work of Castro et al. [9, 10], Hinrichson et al. [28], and Jacobs et al. [33]. Thus, the mechanisation of our proofs in Isabelle/HOL follows this trend in our community.
5.2 Future Work
On the theoretical side, we identify two directions for future work. First, we are keen to investigate the integration of dependent typing into our approach, to support arbitrary expressions as indices of point-of-view names (process references) instead of only values. Second, it will be interesting to develop dedicated testing and verification techniques for first-person choreographies, following recent work for third-person choreographies (e.g., [12, 13, 36]).
Another interesting question is whether a first-person approach could also be applied in MPST. Most MPST theories have a tight correspondence between the syntax of global/local types and the syntax of processes. If this correspondence is kept tight (i.e., a first-person approach is used both in global/local types and in processes), then we expect it to be possible—but still non-trivial—to develop typing rules accordingly and prove soundness. These typing rules would not rely on projection, but verify processes directly against global types. An alternative (presumably more challenging, but arguably more usable) would be to develop an MPST theory in which the correspondence is loosened: combining a first-person approach in global types with a more conventional style for processes.
On the practical side, in combination with an extension of 1CPLT with a code generator (Sect. 4.2), we are eager to conduct a case study on Paxos. This is a popular (family of) distributed algorithm(s) for consensus. Paxos has a number of properties (particularly related to non-determinism) that are fundamentally hard to support with third-person choreographies. We believe first-person choreographies can address these issues.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
If the identifiers were fixed, the process with the greatest identifier would be known already at compile-time, so there would be no need to elect a leader at run-time.
While we are not aware of any formal results about inherent limitations of static projection, we strongly suspect such limitations exist (because, fundamentally, fewer information is available at compile-time than at run-time).
), Buyer2 (
), and Seller (
). As introduced by Honda et al. [30]: “Buyer1 and Buyer2 wish to buy an expensive book from Seller by combining their money. Buyer1 sends the title of the book to Seller, Seller sends to both Buyer1 and Buyer2 its quote, Buyer1 tells Buyer2 how much she can pay, and Buyer2 either accepts the quote or rejects the quote by notifying Seller.”
and \(G_1 {{;}}G_2\) define conditional choice, at the process named p, and sequencing. We write \(p.E {{\rightarrowtriangle }}[q_1 \ldots , q_n].y\) as a shorthand for \(p.E {{\rightarrowtriangle }}q_1.y {{;}}\ldots {{;}}p.E {{\rightarrowtriangle }}q_n.y\). \(\square \)
and \(p \text {?}y\) define a send to the process named q and a receive from the process named p. \(\square \)
), Buyer2 (
), ..., Buyern (
), and Seller (
). It generalises the TwoBuyer distributed system from two buyers to any number. Each buyer contributes a fraction of the quote; Buyern decides to accept/reject. The following global programs define the behaviour of all processes, collectively, for \(n \in \{3, 4\}\) (excerpts): 
means “a communication from Alice to Bob” from the programmer’s point-of-view. At heart, the key novelty of this paper is to shift the narrative perspective in global programs to the first-person points-of-view of the processes. For instance,
means “a communication from me to Bob” from Alice’s point-of-view. This shift in perspective is instrumental for us to support process-parametricity.
and
define the absence of initial behaviour. \(\square \)
,
,
, and \(G_{\texttt {contrib}}^\text {AnyBuyer}\) (all defined in previous examples) are well-typed; we do not need to know n to make this judgment. Thus, any properly initialised run—for any n—is free of communication deadlocks.
: 
in
): 
communications are needed. Existing choreographic programming language require at least \(n^2\) communications.
, and
define sequencing, conditional choice, and conditional iteration. In Exmp. 5, we also used the following syntactic sugar: 
(process reference) is well-typed by
. Shortly, this judgment will allow us to make assumptions about the presence/absence of variables and choreographic procedures in the configurations of any process
that has point-of-view p.
, and \(\varPsi \) by \(\varDelta \), in families of environments
and
. It is the relation induced by the rules in Fig. 6:
and
define a send and a receive of global program G from process
to process
. In this paper, G is of the form \(y {:=}V {{;}}G'\), where V and \(G'\) are a message and a continuation. Action \(\uptau \) defines an internal action.
denote the termination of configuration \((\varPhi , \varPsi , G)\) and the reduction of source configuration \((\varPhi , \varPsi , G)\) to target configuration \((\varPhi ', \varPsi ', G')\) through action A. They are the relations induced by the rules in Fig. 8:
denote an initial family of configurations, where:
denote the set of process references that occur in any configuration of the family.
for each \(p \in R\)
for each \(p \in R\)
, then either \(C' { \mathrel {{\downarrow }}}\), or
, for some \(C''\).
constructors (simplified to save space; see the artifact for the full version): 
(declared on line 1), which associates each value of a constructor with a particular location in the input file (
is a core data type in Rascal for locations). This is essential for the type checker to generate properly located error messages.
constructors, each of which corresponds with a variable in the conclusion of the typing rule:
with p,
with
and
,
with x, and
with e;
is just a shorthand for
.
exists in the data type environment of
; if not, an error message is generated. The second argument of constructor
is the location in the input file where the error message should be displayed. Line 7 recursively calls function
to collect all error messages that result from type-checking data expression
(E) against data type
(
) in data environment
(
). This is expressed using Rascal’s notation for list comprehension:
constructs a list such that each
satisfies the conjunction of
, ... Operator
splices a list into another list.
constructors (simplified to save space; see the artifact for the full version): 
consumes a source configuration as input (i.e., the arguments are directly destructured using pattern matching). Line 2 defines that function
produces a target configuration as output by updating the value of
in
, in accordance with rule [\({\rightarrow }\)-Asgn] (Fig. 8).
