Das Kapitel vertieft die Herausforderungen und Lösungen im Zusammenhang mit der Typisierung von Mehrparteien-Sitzungen (MPST) in Multithreadprogrammen, wobei die Grenzen der Abstraktionen zur Nachrichtenweitergabe hervorgehoben werden. Es führt MPST als Methode ein, um die Sicherheit und Lebendigkeit von Kommunikationsprotokollen zu gewährleisten, und beschreibt den Prozess der Spezifizierung von Protokollen als Verhaltenstypen und die Typüberprüfung von Implementierungen anhand dieser Spezifikationen. Die wichtigste Innovation ist die mpst.embedded-Bibliothek, die Scalas Match-Typen nutzt, um globale und lokale Typen direkt in die Sprache einzubetten. Dieser Ansatz beseitigt die mit externen DSLs verbundenen programmatischen Reibungen und vermeidet undichte Abstraktionen, indem globale und lokale Typen als erstklassige Bürger behandelt werden. Das Kapitel bietet einen detaillierten Überblick über mpst.embedded, einschließlich grundlegender und fortgeschrittener Funktionen wie Full Merge, Delegierung und allgemeine globale Typen. Außerdem werden die technischen Details der Einbettung von MPST in Scala diskutiert, einschließlich Projektions- und Typenprüfungsmechanismen. Der Evaluierungsteil bestätigt die praktische Durchführbarkeit von mpst.embedded durch systematische Messungen der Typenprüfzeiten und die Erforschung seiner Aussagekraft. Das Kapitel schließt mit einem Vergleich zu verwandten Arbeiten und einem Ausblick auf zukünftige Erweiterungen der MPST-Theorie, die in mpst.embedded. aufgenommen werden könnten.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Multiparty session typing (MPST) is a method to make concurrent programming simpler. The idea is to use type checking to automatically detect safety and liveness violations of implementations relative to specifications. In practice, the premier approach to combine MPST with mainstream languages—in the absence of native support—is based on external DSLs and associated tooling.
In contrast, we study the question of how to support MPST by using internal DSLs. Answering this question positively, this paper presents the mpst.embedded library: it leverages Scala’s lightweight form of dependent typing, called match types, to embed MPST directly into Scala. Our internal-DSL-based approach avoids programming friction and leaky abstractions of the external-DSL-based approach for MPST.
1 Introduction
Background With the advent of multicore processors, multithreaded programming—a notoriously error-prone enterprise—has become increasingly important.
Because of this, mainstream languages have started to offer core support for higher-level communication primitives besides lower-level synchronisation primitives (e.g., Clojure, Go, Kotlin, Rust). The idea has been to add message passing as an abstraction for shared memory, as—supposedly—channels are easier to use than locks. Yet, empirical research shows that “message passing does not necessarily make multithreaded programs less error-prone than shared memory” [33].
Anzeige
One of the core challenges is as follows: given a specification S of the communication protocols that an implementation I should fulfil, how to prove that I is safe and live relative to S? Safety means “bad” communication actions never happen: if a communication action happens in I, then it is allowed to happen by S. Liveness means “good” communication actions eventually happen.
Multiparty session typing (MPST) MPST [16] is a method to automatically prove safety and liveness of communication protocol implementations relative to specifications. The idea is to write specifications as behavioural types [1, 19] against which implementations are type-checked. Formally, the central theorem is that well-typedness at compile-time implies safety and liveness at run-time. Over the past 10–15 years, much progress has been made, including the development of many tools to combine MPST with mainstream languages (e.g., F# [29], F\(^\star \) [36], Go [5], Java [17, 18], OCaml [20], Rust [26, 27], Scala [2, 6, 12, 30], and TypeScript [28]). Fig. 1 visualises the idea behind MPST in more detail:
Fig. 1:
MPST
Fig. 2:
A few possible runs of the Negotation protocol
1.
First, a protocol among roles \(r_1, \ldots , r_n\) is implemented as a session of processes \(P_1, \ldots , P_n\) (concrete), while it is specified as a global typeG (abstract). The global type models the behaviour of all processes together.
2.
Next, G is decomposed into local types \(L_1, \ldots , L_n\) by projectingG onto each role. Each local type models the behaviour of one process alone.
3.
Last, safety and liveness are verified by type-checking each \(P_i\) against \(L_i\).
Example 1
The Negotiation protocol, originally defined in the MPST literature by Neykova et al. [29], consists of roles Alice and Bob. Fig. 2 shows three possible runs. First, a proposal is communicated from Alice to Bob. Next, its acceptance, rejection, or a counter-proposal is communicated from Bob to Alice. Next:
In case of an acceptance, a confirmation is communicated from Alice to Bob.
In case of a rejection, the protocol ends.
In case of a counter-proposal, its acceptance, rejection, or another counter-proposal is communicated from Alice to Bob. And so on.
Anzeige
The following recursive global type specifies the protocol:
Global type
specifies the communication of a value of data type \(t_i\) from role p to role q, followed by \(G_i\), for some \({1} {\le } {i} {\le } {n}\); we omit braces when \({n} {=} {1}\). Global type \(\checkmark \) specifies termination. The following recursive local type, projected from the global type, specifies Bob (Alice is similar):
Local types
and
specify the send and receive of a value of data type \(t_i\) from role p to role q, followed by \(L_i\), for some \({1} {\le } {i} {\le } {n}\); we omit braces when \({n} {=} {1}\). Local type \(\checkmark \) specifies termination. The following process, well-typed by the local type, implements a version of Bob:
Process
implements the send of the value of expression e from role p to role q, followed by P, in session x. Process
implements the receive of a value of data type \(t_i\) into variable \(x_i\), followed by \(P_i\), in session x, for some \({1} {\le } {i} {\le } {n}\); we omit braces when \({n} {=} {1}\). Process \(\textbf{0}\) implements termination. Processes \(\textbf{loop}_{x}{P}\) and \(\textbf{recur}_{x}\) implement iteration in session x. \(\square \)
Fig. 3:
Workflow of external-DSL-based MPST tools
In practice [34], the premier approach to combine MPST with mainstream languages—in the absence of native support—is based on: (1) external DSLs1 to write global types; (2) associated tooling to generate corresponding code in mainstream languages, including Scribble [17, 18], its extensions [5, 8, 9, 26‐30, 36], StMungo [25], mpstpp [24], \(\upnu \)Scr [35], Pompset [6], Teatrino [2], and Oven [12].
The key ideas of the external-DSL-based approach were originally conceived by Deniélou, Hu, and Yoshida. It is based on two insights: local types can be interpreted as finite-state machines (FSM) [10, 11], where states and transitions model sends and receives; FSMs can be encoded as object-oriented application programming interfaces (API) [17, 18], where classes and methods model states and transitions. Fig. 3 visualises the workflow. First, the programmer writes a global type in a DSL; this is the input of the MPST tool. Next, the MPST tool projects the global type to local types, interprets the local types as FSMs, and encodes the FSMs as APIs in the mainstream language; this is the output of the MPST tool. Last, the programmer uses the APIs to write processes.
Fig. 4:
Global type for Negotation (Scribble)
Fig. 5:
FSM for Bob
Fig. 6:
Callback-based API for Bob (Scala)
Fig. 7:
Process for Bob
Example 2
Fig. 4 shows a global type for Negotiation (cf. G in Exmp. 1), written in the external DSL of Scribble. Statement
specifies the communication of a value of data type t from p to q. Statement
specifies a choice among \(G_1, \ldots , G_k\) made by r.
Fig. 5 shows the FSM for Bob, derivable from Fig. 4. Transition labels
and \(pq \text {?}t\) specify the send and receive of a value of data type t from p to q.
Fig. 6 shows a callback-based API for Bob in Scala, derivable from Fig. 5. Trait
in the API corresponds with state i of the FSM; methods of trait
correspond with transitions of state i. Traits
and
also extend trait
to be able to start callback-based iteration in states 2 and 3 (i.e., these are the only states on a cycle in the FSM) in a type-sound manner. We note that each method and each callback returns a value of type
to ensure that the program can terminate only when the final state has been reached.
To demonstrate the usage of the API, Fig. 7 shows a process for Bob (cf. P in Exmp. 1). The idea is to write a function,
, that consumes an “initial state object”
as input and produces a “final state object”
as output. First, the only communication action that can be performed, is the one for which
has a method (receiving). When that method is called, the actual receive is performed, and the callback is called with the received value
and a fresh “successor state object”
. Next, the only communication actions that can be performed, are the ones for which
has a method (sending). And so on. \(\square \)
This work The external-DSL-based approach is well-established in the MPST literature: it is used in all MPST tools [5, 6, 8, 9, 12, 17, 18, 20, 24‐30, 35, 36] that support classical MPST as in Fig. 1 (global types and projection; fully automatic; static up-to linearity). However, despite the major impact, it has two weaknesses:
Programming friction: The usage of an external DSL to specify protocols as global types causes programming friction. In general, this is a well-documented issue with external DSLs (e.g., [13]): new syntax needs to be learned; new tools to edit DSL code need to be adopted; extra effort is needed to intermix DSL code with the mainstream language.
Leaky abstractions: As demonstrated in Exmp. 2, APIs generated by MPST tools leak internal details: global types are essentially declarative, whereas the FSMs that seep through the APIs are essentially imperative. This representational gap causes dissonance between the level of abstraction at which global types are produced by the programmer (before API generation), and the level of abstraction at which local types are consumed by that same programmer in terms of FSMs (after API generation).
To avoid these weaknesses, we explore a different approach and study the question of how to support classical MPST by using internal DSLs. Answering this question positively, we present the mpst.embedded library: it leverages Scala’s “lightweight form of dependent typing” [3], called match types, to embed global/local types directly into Scala. As a result, mpst.embedded offers a frictionless interface between global/local types and processes (i.e., no new syntax, editors, or other tools need to be adopted). Moreover, mpst.embedded avoids leaky abstractions by not relying on FSMs; global/local types are first-class citizens.
In this way, mpst.embedded is the first internal-DSL-based MPST tool that supports all key aspects of classical MPST as in Fig. 1 (unlike Imai et al. [20], who do not support n-ary choice and require extra manual work to guide projection). This is a significant contribution, because: (a) internal DSLs have advantages over external DSLs, but (b) it is far from obvious how to build an internal DSL for MPST in a mainstream language without native support for session types.
Technically, to apply classical MPST and offer static guarantees, some form of compile-time computation is needed. This is the role of match types. They are essentially match expressions at the type level, which are evaluated by the Scala compiler as part of its static analysis, and which we use in this work to embed MPST theory. That is, the Scala compiler can check the typing rules of MPST theory by evaluating carefully crafted match types.
First, through extensive examples, we give an overview of the capabilities of mpst.embedded (Sect. 2 and Sect. 3). Next, we present technical details (Sect. 4). Last, we conclude this paper with related work and future work (Sect. 5).
Fig. 8:
Correspondence between mpst.embedded (left) and MPST theory (right)
2 A Tour of mpst.embedded: Basic Features
Global types Fig. 8 (top rows) shows the correspondence between global types in mpst.embedded and in MPST theory. In mpst.embedded, each global type G is built from classes
,
,
, and
. The third type parameter of
is an n-ary product type, called “the branches”. Type parameter X of
is bound in type parameter G to the whole
, to embed a recursive type. Each role p or q, and each recursion variable X, is a Scala string literal type (e.g.,
is a type with one inhabitant,
). Each data type t is a Scala type.
Fig. 9:
Global type for Negotiation
Fig. 10:
Local type for Bob
Fig. 11:
Processes for Alice and Bob
Example 3
Fig. 9 shows a global type for Negotiation (cf. G in Exmp. 1). \(\square \)
Local types and projection Fig. 8 (middle rows) shows the correspondence between local types in mpst.embedded and in MPST theory. We add that local types can be computed from global types fully automatically and statically via type
: the Scala compiler reduces
to the projection of G onto r.
Example 4
Fig. 10 shows a local type for Bob (cf. \(L_{\texttt{b}}\) in Exmp. 1). Alternatively, it can be computed by having the Scala compiler reduce
. \(\square \)
Processes and type checking Fig. 8 (bottom rows) shows the correspondence between processes in mpst.embedded and in MPST theory. In mpst.embedded, each process is a sequence of calls to methods
,
,
, and
of class
. This generic class has two type parameters: one to represent a role (enacted by the process), and another one to represent a local type (with which the process must comply). In turn, instances of
are obtained through calls to method
of class
. This generic class has one type parameter to represent a global type (with which all processes must comply). Method
consumes a role, initialises the session for it, and produces a
object for it. Calls to
are blocking: they return only when all processes have called
.
Intuitively,
and
objects represent executable sessions from the global and local perspective, leveraging the same abstractions as the global and local types by which they are parametrised (no leaky abstractions).
Example 5
Fig. 11 shows processes for Alice and Bob on lines 1–19 and 21–31 (cf. P in Exmp. 1), plus session initiation on lines 33–35. We make three remarks:
The process for Bob looks similar to Fig. 7. However, Fig. 11 is defined in terms of communication actions in a session (
objects), whereas Fig. 7 is defined in terms of transitions of an FSM (
objects).
The process for Bob exactly mimics the recursive structure of local type
. Such mimicry is not a general requirement for well-typed processes, as demonstrated by the process for Alice: instead of exactly mimicking the recursive structure of
(which has a similar recursive structure as
in Fig. 9), it mimics two unfoldings of
, followed by termination. That is, lines 5–15 in Fig. 11 comply with the first unfolding, while lines 16–19 comply with the second unfolding, without entering a loop. \(\square \)
Using mpst.embedded, the Scala compiler statically checks for each call \(\alpha \) on a
object, parametrised by local type L, whether or not \(\alpha \) complies with L. If not, the Scala compiler reports an error. In this way, mpst.embedded assures that well-typedness at compile-time implies safety and liveness at run-time, modulo linear usage of
objects (checked dynamically), and modulo non-terminating/exceptional behaviour (unchecked). These two provisos are standard for MPST tools. As the type parameters of
objects are erased at compile-time, only generic
objects exist at run-time.
Example 6
The following protocol violations are reported at compile-time:
In Fig. 11, replace line 29 with one of the following:
In Fig. 11, uncomment line 26 and replace line 31 with:
The following protocol violation is reported as an error at run-time:
The technical report [22] contains a screenshot of error reporting. \(\square \)
Besides protocol violations, additionally, basic well-formedness violations of global types are reported as errors at compile-time; they are checked as part of the instantiation of generic class
(e.g., Fig. 11, line 33). For instance, for
, we always require \(p \ne q\) and \(n \ge 1\).
3 The Tour, Continued: Advanced Features
Full merging To project global types, an auxiliary partial operator to merge local types—the projections—is needed. There are two variants [31]: “plain” (basic) and “full” (advanced). Plain merge is relatively easy to support, but it works for few local types, so many global types cannot be projected. Conversely, full merge works for many local types, but it is relatively hard to support. For instance, Imai et al. [20] support only manual full merge (i.e., the programmer must write extra protocol-specific code to guide the computation of projections). In contrast, mpst.embedded supports automatic full merge via type
: the Scala compiler reduces
to the full merge of \(L_1\) and \(L_2\).
Fig. 12:
Global type for Two-Buyer
Fig. 13:
Local type for Seller
Fig. 14:
Process for Seller
Fig. 15:
Global types for Three-Buyer
Fig. 16:
Process for Buyer2
Fig. 17:
Process for Buyer3
Example 7
The Two-Buyer protocol, originally defined in the MPST literature by Honda et al. [16], consists of roles Buyer1, Buyer2, and Seller: “[Buyer1 and Buyer2] wish to buy an expensive book from Seller by combining their money. Buyer1 sends the title of the book to Seller, Seller sends to both Buyer1 and Buyer2 its quote, Buyer1 tells Buyer2 how much she can pay, and Buyer2 either accepts the quote or rejects the quote by notifying Seller.” We use an extended version defined by Coppo et al. [7], in which Buyer2 notifies not only Seller about acceptance/rejection, but also Buyer1. In the case of acceptance, Buyer2 sends his address to Seller, and Seller sends back the delivery date to Buyer2.
Fig. 12 and Fig. 13 show a global type for Two-Buyer and a local type for Seller (split into
/
and
/
for presentational reasons.) First, we note that the communication from Buyer1 to Buyer2 on line 5 in the global type has no counterpart on line 5 in the local type; as Seller does not participate in the communication, it is simply skipped in the projection. Second, we note that the communication from Buyer2 to Buyer1 on line 9 in the global type is ignored, too, but the projections of the two branches do need to be combined into one. This is achieved by having the Scala compiler reduce
to
.
Fig. 14 shows a process for Seller. It demonstrates that merging is a type-level concept, hidden from the programmer: the Scala compiler reduces
and type-checks the code against the result transparently. \(\square \)
Delegation Sessions are higher-order:
object
for a first session can be delegated between processes via
object
for a second session, by sending
via
. In the presence of delegation, within each session, well-typedness at compile-time continues to imply safety and liveness at run-time (modulo the “two provisos”; page 8). However, between sessions, liveness is not assured; supporting this would require substantial extra technical machinery [7], so none of the existing MPST tools support it.
Example 8
The Three-Buyer protocol, originally defined in the MPST literature by Coppo et al. [7], consists of roles Buyer1, Buyer2, Buyer3, and Seller. It resembles the Two-Buyer protocol, except that Buyer2 can ask Buyer3 to enact his role on his behalf—unbeknownst to Buyer1 and Seller—through delegation.
Fig. 15 shows global types for Three-Buyer. Global type
specifies the first sub-protocol among Buyer1, Buyer2, and Seller; it is identical to the global type for Two-Buyer. Global type
specifies the second sub-protocol between Buyer2 and Buyer3. Notably, line 8 specifies the delegation from Buyer2 to Buyer3.
Fig. 16 shows a process for Buyer2: on lines 1–4,
objects for two sessions are consumed as inputs (to engage in two sub-protocols); on lines 5–6, the first session is used; on lines 7–10, the second session is used; on line 8, the remainder of the first session is delegated via the second session. Similarly, Fig. 17 shows a process for Buyer3: on lines 1–3, a
object for the first session is consumed as input; on line 5, a
object for the second session is received.
The process for Seller is exactly the same in Three-Buyer as in Two-Buyer (Fig. 14). In particular, Seller does not know that it communicates with Buyer3 instead of Buyer2. Thus, delegation is hidden from each role not involved. \(\square \)
Generic global types By embedding global/local types as Scala types, Scala’s built-in mechanism of type parametrisation is readily available. This allows the programmer to write generic global types with type parameters for roles (common in external-DSL-based MPST tools) and sub-protocols (novel of mpst.embedded).
Fig. 18:
Generic global types for Negotiation
Example 9
To alleviate the repetitive feel of Fig. 9, Fig. 18 shows generic global types that leverage type parameters. Type
generically specifies the communication of an acceptance, rejection, or counter-proposal from
to
(type parameters for roles), followed by
(type parameter for a sub-protocol) in case of a counter-proposal; it can be instantiated twice to replace lines 5–7 and lines 8–10 in Fig. 9. This is done in type
, which generically specifies a role-parametric version of the whole
in Fig. 9. Thus,
is equivalent to
in Fig. 9. \(\square \)
Consistencympst.embedded also supports explicit consistency checking of sets of local types. Details can be found in the technical report [22], as they are rather technical/subtle. We do evaluate consistency checking times in Sect. 4.3, though.
4 Technical Details
As mpst.embedded closely follows MPST theory, and as it uses unique parts of the Scala type system, first, we summarise a few essential preliminaries (Sect. 4.1). Next, we describe our embedding of MPST into Scala (Sect. 4.2).
This section focusses on the basic features of Sect. 2. It allows us to keep the necessary background on MPST theory simple and succinct, while still being able to explain the general ideas of the embedding into the Scala type system in sufficient depth. The advanced features of Sect. 3 are based on more complex theoretical concepts, but their embedding follows similar general ideas.
Fig. 19:
Projection in MPST theory
Fig. 20:
Type checking in MPST theory (excerpt)
4.1 Preliminaries
MPST theory We summarise the theory behind classical MPST (Fig. 1):
Global types, local types, and processes: The syntax was defined and explained in Fig. 8 (right column) and Exmp. 1.
Projection: Let \(G \mathbin {{\upharpoonright }}r\) denote the projection of G onto r; it is defined in Fig. 19. The projection of a communication yields a send if r is the sender, a receive if r is the receiver, or the full merge—denoted by \(\sqcap \)—of the projected branches otherwise (i.e., r does not participate in the communication).
Type checking: Let \(\varGamma \mathrel {{\vdash }} P\) denote well-typedness of P in typing environment \(\varGamma \); it is defined in Fig. 20. Rule [Send] states that a send from p to q in x is well-typed when the local type of x specifies a send, e is well-typed by \(t_j\), and P is well-typed after setting the local type of x to \(L_j\) in the typing environment, for some j. Rule [Recv] states that a receive from p to q in x is well-typed when the local type of x specifies a receive, and \(P_i\) is well-typed after setting the local type of x to \(L_i\) in the typing environment, for each i. Thus, there is asymmetry: for sending, only one send specified must be implemented, but for receiving, each receive specified must be implemented.
Central theorem: Static well-typedness implies dynamic safety and liveness.
Match types in Scala The main feature of the Scala type system that we take advantage of in mpst.embedded is match types. We explain it with an example. Suppose that we need to write a function to convert
s and
s:
However, return type
is not precise enough. For instance, the Scala compiler fails to prove that
is safe, as it cannot infer that
is
. What is missing, is a relation between the actual type of
(e.g.,
) and the return type (e.g.,
). Match types define such relations.
1.
First, we redefine the signature of
as follows:
Thus, we introduce a type parameter
(subtype of
) and declare
to be
. Also, we declare the return value to be of match type
.
2.
Next, the idea is to define
in such a way that the relation between the actual type of
and the return type can be inferred, as follows:
The Scala compiler reduces every occurrence of
to
or
, depending on the instantiation of
(e.g.,
is reduced to
).
3.
Last, for instance, the Scala compiler correctly succeeds/fails to type-check
(safe) and
(unsafe).
Thus, match types are a “lightweight form of dependent typing” [3], to perform “type-level programming”. In the remainder, we use the following built-ins:
and
reduce to
and
.
reduces to
. We note that
can be a type lambda of the form
.
4.2 Embedding MPST into Scala
Global types, local types, processes As explained in Sect. 2, and as shown in Fig. 8, global types and local types are implemented as classes, while processes are implemented as methods of class
. The communication infrastructure for processes is based on concurrent queues. However, a transport layer for distributed processes is also possible (orthogonal concern).
Fig. 21:
Projection in mpst.embedded
Projection Fig. 21 shows match type
. It is used to have the Scala compiler fully automatically and statically compute local types (e.g., line 2 in Fig. 11).
Match type
has two type parameters: a global type
and a role
(cf. \(G \mathbin {{\upharpoonright }}r\)). To reduce
, the Scala compiler matches
to a global type constructor, and it produces a local type exactly as defined in Fig.19. By convention, lower case letters in patterns are type variables; they are bound to types as part of the matching algorithm. For instance, on lines 3–5 in Fig. 21,
is bound to a product type of the form
, where each
is a data type, and each
is a global type. When
is passed to
on lines 3–4, it is converted into
. Alternatively, when
is passed to
on line 5, it is converted into
, which is subsequently passed to
; this is a helper match type that reduces to the full merge of all local types in the product type.
Fig. 22:
Type checking in mpst.embedded (excerpt)
Type checking Fig. 22 shows an excerpt of class
related to type checking. The idea is to have the Scala compiler reduce match types
and
to fully automatically and statically compute the expected types of the callback arguments of methods
and
, given a local type L. The reduction succeeds, and the actual callback argument is well-typed by the expected type, if, and only if, the communication action is well-typed by Lexactly as defined in Fig.20. Otherwise, the Scala compiler reports an error. In this way, mpst.embedded implements the same MPST typing rules as in Fig. 20 in terms of Scala match type reduction, and it provides the same assurances (modulo the “two provisos”; page 8):
if, at compile-time, each process is well-typed by its projection,
then, at run-time, the session of all processes is safe and live,
modulo linear usage of
objects (checked dynamically),
We now explain
and
. Regarding
, Fig. 20 states that a send is well-typed if the local type specifies it directly (rule [Send]) or indirectly (rule [Unfold]). These cases correspond precisely to the two cases in
:
Lines 6–7 state that a send is well-typed if the sender, receiver, and data type match the send of the local type
, and if the callback is a function that consumes a
object, parametrised by the selected branch of
, namely
. We note that
reduces to
.
Line 8 states that a send is also well-typed when it is well-typed by the unfolding of the local type. We note that
reduces to a version of
in which each occurrence of
is replaced with
.
Regarding
, similarly, Fig. 20 states that a receive is well-typed if the local type specifies the receive directly (rule [Recv]) or indirectly (rule [Unfold]). Due to the asymmetry between sends and receives,
(singular) reduces to a single function type, while
(plural) reduces to a product of function types, computed using
. Besides that, they follow the same ideas.
4.3 Evaluation and Discussion
Compile-time performance To validate the practical feasibility of using mpst.embedded, we systematically measured the type checking times during non-incremental compilation of all examples in Sect. 2 and Sect. 3, as well as twelve additional examples from the MPST literature [7, 30, 31] and the Scribble repository [14].2 This is a representative set of protocols, previously developed by other researchers (including the protocols in our examples in Sect. 2 and Sect. 3), of various sizes, that exercise all aspects of classical MPST theory.3
To measure only the protocol-related type checking times, the processes contained almost no computation code; just communication actions in compliance with the protocol. The measurements were obtained using an Intel i7-8569U processor (4 physical/4 virtual cores at 2.8 GHz) and 16 GB of memory, running macOS 14.0, OpenJDK 18.0.2, and Scala 3.3.1. We ran the measurements with consistency checking disabled and enabled, to be able to study the difference.
Table 1.
Type checking times in milliseconds, reported as \(\mu \pm \sigma \), where \(\mu \) is the average (of 31 measurements), and where \(\sigma \) is the standard deviation
\(^\dagger \) The difference between type checking times without consistency \(\mu _1 \pm \sigma _1\) and with consistency \(\mu _2 \pm \sigma _2\) are reported as \(\mu \pm \sigma \), where \(\mu = \mu _2 - \mu _1\) and \(\sigma = \sqrt{\sigma _1^2 + \sigma _2^2}\)
Table 1 shows the results, averaged over 31 runs per protocol. We make two main observations. First, without consistency checks, the type checking times seem sufficiently low for the usage of mpst.embedded to be practically feasible: less than two seconds for the biggest protocol in our benchmark set (SMTP). Moreover, our measurements were obtained using non-incremental compilation and, as such, constitute an upper bound on the expected type checking delays when using incremental compilation. Anecdotally, in our development environment (Visual Studio Code 1.87 with the Metals 1.30 extension for Scala programming), when using incremental compilation, the type checking delays were significantly lower (\({<}100\) ms) than those in Table 1, and not disruptive at all.
Second, with consistency checks (i.e., five examples violate consistency; this was expected), the results show that some overhead is added, but it does not make the usage of mpst.embedded infeasible (\({<}500\) ms). Also, when using incremental compilation, the type checking delays continued to not get in the way.
Experience The implementation of the benchmark set turned out to be, in its own right, a validation activity to experience whether or not the type checker catches all mistakes in practice. This is because, until a protocol implementation is finished, it does not comply with the specification yet. Thus, all until the end, the type checker reports errors to point out missing pieces. This guidance by the type checker effectively prevented us from making unintended programming mistakes, especially when writing the implementations of HTTP and SMTP (which are the more complicated protocols in our benchmark set). It would be interesting to try to reproduce these anecdotal findings in a larger user study.
Expressiveness Our benchmark set shows that mpst.embedded is feature-complete relative to classical MPST theory,\(^\text {3}\) with full merging (e.g., the OAuth2 fragment requires full merge), as intended. Moreover, while the ability to write generic global types does not add expressive power in the formal sense, it enables better reuse of global types and serves as an abstraction/composition mechanism: it allows large protocols to be split into separate smaller sub-protocols—specified as generically as possible to maximise the opportunity for reuse—which can then be “invoked” from each other with concrete arguments. Such generic sub-protocols can also be packaged into libraries and shared between projects.
5 Conclusion
Related work Closest to our approach in this paper is the work by Imai et al. [20]. They developed an internal DSL in OCaml to specify protocols and verify processes based on MPST. However, their tool does not support all key aspects of classical MPST as in Fig. 1: it supports only binary choices instead of n-ary choices (e.g., Exmp. 1, which has ternary choices, is not supported), and it is not fully automatic (i.e., Imai et al. require the programmer to manually write extra protocol-specific code to project global types). In contrast, mpst.embedded supports n-ary choices and is fully automatic.
Another related tool is the Discourje library [15], which offers an MPST-based internal DSL in Clojure. However, Discourje does all verification dynamically, whereas mpst.embedded performs all verification statically up-to linearity.
There are four existing tools to combine MPST with Scala: Scribble-Scala [30], Pompset [6], Teatrino [2], and Oven [12]. Table 2 summarises the differences:
DSLs to specify protocols as global types: Scribble-Scala, Pompset, and Teatrino are based on the external DSL of Scribble, while Oven is based on an external DSL for regular expressions.
Projection of global types: Scribble-Scala, Pompset, and Teatrino apply the classical structural projection operator (defined in terms of the syntax of global types; Sect. 4.2), while Oven applies a non-classical behavioural projection operator (defined in terms of the operational semantics of global types). The latter has additional expressive power to support the usage of regular expressions as global types [23].
Interpretation of local types: Different from Fig. 3, Pompset uses partially-ordered multisets instead of FSMs as an intermediate operational model, while Teatrino directly encodes local types as APIs in Scala.
Encoding as APIs: The APIs generated by Scribble-Scala and Teatrino are built on top of the existing libraries lchannels and Effpi (discussed in more detail below), while Pompset and Oven do not rely on such existing libraries.
Besides these existing tools to combine multiparty session typing with Scala (including global types and projection), there also exist libraries to combine binary session typing with Scala (excluding global types and projection), namely lchannels [30] and Effpi [32]. Conceptually, as mpst.embedded targets multiparty instead of binary, it is not really comparable to lchannels and Effpi. Technically, moreover, lchannels and Effpi do not use match types.
Future work Many extensions of MPST theory have been proposed. We are keen to explore which of them can be incorporated in mpst.embedded using match types. For instance, an important feature that we believe is compatible with mpst.embedded and match types is parameterised MPST with indexed roles as developed by Castro et al. [5]. Another feature that seems representable using match types, is MPST with refinements along the lines of Zhou et al. [36]. In contrast, a feature that seems prohibitively difficult to incorporate, is timed MPST [4]: match types seem unsuitable to statically offer real-time guarantees.
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.
A domain-specific language (DSL) is either external or internal. External DSLs are stand-alone languages with their own dedicated syntax, while internal DSLs are embedded languages into a general-purpose language (GPL) with syntax inherited from that GPL. Both approaches have advantages and disadvantages [13].
Run-time performance (e.g., latency/throughput) depends on the transport mechanism for message passing, which is orthogonal to the contributions of this paper.
That is, the theory as originally defined by Honda et al. [16], but presented in the more recent style of, e.g., Scalas–Yoshida [31], including the full merge operator.
specifies the communication of a value of data type \(t_i\) from role p to role q, followed by \(G_i\), for some \({1} {\le } {i} {\le } {n}\); we omit braces when \({n} {=} {1}\). Global type \(\checkmark \) specifies termination. The following recursive local type, projected from the global type, specifies Bob (Alice is similar):
and
specify the send and receive of a value of data type \(t_i\) from role p to role q, followed by \(L_i\), for some \({1} {\le } {i} {\le } {n}\); we omit braces when \({n} {=} {1}\). Local type \(\checkmark \) specifies termination. The following process, well-typed by the local type, implements a version of Bob: 
implements the send of the value of expression e from role p to role q, followed by P, in session x. Process
implements the receive of a value of data type \(t_i\) into variable \(x_i\), followed by \(P_i\), in session x, for some \({1} {\le } {i} {\le } {n}\); we omit braces when \({n} {=} {1}\). Process \(\textbf{0}\) implements termination. Processes \(\textbf{loop}_{x}{P}\) and \(\textbf{recur}_{x}\) implement iteration in session x. \(\square \)
specifies the communication of a value of data type t from p to q. Statement
specifies a choice among \(G_1, \ldots , G_k\) made by r.
and \(pq \text {?}t\) specify the send and receive of a value of data type t from p to q.
in the API corresponds with state i of the FSM; methods of trait
correspond with transitions of state i. Traits
and
also extend trait
to be able to start callback-based iteration in states 2 and 3 (i.e., these are the only states on a cycle in the FSM) in a type-sound manner. We note that each method and each callback returns a value of type
to ensure that the program can terminate only when the final state has been reached.
, that consumes an “initial state object”
as input and produces a “final state object”
as output. First, the only communication action that can be performed, is the one for which
has a method (receiving). When that method is called, the actual receive is performed, and the callback is called with the received value
and a fresh “successor state object”
. Next, the only communication actions that can be performed, are the ones for which
has a method (sending). And so on. \(\square \)
,
,
, and
. The third type parameter of
is an n-ary product type, called “the branches”. Type parameter X of
is bound in type parameter G to the whole
, to embed a recursive type. Each role p or q, and each recursion variable X, is a Scala string literal type (e.g.,
is a type with one inhabitant,
). Each data type t is a Scala type.
: the Scala compiler reduces
to the projection of G onto r.
. 
,
,
, and
of class
. This generic class has two type parameters: one to represent a role (enacted by the process), and another one to represent a local type (with which the process must comply). In turn, instances of
are obtained through calls to method
of class
. This generic class has one type parameter to represent a global type (with which all processes must comply). Method
consumes a role, initialises the session for it, and produces a
object for it. Calls to
are blocking: they return only when all processes have called
.
and
objects represent executable sessions from the global and local perspective, leveraging the same abstractions as the global and local types by which they are parametrised (no leaky abstractions).
. Such mimicry is not a general requirement for well-typed processes, as demonstrated by the process for Alice: instead of exactly mimicking the recursive structure of
(which has a similar recursive structure as
in Fig. 9), it mimics two unfoldings of
, followed by termination. That is, lines 5–15 in Fig. 11 comply with the first unfolding, while lines 16–19 comply with the second unfolding, without entering a loop. \(\square \)
objects), whereas Fig. 
objects).
object, parametrised by local type L, whether or not \(\alpha \) complies with L. If not, the Scala compiler reports an error. In this way, 
objects (checked dynamically), and modulo non-terminating/exceptional behaviour (unchecked). These two provisos are standard for MPST tools. As the type parameters of
objects are erased at compile-time, only generic
objects exist at run-time.
(e.g., Fig. 11, line 33). For instance, for
, we always require \(p \ne q\) and \(n \ge 1\).
: the Scala compiler reduces
to the full merge of \(L_1\) and \(L_2\).
/
and
/
for presentational reasons.) First, we note that the communication from Buyer1 to Buyer2 on line 5 in the global type has no counterpart on line 5 in the local type; as Seller does not participate in the communication, it is simply skipped in the projection. Second, we note that the communication from Buyer2 to Buyer1 on line 9 in the global type is ignored, too, but the projections of the two branches do need to be combined into one. This is achieved by having the Scala compiler reduce
.
and type-checks the code against the result transparently. \(\square \)
object
for a first session can be delegated between processes via
object
for a second session, by sending
via
. In the presence of delegation, within each session, well-typedness at compile-time continues to imply safety and liveness at run-time (modulo the “two provisos”; page 8). However, between sessions, liveness is not assured; supporting this would require substantial extra technical machinery [7], so none of the existing MPST tools support it.
specifies the first sub-protocol among Buyer1, Buyer2, and Seller; it is identical to the global type for Two-Buyer. Global type
specifies the second sub-protocol between Buyer2 and Buyer3. Notably, line 8 specifies the delegation from Buyer2 to Buyer3.
objects for two sessions are consumed as inputs (to engage in two sub-protocols); on lines 5–6, the first session is used; on lines 7–10, the second session is used; on line 8, the remainder of the first session is delegated via the second session. Similarly, Fig. 17 shows a process for Buyer3: on lines 1–3, a
object for the first session is consumed as input; on line 5, a
object for the second session is received.
generically specifies the communication of an acceptance, rejection, or counter-proposal from
to
(type parameters for roles), followed by
(type parameter for a sub-protocol) in case of a counter-proposal; it can be instantiated twice to replace lines 5–7 and lines 8–10 in Fig. 9. This is done in type
, which generically specifies a role-parametric version of the whole
in Fig. 9. Thus,
is equivalent to
in Fig. 9. \(\square \)
s and
s:
is not precise enough. For instance, the Scala compiler fails to prove that
is safe, as it cannot infer that
is
. What is missing, is a relation between the actual type of
(e.g.,
) and the return type (e.g.,
). Match types define such relations.
as follows: 
(subtype of
) and declare
to be
. Also, we declare the return value to be of match type
.
in such a way that the relation between the actual type of
and the return type can be inferred, as follows: 
to
or
, depending on the instantiation of
(e.g.,
is reduced to
).
(safe) and
(unsafe).
and
reduce to
and
.
reduces to
. We note that
can be a type lambda of the form
.
. The communication infrastructure for processes is based on concurrent queues. However, a transport layer for distributed processes is also possible (orthogonal concern).
. It is used to have the Scala compiler fully automatically and statically compute local types (e.g., line 2 in Fig. 11).
has two type parameters: a global type
and a role
(cf. \(G \mathbin {{\upharpoonright }}r\)). To reduce
, the Scala compiler matches
to a global type constructor, and it produces a local type exactly as defined in Fig. 19. By convention, lower case letters in patterns are type variables; they are bound to types as part of the matching algorithm. For instance, on lines 3–5 in Fig. 21,
is bound to a product type of the form
, where each
is a data type, and each
is a global type. When
is passed to
on lines 3–4, it is converted into
. Alternatively, when
is passed to
on line 5, it is converted into
, which is subsequently passed to
; this is a helper match type that reduces to the full merge of all local types in the product type.
related to type checking. The idea is to have the Scala compiler reduce match types
and
to fully automatically and statically compute the expected types of the callback arguments of methods
and
, given a local type L. The reduction succeeds, and the actual callback argument is well-typed by the expected type, if, and only if, the communication action is well-typed by L exactly as defined in Fig. 20. Otherwise, the Scala compiler reports an error. In this way,
objects (checked dynamically),
and
. Regarding
, Fig. 20 states that a send is well-typed if the local type specifies it directly (rule [Send]) or indirectly (rule [Unfold]). These cases correspond precisely to the two cases in
:
, and if the callback is a function that consumes a
object, parametrised by the selected branch of
, namely
. We note that
reduces to
.
reduces to a version of
in which each occurrence of
is replaced with
.
, similarly, Fig. 20 states that a receive is well-typed if the local type specifies the receive directly (rule [Recv]) or indirectly (rule [Unfold]). Due to the asymmetry between sends and receives,
(singular) reduces to a single function type, while
(plural) reduces to a product of function types, computed using
. Besides that, they follow the same ideas.
