In diesem Kapitel wird eine neuartige Erweiterung für Mehrparteien-Sitzungstypen (MPST) eingeführt, indem Replikation und erstklassige Rollen integriert werden, was die Aussagekraft und Entscheidungsfähigkeit von Kommunikationsprotokollen deutlich verbessert. Das Kapitel beginnt mit der Erörterung der Bedeutung der Überprüfung der Korrektheit von Kommunikationsprotokollen und ihrer Implementierung, wobei die Rolle der Sitzungstypen bei der Gewährleistung von Sicherheit und Konformität hervorgehoben wird. Anschließend vertieft er sich in das Konzept der Mehrparteien-Sitzungstypen (MPST), die binäre Sitzungstypen verallgemeinern, um das Nachdenken über die Kommunikation zwischen mehreren Teilnehmern zu ermöglichen. Der zentrale Beitrag des Kapitels ist die Präsentation von MPST!, einer Mehrparteien-Sprache, die die Replikation und erstklassige Rollen beinhaltet. Das Kapitel belegt die Metatheorie von MPST!, einschließlich der Eigenschaften von Subjektreduktion und Sitzungstreue, und demonstriert ihre Aussagekraft anhand einer Reihe repräsentativer Beispiele. Zu diesen Beispielen gehören die Modellierung von kontextfreien Protokollen, Rassen, gegenseitigem Ausschluss und komplexen Protokollen wie dem Problem der Essphilosophen und einem Auktionsservice. Das Kapitel untersucht auch die Auswirkungen der Replikation auf die Entscheidungsfähigkeit der Schreibmaschinenprüfung und liefert Bedingungen und Strategien, um die Entscheidungsfähigkeit sicherzustellen. Es schließt mit einer Diskussion verwandter Arbeiten und potenzieller Wege zukünftiger Forschung, wobei die praktischen Anwendungen und theoretischen Weiterentwicklungen des MPST! hervorgehoben werden.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Replication is an alternative construct to recursion for describing infinite behaviours in the \(\pi \)-calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce \(\textsf {MPST!} \), a session-typed multiparty process calculus with replication and first-class roles. We show that replication is not an equivalent alternative to recursion in MPST, and that using both replication and recursion in one type system in fact allows us to express both context-free protocols and protocols that support mutual exclusion and races. We demonstrate the expressiveness of \(\textsf {MPST!} \) on examples including binary tree serialisation, dining philosophers, and a model of an auction, and explore the implications of replication on the decidability of typechecking.
1 Introduction
Our world is powered by a multitude of computer systems working together by communicating, i.e., sending and receiving messages according to some protocol. It is therefore vital to verify the correctness of both communication protocols and their implementations, to ensure our programs behave according to their specifications, and to guarantee that specifications are indeed safe.
Session types [9, 14, 15, 31] provide a lightweight method by which a developer can ensure safety of, and conformance to, communication protocols. Session types can be thought of as types for protocols which can be attached to a communication channel to specify how it should be used, and can be used to detect issues such as communication mismatches and deadlocks early in the development process. Multiparty session types (MPST) [7, 16, 25] generalise binary session types to allow reasoning about communication between two or more participants, and have been shown to be expressive enough to capture a range of practical protocols such as the OAuth 2 authentication protocol [27].
Anzeige
Example 1
(Client-Server-Worker). Using generalised MPST [27], we describe the types for three participants in a simple work-offloading system.
The above describes types for a
lient,
erver, and
orker respectively. The
lient, having type
, sends (
) a
uest to the
erver with payload type
, then (
) waits to receive (
) an
wer from the
orker with payload type
. The
erver, upon receiving the
uest from the
lient,
or
ards it to the
orker. Lastly the
orker, after receiving the
or
arded request from the
erver, sends the
wer to the
lient. A MPST system verifies that any written program code conforms to this specification (known as session fidelity), and that this protocol is safe—i.e., that processes send and receive messages of compatible types.
Despite the potential of MPST for safe distributed programming, there remain limitations to the theory that impede their adoption for practical systems. For instance, generalising Example 1 to multiple workers in the style of a load-balancer is non-trivial and has inspired a series of work on the generalisation of direction of choice [28]. Further, generalising the number of clients is also non-trivial—typically, MPST theories assume a global view of all participants in a session. Lastly, the objects of actions in MPST (e.g., the recipient of a sent message) are hard coded because role names are constants.
Example 2
(Load Balancer fornclients). We introduce replication and first-class roles, combined with undirected choice in sends, to generalise Example 1 to support two workers and any number of clients.
Anzeige
The first difference is the use of the bang (
) operator to denote a replicated action, i.e., one which may occur any number of times. This makes the server agnostic to the number of requests. Second, a server now waits for requests—not from a specific client—but from any participant, binding the name of the sender to role variable
. This makes the server agnostic to the source of the requests. The server then makes a choice to forward the request to one of two workers, notably whilst passing the name of the client as one of the payloads. Finally, the server informs the client of the choice it made by sending the name of the worker in that branch. The worker type is also updated to be replicated, as it is dependent on the number of requests forwarded by the server. Notably, it receives the name of the client in the forward message, binding it to
, and uses it to send the final answer. A client may now be defined as:
As a result of the replicated types and first-class role names on the server-side, we may instantiate any number of clients and have them make any number of requests—all without changing the server-side protocol. Conversely, updating the number of workers has no impact on the types of clients. Thus, this extension promotes modular design of components in multiparty systems.
In fact, as we will see in Section 3, the addition of replication—especially when it is used in tandem with recursion—has several surprising consequences, in particular allowing us to describe context-free protocols as well as protocols that deal with races and mutual exclusion.
Contributions. The overarching contribution of this paper is the first integration of replication and first-class roles into a generalised MPST calculus, and an exploration of the impacts of these extensions on expressiveness and decidability. Our specific contributions are as follows:
1.
We present MPST!, the first multiparty session-typed language with replication and first-class roles (Section 2), and prove its metatheory in the form of subject reduction and session fidelity properties (Section 2.4).
2.
We show several expressiveness results through a series of representative examples (Section 3.1): in particular, replication lifts the expressive power of types and thus we give the first account of context-free MPST. We show that combining both replication and recursion allows us to model races and mutual exclusion; we demonstrate nontrivial examples including binary tree serialisation, the dining philosophers problem, and an auction service.
3.
We demonstrate the impacts of replication on the decidability of typechecking (Section 3.2). We show that the decidability of typechecking is contingent on the decidability of a given safety property, and demonstrate conditions guaranteeing a property to be decidable. Finally we show two syntactic approximations to allow us to verify that a property is decidable.
Section 4 gives an account of related work and Section 5 concludes. Detailed proofs of all our presented theorems can be found in the technical report [20].
2 Multiparty Session Types with a Bang!
In this section we introduce \(\textsf {MPST!} \), a conservative extension of existing multiparty session calculi [7, 25, 27] with support for replication and first-class roles.
Fig. 1.
Syntax of MPST!
2.1 Language
Figure 1 shows the syntax of \(\textsf {MPST!} \).
Names, values, and binders. A session name, ranged over by
, represents a collection of interconnected participants. A role is a participant in a multiparty communication protocol, and each communication endpoint
is obtained by indexing a session name with a role. In contrast to existing MPST calculi, MPST! supports first-class roles, meaning that a role may be communicated as part of a message. To this end, a role
may either be a concrete role
(e.g.,
or
in our load balancing example) or a role variable
. A name a is either an endpoint, a variable, or a role variable, whereas a value V is either a channel or a role. Binders b are used when receiving a message and can either be a variable binder or a role variable binder. Concrete values d are used when sending a message (at runtime) and are either an endpoint or a role name value.
Processes. Processes are ranged over by \(P,Q,R,\dots \): process \(P \,|\, Q\) denotes P and Q running in parallel; session restriction
binds session name
in process P; and \(\boldsymbol{0}\) is the inactive process.
As in the \(\pi \)-calculus, but unlike other MPST calculi, \(\textsf {MPST!} \) supports output-guarded choice
, allowing a nondeterministic send along any \(c_i\) to role
with label \(\textsf {m}_i\) and payload \(\widetilde{V_i}\), with the process continuing as \(P_i\). Branching receive
denotes a process waiting on channel c for one of a set of messages from role
with label \(\textsf {m}_i\), binding the received data to \(\widetilde{b_i}\) before continuing according to \(P_i\). It is key to note that the object of a communication action is indicated via
(for both sending and receiving), which can either be a concrete value, or a role variable. The second key difference is the optional use of the bang ! with a branching receive, marking it as replicated—i.e., it may be used 0 or more times, modelling infinitely available servers.
Fig. 2.
Operational semantics for the extended multiparty session \(\pi \)-calculus.
Definition 1
(Reduction context). A reduction context\(\mathbb {C}\) is given as:
.
A reduction context allows us to evaluate processes under parallel composition and name restrictions. With this, reduction rules on processes are given in Figure 2. The rules make use of a standard structural congruence\(\equiv \) [20, Appendix A] that allows us to treat parallel composition as commutative and associative, as well as including the usual \(\pi \)-calculus scope extrusion rule.
Rule [R-C] shows synchronous communication between two processes in session
. The first process, playing role
, offers role
a choice of message labels and associated process continuations. The second process, playing role
, sends a message with label \(\textsf {m}_k\) and transmits payloads \(\widetilde{d}\). The first process reduces to the selected continuation with the transmitted payloads substituted for the binders in the selected branch, and the second process reduces to the continuation Q.
Rules \([\textrm{R} {-}!\textrm{C}_{1}]\) and \([\textrm{R} {-}!\textrm{C}_{2}]\) describe communication with a replicated process R. Rule \([\textrm{R} {-}!\textrm{C}_{1}]\) is similar to R-C but the replicated process remains unchanged and the continuation \(Q_k\) is evaluated in parallel. Rule \([\textrm{R} {-}!\textrm{C}_{2}]\) handles the case where the replicated process does not need to receive from a specific role, but instead allows communication with an arbitrary role: the rule binds the sending role to
in the replicated continuation. We refer to this as a universal receive.
The [R-+] rule evaluates a branching output by nondeterministically evaluating to one of the sending branches; rule [R-X] handles a recursive call. Finally, rules [R-\(\equiv \)] and [R-\(\mathbb {C}\)] are administrative, allowing reduction modulo structural congruence and under contexts respectively.
Fig. 3.
Process definitions for load balancer example
Example 3
(Load Balancer: Process Reduction). We recall the load balancer example from Section 1, but this time, we present processes for each role (Figure 3) to demonstrate how our operational semantics handles communication. Consider a single client
in parallel with three server-side processes:
Using \([\textrm{R} {-}!\textrm{C}_{2}]\) , the client and server reduce. The reduction advances the client to its continuation
, and pulls out a copy of the server’s continuation as a new process. It is key to note that
is acting as a binder in
, therefore, in the continuation we observe a role variable substitution:
The spawned server process will then non-deterministically choose a worker to send to via rule [R-+] ; suppose
is picked.
Communication is now possible between the spawned server process and worker
, using rule \([\textrm{R} {-}!\textrm{C}_{1}]\) . As before, this communication advances the sender process and pulls out a copy of the worker’s continuation:
The client can now learn which worker was chosen, terminating the spawned server process, then the answer is exchanged between the worker and client:
Syntax of types. Session types
type communication endpoints. They consist of branching types
, replicated branching types
, selection types
, recursive types
and variables
, and the
type.
Branching session types have the form
indicating that role
offers a choice of message labels
with payload types
and continuations
. Similarly, selection session types
indicate an internal choice towards one of a set of roles
, with a message label, given payload types and continues as the corresponding continuation type. A replicated branching type
types a replicated channel. As with processes, role
can either be a concrete role, or a role variable in binding position.
Our type system supports singleton types for roles: role
has singleton type
, used to pattern-match specific roles in payloads. Static types
are used for protocol specification, whereas runtime types
are used by the type semantics to include a notion of parallel composition at type level: originally introduced by Le Brun and Dardha [4], a type
allows a channel to be associated with multiple “active” session types.
We assume that branching and selection types include a non-empty set of messages with pairwise distinct message names \(\textsf {m}_i\) (per role for
). We further take an equi-recursive view of types, identifying a recursive type with its unfolding (i.e.,
) and require that recursion variables are guarded.
Fig. 4.
Syntax of Types
Definition 2
(Subtyping). The subtyping relation
is co-inductively defined on types by the following inference rules:
Our definition of subtyping (Definition 2) is mostly standard. We adopt the convention of smaller types being ones with less external choice and more internal choice (à la Gay and Hole [13]). Subtyping of replication is based on regular branching; and parallel types are related iff their session types are subtypes. Subtypes are related up-to their recursive unfolding, and subtyping is reflexive.
Definition 3
(Type Congruence).Type congruence allows us to treat parallel runtime types as commutative and associative with identity element
.
Fig. 5.
Typing contexts and context operations.
Figure 5 shows the definition of typing contexts and their operations. Context
is used to type recursive process definitions, mapping process variables X to tuples of parameter types. Context
maps channels to types, and role variable singletons. Context composition
is defined iff
and
have disjoint domains. We lift subtyping and type congruence to contexts in the usual way.
As inspired by (e.g.) [31], linearity is enforced through the use of a context split operation
that splits a context
into two environments
and
. These environments may share variables with unrestricted types and role variables. Additionally, a channel c with runtime type
may be split such that
contains
and
contains
; this allows us to type endpoints used by different replicated processes. The inverse operation is context addition
that combines
and
into an environment
; again roles may be shared across environments. In the case that we have
(i.e., a linear variable used in two different contexts), context addition results in c having the combined runtime type
. The role insertion operation
is used when typing replicated receives and extends a context with a mapping
in the case that
is a role variable, and leaves
unchanged otherwise.
Before presenting the typing rules, we introduce the notion of a session protocol, mapping role names to session types. The
function associates a session protocol
to a concrete session
to form a typing context.
Definition 4
(Session Protocol). A session protocol
is attached to a session through the restriction operation in the form of
, dictating the protocol for
in P. A protocol
is a partial mapping from role to session type, given as:
A protocol
is well-formed iff it does not contain parallel types. We obtain a typing context by associating roles in a protocol with a session name. Formally:
Next, we introduce predicate \(\textsf {end}\) on type contexts. This ensures that an environment is end-typed: that is, its session types are congruent to type
.
Definition 5
(End-typed environment). A context is end-typed, written
, iff it only maps channels to session type
.
Fig. 6.
Typing rules.
Figure 6 shows the typing rules for MPST!. There are three judgements: the value typing judgement
assigns type
to value V under context
and consists of four rules. Rule [T-Wkn] allows weakening: if value V has type
under some environment
, and we have an end-typed environment
such that
, then the rule allows us to conclude that V has type
under
. Rule
types concrete roles as singleton types under the empty environment, whereas
types a role variable provided that it is contained within the type environment. Finally, rule [T-Sub] types a linear variable, allowing for subtyping. Judgement
simply looks up process variable X in process environment
, returning its parameter types; this is achieved by rule [T-X] .
The final judgement
states that process P is typable under recursion environment
and type environment
. Rule [T-\(\boldsymbol{0}\)] types the inactive process under an end-typed environment. Rule [T-|] types parallel processes under a split environment. Rule [T-\(+\)] types an output-directed choice; since this operation uses branching control flow, each choice must be typable under the same environment.
Rules
and
type replicated and non-replicated receives respectively. In both cases the rules check that the channel has a receiving session type. Both rules check that each branch is typable by extending a common typing context with the variables bound by the receives, along with the continuation type for the session channel. In the case of a replicated receive there are two differences: first, the context used to type each branch must be end-typed (in order to avoid duplicating linear resources). Second, since the role
may be a binding occurrence of a role variable
, the context used to type each branch must be extended with the role variable (if applicable) using the insertion operator.
Rule [T-\(\nu \)] types a session name restriction
. As is standard in generalised MPST [27], the session protocol must satisfy a safety property\(\varphi \). We discuss specifics of this property in Section 2.3, and how it is used in Section 2.4. Informally, the property ensures that all process communication is “compatible”, and is the weakest property required to prove subject reduction. We then prove our metatheory parametric on the largest safety property, allowing it to be customised to verify more precise properties (e.g., to ensure deadlock-freedom or termination), based on the requirements of a specific protocol.
Rule
types an output if the sending channel can be mapped to a selection type with payload types that match the values being sent. The rule ensures that role
is either a value, or it exists in the type context—i.e., messages cannot be sent to unbound role variables. The selection type continuation should be used, along with the common context, to type the continuation process.
Lastly, rules [T-Def] and [T-Call] type recursive processes. The former populates the recursion environment whilst ensuring that process declarations are well typed under the variables they bind. The latter checks that types of values used in a process call match what was specified in the declaration.
Example 4
(Load Balancer: Type Checking). By introducing a name restriction for session
that includes the types from Example 2, we can type the processes from Example 3 under empty typing contexts:
Fig. 7.
Type semantics.
2.3 Type Semantics
To reason about the interactions between session types, following Scalas & Yoshida [27], we endow typing contexts
with LTS semantics as shown in Figure 7. Each action
denotes an output, input, and synchronising communication respectively. Context reduction
is defined iff
for some
, and we write
for the transitive and reflexive closure of
. We write
iff
for some
.
Transitions
and
are standard: a context can fire an input label (resp. output label) matching any of the labels in the top-level branch type (resp. selection type). This transitions the entry to the continuation of the chosen type.
Transition
models the receipt of a message by a replicated input. The two main differences to the linear receive are: (i) the role
used in the transition label is allowed to be a role variable name; and (ii) firing an input does not advance the type, but instead pulls out a copy of the continuation and places it in parallel. Role
is considered bound in
and its continuations, but is free in pulled out copies of the continuations composed in parallel (
).
Transition rules
,
,
allow contexts to reduce under a larger context, or when types are guarded by recursive binders. Concretely,
allows transitions to ignore role singletons;
allows a context to perform a transition when split from a larger context (the transition result must be added back in); and
allows recursive binders to be treated equal to their unfolding.
Transitions
and
model type-level communication; for simplicity and without loss of generality we assume a convention wherein session-typed payloads precede role-typed payloads. Both rules state that if a context can be split such that one part fires an output label, and the other fires an input with matching roles, message label and payloads, then the entire context can transition via a communication action. We note that payloads will consist of either session types or role singletons. For the former, sender payloads must be subtypes of the receiver payloads; for the latter, role substitution occurs after communication.
caters for universal receives, where the input label consists of a role variable in binding position—this is reflected in the role substitution. We say that a context reduces iff it can transition via communication actions.
Example 5
(Load Balancer: Context Reduction). We now use the protocol from Example 4 to demonstrate context reduction in action. Initially, the only communication action possible is between the client and server, via
.
It is key to note the role substitution for the type of
above; specifically, how the substitution affects the parallel type extracted through communication, but does not affect the replicated type
. From here, there are multiple reduction paths, but let us observe the reduction path in which
communicates with
.
Note how reduction is possible because the context split allows the server’s parallel type to be extracted into its own context. Then, reduction occurs via
and
. From here, the context reduces in a similar fashion: first the server communicates a role with the client; followed by the final communication between the client and worker.
Safety. In order to type a session restriction, rule [T-\(\nu \)] in Figure 6 requires that the session’s protocol of the session must obey a safety property\(\varphi \). Informally, a safety property requires that processes exchange values of compatible types and that a sender only ever selects available branches. Safety is the weakest typing context property required in order to prove subject reduction.
Definition 6
(Safety).\(\varphi \) is a safety property on type environment
iff:
A property \(\varphi \) is considered safe iff it conforms to all conditions specified in Definition 6. Conditions
and
are concerned with communication. They state that if two roles in the same session have an output and input type respectively which point at each other, then: (i) they should have at least one common message label; (ii) for each common label, their payloads should be equal in length; and (iii) for each common label, all session types in the payload of the sender should be subtypes of what is expected by the receiver.
Condition
requires safety to hold after the unfolding of recursive binders;
requires all role variables used in a context to be bound by that same context; and
requires safety to hold after context reduction.
Users of the type system can re-instantiate \(\varphi \) with custom properties (e.g., termination), as long as the property used meets the safety requirements.
2.4 Metatheory
Unlike most session type theories, generalised MPST do not syntactically guarantee any properties on the processes they type. Rather, they provide a framework for verifying runtime properties on the type context, from which process-level properties may be inferred—the benefit being that these properties are undecidable to check on processes, yet decidable in the realm of the type system. Furthermore, its generalised nature allows for fine-tuning based on specific requirements of its applications. Informally, generalisation of the type system works by proving the metatheory parametric of the largest safety property captured by \(\varphi \) in Definition 6; i.e., all theorems proved and presented which involve a type context
, assume that
holds, or “
is safe”. Essentially, \(\varphi \) describes the minimum (and most general) safety requirements made for subject reduction to hold. This proof technique allows \(\varphi \) to be re-instantiated with more specific properties without having to reprove any of the base metatheory. (We occasionally reference properties other than safety in examples.)
2.5 Subject Reduction and Session Fidelity
The main results of a generalised MPST system are subject reduction (Theorem 1) and session fidelity (Theorem 2). These theorems allow the type system to be used as a framework for verifying custom properties by re-instantiating \(\varphi \). We note that discussing how the generalised type system can be used as a verification framework is not the focus of this paper (to this end, we address the interested reader to Scalas and Yoshida [27, Section 5]); rather, we build on generalised MPST theory as a means of investigating the expressiveness of replication and first-class roles in MPST. Hence, the following presents the two theorems—highlighting key differences with what is standard—but we do not demonstrate the verification of runtime properties (which is standard). Proofs are in the technical report [20].
Theorem 1
(Subject Reduction). If
with
and \(P \rightarrow P^\prime \), then
s.t.
and
with
.
Intuitively, subject reduction states that any safe and well-typed process remains safe and well-typed after process reduction. More formally, the theorem asserts that if a process is typed under a safe context, then the context can match any process reduction to type its continuation whilst retaining safety.
Session fidelity states that if a context can reduce, then a process it types can observe at least one of its reductions. By virtue of subtyping, a context is allowed to specify paths which need not be followed by a process it types; the key point is that session fidelity requires that there is at least one observable reduction. Using session fidelity, one can prove properties about communication occurring within a single session. It does not, however, provide grounds for showing such properties on interleaved session communication. Hence, as is standard in generalised MPST, we define additional assumptions on processes required for session fidelity to hold.
Definition 7
(Only plays one role). (The following is a slight adaptation of [27, definition 5.3].) Assuming
, we say P:
1.
has guarded definitions iff each subterm of P with the form
we have:
implies a process call \({\textrm{Y}}\langle \dots ,x_i,\dots \rangle \) can only occur in Q as a subterm of a communication action over channel \(x_i\).
2.
only plays rolein, by
iff (i) Item 1 holds for P; (ii)\(\textsf {fv}(P)\) = \(\emptyset \); (iii)
with
and
; (iv) in all subterms
of P, we have
.
The purpose of Item 1 is to prevent processes from infinitely reducing via [R-X] without communicating, and Item 2 identifies a typical application of MPST where a number of processes
communicate over a multiparty session
, with each process playing a single role. The difference in our definition to the standard is that processes
should play a single role and not a unique role. This is due to the introduction of replication in our language; note how reduction with a replicated process is guaranteed to produce multiple processes playing the same role and is reflected in our definition in condition (iii) of Item 2 , where a channel is mapped to runtime type
, allowing for parallel composition.
Informally, the session fidelity theorem states that, given a safe context that types a process of a particular structure—i.e., one governed by the session fidelity assumptions of Definition 7—then if the context can reduce, the typed process can match at least one reduction. Furthermore, after the process matches the context reduction, it remains within the session fidelity assumption structure.
Theorem 2
(Session Fidelity). Assume
with
and
where each
is either \(\boldsymbol{0}\) (up-to \(\equiv \)), or only plays role
in
. Then,
implies
s.t.
, \(P \rightarrow ^* P^\prime \) and
, where
and each
is either \(\boldsymbol{0}\) (up-to \(\equiv \)), or only plays role
in
.
We now turn our attention to the main focus of this paper, i.e., exploring the expressiveness and decidability of replication and first-class roles in MPST.
3 Expressivity and Decidability
This section discusses, and shows by example, the benefits and limitations of MPST!. Section 3.1 demonstrates the exressivity gained by using replication and first-class roles in MPST, whilst Section 3.2 presents our decidability results.
3.1 Expressivity
We begin by demonstrating a common design pattern used for describing protocols, which we call services. We build a number of services to showcase language features, and to describe protocols which—to the best of our knowledge—were previously untypable in any MPST theory. Specifically, using the increased expressiveness of replication and first-class roles, we define types for binary trees, the dining philosophers problem, and an auction. Importantly, all examples shown adhere to the decidability requirements discussed later (cf. Section 3.2).
Services. A service is a building-block of a protocol, involving some universal receive, with the aim of offering a specific interaction. A client interacts with a service to achieve the communication pattern it offers. Importantly, services may be clients of other services, promoting a modular design of protocols in MPST!.
Example 6
(Ping). The ping service simply responds to a ping with a pong.
A basic yet useful service is given in Example 6, where role
offers a ping service. As a convention, we will use capitals for naming services. We highlight the importance of both replication and free role names in types to be able to design modular components of a protocol—both are integral to designing a sub-protocol agnostic of the larger scope in which it is used.
Context-Free MPST. Context-free session types [1, 22, 29] are a formalism that replace prefix-style session types with individual actions, along with a sequencing operator ; with neutral element skip. The goal of this line of work is to express communication protocols that are not possible under tail-recursive session types, given their restriction to regular languages. The classic example is that of communicating a serialised binary tree.
Example 7
(Binary tree in standard context-free STs). Consider a binary tree data type described by the following context-free grammar.
We could attempt to represent a protocol that serialises this data type as follows:
However, this type is not precise enough—it does not guarantee that the correct structure of a binary tree is maintained. Work on context-free session types solves this by proposing type systems allowing the following specification:
Selecting the
label now guarantees that two sub-trees will follow.
The parallel types presented in Section 2.2, although not exposed directly to users, lift expressiveness of types in MPST!. In fact, since replicated branches are permanently available (by composing continuation types in parallel), we can simulate the sequencing operator ; using type-level parallel composition.
Example 8
(Binary Tree Service). Recall the ping service
from Example 6. We build a binary tree service
using
as shown below:
The service begins by receiving a request for a
from a client. It then sends a
to the ping service, exposing a replicated branch waiting to receive the
reply. The client is now free to build the binary tree. It is key to note that any
sent to the service will subsequently forward two
requests to
. In turn, this communication will pull out two copies of the type continuation
, forcing the client to maintain the appropriate binary tree structure. For example, if a client
wishes to build a tree consisting of one root node and two leaf nodes, its type would be defined as:
The metatheoretic framework can be used to determine that any protocol failing to abide by the binary tree structure will result in a deadlock; whilst any safe protocol that obeys the correct structure is terminating, e.g. the protocol
.
An obscure limitation of the tree service in Example 8 is that it can only be used by a single client. Consider, for example, two separate clients sending a
message to
. Since both tree service types communicate with
to unroll the replicated branch
, the protocol becomes non-deterministic in a non-confluent manner and can result in deadlocked behaviour. To resolve this issue, we amend the tree service to accept a payload role which should act as a personal ping service for the client; this guarantees that the tree type is only unrolled by the client that made the initial request.
Example 9
(Multi-Client Binary Tree). We now redesign the binary tree service, this time capable of concurrently building multiple trees for different clients. The key difference here being that the new service,
, accepts a role as a payload on the initial request to which it will issue its
s.
Multiple clients can now issue concurrent requests to the tree service whilst maintaining safety. A sample (terminating) protocol is that of
, where
, and the types for
are given by:
Replication vs. Recursion. We have seen that replication and parallel composition increases the expressive power of MPST beyond that of tail-recursion. Naturally, one might ask, “is recursion still needed?” We find replication and recursion in MPST to be mutually non-inclusive—i.e., both can produce protocols which cannot be typed under the other construct. We have already demonstrated this in one direction with the binary tree examples; below we showcase how recursion cannot be replaced by replication.
Example 10
(Lock Service). The lock service provides clients with a mutex lock.
When a client requests a lock from
, a copy of the recursive continuation is exposed. The recursive definition allows sequences of
and
messages to be received. It is key to note that, whilst replication maintains a top-level branch that is permanently available to receive a message, the top-level action in a recursive definition is not fixed.
Copies of the continuation type of a replicated receive are executed concurrently. Example 10 provides a service for roles to enter race-sensitive portions of a protocol, as if it were an atomic action. We demonstrate its use by typing the dining philosophers problem.
Example 11
(Dining Philosophers). A number of philosophers gather to eat on a round table. Each plate is separated by a single chopstick, and a philosopher needs two chopsticks to eat. The dining philosophers problem requires the philosophers to employ an algorithm to ensure the table does not get deadlocked. In such a setting, we can view chopsticks as services and philosophers as clients. Assuming a size of n-philosophers, we define the type for a chopstick as:
Before offering its service, a chopstick requests a lock from
. This ensures that every chopstick has its own lock that it may
and
. The lock is used to guarantee that a chopstick is only ever taken by a single philosopher at a time. A chopstick then waits for a
request from a philosopher; receiving one will result in it attempting to
the lock. This acquisition is only successful if the same role has not already requested it in some other parallel composition. If the lock was already acquired, then the
will block until the lock is released. Acquiring the lock sends an
back to the philosopher, symbolising that they have successfully obtained the chopstick. When done from eating, the philosopher may then send back a
message, which in turn releases the lock, as the chopstick is now available to be taken by a different philosopher.
We can now write an algorithm for philosophers. First, a naive approach:
Every philosopher
has a similar type. They begin by requesting to take the chopsticks to their left and right—note that this results in every chopstick receiving two
requests. Receiving both
messages means the philosopher can eat, and subsequently
back the chopsticks. Finally, when finished, philosophers send a
to role
, acting as a clean-up for the protocol. The protocol
is safe, but fails typechecking for \(\varphi = \textit{terminating}\). In fact, the naïve protocol allows for scenarios in which all philosophers take a single chopstick, resulting in a deadlock. This problem has many solutions; we present the simplest in which philosophers take turns to eat. (Key changes are underlined.)
Here, all philosophers other than the first must wait for the previous to
ish eating before they can request to take their chopsticks. The updated protocol
now typechecks for \(\varphi =\)terminating.
The previous examples demonstrate how recursion hidden by a universal receive can be used to mimic changes in state. Our final example does the inverse, i.e., we show how a universal receive hidden by a recursive binder can be used to model resources which eventually reach some permanent state. In addition, we show that universal receives model fair races, since they do not impose an order on how communication is handled.
Example 12
(Auction). A merchant
sets up an auction
to accept bids from some buyers
. A merchant can employ different mechanisms for choosing who to sell to (e.g., first come first served, highest bid, biased selling, etc.); but must always respond to buyers with either a
,
, or
message.
Buyers
race to send
s to the auction service. In turn, the auction forwards bids and buyer role identifiers to the merchant, who processes bids sequentially (but still in an arbitrary order). If the merchant declines a bid, then the client is offered another chance; if the merchant accepts a bid, then it exposes a replicated receive which informs any further buyers that the product is no longer available. It is key to note that, unlike in Example 11 where we used locks to avoid race conditions, races here are not only allowed but are integral to the protocol. Additionally, by uncovering a replicated receive, the merchant enters a permanent state. These two characteristics guarantee that, no matter the selling algorithm employed by the merchant: (i) bids always arrive in a fair arbitrary order; and (ii) the product can only be sold once.
Discussion. We have now shown that replication and recursion are mutually non-inclusive, and that our extension increases the expressiveness of MPST. It is important to understand the dependencies between added features and the expressiveness gained. Since MPST! is a conservative extension, it is guaranteed that the increase of expressiveness derives from our two extensions: 1. the addition of replication; and 2. the addition of first-class roles.
Replication alone is enough to increase the expressiveness of MPSTs w.r.t. the Chomsky hierarchy. We note that, e.g., Example 8 could be easily re-written without the universal receive, especially since it should not be used by multiple clients to uphold deadlock-freedom—thus, replication in MPSTs increases their expressiveness to that of context-free languages.
First-class roles in our formalism refers to: (i)universal receives acting as binders on role variables; and (ii) the ability to pass roles as payloads in messages. Universal receives allow protocols to be designed agnostic of the client pool (consider Examples 2,6,9 and 10); and also act as a fair way of introducing races—e.g. Example 2 describes a load balancer that responds to requests in no particular order. Role passing allows for safe distributed choice. In a load balancer (in general), it is impossible for a client to know which worker will service its request. In Example 2, role passing allows the server to inform clients of its choice, and also informs the worker of the identity of the client. Role passing increases expressiveness by introducing dependencies into a protocol. For instance, Example 12 uses role passing to ensure the merchant correctly services the right buyers; without it, a merchant could not respond to requests without bias.
As a final note, first-class roles are different to, e.g., delegation or multiple sessions (both supported in MPST!) since they act inside a session. Therefore our system can still be used to check for properties such as deadlock-freedom, which is not possible with interleaved sessions without other mechanisms such as an interaction typing system [3] or priorities [8].
3.2 Decidability
As one may expect, the added expressiveness of replication and first-class roles into types does not come without a cost. Unlike the base theory that this work extends, even though our language models synchronous communication, typechecking may be undecidable in the general case. In the following, we discuss decidability of typechecking in detail. We show that typechecking is only as decidable as the safety property; we provide examples of types that make typechecking problematic; and we provide strategies for determining whether a protocol is captured by a decidable subset of MPST!.
Theorem 3
(Decidablility of type checking). If \(\varphi \) is decidable, then typechecking is decidable.
Proof
Since typing rules in Figure 6 can be deterministically applied based on the structure of a process P, and a typing context need only be split a finite number of times to separate all linear types, there are a finite number of contexts that can be tried for each rule that requires a context split. Lastly, subtyping is decidable [13] (decidability of subtyping replicated types is equivalent to regular branching types, and of parallel types is equivalent to checking multiple session types); and \(\varphi \) is decidable by assumption. \(\square \)
Theorem 3 states that decidability of type checking is only as decidable as property \(\varphi \). In Example 14, we will demonstrate why \(\varphi \) may not necessarily be decidable in the general case for the type semantics presented in Figure 7. To do this, we first define behavioural sets of type contexts (as in [26, appendix K]).
Definition 8
(Behavioural set). The behavioural set of a type context, written
, is given by
; where \(\textsf {unf}^*\) is the closure of \(\textsf {unf}\)—a function that unfolds all top-level recursive binders in a set of contexts. (Full definitions of \(\textsf {unf}\) and \(\textsf {unf}^*\) are standard [20, Appendix D].)
Informally, the behavioural set of a context
is the set of (i) its reductions; and (ii) its reductions’ unfoldings. The benefit of \(\textsf {beh}\) is that it mechanically abides by conditions
and
from Definition 6. Therefore, to determine whether
is a safety property, all that is required is to exhaustively check the contexts that inhabit
against the remaining conditions of Definition 6.
Example 13
Consider a context
. The behavioural set of
is given by:
Notice that the left element is the original context after 0 reduction steps, whereas the right element is the unfolding of
. Moreover, any further reductions only yield contexts (and unfoldings) already captured by these two elements.
The next example context is problematic for typechecking.
Example 14
Consider a context
. The behavioural set of
is given by:
Indeed,
is infinite. This is a result of how replication and parallel composition are modelled in Figure 7. In fact, the type semantics for replicated communication allows for context reduction to yield larger types. Note how in this example, the contexts that inhabit
get infinitely larger by pulling out infinitely many copies of type
.
Furthermore, we point out that infinite behavioural sets are not only a result of recursive communication with replicated branches. Consider, e.g. a
=
. Such a context will also pull out infinitely many copies of type
, because the replicated communication forms an infinite loop. Lastly, it is key to note that
is finite for any
that does not contain replicated branches, since there is no other way for a context reduction to yield a larger type.
Knowing whether
is (in-)finite is key for our main decidability result.
Theorem 4
(Decidability of\(\textsf {beh}\)). Let
. If
is finite, then \(\varphi \) is decidable.
Proof
Since
contains all possible reductums and unfoldings of
, then conditions
and
are satisfied immediately. Therefore, to determine whether
is a safety property, we may exhaustively check all inhabitants of
against conditions
,
,
, which is decidable since
is finite (by assumption); and since subtyping and \(\textsf {frv}\) are decidable. \(\square \)
Theorem 4 states that \(\varphi \) is decidable for any
where
is a finite set. In other words, if a protocol can be shown to have a finite behavioural set, then typechecking for that protocol is decidable. This could be done manually for each protocol; however, to further increase the practicality of our type system, we present two strategies for restricting protocols into a subset of MPST! with finite behavioural sets.
Decidability Strategies. The strategies we present for restricting protocols to decidable subsets of MPST! all follow a similar blueprint. Essentially, we wish to establish properties on
with decidable approximations that imply that
is finite. Then, by Theorems 3 and 4 we obtain decidable typechecking.
The following defines, and gives examples, of each strategy; then, we show these strategies are sound and discuss how they can be approximated.
Definition 9 prevents types like
in Example 14 using a naïve approach; put simply, \(\textsf {tf}\) captures protocols where all clients of a replicated server are intrinsically non-recursive and non-replicated.
Definition 9
(Trivially finite). A context
is trivially finite,
, iff:
1.
no type in the body of a recursive binder sends to a replicated branch; and
2.
continuations of replicated branches do not send to other replicated branches.
Example 15
The protocols modelling the dining philosophers problem in Example 11 are trivially finite. Note how the chopstick services make the initial request to the lock service before they offer their replicated branch.
For other protocols we need a more nuanced strategy. Definition 10 formalises “loops” in a protocol which may result from replicated servers infinitely bouncing messages amongst each other (such as
in Example 14).
Definition 10
(Loop free). Given a protocol
, and a context
derived from
(possibly after a number of reductions), a cycle in the LTS of
is defined as the series of transitions s.t., for
where \(k \in I\), and for any
. A cyclic replicated communication path (CRCP) is defined as a cycle with these added conditions:
1.
s.t. either
or
appears after a recursive binder in
, for any
; and
2.
\(\forall x \in 1..n : \)
we have:
s.t. either
or
appears after a recursive binder in
.
We say
is loop free, written
, iff the LTS of
does not contain a CRCP.
Essentially, a cycle in the LTS of a context
: (i) starts with an incoming communication action into a replicated type; (ii) performs some intermediary transitions; and (iii) ends with the transition that began the cycle. A CRCP is a special case of a cycle, where all intermediary transitions must also be between roles that have a replicated type; or form part of the body of a recursive type. Finally, a context is loop free iff its LTS does not produce any CRCPs.
Example 16
Contexts
and
from Example 14 contain CRCPs:
contains a CRCP at
with 0 intermediary transitions; and
contains two CRCPs, at
and
, both with 1 intermediary transition forming part of a replicated type.
Example 17
The protocols in Examples 2,8,9 are loop free: Example 2 because there are no cycles; Examples 8 and 9 because the cycle between the pong branch on
(resp.
) and the ping branch on
(resp.
) includes communication with the (non-replicated/-recursive) client; breaking the CRCP.
Proposition 1
If
is infinite, then
contains a CRCP.
Proof
From the type semantics (Figure 7), we observe that the only reductions that can yield larger types are communications with replicated branches. Therefore, it follows that for
to be infinite, there must be some reoccurring transitions in the LTS of
that repeatedly communicates with a replicated branch—i.e., there is a communication action on a replicated branch, followed by any number of intermediary transitions which then end with the initial communication action on the replicated branch; where all intermediary transitions must be non-finite. This is the definition of a CRCP (Definition 10). \(\square \)
Theorem 5
(Strategy soundness). Given a context
,
implies
is finite, for \(\varPhi \in \{\textsf {tf},\textsf {lf}\}\)
Proof
Casetf. By contradiction: assume
is infinite, then, by Proposition 1,
contains a CRCP; but, by Definition 10, a CRCP will violate at least one of the conditions for tf in Definition 9—contradiction.
Caself. By contradiction: assume
is infinite, then, by Proposition 1,
contains a CRCP—contradiction; therefore
is finite. \(\square \)
Approximations. Properties tf and lf are both decidable for all protocols without first-class roles: tf can be determined via a linear traversal of a type context; and lf can be checked by constructing a directed graph of visited replicated branches in a context, then checking that the graph is acyclic (which is decidable). An approximation is only required for protocols using role variables, since their values can only be known at runtime. This approximation would treat any role variable in a selection type to have the capability of reaching any other role.
Example 18
(Approximation false negative). Consider the following protocol:
Although the above is trivially finite (
and
do not communicate), it would be falsely flagged as nottf because
is over-approximated to include
.
It is key to note that false negatives of the approximation are avoidable by requiring unique branching labels on replicated types. Furthermore, even with the approximation, all examples presented in this paper (except Example 12) are captured by either lf or tf. With respect to Example 12, the presented protocol still yields a finite behavioural set, and thus by Theorem 4 and Theorem 3, typechecking it is decidable. We aim to continue exploring further strategies (especially ones which can capture protocols such as Example 12) in future work.
4 Related Work
The MAG\(\pi \) calculus [19] makes use of generalised MPST theory in order to type failure-prone communications (i.e., message loss, reordering, and delays). Key to their approach is the use of timeouts to detect and handle message loss; as with related approaches (e.g., Barwell et al. [2]), this often means that session types are made more complex in order to handle each potential failure point. Our approach is most closely related to that of Le Brun & Dardha [4], who introduce MAG\(\pi \)! as a modification of MAG\(\pi \) to incorporate type-level replication: this has the advantage of simplifying client-server interactions by only requiring clients to handle potential failures. However, the aims of our work and that of Le Brun & Dardha [4] are significantly different: while their aim is specifically to use replication as a methodology to simplify failure handling, our work is a more fundamental study of the consequences of type-level replication on expressiveness and decidability. In particular we make use of a more standard base MPST calculus (i.e., a calculus that does not include undirected receives, nor rules that model failures and message reordering), and we make use of synchronous communication semantics. Nevertheless our calculus allows for more interesting use of replication: unlike MAG\(\pi \)! we allow nested replication and recursion, whereas MAG\(\pi \)! only allows replication at the top-level and processes must be finite. Furthermore, as a result of our inclusion of first-class roles, as well as using replication in tandem with recursion, we can type protocols that make non-trivial use of mutual exclusion and races, all of which would be inexpressible inMAG\(\pi \)!.
Toninho & Yoshida [30] assess the relative expressiveness of a multiparty session calculus and a process calculus inspired by classical linear logic, showing that MPST calculi allow strictly more expressive process networks (i.e., those that can include cycles). As part of this investigation they explore a limited form of type-level replication that permits a liveness property. However, their system does not consider first-class roles and pre-dates generalised MPST so is guided primarily by global types, and is therefore less expressive than \(\textsf {MPST!} \).
Replicated session types have been used to a limited extent in a wide variety of works on binary session types (e.g., [5, 6, 8, 32]), primarily in works pertaining to Curry-Howard interpretations of propositions as session types, where the exponential modality from linear logic !A is typically linked to replication from the \(\pi \)-calculus. Several further lines of work investigate client-server communication following this correspondence. Kokke et al. [18] investigate an extension of the logically-inspired HCP calculus [17] with two dual modalities \(!_{n}A\) and \(?_{n}A\) to type a pool of n clients and a replicated server that can service n requests respectively, and show that their calculus allows nondeterministic behaviour while still preventing deadlocks and ensuring termination. Qian et al. [23] develop CSLL (client-server linear logic) that uses the dual coexponential modalities
and
to type servers and client pools respectively, along with rules to merge client pools. The subtle difference between the
modality and the exponential !A being that the former (informally) serves type Aonly as many times as required according to client requests. This is similar to how our type system operates, given that replicated receives only pull out copies of continuations upon communication. Multiple requests induce non-determinism into further reductions; in our work this is observed through parallel types, which in the work of Qian et al. [23] is observed through hyperenvironments [12, 17]. Unlike all these works, we focus on multiparty session types, where interacting with a replicated channel spawns a process that remains in the same session. This results in our key novelty, i.e., our account of replication in the type semantics with the use of parallel types.
Marshall & Orchard [21] investigate the effects of adding a semiring graded necessity modality (a generalisation of the ! modality) to a session-typed \(\lambda \)-calculus, showing interesting consequences such as replicated servers and multicast communication. We posit that the two systems can type different protocols: while MPST! cannot straightforwardly encode multicast communication, it is difficult to see how their approach would scale to the examples we describe in Section 3.
Rocha & Caires [24] introduce CLASS, a process calculus with a correspondence to Differential Linear Logic [11]. CLASS integrates session-typed communication, reference cells with mutual exclusion, and replication. Their calculus guarantees preservation and progress, the proof of the latter property requiring a logical relation. CLASS can encode the dining philosophers problem, making essential use of shared state; in contrast our implementation relies on the interplay between replication and recursion.
Deniélou et al. [10] introduce parameterised MPST as a means of designing protocols for parallel algorithms. Their formalism allows for parameterisation of participants in the form of
, representing the \(i^{\textrm{th}}\) client from some group of n clients, for a bound n. The key difference between this formalism and MPST! is that our approach preserves, and allows for the fair handling of, races. Parameterised MPST enforce a predetermined prioritisation on the order of communication (thus, Example 12 cannot be expressed in that system).
5 Conclusion
We presented MPST!, a conservative extension of the standard multiparty session \(\pi \)-calculus which introduces for the first time replication and first-class roles, and proved its metatheory. We have shown that the interplay between replication and recursion allows us to describe interesting and previously inexpressible MPST protocols such as those that rely on races and mutual exclusion, as well as giving a method by which we can express context-free protocols. Although replication can have implications for decidability of typechecking, we have identified sufficient conditions that can determine decidability and provided syntactic approximations for decidability. For future work, it would be interesting to investigate an extension of MPST! with polymorphism, as this would improve on the modular design of protocols already promoted by the type system. Furthermore, we wish to continue exploring the decidability of typechecking to find more general approximations.
Acknowledgements
We thank the anonymous reviewers for their detailed and insightful comments. This work was supported by EPSRC Grants EP/X027309/1 (Uni-pi) and EP/T014628/1 (STARDUST).
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.
lient,
erver, and
orker respectively. The
lient, having type
, sends (
) a
uest to the
erver with payload type
, then (
) waits to receive (
) an
wer from the
orker with payload type
. The
erver, upon receiving the
uest from the
lient,
or
ards it to the
orker. Lastly the
orker, after receiving the
or
arded request from the
erver, sends the
wer to the
lient. A MPST system verifies that any written program code conforms to this specification (known as session fidelity), and that this protocol is safe—i.e., that processes send and receive messages of compatible types.
) operator to denote a replicated action, i.e., one which may occur any number of times. This makes the server agnostic to the number of requests. Second, a server now waits for requests—not from a specific client—but from any participant, binding the name of the sender to role variable
. This makes the server agnostic to the source of the requests. The server then makes a choice to forward the request to one of two workers, notably whilst passing the name of the client as one of the payloads. Finally, the server informs the client of the choice it made by sending the name of the worker in that branch. The worker type is also updated to be replicated, as it is dependent on the number of requests forwarded by the server. Notably, it receives the name of the client in the forward message, binding it to
, and uses it to send the final answer. A client may now be defined as:
, represents a collection of interconnected participants. A role is a participant in a multiparty communication protocol, and each communication endpoint
is obtained by indexing a session name with a role. In contrast to existing MPST calculi, MPST! supports first-class roles, meaning that a role may be communicated as part of a message. To this end, a role
may either be a concrete role
(e.g.,
or
in our load balancing example) or a role variable
. A name a is either an endpoint, a variable, or a role variable, whereas a value V is either a channel or a role. Binders b are used when receiving a message and can either be a variable binder or a role variable binder. Concrete values d are used when sending a message (at runtime) and are either an endpoint or a role name value.
binds session name
in process P; and \(\boldsymbol{0}\) is the inactive process.
, allowing a nondeterministic send along any \(c_i\) to role
with label \(\textsf {m}_i\) and payload \(\widetilde{V_i}\), with the process continuing as \(P_i\). Branching receive
denotes a process waiting on channel c for one of a set of messages from role
with label \(\textsf {m}_i\), binding the received data to \(\widetilde{b_i}\) before continuing according to \(P_i\). It is key to note that the object of a communication action is indicated via
(for both sending and receiving), which can either be a concrete value, or a role variable. The second key difference is the optional use of the bang ! with a branching receive, marking it as replicated—i.e., it may be used 0 or more times, modelling infinitely available servers.
.
. The first process, playing role
, offers role
a choice of message labels and associated process continuations. The second process, playing role
, sends a message with label \(\textsf {m}_k\) and transmits payloads \(\widetilde{d}\). The first process reduces to the selected continuation with the transmitted payloads substituted for the binders in the selected branch, and the second process reduces to the continuation Q.
in the replicated continuation. We refer to this as a universal receive.
in parallel with three server-side processes:
, and pulls out a copy of the server’s continuation as a new process. It is key to note that
is acting as a binder in
, therefore, in the continuation we observe a role variable substitution:
is picked.
, using rule \([\textrm{R} {-}!\textrm{C}_{1}]\) . As before, this communication advances the sender process and pulls out a copy of the worker’s continuation:
type communication endpoints. They consist of branching types
, replicated branching types
, selection types
, recursive types
and variables
, and the
type.
indicating that role
offers a choice of message labels
with payload types
and continuations
. Similarly, selection session types
indicate an internal choice towards one of a set of roles
, with a message label, given payload types and continues as the corresponding continuation type. A replicated branching type
types a replicated channel. As with processes, role
can either be a concrete role, or a role variable in binding position.
has singleton type
, used to pattern-match specific roles in payloads. Static types
are used for protocol specification, whereas runtime types
are used by the type semantics to include a notion of parallel composition at type level: originally introduced by Le Brun and Dardha [4], a type
allows a channel to be associated with multiple “active” session types.
). We further take an equi-recursive view of types, identifying a recursive type with its unfolding (i.e.,
) and require that recursion variables are guarded.
is co-inductively defined on types by the following inference rules:
.
is used to type recursive process definitions, mapping process variables X to tuples of parameter types. Context
maps channels to types, and role variable singletons. Context composition
is defined iff
and
have disjoint domains. We lift subtyping and type congruence to contexts in the usual way.
that splits a context
into two environments
and
. These environments may share variables with unrestricted types and role variables. Additionally, a channel c with runtime type
may be split such that
contains
and
contains
; this allows us to type endpoints used by different replicated processes. The inverse operation is context addition
that combines
and
into an environment
; again roles may be shared across environments. In the case that we have
(i.e., a linear variable used in two different contexts), context addition results in c having the combined runtime type
. The role insertion operation
is used when typing replicated receives and extends a context with a mapping
in the case that
is a role variable, and leaves
unchanged otherwise.
function associates a session protocol
to a concrete session
to form a typing context.
is attached to a session through the restriction operation in the form of
, dictating the protocol for
in P. A protocol
is a partial mapping from role to session type, given as:
is well-formed iff it does not contain parallel types. We obtain a typing context by associating roles in a protocol with a session name. Formally: 
.
, iff it only maps channels to session type
.
assigns type
to value V under context
and consists of four rules. Rule [T-Wkn] allows weakening: if value V has type
under some environment
, and we have an end-typed environment
such that
, then the rule allows us to conclude that V has type
under
. Rule
types concrete roles as singleton types under the empty environment, whereas
types a role variable provided that it is contained within the type environment. Finally, rule [T-Sub] types a linear variable, allowing for subtyping. Judgement
simply looks up process variable X in process environment
, returning its parameter types; this is achieved by rule [T-X] .
states that process P is typable under recursion environment
and type environment
. Rule [T-\(\boldsymbol{0}\)] types the inactive process under an end-typed environment. Rule [T-|] types parallel processes under a split environment. Rule [T-\(+\)] types an output-directed choice; since this operation uses branching control flow, each choice must be typable under the same environment.
and
type replicated and non-replicated receives respectively. In both cases the rules check that the channel has a receiving session type. Both rules check that each branch is typable by extending a common typing context with the variables bound by the receives, along with the continuation type for the session channel. In the case of a replicated receive there are two differences: first, the context used to type each branch must be end-typed (in order to avoid duplicating linear resources). Second, since the role
may be a binding occurrence of a role variable
, the context used to type each branch must be extended with the role variable (if applicable) using the insertion operator.
. As is standard in generalised MPST [27], the session protocol must satisfy a safety property \(\varphi \). We discuss specifics of this property in Section 2.3, and how it is used in Section 2.4. Informally, the property ensures that all process communication is “compatible”, and is the weakest property required to prove subject reduction. We then prove our metatheory parametric on the largest safety property, allowing it to be customised to verify more precise properties (e.g., to ensure deadlock-freedom or termination), based on the requirements of a specific protocol.
types an output if the sending channel can be mapped to a selection type with payload types that match the values being sent. The rule ensures that role
is either a value, or it exists in the type context—i.e., messages cannot be sent to unbound role variables. The selection type continuation should be used, along with the common context, to type the continuation process.
that includes the types from Example 
with LTS semantics as shown in Figure 7. Each action
denotes an output, input, and synchronising communication respectively. Context reduction
is defined iff
for some
, and we write
for the transitive and reflexive closure of
. We write
iff
for some
.
and
are standard: a context can fire an input label (resp. output label) matching any of the labels in the top-level branch type (resp. selection type). This transitions the entry to the continuation of the chosen type.
models the receipt of a message by a replicated input. The two main differences to the linear receive are: (i) the role
used in the transition label is allowed to be a role variable name; and (ii) firing an input does not advance the type, but instead pulls out a copy of the continuation and places it in parallel. Role
is considered bound in
and its continuations, but is free in pulled out copies of the continuations composed in parallel (
).
,
,
allow contexts to reduce under a larger context, or when types are guarded by recursive binders. Concretely,
allows transitions to ignore role singletons;
allows a context to perform a transition when split from a larger context (the transition result must be added back in); and
allows recursive binders to be treated equal to their unfolding.
and
model type-level communication; for simplicity and without loss of generality we assume a convention wherein session-typed payloads precede role-typed payloads. Both rules state that if a context can be split such that one part fires an output label, and the other fires an input with matching roles, message label and payloads, then the entire context can transition via a communication action. We note that payloads will consist of either session types or role singletons. For the former, sender payloads must be subtypes of the receiver payloads; for the latter, role substitution occurs after communication.
caters for universal receives, where the input label consists of a role variable in binding position—this is reflected in the role substitution. We say that a context reduces iff it can transition via communication actions.
.
above; specifically, how the substitution affects the parallel type extracted through communication, but does not affect the replicated type
. From here, there are multiple reduction paths, but let us observe the reduction path in which
communicates with
. 
and
. From here, the context reduces in a similar fashion: first the server communicates a role with the client; followed by the final communication between the client and worker.
iff:
and
are concerned with communication. They state that if two roles in the same session have an output and input type respectively which point at each other, then: (i) they should have at least one common message label; (ii) for each common label, their payloads should be equal in length; and (iii) for each common label, all session types in the payload of the sender should be subtypes of what is expected by the receiver.
requires safety to hold after the unfolding of recursive binders;
requires all role variables used in a context to be bound by that same context; and
requires safety to hold after context reduction.
, assume that
holds, or “
is safe”. Essentially, \(\varphi \) describes the minimum (and most general) safety requirements made for subject reduction to hold. This proof technique allows \(\varphi \) to be re-instantiated with more specific properties without having to reprove any of the base metatheory. (We occasionally reference properties other than safety in examples.)
with
and \(P \rightarrow P^\prime \), then
s.t.
and
with
.
, we say P:
implies a process call \({\textrm{Y}}\langle \dots ,x_i,\dots \rangle \) can only occur in Q as a subterm of a communication action over channel \(x_i\).
in
, by
iff (i) Item 1 holds for P; (ii) \(\textsf {fv}(P)\) = \(\emptyset \); (iii)
with
and
; (iv) in all subterms
of P, we have
.
communicate over a multiparty session
, with each process playing a single role. The difference in our definition to the standard is that processes
should play a single role and not a unique role. This is due to the introduction of replication in our language; note how reduction with a replicated process is guaranteed to produce multiple processes playing the same role and is reflected in our definition in condition (iii) of Item 2 , where a channel is mapped to runtime type
, allowing for parallel composition.
with
and
where each
is either \(\boldsymbol{0}\) (up-to \(\equiv \)), or only plays role
in
. Then,
implies
s.t.
, \(P \rightarrow ^* P^\prime \) and
, where
and each
is either \(\boldsymbol{0}\) (up-to \(\equiv \)), or only plays role
in
.
offers a ping service. As a convention, we will use capitals for naming services. We highlight the importance of both replication and free role names in types to be able to design modular components of a protocol—both are integral to designing a sub-protocol agnostic of the larger scope in which it is used.
label now guarantees that two sub-trees will follow.
from Example 6. We build a binary tree service
using
as shown below:
from a client. It then sends a
to the ping service, exposing a replicated branch waiting to receive the
reply. The client is now free to build the binary tree. It is key to note that any
sent to the service will subsequently forward two
requests to
. In turn, this communication will pull out two copies of the type continuation
, forcing the client to maintain the appropriate binary tree structure. For example, if a client
wishes to build a tree consisting of one root node and two leaf nodes, its type would be defined as:
.
message to
. Since both tree service types communicate with
to unroll the replicated branch
, the protocol becomes non-deterministic in a non-confluent manner and can result in deadlocked behaviour. To resolve this issue, we amend the tree service to accept a payload role which should act as a personal ping service for the client; this guarantees that the tree type is only unrolled by the client that made the initial request.
, accepts a role as a payload on the initial request to which it will issue its
s.
, where
, and the types for
are given by: 
, a copy of the recursive continuation is exposed. The recursive definition allows sequences of
and
messages to be received. It is key to note that, whilst replication maintains a top-level branch that is permanently available to receive a message, the top-level action in a recursive definition is not fixed.
. This ensures that every chopstick has its own lock that it may
and
. The lock is used to guarantee that a chopstick is only ever taken by a single philosopher at a time. A chopstick then waits for a
request from a philosopher; receiving one will result in it attempting to
the lock. This acquisition is only successful if the same role has not already requested it in some other parallel composition. If the lock was already acquired, then the
will block until the lock is released. Acquiring the lock sends an
back to the philosopher, symbolising that they have successfully obtained the chopstick. When done from eating, the philosopher may then send back a
message, which in turn releases the lock, as the chopstick is now available to be taken by a different philosopher.
has a similar type. They begin by requesting to take the chopsticks to their left and right—note that this results in every chopstick receiving two
requests. Receiving both
messages means the philosopher can eat, and subsequently
back the chopsticks. Finally, when finished, philosophers send a
to role
, acting as a clean-up for the protocol. The protocol
is safe, but fails typechecking for \(\varphi = \textit{terminating}\). In fact, the naïve protocol allows for scenarios in which all philosophers take a single chopstick, resulting in a deadlock. This problem has many solutions; we present the simplest in which philosophers take turns to eat. (Key changes are underlined.) 
ish eating before they can request to take their chopsticks. The updated protocol
now typechecks for \(\varphi =\) terminating.
sets up an auction
to accept bids from some buyers
. A merchant can employ different mechanisms for choosing who to sell to (e.g., first come first served, highest bid, biased selling, etc.); but must always respond to buyers with either a
,
, or
message. 
race to send
s to the auction service. In turn, the auction forwards bids and buyer role identifiers to the merchant, who processes bids sequentially (but still in an arbitrary order). If the merchant declines a bid, then the client is offered another chance; if the merchant accepts a bid, then it exposes a replicated receive which informs any further buyers that the product is no longer available. It is key to note that, unlike in Example 11 where we used locks to avoid race conditions, races here are not only allowed but are integral to the protocol. Additionally, by uncovering a replicated receive, the merchant enters a permanent state. These two characteristics guarantee that, no matter the selling algorithm employed by the merchant: (i) bids always arrive in a fair arbitrary order; and (ii) the product can only be sold once.
, is given by
; where \(\textsf {unf}^*\) is the closure of \(\textsf {unf}\)—a function that unfolds all top-level recursive binders in a set of contexts. (Full definitions of \(\textsf {unf}\) and \(\textsf {unf}^*\) are standard [20, Appendix D].)
is the set of (i) its reductions; and (ii) its reductions’ unfoldings. The benefit of \(\textsf {beh}\) is that it mechanically abides by conditions
and
from Definition 6. Therefore, to determine whether
is a safety property, all that is required is to exhaustively check the contexts that inhabit
against the remaining conditions of Definition 6.
. The behavioural set of
is given by:
. Moreover, any further reductions only yield contexts (and unfoldings) already captured by these two elements.
. The behavioural set of
is given by:
is infinite. This is a result of how replication and parallel composition are modelled in Figure 7. In fact, the type semantics for replicated communication allows for context reduction to yield larger types. Note how in this example, the contexts that inhabit
get infinitely larger by pulling out infinitely many copies of type
.
=
. Such a context will also pull out infinitely many copies of type
, because the replicated communication forms an infinite loop. Lastly, it is key to note that
is finite for any
that does not contain replicated branches, since there is no other way for a context reduction to yield a larger type.
is (in-)finite is key for our main decidability result.
. If
is finite, then \(\varphi \) is decidable.
contains all possible reductums and unfoldings of
, then conditions
and
are satisfied immediately. Therefore, to determine whether
is a safety property, we may exhaustively check all inhabitants of
against conditions
,
,
, which is decidable since
is finite (by assumption); and since subtyping and \(\textsf {frv}\) are decidable. \(\square \)
where
is a finite set. In other words, if a protocol can be shown to have a finite behavioural set, then typechecking for that protocol is decidable. This could be done manually for each protocol; however, to further increase the practicality of our type system, we present two strategies for restricting protocols into a subset of MPST! with finite behavioural sets.
with decidable approximations that imply that
is finite. Then, by Theorems 3 and 4 we obtain decidable typechecking.
in Example 14 using a naïve approach; put simply, \(\textsf {tf}\) captures protocols where all clients of a replicated server are intrinsically non-recursive and non-replicated.
is trivially finite,
, iff:
in Example 14).
, and a context
derived from
(possibly after a number of reductions), a cycle in the LTS of
is defined as the series of transitions s.t., for
. A cyclic replicated communication path (CRCP) is defined as a cycle with these added conditions: 
s.t. either
or
appears after a recursive binder in
, for any
; and
we have:
s.t. either
or
appears after a recursive binder in
.
is loop free, written
, iff the LTS of
does not contain a CRCP.
: (i) starts with an incoming communication action into a replicated type; (ii) performs some intermediary transitions; and (iii) ends with the transition that began the cycle. A CRCP is a special case of a cycle, where all intermediary transitions must also be between roles that have a replicated type; or form part of the body of a recursive type. Finally, a context is loop free iff its LTS does not produce any CRCPs.
and
from Example 14 contain CRCPs:
contains a CRCP at
with 0 intermediary transitions; and
contains two CRCPs, at
and
, both with 1 intermediary transition forming part of a replicated type.
(resp.
) and the 
(resp.
) includes communication with the (non-replicated/-recursive) client; breaking the CRCP.
is infinite, then
contains a CRCP.
to be infinite, there must be some reoccurring transitions in the LTS of
that repeatedly communicates with a replicated branch—i.e., there is a communication action on a replicated branch, followed by any number of intermediary transitions which then end with the initial communication action on the replicated branch; where all intermediary transitions must be non-finite. This is the definition of a CRCP (Definition 10). \(\square \)
,
implies
is finite, for \(\varPhi \in \{\textsf {tf},\textsf {lf}\}\)
is infinite, then, by Proposition 1,
contains a CRCP; but, by Definition 10, a CRCP will violate at least one of the conditions for tf in Definition 9—contradiction.
is infinite, then, by Proposition 1,
contains a CRCP—contradiction; therefore
is finite. \(\square \)
and
do not communicate), it would be falsely flagged as not tf because
is over-approximated to include
.
and
to type servers and client pools respectively, along with rules to merge client pools. The subtle difference between the
modality and the exponential !A being that the former (informally) serves type A only as many times as required according to client requests. This is similar to how our type system operates, given that replicated receives only pull out copies of continuations upon communication. Multiple requests induce non-determinism into further reductions; in our work this is observed through parallel types, which in the work of Qian et al. [23] is observed through hyperenvironments [12, 17]. Unlike all these works, we focus on multiparty session types, where interacting with a replicated channel spawns a process that remains in the same session. This results in our key novelty, i.e., our account of replication in the type semantics with the use of parallel types.
, representing the \(i^{\textrm{th}}\) client from some group of n clients, for a bound n. The key difference between this formalism and MPST! is that our approach preserves, and allows for the fair handling of, races. Parameterised MPST enforce a predetermined prioritisation on the order of communication (thus, Example 12 cannot be expressed in that system).
