Das Kapitel geht den Herausforderungen bei der Entwicklung korrekter verteilter Kommunikationsprotokolle nach und konzentriert sich auf asynchrone Nachrichten, die durch zuverlässige FIFO-Kanäle laufen. Es führt einen Top-Down-Ansatz ein, der zunächst globales Verhalten spezifiziert, gefolgt von der Synthese lokaler Spezifikationen, um korrektes Verhalten zu gewährleisten. In diesem Kapitel werden Protocol State Machines (PSMs) als allgemeiner Formalismus für globale Protokollspezifikationen dargestellt, die aussagekräftiger sind als traditionelle globale Typen und High-Level Message Sequence Charts (HMSCs). Communicating State Machines (CSM) werden für lokale Protokollspezifikationen verwendet und stellen eine kanonische Repräsentation für dezentrale asynchrone Kommunikation dar. Das Kapitel beleuchtet die Beziehung zwischen globalen Typen, lokalen Typen und Programmen und betont die Notwendigkeit von Projektion und Typenprüfung, um die Protokollkorrektheit sicherzustellen. Es führt das AMP-Framework ein, das Ausdruckskraft, Entkopplung und Robustheit im Top-Down-Protokolldesign erreicht. Das Kapitel behandelt die Expressivität von AMP, seine Handhabung von Projektion und Typenprüfung und seine Robustheit bei der Identifizierung einer großen Klasse von PSMs, für die Projektion entscheidbar ist. Außerdem wird die Abwärtskompatibilität von AMP mit bestehenden Mehrparteien-Sitzungstypen (MST) untersucht, was es zu einem vielseitigen Backend für Top-Down-Protokolldesigntools macht. Das Kapitel schließt mit einer detaillierten technischen Entwicklung des AMP-Rahmenwerks, einschließlich der Definition von PSMs, CSMs und des Typsystems zur Sicherstellung der Protokollkorrektheit.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We propose the Automata-based Multiparty Protocols framework (AMP) for top-down protocol development. The framework features a new very general formalism for global protocol specifications called Protocol State Machines (PSMs), Communicating State Machines (CSMs) as specifications for local participants, and a type system to check a \(\pi \)-calculus with session interleaving and delegation against the CSM specification. Moreover, we define a large class of PSMs, called “tame”, for which we provide a sound and complete PSPACE projection operation that computes a CSM describing the same protocol as a given PSM if one exists. We propose these components as a backwards-compatible new backend for frameworks in the style of Multiparty Session Types. In comparison to the latter, AMP offers a considerable improvement in expressivity, decoupling of the various components (e.g. projection and typing), and robustness (thanks to the complete projection).
1 Introduction
Designing correct distributed communication protocols is an important and hard problem. Consider a finite set of protocol participants (i.e. independent processes) whose only means of interaction between each other is asynchronous message passing through reliable FIFO channels. The goal is to program each participant so that some global emergent behaviour is achieved, e.g. a leader is elected. Unfortunately, even when each participant is finite-state, the presence of unbounded delays (i.e. unbounded communication channels) makes any non-trivial property of the emergent global behaviour undecidable [10].
The top-down protocol design approach proposes to work around this issue by a reversal in the methodology: instead of first programming the participants and then checking that their global behaviour is what we desired it to be, we first specify the desired global behaviour and then synthesize each participant’s local specification so that local behaviour gives rise to the correct global behaviour by construction. Each participant’s concrete implementation is then checked against its local specification, which (a) can be achieved by static means like type systems, and (b) makes the verification of the implementation local and modular.
Anzeige
Multiparty Session Types (MSTs) [37] is one of the most prominent and extensively studied formalisms supporting this top-down design methodology. The key components of the framework, depicted in Fig. 1, are: (1) Global Types: a dedicated language to specify correct global behaviour; (2) Local Types: a dedicated language to specify each participant’s actions in the protocol; (3) Programs: a programming language (typically a \(\pi \)-calculus) to express concrete implementations of each participant of the protocol.
Imagine, as a simple example, we want to specify a centralised leader election protocol, where an arbiter
selects a leader among
and
and the selected participant communicates the win to the other. A possible global type representing the protocol is
where
says that
sends \(\textsf{sel}\) and
receives it and \(+\) denotes branching. The local type of
would then be
where
means “
receives message \(\textsf{sel}\) from
” and
means “
sends message \(\textsf{win}\) to
’. Thus,
is supposed to listen for a message from
or from
; in the former case it would then communicate the win to
, in the latter, just concede. A program implementation may consist of a process for each participant; the process for the arbiter
may implement any specific policy for selecting the leader (e.g. always choose
), as long as the communications follow the protocol.
Fig. 1.
The components of top-down frameworks.
The relationship between the three representations of the protocol, i.e. global types, local types, and programs, is delicate. First, the global type and the local types should give rise to the same behaviour; however it is not always possible to capture the behaviour of a global type with local types. Suppose, for instance, that we modified the leader election protocol G to
While, from a global perspective, it is possible to insist on the losing participant informing the winner that they lost, locally, the losing participant has no way to determine whether they won or not. Therefore \(G'\) is not realisable by local processes: we say it is not projectable. Second, local types are a more abstract representation of the system than programs, but we still want to show that, when implementation details are omitted, a program only performs communications that adhere to the local specification.
In MSTs, the relationship between the three layers of the framework are enforced through two procedures: (i) Projection, which (when possible) extracts, from a global type G, some local types that are guaranteed to behave as described by G; and (ii) Type Checking, which checks that the program implementation of each participant adheres to the behaviour specified in its local type.
Anzeige
In a perfect world, a framework for top-down protocol design should be:
1.
Expressive: It should support as many protocols as possible.
2.
Decoupled: Its components (global/local specifications, programs, projection, type checking) should depend on each other as little as possible, and be specified independently of their algorithmic implementation, to allow for reuse and modularity.
3.
Robust: It should only reject a global specification if there is a genuine issue with it (i.e. no false positives).
Unfortunately, the MST frameworks in the literature leave something to be desired against this ideal picture. They all suffer from:
Expressivity Limitations: Many legitimate protocols are rejected either because the global specification syntax is too restricted, or because the projection algorithm cannot handle them. For example, every MST framework we are aware of can only handle global types with directed choice, i.e. where every branching point involves exactly one sender and one receiver. This immediately rules out our example leader election protocol G because the branches involve different receivers.
Decoupling Limitations: In MSTs, the syntax of global types directly influences the definition of the projection algorithm and the syntax of the local types, which in turn influence the type system design. Typically, changing one of the framework’s components requires adapting (and reproving correctness of) all the others. Furthermore, many MST frameworks solely give the intended relation between global and local types through the projection algorithm and do not give a declarative definition.
Robustness Limitations: The heuristic nature of the projection algorithms makes it very hard to predict if a global type will be handled or not by an MST framework, even in the case where the behaviour specified by the global type is unproblematic.
In this paper, we propose a new foundation for top-down protocol design machinery, dubbed AMP (Automata-based Multiparty Protocols), that achieves the expressivity, decoupling and robustness goals.
Expressivity of AMP. Figure 1 shows the components of AMP. To achieve expressivity, we propose a new general formalism for (finite-control) global protocol specifications, which we call Protocol State Machines (PSMs). The formalism is based on automata which are given semantics in terms of (finite and infinite) sets of words, over an alphabet of send (
) and receive (
) actions. PSMs remove many of the restrictions of global types, while retaining their character: they specify the expected behaviour from a global perspective, and satisfy some basic correctness properties by construction (e.g. every send is eventually received, no type mismatches, etc). Owing to their generality, PSMs can represent any global type, but can go well beyond them: they also strictly subsume High-Level Message Sequence Charts (HMSCs). For maximizing expressivity at the local level, we adopt Communicating State Machines (CSMs) as the formalism for local protocol specifications. They are a canonical representation for decentralised asynchronous communication and as such do not impose constraints over what can be represented. Finally, to maximise expressivity at the program level, we consider a \(\pi \)-calculus with session interleaving and delegation.
Decoupling of AMP. In AMP, decoupling is achieved through its handling of projection and type checking. For projection, the framework merely specifies the semantic requirements that a correct projection algorithm needs to satisfy: essentially that it produces a deadlock-free CSM which represents the same language as the input PSM. This limits the impact of projection on global and local specifications, and leaves open any algorithmic/manual strategy to achieve the projection goal. (We discuss how AMP proposes to actually implement projection in the discussion of robustness). For example, scenarios in which the user provides both the PSM and the CSM and a proof that they represent the same language and the CSM satisfies desirable properties (like deadlock freedom) or where an algorithm infers a PSM from a CSM, are both compatible with our framework thanks to this declarative approach to projection. This treatment is in line with some MST works where the fundamental property of projection is expressed in terms of some behavioural equivalence between local and global types. For type checking, decoupling is achieved by defining the type system by depending exclusively on programs and CSMs. The standard guarantees of subject reduction, communication safety and session fidelity are proven by appealing to properties of CSMs. This demonstrates how effective CSMs are in providing a clean decoupled interface between projection and type checking.
Robustness of AMP. Finally, we demonstrate how robustness can be achieved in AMP, by identifying a large class of PSMs, called Tame PSMs, for which we provide a decidable, sound and complete projection operation. Tame PSMs extend the reach of sound and complete projection beyond global types and can handle a large class of HMSCs as well as protocols that cannot be expressed as either global types nor HMSCs. The main constraint that makes a PSM tame is what we call sender-driven choice: that at any branching point, the sender in all the branches is the same participant and takes distinct actions in the branches. Our projection algorithm builds on a recently proposed complete projection for sender-driven global types [48]. Thanks to a surprising reduction, we manage to extend the algorithm to tame PSMs while keeping the complexity in PSPACE. Due to the fact that our projection operation is complete, only protocols that do not admit any valid projection will be rejected: those are protocols which simply cannot be implemented by local processes. We also show that our class is in a sense “maximally robust”: lifting the sender-driven restriction makes projection undecidable, even for global types. AMP is also robust in the sense that one can select the desired guarantees of the type system and check whether they can be enforced by checking (syntactic) properties of the global protocol, pinpointing exactly which guarantee is provided by a PSM. Finally, we show that the framework is backwards-compatible with MSTs: not only can we encode global types into PSMs and project them, we also pinpoint the (simple) conditions under which our projection yields CSMs which are equivalent to local types.
Contributions. In summary:
We propose PSMs as an expressive general formalism for (finite-control) global protocol specifications.
We propose CSMs as a canonical model for local protocol specifications and specify their desired relationship with PSMs declaratively.
We define the first session type system based on CSMs, pinpointing exactly the properties of the CSM that are needed to provide each of the desired guarantees; these properties can be enforced by construction by ensuring the PSMs conform to some simple checks.
We define Tame PSMs (encompassing all directed and sender-driven global types) and give a sound and complete projection algorithm for them.
We show that sender-driven choice is a necessary restriction even for global types: projection is undecidable otherwise.
We characterise which class of PSMs corresponds to global types, and which CSMs correspond to local types, giving us full backward-compatibility with standard MST theory.
We think of AMP as a backend for top-down protocol design tools with the following workflow. Any specific tool, e.g. Scribble [71], provides a dedicated syntax for types and processes. Then, a global specification is compiled to a PSM (where the compiler guarantees its tameness, which would be trivial for global types) and invokes the projection of AMP, producing a CSM. This could be re-translated for user consumption, but also be used to drive typing using AMP. Failure of projection can be directly translated by the frontend to an explanation of why the protocol is flawed and must be repaired. Given the generality of PSMs, it should also be easier to experiment with extensions of the frontend language.
All proofs, omitted details, and additional examples can be found in [62].
2 Motivation and Key Ideas
In this section, we give an informal overview of the key ideas behind AMP before proceeding with the formal development from Section 3.
2.1 Global Specifications via Protocol State Machines
Our first goal is to define an expressive formalism for specifying global protocols, that is also constrained enough to make it tractable for top-down protocol development. One of the most accomplished such formalisms, used in MSTs, is global types. Figure 2 shows an example of a global type, represented in Figure 3 as an HMSC.
Fig. 2.
Example global type.
Fig. 3.
A protocol as an HMSC.
The term
indicates the transmission of message \(m_1\) from
to
. The symbol \(\textbf{0}\) denotes termination of the protocol. Recursion can be specified by binding a recursion variable X with \(\mu {X}\) and using X subsequently to jump back to where X was bound. Branching is denoted by \(+\). In the example,
can pick between three branches by sending different messages to
. Subsequently,
sends messages to
in all branches: 1 in the top and middle branch and 3 in the bottom branch. Participant
is supposed to send messages \(v_1\) or \(v_2\) in the top and middle branch while it receives from
in the bottom branch, which also recurses using X.
What makes these formalisms tractable? Their first key characteristic is that, as a specification tool, they allow the user to (a) adopt a global point of view, describing what coordination between all the participants is induced by the protocol; (b) express this coordination without enumerating all possible interleavings of the send and receive events that can happen due to the asynchronous nature of communication, e.g.
indicates the send of the message immediately followed by its receipt, although in any asynchronous implementation, the receipt might happen at a much later point, after other independent events took place. In Fig. 2,
may lag behind arbitrarily while
and
keep sending messages. The second key characteristic of global types and HMSCs is that they are finite-control: their control structure can be described using a finite graph. This makes it possible to algorithmically manipulate them, e.g. for verifying they satisfy some desirable properties, or for extracting local protocol specifications.
Our aim is to distil these two characterising features and remove any other restriction that is not necessary, to obtain a more expressive global specification formalism. To do this, we take a language-theoretic view of protocols, where a protocol is seen as the set of sequences of send and receive events that are considered compliant with it. More precisely, a send event
records that
sent the message \(m\) to
; a receive event
records that
received message \(m\) from
. A protocol specification is the language of desired finite or infinite words of events. For the purpose of this section, we will focus on finite words, but the technical development considers both finite and infinite words.
Not all languages over these events are meaningful in the context of protocols. First, the sequences of events might not be feasible when using FIFO channels (e.g.
is not FIFO); we write \(\textsf{FIFO} \) for the language of all words that satisfy FIFO order. Second, if
is accepted by a protocol, it ought to also accept
as this kind of reorderings are induced by the scheduling of participants and network delays which are out of the control of participants. We write \(\mathcal {C}(L)\) for the closure of the language L under such reorderings. Thus a language \(L \subseteq \textsf{FIFO} \) represents the global interaction patterns of the protocols; moreover L can specify only some of these interactions and get all the ones that should also be possible under the asynchronous semantics by declaring the full set of acceptable words to be \(\mathcal {C}(L)\).
Now, to obtain a finite-control formalism, we propose to express such a “core” language L for the protocol \(\mathcal {C}(L)\) using a finite state machine M with \(\mathcal {L}(M)=L\). Since \(\textsf{FIFO} \) is not regular, the only feasible way of ensuring \( \mathcal {L}(M) \subseteq \textsf{FIFO} \) is by requiring M to keep track of which sent messages are still pending, which a finite-state machine can only do up to some maximum capacity for the send buffers. We thus arrive at the requirement that \(\mathcal {L}(M) \subseteq \textsf{FIFO} _B\), where \( \textsf{FIFO} _B \) is the set of words respecting FIFO but where the number of pending sends never exceed \(B\in \mathbb {N}\) at any point in time. Note that \(\textsf{FIFO} _B\) is regular.
Building on these observations, we define a Protocol State Machine (PSM) to be a finite state machine M recognising words of send and receive events, with \(\mathcal {L}(M) \subseteq \textsf{FIFO} _B\) for some \(B\in \mathbb {N}\). Fig. 4 shows the protocol of Fig. 2 as a PSM. Interpreted as a mere automaton M, it recognises a language \(\mathcal {L}(M)\) of words with at most one pending send at all time. (We call M
because the total number of messages in flight is at most 1; if we allowed 1 message per channel, it would be called a \(1\)-PSM.) As a PSM, however, M denotes the language \( \mathcal {C}(\mathcal {L}(M)) \), which admits words with unbounded channel behaviours and is not even regular in general. For instance, \( \mathcal {C}(\mathcal {L}(M)) \) includes words starting with
where
is running at a lower rate than the other participants, and leaves n pending sends from
and from
before it consumes them.
PSMs achieve a substantial gain in expressivity while retaining the key characteristics of global types. In terms of expressivity, every global type can be encoded as a
; furthermore PSMs can be used to encode HMSCs, which strictly subsume global types because the latter cannot specify simultaneous message exchanges between a pair of participants [63]. PSMs can even represent protocols that are outside the reach of HMSCs. Consider, for example, the PSM in Fig. 5. In that protocol,
commits to some integer (abstracted as the label \(\textsf{int}\)) at the beginning by sending it to
and sends a \(\textsf{go}\) signal to
. Note that here we use the paired send and receive notation
to emit the two events in sequence. Then
and
engage in some negotiation of arbitrary length until
decides to exit the loop, at which point
is finally allowed to receive the message sent by
. No HMSC can represent such protocol: the matching events
and
are separated by an arbitrary number of events (with no opportunity for reordering up to \(\mathcal {C}(\hbox {-})\)); since matching events in HMSCs need to belong to the same basic block, such block would also need to contain the arbitrarily many events in between, which is impossible.
Fig. 5.
A protocol not expressible as an HMSC. Transitions labelled with
should be interpreted as emitting the sequence
.
Of course, this level of generality would be pointless if we were not able to provide for it in the other components of top-down protocol design. We start by studying the first crucial component: projection.
2.2 From Global to Local Specifications: Projection
When considering projection, our first concern is the goal of decoupling: we want to define a general interface for projection, such that both different algorithmic implementations of projection can be used without altering the design of the rest of the framework; and such that typing is not dependent on global specifications (nor projection details).
In AMP, the key to decoupling is in choosing Communicating State Machines (CSMs) as the formalism for local specifications. A CSM
associates a finite state automaton
to each participant
, where transitions can either send or receive on the channels of
; the semantics of
is defined on configurations that include the local states for each participant and an (unbounded) FIFO buffer for each channel. They induce a FIFO language
over send/receive events, by considering as final the configurations where all the participants are in final local states and all the buffers are empty. CSMs thus represent a canonical general model of finite-control asynchronous protocol implementations.
Fig. 6.
Example CSM.
Per se, this is not a particularly original choice: MST’s local types have been linked to CSMs of a certain shape before [23, 60], and HMSC-based work used them as local specifications. What AMP demonstrates is that it is possible to build the entire top-down methodology around CSMs (with fewer restrictions), including a session type system, gaining both in expressivity and in decoupling.
Having fixed our model for local behaviour, we can ask when it defines behaviour consistent with a global specification. We say a CSM
is a projection of a PSM M if
is deadlock-free and
. We focus on the (projection) synthesis problem, producing a CSM as result. The corresponding decision problem is the projectability problem, which simply asks if there exists such a CSM. Notably, projectability can have lower complexity.
Even for simple protocols, projection can be tricky. Take the example of Fig. 2:
can never distinguish between the top two branches, as its only observations would be to have received 1 from
. The instance of the protocol with \(m_1 \ne m_2\) and \(v_1 \ne v_2\) would thus not be projectable. If \(m_2 = m_3\) then
would not be able to send the appropriate message to
. Therefore, the only projectable instances with no redundant branches are the ones where \(m_1\), \(m_2\), and \(m_3\) are pair-wise distinct and \(v_1 = v_2\). Figure 6 shows a candidate projection of the PSM in Fig. 2. If \(m_2 = m_3\) or \(v_1 \ne v_2\), the PSM is not projectable, and in fact the CSM can reach a deadlock.
Given CSMs are Turing-complete models, it is unsurprising that checking if a given CSM is a projection of a given PSM is undecidable. The key advantage of the top-down approach boils down to the fact that it is nevertheless often possible to efficiently compute a valid projection from a global specification. This is precisely the goal of the projection operation. A projection operation \((\hbox {-}){\upharpoonright }\) is a function taking a PSMs as input and returning either \(\bot \) or a CSM; it is a sound projection if for all PSM M, if
then
is a projection of M; it is a complete projection if for all projectable M, \(M{\upharpoonright }\ne \bot \).
The MST literature proposed a number of sound but incomplete projection algorithms for global types. Incompleteness makes MST frameworks lack robustness: a projectable global type might still be rejected by the framework because the projection is unable to handle it; this leaves the user in the awkward position of having to build a mental model for the projection algorithm to be able to design viable global types. Li et al. [48] proposed the first sound and complete projection algorithm for sender-driven global types. Its PSPACE complexity stems from the need for determinisation. Their evaluation, though, showed that these corner cases will likely not occur in reality. This provides initial evidence that robustness is achievable without compromising efficiency.
As is to be expected, the jump in expressivity by adopting PSMs cannot come for free: the problem of computing a sound and complete projection for PSMs is in general undecidable, a fact inherited from being able to encode HMSCs. This does not defeat us, however: one of our main positive results is the definition of a very large class of PSMs, called Tame PSMs, that enjoys sound and complete PSPACE projection. A PSM is tame if it satisfies three constraints: (a) a technical refinement of the notion of the bound B for buffers, (b) that final states have no outgoing transitions, and (c) sender-driven choice: at each branching point, there is a single sender taking distinct actions.
Our proof works by reducing the problem to an instance of projectability of MSTs with sender-driven choice, which was proven to be decidable in PSPACE [48]. Our reduction is surprising because it produces a transformed protocol which is different from the original one: the encoded protocol language is different and involves additional participants and additional message exchanges; and yet its synthesized local specifications can be transformed back to local specifications for the original protocol. Due to the mismatch in expressivity between PSMs and global types, it is necessary that the reduction modifies the protocol semantics. Furthermore, we show the reduction preserves the complexity class, giving us a PSPACE algorithm for projectability of sender-driven PSMs.
Despite being a restriction, Tame PSMs are still much more general than global types: every sender-driven global type gives rise to a Tame PSM; moreover, every example given so far is tame. While the first two constraints (a) and (b) are not severe, the third condition (c) imposes a genuine restriction on expressivity.
In fact our main negative result is that sender-driven choice is in a sense “minimal”: we prove that projectability is undecidable for global types (the most primitive kind of PSMs) with general choice (aka “mixed choice”).
2.3 Processes and Typing
To complete the top-down toolkit, we provide a mean to check that a program correctly implements a protocol specified as a CSM. We achieve this by defining a CSM-based session type system for an expressive variant of \(\pi \)-calculus with session interleaving and delegation. The process calculus is adapted from [59] which represents a feature-rich modern presentation of multiparty session typing.
The type system’s main soundness argument hinges, as is standard, on a subject reduction result: if a typable program can take a step, it remains typable. From this, we derive two main safety correctness guarantees: typable programs cannot produce type mismatches (i.e. receiving a message that the process is not expecting) and terminated sessions do not leave orphan messages behind. We further prove a progress property under standard restrictions: roughly speaking, if the process contains only one session, then, if the type of the session is not final, the process can take a step (among the ones allowed by the type). Global progress in the presence of session interleaving is out of scope of this paper, but it may be attainable by adapting the (orthogonal) analysis employed in [18, 44].
In line with our decoupling goal, the guarantees of the type system are derived from the key properties of CSMs produced by projection (e.g. deadlock freedom). This makes it even compatible with the bottom-up methodology of [59] which forgoes global types and proposes to check key properties on local types directly. If a CSM satisfying the desired properties is provided to our type system, the corresponding guarantees apply to typable processes regardless of the existence of a PSM representing the protocol. This also liberates the type system completely from the choice of representation for global protocols.
Overall we obtain an expressive, decoupled and robust backend for top-down protocol development. Finally, we also show that this backend is backwards-compatible with MSTs: not only every sender-driven global type can be encoded as Tame PSM, but we also prove that, when there exists a local type that is a projection of a global type, our projection produces a CSM that can be translated back to a local type. This shows under which conditions PSMs and global types as well as CSMs and local types are equivalent, despite their structural differences.
3 Automata-based Protocol Specifications
We start our technical development by introducing a language-theoretic view of protocol specifications. We define protocols as special languages of words, and use CSMs as our local specifications of such languages. Finally, we introduce PSMs as global protocol specifications.
3.1 State Machines and Protocol Languages
Let \(\varDelta \) be a finite alphabet. The set of finite words over \(\varDelta \) is denoted by \(\varDelta ^*\), the set of infinite words by \(\varDelta ^\omega \), and their union by \(\varDelta ^\infty \). We write \(\varepsilon \) for the empty word. For two strings \(u \in \varDelta ^*\) and \(v \in \varDelta ^\infty \), their concatenation is \(u \cdot w\), and we say that u is a prefix of v, written \(u \le v\), if there is some \(w\in \varDelta ^\infty \) such that \(u \cdot w = v\); \(\operatorname {pref}(v)\) denotes all prefixes of v and is lifted to languages as expected. For a language \(L \subseteq \varDelta ^{\infty }\), we distinguish between the language of finite words \(L_{\operatorname {fin}} := L \cap \varDelta ^*\) and the language of infinite words \(L_{\inf } := L \cap \varDelta ^\omega \).
Definition 3.1
(State machines). A state machine\(A = (Q, \varDelta , \delta , q_{0}, F)\) is a 5-tuple with a finite set of states Q, an alphabet \(\varDelta \), a transition relation \(\delta \subseteq Q \times (\varDelta \cup \{\varepsilon \}) \times Q\), an initial state \(q_{0}\in Q\) from the set of states, and a set of final states F with \(F \subseteq Q\). If \((q, a, q')\in \delta \), we also write \(q \xrightarrow {a} q'\). A run is a finite or infinite sequence \(q_0\xrightarrow {a_0} q_1 \xrightarrow {a_1} \ldots \), with \(q_i~\in ~Q\) and \(a_i\in \varDelta \cup \{\varepsilon \}\) for \(i\ge 0\), such that \(q_0\) is the initial state, and for each \(i\ge 0\), it holds that \((q_i, a_i, q_{i+1})\in \delta \). The trace of such run is the word \(a_0\cdot a_1 \cdot \ldots \in \varDelta ^\infty \). A run is maximal if it ends in a final state or is infinite. The (core) language\(\mathcal {L}(A)\) of A is the set of traces of all maximal runs. If Q is finite, we say A is a finite state machine (FSM). A state machine is dense if for every \(q \xrightarrow {x} q' \in \delta \), the transition label x is \(\varepsilon \) implies that q has only one outgoing transition. A state machine is deterministic if \( \forall (q, a, q') \in \delta .\, a \ne \varepsilon \) and \( \forall (q, a, q'), (q, a, q'') \in \delta .\, q' = q'' \). We call a dense state machine deterministic if \( \forall (q, a, q'), (q, a, q'') \in \delta .\, q' = q'' \). A state \(q \in Q\) is called a sink state if it has no outgoing transitions, i.e. \(\forall a \in \varDelta \cup \{\varepsilon \}, q' \in Q.\, (q, a, q') \notin \delta \). We say a state machine is sink-final if, for every state, it is final iff it is a sink.
A language-theoretic view of protocols. Let \(m\in \mathcal {V}\) be a finite set of messages and
be a finite set of participants. The alphabet of
’s send and receive events is the set
. A send event
records that
sent the message \(m\) to
; a receive event
records that
received message \(m\) from
. The alphabet of all events is the set
. A paired event is a send event and its corresponding receive event:
. We define the alphabet of paired events as
. For the remainder of the paper, we fix an arbitrary set of participants \(\mathcal {P}\) and messages \(\mathcal {V}\), and often write \(\varGamma \) for \(\varGamma _\mathcal {P}\) and \(\varSigma \) for \(\varSigma _\mathcal {P}\). Given a word, we can project it to all letters of a certain shape: for instance,
is the subword of w with all of its send events where
sends any message to
. We write \(\mathcal {V}(w)\) for the sequence of values in w (in the same order). In \(w = w_1 \ldots \in \varGamma ^\infty \), a send event
is matched by a receive event
if \(i < j\) and
=
. A send event \(w_i\) is unmatched if there is no such receive event \(w_j\). A language \(L \subseteq \varGamma ^\infty \) satisfies feasible eventual reception if for every finite word \(w := w_1 \ldots w_n \in \operatorname {pref}(L)\) with an unmatched send event \(w_i\), there is an extension \(w \le w' \in L\) such that \(w_i\) is matched in \(w'\).
A sequence of send and receive events shall describe the execution of a protocol. We define when such a sequence uses channels in FIFO manner.
Definition 3.2
(FIFO Language). A word \(w \in \varGamma ^\infty \) is FIFO-compliant if for each prefix \(w'\) of w, it holds that
is a prefix of
, for every
. We denote the set of all infinite FIFO-compliant words by \(\textsf{FIFO} _{\inf }\). For finite words, we require that all send events are matched. Thus,
. We denote the (non-regular) set of all FIFO words by \(\textsf{FIFO} = \textsf{FIFO} _{\inf } \uplus \textsf{FIFO} _{\operatorname {fin}}\). A language \(L \subseteq \textsf{FIFO} \) is a called a FIFO language.
As the model of distributed implementation of a protocol, we adopt communicating state machines: parallel compositions of finite-control processes communicating asynchronously via point-to-point FIFO channels.
Definition 3.3
(Communicating state machines). We call
a communicating state machine (CSM) over \(\mathcal {P}\) and \(\mathcal {V}\) if
is a finite state machine with alphabet
for every
. The semantics of a CSM
is the language
whose definition is standard (see [62]). Roughly, for each pair of distinct participants
there are two FIFO channels
allowing communication between the participants in the two directions. The FSM
describes the possible actions of participant
. A transition
indicates that when
takes a step from
to
, it will send a message \(m\) to
by enqueuing it in channel
. Similarly,
prescribes the reception by
of message \(m\) from the channel
. A CSM’s run always starts with empty channels and each participant running its respective initial state. We denote the set of all reachable configurations (from the initial configuration) by
. A deadlock of
is a reachable configuration with no outgoing transition that has at least one non-empty channel or at least one participant not in a (local) final state.
The formal definition is given in [62]. As an example, Fig. 6 shows the three state machines constituting a CSM.
The goal of a protocol designer is to define a protocol that can be realised as a CSM. The projectable languages are exactly those protocols which can.
Definition 3.4
(Projections and Projectability). A language \(L \subseteq \varGamma ^\infty \) is said to be projectable if there exists a deadlock-free CSM
such that it generates the same language (protocol fidelity), i.e.,
. We say that
is a projection of L.
The asynchronous nature of CSMs makes them unable to enforce the order between certain events without explicit synchronisation. For instance, any CSM producing a word
will necessarily produce also
. Which events can be reordered is context-dependent: the events in the word
cannot be swapped, as the receive is only possible after the send. But in
the last two events can be reordered. This has been formalised as equivalence relation by Majumdar et al. [51], which can be seen as an instance of Lamport’s happens-before relation [46] for systems with point-to-point FIFO channels.
Definition 3.5
The indistinguishability relation\({\sim } \subseteq \varGamma ^* \times \varGamma ^*\) is the smallest equivalence relation such that
(1)
If
, then
.
(2)
If
, then
.
(3)
If
, then
.
(4)
If
, then
.
We define \(u \preceq _\sim v\) if there is \(w\in \varGamma ^*\) such that \(u \cdot w \sim v\). Observe that \(u \sim v\) iff \(u \preceq _\sim v\) and \(v \preceq _\sim u\). For infinite words \(u, v\in \varGamma ^\omega \), we define \(u \preceq _\sim ^\omega v\) if for each finite prefix \(u'\) of u, there is a finite prefix \(v'\) of v such that \(u' \preceq _\sim v'\). Define \(u \sim v\) iff \(u \preceq _\sim ^\omega v\) and \(v\preceq _\sim ^\omega u\). We lift the equivalence relation \(\sim \) on words to languages. For a language L, we define
For finite words \(\mathcal {C}(\hbox {-})\) is standard. For infinite words, though, the situation is a bit counterintuitive. Let us consider
. It is easy to construct a CSM
, with FSMs
and
, that accepts w. CSMs do not promise any sort of fairness for infinite runs so there is an infinite run for
where only
s transitions are scheduled. This is why \(\mathcal {C}(\hbox {-})\) is defined using \(\preceq ^\omega _\sim \), giving
3.2 Protocol State Machines
We now introduce PSMs as a mean to specify protocol languages from a global, centralised perspective. The idea, shared with both global types and HMSCs, is to specify only a core subset of the admissible executions, e.g. the ones where there is a bounded delay between sends and matching receives, and obtain the full set of admissible executions by closing the core language using \(\mathcal {C}(\hbox {-})\).
We adapt the notion of B-bounded from [27] to formalise the idea of “bounded delay” between matching events.
Definition 3.8
(B-bounded and). Let \(B \in \mathbb {N}\) be a natural number. A FIFO-compliant word w is B-bounded, resp.
, if for every prefix \(w'\) of w and participants
it holds that
resp.
We define the (regular) set of B-bounded FIFO words: \(\textsf{FIFO} _B := \{ w \in \textsf{FIFO} \mid w \text { is B-bounded}\}\).
Definition 3.9
(Protocol State Machine). A dense FSM \(M = (Q, \varGamma , \delta , q_{0}, F)\) is a B-PSM if \(\mathcal {L}(M) \subseteq \textsf{FIFO} _B\) and \(\mathcal {L}(M)\) satisfies feasible eventual reception. The semantics of \(M \) defined as \(\mathcal {S}(M) := \mathcal {C}(\mathcal {L}(M))\). Moreover, \(M \) is a PSM if it is a B-PSM for some B.
By definition, PSMs specify FIFO languages; importantly, although the core language \(\mathcal {L}(M)\) is \(B\)-bounded, the semantics \(\mathcal {C}(\mathcal {L}(M))\) includes non-B-bounded words and will not even be regular in general. Note that, it is decidable to check if an FSM is a \(B\)-PSM.
In [62], we show that \(\mathcal {C}(\hbox {-})\) preserves and reflects feasible eventual reception: if \(L \subseteq \varGamma ^\infty \) satisfies feasible eventual reception, then \(\mathcal {C}(L)\) does, and if \(\mathcal {C}(L)\) satisfies feasible eventual reception, then L does. More generally, every property that is preserved by \(\mathcal {C}(\hbox {-})\) can be soundly checked on the core language of a PSM. If the property is also reflected by \(\mathcal {C}(\hbox {-})\), the property holds if and only if it holds for the core language.
Definition 3.10
A PSM \(M \) is a
if its core language \(\mathcal {L}(M)\) is
. We may abuse notation and use \(\varSigma _\mathcal {P}\) as alphabet for
.
Example 3.11
(Kindergarten Leader Election). We consider a protocol between two participants
(evens) and
(odds). It can be used to quickly settle a dispute between children (hence the name). Both children pick 0 or 1 and tell each other their pick at the same time. Child
wins if the sum is even while
wins if the sum is odd. At the end, the loser concedes by sending the message \(\textsf{win}\) to the winner. The protocol is specified as a PSM in Fig. 7a (and as an HMSC in Fig. 7b). Note that specifying this protocol requires the ability of issuing send and receive events independently. If one insisted on issuing send and matching receives together, as in global types and
, one of the children would be forced to reveal their hand first, undermining the purpose of the protocol.
Fig. 7.
Kindergarten Leader Election (KLE).
4 Projection: From PSMs to CSMs
A CSM
is a projection of a PSM M, if
is a projection of \( \mathcal {S}(M) \). In this section, we explain two main results. The first is positive: we show that sound and complete projection is decidable for Tame PSMs. The second is negative: we show that the sender-driven restriction of Tame PSMs is necessary: if we drop the restriction, projectability becomes undecidable even for sink-final
. The full proofs can be found in [62].
4.1 Sound and Complete Projection for Tame PSMs
The idea of the decidability result is to reduce projectability of a Tame PSM to projectability of a (different) sender-driven global type, which can then be handled using the sound and complete algorithm of [48]. Furthermore, the reduction is such that a projection of the original PSM can be read off a projection of the global type. Before sketching the idea behind the reduction, we define Tame PSMs formally. Tame PSMs satisfy three conditions: they are sink-final, sender-driven, and satisfy some more fine-grained bounds on the message queues.
Definition 4.1
(Choice restrictions for PSMs). Let \(M = (Q, \varGamma , \delta , q_{0}, F)\) be a PSM. The PSM \(M \) satisfies sender-driven choice if there is a function \(\lambda :Q \rightarrow \mathcal {P}\) such that for all states \(q, q'\) such that \(q \xrightarrow {x} q'\) with \(x \in \varGamma _!\), it holds that \(\lambda (q)\) is the sender for x, i.e.,
. In addition, we say \(M \) is directed if for every state q, there is also a dedicated receiver
i.e., all transition labels from q are of the form
Last, if there is no dedicated sender but all transitions are still distinct, i.e. \(M \) is deterministic, we say that it satisfies mixed choice.
Definition 4.2
(Channel bounds for PSMs). We define channel bounds as a partial function \(\beta :\textsf{Chan}\rightharpoonup \mathbb {N}\) from channels to natural numbers, where \(\operatorname {dom}(\beta )\) denotes the domain of \(\beta \). Given a PSM \(M \), we say that \(M \) respects \(\beta \) if the following holds for every
If
then every message from
to
is immediately followed by a receive: for every state q and transition from q to \(q'\) labelled with
it holds that there is a single transition from \(q'\) and it is labelled with
.
If
, then
is
-bounded for every \(w \in \mathcal {S}(M)\).
A PSM that respects \(\beta \) with \(\beta = \emptyset \) is a PSM which only uses paired events, just like global types do. Thus checking the condition with \(\beta = \emptyset \) is a trivial syntactic check. For general PSMs, it is possible to generate valid channel bounds with a sound algorithm we propose in [62]. We conjecture the algorithm to be also complete, i.e. to always output some bounds if they exist.
Definition 4.3
(Tame PSMs). A Tame PSM is a pair \((M,\beta )\) where the PSM M is sender-driven, sink-final, and respects the channel bounds \(\beta \).
We can now sketch the idea behind the reduction. Fundamentally, the gap in expressivity between Tame PSMs and sender-driven global types is that in PSMs sends and matching receives do not need to appear one right after the other. One can observe, however, that one could replicate the same asynchrony of some trace
by introducing an intermediary participant
that is always ready to forward messages from
, leading to a trace
where the sends and matching receives between participants and the intermediaries are now immediately adjacent. The channel bounds \(\beta \) tell us exactly for which channels we need to introduce intermediaries; moreover the bound on the buffers induced by \(\beta \) makes sure that these intermediaries will not introduce any spurious dependency in the executions. To consolidate the idea, we show how it applies to our KLE example.
Fig. 8.
Kindergarten Leader Election after the Channel-participant Encoding.
Example 4.4
(Revisiting the KLE protocol). In Example 3.11, we introduced the Kindergarten Leader Election protocol, whose communication pattern cannot be represented as a
/global type: both children need to commit to the number they send before they receive the other’s message. Its PSM (Fig. 7) is however tame: it is sink-final, sender-driven and respects
. The “intermediary forwarders” idea applied to the protocol results in a protocol where some teachers (the intermediaries) will act as depositories for the initial choices of the two children. After committing their choice, each child is allowed to learn from the teacher the choice of the other child. The resulting PSM is given in Fig. 8. The names of the additional participants indicate the direction of communication:
forwards messages from
to
. Obviously, this encoding does not specify the same protocol. Still, our construction shows that one can obtain a projection of the original protocol from a projection of the modified one, by appropriately removing the forwarding actions of the teachers.
The example illustrates the simple case where \(\beta (\hbox {-}) \le 1\); in the more general case, the reduction is more involved and requires more intermediaries.
The workflow of our encoding is visualised in Fig. 9. Given a PSM \(M \), one first computes its encoding \(\texttt {enc}_{\operatorname {PSM}}(M)\). Second, one synthesizes a projection
of the encoded protocol using results from [48]. Third, one decodes to obtain a projection
of \(M \).
Fig. 9.
Workflow of encoding.
Theorem 4.5
Checking projectability of Tame PSMs is in PSPACE. One can also synthesize a projection in PSPACE.
Now, we show that the sender-driven choice restriction for Tame PSMs is necessary for projectability to be decidable. General PSMs inherit undecidability of projectability from HMSCs, which in turn was proven by Lohrey [50, Thm. 3.4]. Given our positive result for Tame PSMs, the proof for undecidability ought to break in the presence of sender-driven choice. The original proof goes through several (often implicitly given or omitted) automata-based transformations and does not give any insights about where and how the transformations break under the assumption of sender-driven choice.
Theorem 4.6
The projectability problem for sink-final mixed-choice
is undecidable.
We reduce the membership problem for Turing Machines to checking projectability of a sink-final mixed-choice
with five participants. Initially, there is a branching which only two participants are involved in and learn about. Subsequently, all participants communicate Turing machine computations in the form of configurations in both branches. If the (projected) language of one of the other participants is not the same for both branches, the PSM cannot be implementable because they do not know which branch to comply with and easily deadlock. We also show that the reverse is the case. Hence, we specify a language for each branch and make both coincide if and only if the Turing Machine has no accepting computation, which is the case if and only if the PSM is projectable.
The full proof is in [62]. We adopt the proof strategy of Lohrey to PSMs and make every transformation explicit and carefully check which structural properties the transformations preserve, yielding a stronger undecidability result concerning the most rudimentary of PSMs:
.
5 Typing Programs against CSMs
We now overview the key ideas behind AMP’s type system. The formal details and full proofs can be found in [62]. To define programs, we take inspiration from the process calculus with session interleaving and delegation of [59]. The syntax of AMP’s programs is reproduced in Fig. 10. The processes P represent the static program text. As is standard, \(\textbf{0}\) is the terminated process, \(\parallel \) denotes parallel composition, \( \textsf{Q}[\vec {c}] \) denotes a sequential process running the code defined by a finite set of definitions \(\mathcal {D}\). The prefixes
and
denote internal and external choice respectively, with a non-empty finite set of indices I. The endpoint of participant
of a channel between
and
in a session s, is denoted by
;
can send a label l and some payload p to
in session s by
, the dual reception is denoted by
(which binds the payload to x). To model delegation, a process must be able to send to another the capability to act as participant
in session s, denoted
; the receiving process will bind such capability to a variable x and use it to form endpoints
; we thus have in general send/receive actions on
where c can be a variable or some
.
The process
denotes the creation of a new bound session s used in P. The session is annotated with a (computationally irrelevant) CSM
, taking the place of what is often a global type. So far, we treated messages in CSMs very abstractly as elements of a finite alphabet. In processes, messages are more structured: they have a label (from a finite set) and a payload (of some type). The messages used by the CSM will thus be pairs \(l(t)\) of a label l and a payload type t, with the convention that if, from a state q, there are two outgoing transitions with the same sender, receiver and label, they will agree on the type.
In applications, the payload can be of any base type (e.g. integers, strings), or be a channel capability
(for delegation). Since supporting base types is a simple exercise, we follow [59] and focus on the harder case of channel capabilities as payloads. When using a CSM
as a protocol specification for a session s, it is natural to consider the (control) states
of
to be the local types that can be associated to
. Therefore, in our setting we will consider the set L of the states of any
annotating the process, as the possible payload types. For simplicity, we assume all CSMs use disjoint sets of states, so that we can unambiguously refer to the transitions from any state q by \(\delta (q)\).
In particular, if the protocol specified by
can delegate channels of a session following some CSM
, then the message alphabet of
will include states of
. When the CSMs are obtained through projection, it is natural to first obtain
so we can refer to its states in writing the PSM that projects to
. We thus assume there is an acyclic “delegation partial order” between the CSMs of a process:
means that
can use the states of
in its messages.
Fig. 10.
Syntax of AMP’s \(\pi \)-calculus.
The semantics of the calculus is defined on runtime configurations R (defined in Fig. 10), which are processes which additionally contain message queues \(s\blacktriangleright \sigma \) for each active session s. Here \(\sigma \) is a map from pairs of participants to sequences of messages. The reduction semantics is standard (cf. [62]). The only reduction rules we highlight here are the ones leading to an error configuration:
The first rule models unsafe communication: a process is stuck because all the queues it is waiting to receive from are not empty, but the labels of the first messages do not match any of the cases the process is expecting. The second rule models orphan messages: a session where all participants terminated but that has still non-empty message queues. The safety guarantees of our type system will rule out both cases. Note that [58, 59] focuses on communication safety. In addition, they consider S-deadlock freedom, which implies no orphan messages, but is an undecidable property that needs to be checked and is not necessarily transferred to processes by the type system: the property only holds if there is only one session, in which case much stronger conditions transfer. In our setting, deadlock freedom is transferred throughout by projection and the type system, yielding no orphan messages.
Fig. 11.
Typing rules for processes; \(\operatorname {init}(\hbox {-})\) denotes a CSM’s initial state.
Figure 11 shows the crucial rules of AMP’s type system. The typing judgement
uses a process P, a typing context \(\varTheta \) for the types of the parameters \(\vec {c}\) of sequential processes \(\textsf{Q}[\vec {c}]\) (the definitions of which are typed separately against \(\varTheta \)); a typing context \(\varLambda \) associating the variables x and the channel capabilities
occurring free in P, with some CSM state \(q\in L\). Rule PT-\(\textbf{0}\) says that a terminated process is typable in the environment with no capabilities. Rule PT-end permits to discard the capabilities that have terminated: \(\operatorname {end}(q)\) holds for final states with no outgoing receive transition. Rules PT-\( \mathop {\mathrm { \& }}\limits \) and
deal with communication. Assume
. According to PT-\( \mathop {\mathrm { \& }}\limits \), to receive a message as participant
in session c, we look for the type q of c in the typing context and check the CSM transitions \(\delta (q)\) are all receives
. Then the process needs to be able to receive any branch i, resulting in the continuation \(P_i\) which is typed in the context extended with the corresponding payload type \(y_i:p_i\), and with the type of c changed to \(q_i\). According to
, to send, as c with type q, a message non-deterministically picked from a number of branches \(i\in I\), we have to make sure q allows each branch, including matching the types of the payloads. Then each branch i continues as \(P_i\) which is typed in a context where c has type \(q_i\) and we lost ownership of the payload \(c_i\). Finally, PT-\(\upnu \) types a new session s used by P, by adding to the context a new binding
for each participant
of the CSM
annotating the session, with
being the initial state of
in
.
The first correctness criterion for the type system is to prove subject reduction: if a process is typable, then every configuration reachable from it will be typable. Thus, to state subject reduction, we need to define when a runtime configuration is typable. For this purpose, we define a second judgement
that includes a third typing context \(\varOmega \) used to type session message queues: associating to each channel
a sequence of message types l(q) (label and payload type). The key to make typing of runtime configurations an inductive invariant, is the following rule:
The main difference between RT-\(\upnu \) and PT-\(\upnu \) is that the typing context is not populated with capabilities associated to initial states; instead the prover can pick any CSM configuration \((\vec {q}, \xi )\) —where \(\vec {q}\) collects the local state of each participant, and \(\xi \) the contents of the message queues— that is reachable from the initial configuration of
. The states and the queues are used to initialise the typing context to type the process R using the restricted session.
In what follows we assume the definitions \(\mathcal {D}\) can be typed according to \(\varTheta \). We say a process/runtime configuration is well-annotated if every CSM appearing in it is (1) deadlock-free, and (2) satisfies feasible eventual reception. Here, annotated indicates that the CSMs have no computational meaning but well shows the need for certain guarantees, which our type system can preserve. Note that a process is automatically well-annotated if the CSMs are obtained via projection.
Theorem 5.1
(Subject Reduction). Given a well-annotated R, if
and \(R \longrightarrow R'\), then
Corollary 5.2
(Type Safety). For a well-annotated R, if
and \(R \longrightarrow ^* R'\), then \(R'\) does not contain \(\textbf{err}\).
For progress, the situation is more delicate: just like in [59] and most other MST systems, allowing session interleaving may introduce inter-session dependencies that are not modelled in the global protocol (which only pertains intra-session dependencies). We thus prove progress under these assumptions: (i) there is only one session running, and (ii) that each of its participants is implemented by a distinct process, and (iii) the CSM annotating it is sink-final. To encode these extra restrictions, we define a “Session Fidelity” variant of the typing judgement
which uses a subset of the rules of
to enforce the restrictions above. Let \(\varLambda ^s_{\vec {q}}\) and \(\varOmega ^s_{\xi }\) be defined as in the premises of RT-\(\upnu \).
Theorem 5.3
(Progress). Let \((\vec {q}, \xi )\) be a configuration of a sink-final, deadlock-free CSM
satisfying feasible eventual reception. If
, and \( (\vec {q}, \xi ) \) can take a step, then there exist some \(R'\) and
, such that \(R \longrightarrow R'\),
, and
Progress hinges on deadlock freedom of the CSM. In general, any (language) property of a PSM that is preserved and reflected by \(\mathcal {C}(\hbox {-})\) holds for its projection. However, as for progress, it is not necessarily easy to make the type system enforce the preservation of these properties at the global process level and requires careful treatment. [18] demonstrated how Kobayashi-style techniques [44] that can be used to show progress in the presence of session interleaving. We conjecture a similar system can be added on top of AMP’s type system.
6 Applications of AMP to MST Frameworks
Standard (expression-based) global types from MST frameworks can be seen as restricted special cases of PSMs. What is gained from using AMP for global types seen as PSMs? Is anything lost in doing so? In this section, we evaluate AMP as a backend for projection/typing of standard global types. The key consequences of our results are:
(a)
Every sender-driven global type is a tame sink-final
.
(b)
Tame sink-final
can be represented as a sender-driven global type.
(c)
Every collection of (expression-based) local types
can be expressed as a CSM
and vice versa.
(d)
AMP’s projection is deadlock-free by construction, but MSTs typically insist on freedom of a stricter notion of deadlock which we call soft deadlock. We show AMP’s projection can also be set to ensure soft deadlock freedom, without losing completeness.
These results help us settle two open questions:
Expression-based global/local types are equi-expressive with respect to state-machine-based global/local specifications.
Allowing mixed-choice in global types makes projectability undecidable.
Here, we give an overview while [62] presents the results in detail.
Global and local types. In most MST frameworks, protocols are specified using expression-based global types (G), which get projected to expression-based local types (L). Their syntax is specified as follows:
where \(\textbf{0}\) explicitly denotes termination and \(\mu {X}\) binds a recursion variable X. The remaining operators specify how messages are exchanged: for local types, sending and receiving are separate actions, while for global types they are specified in a single paired event. Typically only deterministic global types are considered, i.e. where every
has no \(i\ne j\) with
. The choice restrictions we discussed, can be imposed on global types, e.g. sender-driven choice requires that, for
, for all \(i,j \in I\),
.
The standard semantics of global types has been given as a transition system, or as sets of traces. In both cases, the semantics allows reordering of events that are not causally related, e.g.
allows
and
to communicate before
and
. This is formalised, in the presentation of [48, 51, 60] (which we adopt here) as defining the semantics of a global type to be a set of traces closed under the indistinguishability relation \(\sim \). With this view, it is immediate to represent any global type as a PSM. Given the restricted format of global types, the PSMs corresponding to translations of global types (like the one in Fig. 4) are
with a specific shape: they are tree-like, sink-final and recursion only happens at leaves and to ancestors [60]. On the face of it, it is unclear whether every
can be modelled as global type.
Theorem 6.1
For every sink-final
M, there is a global type \(\textsf{GAut}(M)\) with the same core language (and hence the same semantics). If M is non-deterministic (mixed-choice, sender-driven, or directed, resp.), then \(\textsf{GAut}(M)\) is non-deterministic (mixed-choice, sender-driven, or directed, resp.).
The main idea of Theorem 6.1 is that one can see a global type as a special regular expression, and thus we can adapt techniques like Arden’s lemma and Brzozowski derivatives to the case of PSMs. The key difficulty in the proof lays in showing the branching conditions are preserved: the standard automata transformations change the branching structure, and we need to produce new variants that do.
Similarly, local types can be directly read as the FSMs of a CSM. We can also provide an inverse transformation (preserving branching).
Theorem 6.2
Let
be a sink-final FSM over
without mixed-choice states for a participant
. One can construct a local type
for
with
.
Deadlocks and protocol termination. In MSTs, local types can only terminate with a \(\textbf{0}\), which signals at the same time that it is valid to stop the protocol, and that there is no further potential action. This implies that for a global type to be projectable into local types, all the participants need to know unambiguously when the protocol terminated globally. In contrast, using CSMs, it is possible to mark as final a state with outgoing transitions. Consider for instance the (directed) global type
. AMP’s projection would produce the FSM
as the projection for
. It contains a non-sink final state:
is not informed of which branch was taken and needs to be prepared to terminate, or receive one more message.
AMP’s projection produces deadlock-free CSMs, where deadlocks are defined as configurations which cannot take a step, but their queues are not empty or some participant is in a non-final state. Projections to local types ensure the absence of another type of deadlock: a soft deadlock, i.e. a configuration that is a deadlock, or that cannot take a step but where some participant is in a non-sink state. Is the possibility of soft deadlocks desirable? We argue that this depends on the domain of application: in distributed computing, it would be fine if a server kept listening for incoming requests while, in embedded computing, it can be key that all participants eventually stop. We can show that it is possible to use AMP in both scenarios, without giving up on completeness.
Definition 6.3
(Strong Projectability). A language \(L \subseteq \varGamma ^\omega \) is said to be strongly projectable if there exists a CSM
such that
is free from soft deadlocks (soft deadlock freedom), and L is the language of
(protocol fidelity). We say that
is a strong projection of L.
Theorem 6.4
Let \(G \) be a projectable global type. Then, the subset construction
[48, Def. 5.4] is sink-final for every participant
if and only if there is a CSM that is a strong projection of \(G \) and this CSM satisfies feasible eventual reception or every of its state machines is deterministic.
If we aim for a strong projection of a projectable global type, we construct the global type’s subset construction and check if it is sink-final. If it is not, there is no strong projection of it. If this is undesirable, the protocol needs redesigning. Theorem 6.2 can yield local types and \(\textsf{LAut}(L)\) is the FSM for a local type L.
Undecidability for mixed-choice. Finally, these results together with our results from Section 4.2, can settle the open question of whether we can project mixed-choice global types algorithmically.
Corollary 6.5
Both the projectability problem and the strong projectability problem for mixed-choice global types are undecidable.
7 Related Work
Multiparty session types. Inspired by linear logic [33], Honda [36] proposed binary sessions types for sessions with two participants. Multiparty session types [37] extended the idea to multiple participants. Deniélou and Yoshida [23] were the first to extensively explore the relation between CSMs and local types, but their projection is not complete and only supports directed choice; moreover the approach was found to be somewhat flawed [59]. MSTs have been incorporated into a number of programming languages [3, 17, 42, 47, 49, 54, 57]. They have also been applied to various other domains like operating systems [25], web services [71], distributed algorithms [45], timed systems [8], cyber-physical systems [52], and smart contracts [22]. A number of works are devoted to mechanising MST meta-theory [14, 40, 41, 64]. Our results could potentially extend the expressivity of the types involved in these applications.
MST projectability/projection. Via a reduction to globally-cooperative HMSCs, Stutz [60] proved MST projectability to be decidable for the class of global types that can —but do not have to— terminate (called \(\textbf{0}\)-reachable). Li et al. [48] provided a direct MST projection algorithm that is complete for sender-driven global types, providing a PSPACE upper bound. Our results use a reduction to these later developments. The global specifications in [48] can be shown to be special cases of Tame
so our results strictly expand the reach of their results. For example, the protocols of Figs. 5 and 7 are all tame, yet out of the reach of both works. We also clarify the discrepancy between the notion of deadlock in global types and in [48] (cf. Section 6). Finally, [48, 60] do not have a type system, providing no way to link properties of projections with the ones of processes. Preliminary versions of some of our results appeared in the PhD thesis of the first author [61].
The almost totality of asynchronous MST works can only handle directed choice. An exception is [12], where unrestricted global types are considered (without a type system). They propose an incomplete projection algorithm that is correct with respect to a different notion of correct projection than the standard one we adopt and generalise. We refer to [51] for a survey on choice restrictions.
Hu and Yoshida [38] propose a scheme with global types and an incomplete projection, where the global types are not safe by construction and the restrictions on choice only appear at the local types. The safety of global types is ensured by a combination of model-checking with message buffers of size 1, and syntactic restrictions that ensure that any unsafety that might arise, will be visible in the 1-bounded executions. For PSMs satisfying the syntactic restrictions, the same approach could be applied. The types of [38] also include connect/disconnect actions, which can be emulated in AMP by excluding deadlocks (but not soft deadlocks) and using non-sink final states.
Choreography automata and languages. Choreography Automata [4] are syntactically similar to
, but do not employ any closure operation, requiring the user to specify all the allowed interleavings, and preventing finite state representations for many common communication patterns. In addition, Majumdar et al. [51] showed that their conditions for projectability are flawed for the asynchronous case (fixes for the synchronous case appeared in [31, p. 8]). Barbanera et al. [5] applies a language-theoretic approach to a limited class of synchronous choreographies (with no claim of completeness of projection).
Bottom-up MSTs. A number of MST-based works deviate from the top-down approach. For instance, [59] proposes a type system that only requires local types and not a global type. The typing ensures some operational correspondence between local types and processes, making it possible to model check local types to determine properties of the program. Their local types in the asynchronous setting are Turing-powerful, and therefore model checking is of limited use. By virtue of the decoupling achieved by our type system, AMP can be used in a bottom-up way too: safety of the CSM used to type a process, implies safety of the process, regardless of whether the CSM is obtained by projection or just given. Dagnino et al. [21] and Castellani et al. [13] also use a bottom-up strategy by reconstructing a so-called deconfined global type from the parallel composition of local programs of a single session. Deconfined global types are not automatically safe, and checking their safety is shown to be undecidable.
Extensions for MSTs. A number of extensions for MSTs have been considered (see [7] for a survey), including: parametrisation [16, 24], dependent types [24, 66, 67], graduality [39], fault-tolerance [6, 70]. Context-free session types [43, 65] specify binary sessions that are not representable with finite-control. It would be interesting to consider projection for PSMs generated by pushdown automata.
Distributed synthesis. In automata theory, distributed synthesis seeks a way to transform a sequential specification into an equivalent distributed implementation, which is close in spirit with the idea of extracting local types from global types. One of the few positive results in this area is Zielonka’s theorem [72], which shows that every regular trace language can be recognised by a so-called “asynchronous automaton”. Despite their name, asynchronous automata can be seen as a parallel composition of participants interacting through synchronous actions. In contrast, PSMs and CSMs represent non-regular FIFO languages, giving rise to a harder challenge.
High-level message sequence charts. HMSCs were defined in an industry standard [69], inspiring extensive academic research [26, 28, 29, 53, 56]. Projectability has been studied for HMSCs under the name “safe realisability” [2, 30, 50], and was shown to be undecidable in general [50]. Several restrictions of HMSCs have been proposed to make projectability decidable. For a detailed survey, we refer to [60]. Compared to PSMs, HMSCs only model finite runs; their PSM encoding equips them with an infinite run semantics. With our developments, it is fairly straightforward to obtain a projection operation for sender-driven, sink-final HMSCs that respect some channel bounds. This class is incomparable to any of the decidable HMSC classes proposed in the literature. Since our type system only depends on CSMs, regardless of how they are obtained, AMP can type check a program against a projectable HMSC.
Choreographic programming. Choreographic programming [19, 32, 35] adopts the top-down approach even more radically than MSTs. In choreographic programming, the endpoint projection (EPP) aims at synthesizing a fully-featured program implementation directly from the global specification. As a result, the global specification describes the local computation alongside the communication structure (requiring infinite-state formalisms). In choreographies, one typically works with non-finite-control-state global specifications, so the hopes for a complete and decidable EPP are slim, justifying giving up on completeness. By only considering local computation in processes, the MST/AMP approach avoids this issue. Nevertheless, our results could still be useful for EPP when applied to the pure communication structure of choreographies. Notably, our method can project examples that cannot be projected using EPPs from the literature. Consider the choreography
, where message payloads are irrelevant and hence omitted and
denotes non-deterministic choice by
. The example is syntactically valid in [20] and can be easily encoded as a global type with sender-driven choice. However, their EPP would be undefined for
and
: it uses the merge from [11], which can only merge same sender receives. Our results would instead produce the desired projection.
Communicating state machines. CSMs are the canonical automata model for distributed systems. They have been studied in the context of model checking projections and do not apply a top-down methodology. The verification problem is undecidable in general since CSMs are Turing-powerful [10]. Several strategies to yield decidable classes have been proposed: assuming channels are lossy [1], restricting the communication topology [55, 68], or only allowing half-duplex communication for two participants [15]. The concept of existential boundedness [27] was initially defined for CSMs and yields decidability of control state reachability. The same holds for synchronisability [9, 34], which, intuitively, requires that every execution can be re-ordered (up to \(\sim \)) into phases of sends and receives such that messages can only be received in the same phase. Global types can only express 1-synchronisable and half-duplex communication [63].
Acknowledgments
The authors thank Anca Muscholl and Jorge A. Pérez for their discussions. This work was partially supported by the Luxembourg National Research Fund (FNR) under the grant agreement C22/IS/17238244/AVVA and by the ERC Consolidator Grant for the project “PERSIST” under the EU’s Horizon 2020 research and innovation programme (grant No. 101003349).
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.
selects a leader among
and
and the selected participant communicates the win to the other. A possible global type representing the protocol is
where
says that
sends \(\textsf{sel}\) and
receives it and \(+\) denotes branching. The local type of
would then be
where
means “
receives message \(\textsf{sel}\) from
” and
means “
sends message \(\textsf{win}\) to
’. Thus,
is supposed to listen for a message from
or from
; in the former case it would then communicate the win to
, in the latter, just concede. A program implementation may consist of a process for each participant; the process for the arbiter
may implement any specific policy for selecting the leader (e.g. always choose
), as long as the communications follow the protocol.
While, from a global perspective, it is possible to insist on the losing participant informing the winner that they lost, locally, the losing participant has no way to determine whether they won or not. Therefore \(G'\) is not realisable by local processes: we say it is not projectable. Second, local types are a more abstract representation of the system than programs, but we still want to show that, when implementation details are omitted, a program only performs communications that adhere to the local specification.
) and receive (
) actions. PSMs remove many of the restrictions of global types, while retaining their character: they specify the expected behaviour from a global perspective, and satisfy some basic correctness properties by construction (e.g. every send is eventually received, no type mismatches, etc). Owing to their generality, PSMs can represent any global type, but can go well beyond them: they also strictly subsume High-Level Message Sequence Charts (HMSCs). For maximizing expressivity at the local level, we adopt Communicating State Machines (CSMs) as the formalism for local protocol specifications. They are a canonical representation for decentralised asynchronous communication and as such do not impose constraints over what can be represented. Finally, to maximise expressivity at the program level, we consider a \(\pi \)-calculus with session interleaving and delegation.
indicates the transmission of message \(m_1\) from
to
. The symbol \(\textbf{0}\) denotes termination of the protocol. Recursion can be specified by binding a recursion variable X with \(\mu {X}\) and using X subsequently to jump back to where X was bound. Branching is denoted by \(+\). In the example,
can pick between three branches by sending different messages to
. Subsequently,
sends messages to
in all branches: 1 in the top and middle branch and 3 in the bottom branch. Participant
is supposed to send messages \(v_1\) or \(v_2\) in the top and middle branch while it receives from
in the bottom branch, which also recurses using X.
indicates the send of the message immediately followed by its receipt, although in any asynchronous implementation, the receipt might happen at a much later point, after other independent events took place. In Fig. 2,
may lag behind arbitrarily while
and
keep sending messages. The second key characteristic of global types and HMSCs is that they are finite-control: their control structure can be described using a finite graph. This makes it possible to algorithmically manipulate them, e.g. for verifying they satisfy some desirable properties, or for extracting local protocol specifications.
records that
sent the message \(m\) to
; a receive event
records that
received message \(m\) from
. A protocol specification is the language of desired finite or infinite words of events. For the purpose of this section, we will focus on finite words, but the technical development considers both finite and infinite words.
is not FIFO); we write \(\textsf{FIFO} \) for the language of all words that satisfy FIFO order. Second, if
is accepted by a protocol, it ought to also accept
as this kind of reorderings are induced by the scheduling of participants and network delays which are out of the control of participants. We write \(\mathcal {C}(L)\) for the closure of the language L under such reorderings. Thus a language \(L \subseteq \textsf{FIFO} \) represents the global interaction patterns of the protocols; moreover L can specify only some of these interactions and get all the ones that should also be possible under the asynchronous semantics by declaring the full set of acceptable words to be \(\mathcal {C}(L)\).
because the total number of messages in flight is at most 1; if we allowed 1 message per channel, it would be called a \(1\)-PSM.) As a PSM, however, M denotes the language \( \mathcal {C}(\mathcal {L}(M)) \), which admits words with unbounded channel behaviours and is not even regular in general. For instance, \( \mathcal {C}(\mathcal {L}(M)) \) includes words starting with
where
is running at a lower rate than the other participants, and leaves n pending sends from
and from
before it consumes them.
; furthermore PSMs can be used to encode HMSCs, which strictly subsume global types because the latter cannot specify simultaneous message exchanges between a pair of participants [63]. PSMs can even represent protocols that are outside the reach of HMSCs. Consider, for example, the PSM in Fig. 5. In that protocol,
commits to some integer (abstracted as the label \(\textsf{int}\)) at the beginning by sending it to
and sends a \(\textsf{go}\) signal to
. Note that here we use the paired send and receive notation
to emit the two events in sequence. Then
and
engage in some negotiation of arbitrary length until
decides to exit the loop, at which point
is finally allowed to receive the message sent by
. No HMSC can represent such protocol: the matching events
and
are separated by an arbitrary number of events (with no opportunity for reordering up to \(\mathcal {C}(\hbox {-})\)); since matching events in HMSCs need to belong to the same basic block, such block would also need to contain the arbitrarily many events in between, which is impossible.
should be interpreted as emitting the sequence
.
associates a finite state automaton
to each participant
, where transitions can either send or receive on the channels of
; the semantics of
is defined on configurations that include the local states for each participant and an (unbounded) FIFO buffer for each channel. They induce a FIFO language
over send/receive events, by considering as final the configurations where all the participants are in final local states and all the buffers are empty. CSMs thus represent a canonical general model of finite-control asynchronous protocol implementations.
is a projection of a PSM M if
is deadlock-free and
. We focus on the (projection) synthesis problem, producing a CSM as result. The corresponding decision problem is the projectability problem, which simply asks if there exists such a CSM. Notably, projectability can have lower complexity.
can never distinguish between the top two branches, as its only observations would be to have received 1 from
. The instance of the protocol with \(m_1 \ne m_2\) and \(v_1 \ne v_2\) would thus not be projectable. If \(m_2 = m_3\) then
would not be able to send the appropriate message to
. Therefore, the only projectable instances with no redundant branches are the ones where \(m_1\), \(m_2\), and \(m_3\) are pair-wise distinct and \(v_1 = v_2\). Figure 6 shows a candidate projection of the PSM in Fig. 2. If \(m_2 = m_3\) or \(v_1 \ne v_2\), the PSM is not projectable, and in fact the CSM can reach a deadlock.
then
is a projection of M; it is a complete projection if for all projectable M, \(M{\upharpoonright }\ne \bot \).
be a finite set of participants. The alphabet of
’s send and receive events is the set
. A send event
records that
sent the message \(m\) to
; a receive event
records that
received message \(m\) from
. The alphabet of all events is the set
. A paired event is a send event and its corresponding receive event:
. We define the alphabet of paired events as
. For the remainder of the paper, we fix an arbitrary set of participants \(\mathcal {P}\) and messages \(\mathcal {V}\), and often write \(\varGamma \) for \(\varGamma _\mathcal {P}\) and \(\varSigma \) for \(\varSigma _\mathcal {P}\). Given a word, we can project it to all letters of a certain shape: for instance,
is the subword of w with all of its send events where
sends any message to
. We write \(\mathcal {V}(w)\) for the sequence of values in w (in the same order). In \(w = w_1 \ldots \in \varGamma ^\infty \), a send event
is matched by a receive event
if \(i < j\) and
=
. A send event \(w_i\) is unmatched if there is no such receive event \(w_j\). A language \(L \subseteq \varGamma ^\infty \) satisfies feasible eventual reception if for every finite word \(w := w_1 \ldots w_n \in \operatorname {pref}(L)\) with an unmatched send event \(w_i\), there is an extension \(w \le w' \in L\) such that \(w_i\) is matched in \(w'\).
is a prefix of
, for every
. We denote the set of all infinite FIFO-compliant words by \(\textsf{FIFO} _{\inf }\). For finite words, we require that all send events are matched. Thus,
. We denote the (non-regular) set of all FIFO words by \(\textsf{FIFO} = \textsf{FIFO} _{\inf } \uplus \textsf{FIFO} _{\operatorname {fin}}\). A language \(L \subseteq \textsf{FIFO} \) is a called a FIFO language.
a communicating state machine (CSM) over \(\mathcal {P}\) and \(\mathcal {V}\) if
is a finite state machine with alphabet
for every
. The semantics of a CSM
is the language
whose definition is standard (see [62]). Roughly, for each pair of distinct participants
there are two FIFO channels
allowing communication between the participants in the two directions. The FSM
describes the possible actions of participant
. A transition
indicates that when
takes a step from
to
, it will send a message \(m\) to
by enqueuing it in channel
. Similarly,
prescribes the reception by
of message \(m\) from the channel
. A CSM’s run always starts with empty channels and each participant running its respective initial state. We denote the set of all reachable configurations (from the initial configuration) by
. A deadlock of
is a reachable configuration with no outgoing transition that has at least one non-empty channel or at least one participant not in a (local) final state.
such that it generates the same language (protocol fidelity), i.e.,
. We say that
is a projection of L.
will necessarily produce also
. Which events can be reordered is context-dependent: the events in the word
cannot be swapped, as the receive is only possible after the send. But in
the last two events can be reordered. This has been formalised as equivalence relation by Majumdar et al. [51], which can be seen as an instance of Lamport’s happens-before relation [46] for systems with point-to-point FIFO channels.
, then
.
, then
.
, then
.
, then
.
,
.
. It is easy to construct a CSM
, with FSMs
and
, that accepts w. CSMs do not promise any sort of fairness for infinite runs so there is an infinite run for
where only
s transitions are scheduled. This is why \(\mathcal {C}(\hbox {-})\) is defined using \(\preceq ^\omega _\sim \), giving
). Let \(B \in \mathbb {N}\) be a natural number. A FIFO-compliant word w is B-bounded, resp.
, if for every prefix \(w'\) of w and participants
it holds that
resp.
We define the (regular) set of B-bounded FIFO words: \(\textsf{FIFO} _B := \{ w \in \textsf{FIFO} \mid w \text { is B-bounded}\}\).
if its core language \(\mathcal {L}(M)\) is
. We may abuse notation and use \(\varSigma _\mathcal {P}\) as alphabet for
.
(evens) and
(odds). It can be used to quickly settle a dispute between children (hence the name). Both children pick 0 or 1 and tell each other their pick at the same time. Child
wins if the sum is even while
wins if the sum is odd. At the end, the loser concedes by sending the message \(\textsf{win}\) to the winner. The protocol is specified as a PSM in Fig. 7a (and as an HMSC in Fig. 7b). Note that specifying this protocol requires the ability of issuing send and receive events independently. If one insisted on issuing send and matching receives together, as in global types and
, one of the children would be forced to reveal their hand first, undermining the purpose of the protocol.
is a projection of a PSM M, if
is a projection of \( \mathcal {S}(M) \). In this section, we explain two main results. The first is positive: we show that sound and complete projection is decidable for Tame PSMs. The second is negative: we show that the sender-driven restriction of Tame PSMs is necessary: if we drop the restriction, projectability becomes undecidable even for sink-final
. The full proofs can be found in [62].
. In addition, we say \(M \) is directed if for every state q, there is also a dedicated receiver
i.e., all transition labels from q are of the form
Last, if there is no dedicated sender but all transitions are still distinct, i.e. \(M \) is deterministic, we say that it satisfies mixed choice.
then every message from
to
is immediately followed by a receive: for every state q and transition from q to \(q'\) labelled with
it holds that there is a single transition from \(q'\) and it is labelled with
.
, then
is
-bounded for every \(w \in \mathcal {S}(M)\).
by introducing an intermediary participant
that is always ready to forward messages from
, leading to a trace
where the sends and matching receives between participants and the intermediaries are now immediately adjacent. The channel bounds \(\beta \) tell us exactly for which channels we need to introduce intermediaries; moreover the bound on the buffers induced by \(\beta \) makes sure that these intermediaries will not introduce any spurious dependency in the executions. To consolidate the idea, we show how it applies to our KLE example.
/global type: both children need to commit to the number they send before they receive the other’s message. Its PSM (Fig. 7) is however tame: it is sink-final, sender-driven and respects
. The “intermediary forwarders” idea applied to the protocol results in a protocol where some teachers (the intermediaries) will act as depositories for the initial choices of the two children. After committing their choice, each child is allowed to learn from the teacher the choice of the other child. The resulting PSM is given in Fig. 8. The names of the additional participants indicate the direction of communication:
forwards messages from
to
. Obviously, this encoding does not specify the same protocol. Still, our construction shows that one can obtain a projection of the original protocol from a projection of the modified one, by appropriately removing the forwarding actions of the teachers.
of the encoded protocol using results from [48]. Third, one decodes to obtain a projection
of \(M \).
is undecidable.
with five participants. Initially, there is a branching which only two participants are involved in and learn about. Subsequently, all participants communicate Turing machine computations in the form of configurations in both branches. If the (projected) language of one of the other participants is not the same for both branches, the PSM cannot be implementable because they do not know which branch to comply with and easily deadlock. We also show that the reverse is the case. Hence, we specify a language for each branch and make both coincide if and only if the Turing Machine has no accepting computation, which is the case if and only if the PSM is projectable.
.
and
denote internal and external choice respectively, with a non-empty finite set of indices I. The endpoint of participant
of a channel between
and
in a session s, is denoted by
;
can send a label l and some payload p to
in session s by
, the dual reception is denoted by
(which binds the payload to x). To model delegation, a process must be able to send to another the capability to act as participant
in session s, denoted
; the receiving process will bind such capability to a variable x and use it to form endpoints
; we thus have in general send/receive actions on
where c can be a variable or some
.
denotes the creation of a new bound session s used in P. The session is annotated with a (computationally irrelevant) CSM
, taking the place of what is often a global type. So far, we treated messages in CSMs very abstractly as elements of a finite alphabet. In processes, messages are more structured: they have a label (from a finite set) and a payload (of some type). The messages used by the CSM will thus be pairs \(l(t)\) of a label l and a payload type t, with the convention that if, from a state q, there are two outgoing transitions with the same sender, receiver and label, they will agree on the type.
(for delegation). Since supporting base types is a simple exercise, we follow [59] and focus on the harder case of channel capabilities as payloads. When using a CSM
as a protocol specification for a session s, it is natural to consider the (control) states
of
to be the local types that can be associated to
. Therefore, in our setting we will consider the set L of the states of any
annotating the process, as the possible payload types. For simplicity, we assume all CSMs use disjoint sets of states, so that we can unambiguously refer to the transitions from any state q by \(\delta (q)\).
can delegate channels of a session following some CSM
, then the message alphabet of
will include states of
. When the CSMs are obtained through projection, it is natural to first obtain
so we can refer to its states in writing the PSM that projects to
. We thus assume there is an acyclic “delegation partial order” between the CSMs of a process:
means that
can use the states of
in its messages.
uses a process P, a typing context \(\varTheta \) for the types of the parameters \(\vec {c}\) of sequential processes \(\textsf{Q}[\vec {c}]\) (the definitions of which are typed separately against \(\varTheta \)); a typing context \(\varLambda \) associating the variables x and the channel capabilities
occurring free in P, with some CSM state \(q\in L\). Rule PT- \(\textbf{0}\) says that a terminated process is typable in the environment with no capabilities. Rule PT-end permits to discard the capabilities that have terminated: \(\operatorname {end}(q)\) holds for final states with no outgoing receive transition. Rules PT- \( \mathop {\mathrm { \& }}\limits \) and
deal with communication. Assume
. According to PT- \( \mathop {\mathrm { \& }}\limits \), to receive a message as participant
in session c, we look for the type q of c in the typing context and check the CSM transitions \(\delta (q)\) are all receives
. Then the process needs to be able to receive any branch i, resulting in the continuation \(P_i\) which is typed in the context extended with the corresponding payload type \(y_i:p_i\), and with the type of c changed to \(q_i\). According to
, to send, as c with type q, a message non-deterministically picked from a number of branches \(i\in I\), we have to make sure q allows each branch, including matching the types of the payloads. Then each branch i continues as \(P_i\) which is typed in a context where c has type \(q_i\) and we lost ownership of the payload \(c_i\). Finally, PT- \(\upnu \) types a new session s used by P, by adding to the context a new binding
for each participant
of the CSM
annotating the session, with
being the initial state of
in
.
that includes a third typing context \(\varOmega \) used to type session message queues: associating to each channel
a sequence of message types l(q) (label and payload type). The key to make typing of runtime configurations an inductive invariant, is the following rule:
. The states and the queues are used to initialise the typing context to type the process R using the restricted session.
and \(R \longrightarrow R'\), then
and \(R \longrightarrow ^* R'\), then \(R'\) does not contain \(\textbf{err}\).
which uses a subset of the rules of
to enforce the restrictions above. Let \(\varLambda ^s_{\vec {q}}\) and \(\varOmega ^s_{\xi }\) be defined as in the premises of RT- \(\upnu \).
satisfying feasible eventual reception. If
, and \( (\vec {q}, \xi ) \) can take a step, then there exist some \(R'\) and
, such that \(R \longrightarrow R'\),
, and
.
can be represented as a sender-driven global type.
can be expressed as a CSM
and vice versa.
has no \(i\ne j\) with
. The choice restrictions we discussed, can be imposed on global types, e.g. sender-driven choice requires that, for
, for all \(i,j \in I\),
.
allows
and
to communicate before
and
. This is formalised, in the presentation of [48, 51, 60] (which we adopt here) as defining the semantics of a global type to be a set of traces closed under the indistinguishability relation \(\sim \). With this view, it is immediate to represent any global type as a PSM. Given the restricted format of global types, the PSMs corresponding to translations of global types (like the one in Fig. 4) are
with a specific shape: they are tree-like, sink-final and recursion only happens at leaves and to ancestors [60]. On the face of it, it is unclear whether every
can be modelled as global type.
M, there is a global type \(\textsf{GAut}(M)\) with the same core language (and hence the same semantics). If M is non-deterministic (mixed-choice, sender-driven, or directed, resp.), then \(\textsf{GAut}(M)\) is non-deterministic (mixed-choice, sender-driven, or directed, resp.).
be a sink-final FSM over
without mixed-choice states for a participant
. One can construct a local type
for
with
.
. AMP’s projection would produce the FSM 
. It contains a non-sink final state:
is not informed of which branch was taken and needs to be prepared to terminate, or receive one more message.
such that
is free from soft deadlocks (soft deadlock freedom), and L is the language of
(protocol fidelity). We say that
is a strong projection of L.
[48, Def. 5.4] is sink-final for every participant
if and only if there is a CSM that is a strong projection of \(G \) and this CSM satisfies feasible eventual reception or every of its state machines is deterministic.
so our results strictly expand the reach of their results. For example, the protocols of Figs. 5 and 7 are all tame, yet out of the reach of both works. We also clarify the discrepancy between the notion of deadlock in global types and in [48] (cf. Section 6). Finally, [48, 60] do not have a type system, providing no way to link properties of projections with the ones of processes. Preliminary versions of some of our results appeared in the PhD thesis of the first author [61].
, but do not employ any closure operation, requiring the user to specify all the allowed interleavings, and preventing finite state representations for many common communication patterns. In addition, Majumdar et al. [51] showed that their conditions for projectability are flawed for the asynchronous case (fixes for the synchronous case appeared in [31, p. 8]). Barbanera et al. [5] applies a language-theoretic approach to a limited class of synchronous choreographies (with no claim of completeness of projection).
, where message payloads are irrelevant and hence omitted and
denotes non-deterministic choice by
. The example is syntactically valid in [20] and can be easily encoded as a global type with sender-driven choice. However, their EPP would be undefined for
and
: it uses the merge from [11], which can only merge same sender receives. Our results would instead produce the desired projection.
