Keywords

1 Introduction

In the present era of communication-centric software systems, it is increasingly recognised that the structure of communication is an essential aspect of system design. (Multiparty) session types [18, 19, 31] allow communication structures to be codified as type definitions in programming languages, which can be exploited by compilers, development environments and runtime systems, for compile-time analysis or runtime monitoring. A substantial and ever-growing literature on session types and, more generally, behavioural types [20] provides a rich theoretical foundation, now being applied to a range of programming languages [1, 16].

Session type systems must control aliasing of the endpoints of communication channels, in order to avoid race conditions. If agents A and B both think they are running the client side of a protocol with the same server S, then a message sent by A advances the session state without B’s knowledge, which interferes with B’s attempt to run the protocol.

In order to guarantee unique ownership of channel endpoints and eliminate aliasing, most session type systems use strict linear typing. For more flexibility, some others use affine typing, which allows channels to be discarded, but they still forbid aliasing. It is possible to allow a session-typed channel to become sharable in the special case in which the session type reaches a point which is essentially stateless. However, in such systems, channels are linearly typed for the most interesting parts of their lifetimes—we discuss these possibilities in Sect. 6.

This leads us to our research questions:

  • Q1 Are session types intrinsically related to linearity or affinity?

  • Q2 Can we define session type systems without linear types?

  • Q3 How can we check resource (channel) sharing and aliasing, to guarantee communication safety and session fidelity, i.e., type safety?

Fig. 1.
figure 1

Producer-consumer system: Producer—P and Consumer—C sharing access to Buffer—B by implementing the same role . (a) P and C communicate with B in session s; (b) P and C exchange the capability to use channel in session \(s_1\) and then use it to communicate with B in session s

Full size image

The goal of this paper is to investigate questions Q1–Q3. To give a more flexible approach to resource sharing and access control, we propose a system of multiparty session types (MPST) that includes techniques from the Capability Calculus [11], and from Walker et al.’s work on alias types [35]. The key idea is to split a communication channel into two entities: (1) the channel itself, and (2) its usage capability. Both entities are first-class and can be referred to separately. Channels can now be shared, or stored in shared data structures, and aliasing is allowed. However, in order to guarantee communication safety and session fidelity, i.e., type safety, capabilities are used linearly so that only one alias can be used at a time.

This approach has several benefits, and improves on the state of the art: (i) for the first time, it is now possible for a system to have a communication structure defined by shared channels, with the capabilities being transferred from process to process as required; (ii) a capability can be implemented as a simple token, whereas delegation of channels requires a relatively complex implementation, thus making linearity of capabilities more lightweight than linearity of channels.

Example 1

(Producer-Consumer Fig. 1). Producer \(\mathsf {P} \) and consumer \(\mathsf {C} \) communicate via buffer \(\mathsf {B} \) in session \(\mathtt {s}\), given in Fig. 1 (a). \(\mathsf {P} \) and \(\mathsf {C} \) implement role , and \(\mathsf {B} \) implements role . Shared access to buffer \(\mathsf {B} \) is captured by the fact that both \(\mathsf {P} \) and \(\mathsf {C} \) implement the same role and use the same channel to communicate with \(\mathsf {B} \).

Following MPST theory, we start by defining a global type, describing communications among all participants:

In , protocol proceeds as follows: \(\mathsf {P} \) (playing ) sends an \(\mathsf {add} \) message to \(\mathsf {B} \) (playing ), to add data. In sequence, \(\mathsf {C} \) (playing ) sends a \(\mathsf {request} \) message to \(\mathsf {B} \), to ask for data. \(\mathsf {B} \) replies with a \(\mathsf {send} \) message, sending data to \(\mathsf {C} \) (playing ), and the protocol repeats as . Projecting the global protocol to each role gives us a local session type. In particular, for \(\mathsf {B} \), implementing role , we obtain:

where the annotations show the other role participating in each interaction. For the shared access by \(\mathsf {P} \) and \(\mathsf {C} \) (role ), we obtain:

Finally, the definitions of processes are as follows—we will detail the syntax in Sect. 2.

Unfortunately, the system of processes above is not typable using standard multiparty session type systems because role is shared by \(\mathsf {P} \) and \(\mathsf {C} \), thus violating linearity of channel . To solve this issue and still allow sharing and aliasing, in our work, instead of associating a channel c with a session type , we separately associate c with a tracked type , and with capability \(\rho \), . The capability can be passed between \(\mathsf {P} \) and \(\mathsf {C} \) as they take turns in using the channel, illustrated in Fig. 1 (b). As a first attempt, we now define the following global type, getting us closer to our framework.

However, a type such as is usually too specific because it refers to the capability of a particular channel. It is preferable to be able to give definitions that abstract away from specific channels. We therefore introduce existential types, in the style of [35], which package a channel with its capability, in the form .

With the existential types in place, we can define our global type in the following way. It now includes an extra initial message from \(\mathsf {P} \) to \(\mathsf {C} \) containing the channel used with the buffer. The session types and are the same as before.

In Sect. 4 we complete this example by showing the projections to a local type for each role, and the definitions of processes that implement each role. \(\square \)

Contributions of the paper

  1. (i)

    MPST with capabilities: we present a new version of MPST theory without linear typing for channels, but with linearly-typed capabilities. In Sect. 2 we define a multiparty session \(\pi \)-calculus with capabilities, and its operational semantics, and in Sect. 3 we define a MPST system for it.

  2. (ii)

    Producer-Consumer Case Study: in Sect. 4 we present a detailed account of the producer-consumer case study, capturing the core of resource sharing and use of capabilities.

  3. (iii)

    Type Safety: in Sect. 5 we state the type safety property, and outline its proof.

Fig. 2.
figure 2

Multiparty session \(\pi \)-calculus

Full size image

2 Multiparty Session \(\pi \)-Calculus with Capabilities

Our \(\pi \)-calculus with multiparty session types is based on the language defined by Scalas et al. [28]. The syntax is defined in Fig. 2. We assume infinite sets of identifiers for variables (x), sessions (\(\mathtt {s}\)), capabilities ( ) and roles ( ).

The calculus combines branch (resp., select) with input (resp., output), and a message l(v) consists of a label l and a payload v, which is a value. A message in session \(\mathtt {s}\) from role to role has the prefix , where is represented by \(\mathtt {c}\) in the grammar. The select and branch operations come in two forms. The first form is standard, and the second form handles packages, which are the novel feature of our type system. A package consists of a capability and a channel of type . We will see in Sect. 3 in the typing rules, the capability is existentially quantified. This enables a channel to be delegated, with the information that it is linked to some capability, which will be transmitted in a second message.

Fig. 3.
figure 3

Structural congruence (processes)

Full size image

As usual, we define structural congruence to compensate for the limitations of textual syntax. It is the smallest congruence satisfying the axioms in Fig. 3. The definition uses the concepts of free channels of a process, \( fc (P)\); free process variables of a process, \( fpv (P)\); and defined process variables of a process declaration, \( dpv (D)\). We omit the definitions of these concepts, which are standard and can be found in [28].

We define a reduction-based operational semantics by the rules in Fig. 4. Rule is a standard communication between roles and . Rule is communication of an existential package. Rule defines a standard approach to handling process definitions. The rest are standard contextual rules.

Fig. 4.
figure 4

Reduction (processes)

Full size image

3 Multiparty Session Types with Capabilities

We now introduce a type system for the multiparty session \(\pi \)-calculus. The general methodology of multiparty session types is that system design begins with a global type, which specifies all of the communication among various roles. Given a global type and a role , projection yields a session type or local type that describes all of the communication involving . This local type can be further projected for another role , to give a partial session type that describes communication between and .

Fig. 5.
figure 5

Types, capabilities, environments

Full size image

Global Types. Figure 5. Each interaction has a source role and a target role . We combine branching and message transmission, so an interaction has a label \(l_i\), a payload of type , or of type , and a continuation type . If there is only one branch then we usually abbreviate the syntax to , respectively . Recursive types are allowed, with the assumption that they are guarded. Base types can be types like , etc. Payload types are either base types, tracked types, capability types or closed session types.

Local (session) Types. Figure 5. The single form of interaction from global types splits into select (internal choice) and branch (external choice). The branching type describes a channel that can receive a label from role (for some \(i \in I\), chosen by ), together with a payload of type ; then, the channel must be used as the continuation type . The selection type , describes a channel that can choose a label (for any \(i \in I\)), and send it to together with a payload of type ; then, the channel must be used as . The types for pack select and pack branch act in a similar manner, and bind the capability for the continuation type . Session types also allow guarded recursion.

The relationship between global types and session types is formalised by the notion of projection.

Definition 1

The projection of onto a role , written , is:

figure az

Where the merge operator for session types, , is defined by:

figure bb

Projecting or a type variable onto any role does not change it. Projecting a recursive type onto means projecting onto . However, if does not involve then is a type variable, , and it must be replaced by to avoid introducing an unguarded recursive type. Projecting an interaction between and onto either or produces a select or a branch. Projecting onto a different role ignores the interaction and combines the projections of the continuations using the merge operator.

The merge operator, , introduced in [13, 36], allows more global types to have defined projections, which in turn allows more processes to be typed. Different external choices from the same role are integrated by merging the continuation types following a common message label, and including the branches with different labels. Merging for internal choices is undefined unless the interactions are identical. This excludes meaningless types that result when a sender is unaware of which branch has been chosen by other roles in a previous interaction.

Definition 2

For a session type denotes the set of roles occurring in . We write for , and for .

Partial Session Types. Figure 5 have the same cases as local types, without role annotations. Partial types have a notion of duality which exchanges branch and select but preserves payload types.

Definition 3

is the dual of , defined by:

Similarly to the projection of global types to local types, a local type can be projected onto a role to give a partial type. This yields a partial type that only describes the communications in S that involve . The definition follows the same principles as the previous definition (cf. Definition 1).

Definition 4

is the partial projection of onto :

figure cg

Where the merge operator for partial session types, , is defined by:

figure ci

Unlike session type merging, can combine different internal choices, but not external choices because that could violate type safety. Different internal choices can depend on the outcome of previous interactions with other roles, since this dependency can be safely approximated as an internal choice. Different external choices, however cannot capture this dependency.

Example 2 (Projections of Global and Local Types)

Consider the global type of the producer-consumer example from the introduction.

Fig. 6.
figure 6

Subtyping for local session types.

Full size image

It captures the interaction between the producer and consumer entities through roles , and between producer, consumer and buffer through roles (shared between producer and consumer) and . Projecting onto gives the session type

and further projecting onto \(\mathtt {c}\) gives the partial session type:

Definition 5 (Subtyping)

Subtyping on session types is the largest relation such that (i) if , then , and (ii) is closed backwards under the coinductive rules in Fig. 6.   Subtyping on partial session types is defined coinductively by the rules in Fig. 7.

Fig. 7.
figure 7

Subtyping for partial session types.

Full size image

Intuitively, the subtyping relation says that a session type is “smaller” than when is “less demanding” than i.e., when allows more internal choices, and imposes fewer external choices, than . Clause (i) links local and partial subtyping, and ensures that if two types are related, then their partial projections exist. This clause is used later in defining consistency in Definition 8. In the second clause  (ii) rules , define subtyping on branch/select types, and , define subtyping on branch pack/select pack types. and are covariant in their continuation types as well as in the number of branches offered, whereas , and are contravariant in both. relates base types, if they are related by . relates terminated channel types. and are standard under coinduction [26, sect. 21], relating types up-to their unfolding.

Capabilities. In our type system linearity is enforced via capabilities, rather than via environment splitting as in most session type systems. Each process has a capability set associated with it, allowing it to communicate on the associated channels. The tracked type is a singleton type associating a channel to capability and to no other, which in turn maps to the channel’s session type . Hence two variables with the same capability \(\rho \) are aliases for the same channel. Individual capabilities are joined together using the \(\otimes \) operator: . The ordering is insignificant. The type system maintains the invariant that are distinct.

Definition 6 (Terminated capabilities)

A capability set is terminated if for every .

Definition 7 (Substitution of capabilities)

There are two important concepts relating the environment and the capability set : completeness and consistency, used in our type system.

Completeness means that if a channel is in and its capability is in , then also contains the other endpoints of the channel and contains the corresponding capability. In this case, there is a self-contained collection of channels that can communicate. Consistency means that the opposite endpoints of every channel have dual partial types.

Definition 8 (Completeness and consistency)

is complete iff for all with and implies and .

  is consistent iff for all we have .

Fig. 8.
figure 8

Typing rules

Full size image

Definition 9

Typing judgements are inductively defined by the rules in Fig. 8, and have the form: for values, or for processes (with consistent, and is defined .

is an environment of typed variables and channels together with their capability typing. , defined in Fig. 5 is an environment of typed process names, used in rules and for recursive process definitions and calls. If a channel is in , with type , then also contains for some session type . The capability might, or might not, be in , to show whether or not the channel can be used. If is in , then it occurs with the same session type: .

Rule takes the type for a capability from the capability set. and are standard. has a standard condition that all session types have reached , expressed as the capability set being \( \text{ terminated }\). combines the capability sets in a parallel composition. is a standard subsumption rule using (Definition 5), the difference being the type in the capability set. (resp. ) states that the selection (resp. branching) on channel is well typed if the capability associated with it is of compatible selection (resp. branching) type and the continuations \(P_i, \forall i \in I\) are well-typed with the continuation session types. is similar to , with the notable difference that an existential package is created for the channel being sent, containing the channel and its abstracted capability. Note that the actual capability to use the endpoint remains with process . is similar to , with the difference that it unpackages the channel received and binds its capability type in the continuation session type (used to identify the correct capability when received later). requires the restricted environment and the associated capability set to be complete (Definition 8). takes account of capability sets as well as parameters, and similarly requires capability sets. The parameters of a defined process include any necessary capabilities, which then also appear in the corresponding , because not all capabilities associated with the channel parameters need to be present when the call is made.

4 Case Study: Producer-Consumer

We now expand on the producer-consumer scenario from Sect. 1 by discussing the process definitions and showing part of the typing derivation. To lighten the notation, we present a set of mutually recursive definitions, instead of using the formal syntax of \(\mathsf {def}\ldots \mathsf {in}\).

Recall that the example consists of three processes: the producer, the consumer, and a one-place buffer (Fig. 1). The producer and the consumer communicate with the buffer on a single shared channel. Each of the two must wait to receive the capability to communicate on the channel before doing so.

The buffer \(\mathsf {B} \) is parameterised by channel \(\mathtt {x}\) and by the capability for it, , and alternately responds to \(\mathsf {add} \) and \(\mathsf {request} \) messages. At the end of the definition, shows the held capability and its session type.

The producer is represented by two process definitions: \(\mathsf {Produce} \) and \(\mathsf {P} \). \(\mathsf {Produce} \) is a recursive process with several parameters. Channels \(\mathtt {x}\) and \(\mathtt {y}\) are used to communicate with the consumer and the buffer, respectively. Their capabilities are . Finally, \(\mathsf {i} \) is the value to be sent to the buffer. The process sends a value to the buffer (\(\mathsf {add} (\mathsf {i}))\), transfers the capability for the shared channel \(\mathtt {y}\) and receives it back from the consumer. Process \(\mathsf {P} \) is the entry point for the producer. It has the same parameters as \(\mathsf {Produce} \), except for \(\mathsf {i} \). The only action of \(\mathsf {P} \) is to send the consumer a shared reference to the channel used for communication with the buffer —

In a similar way, the consumer is represented by \(\mathsf {Consume} \) and \(\mathsf {C} \). The parameters, however, are different. \(\mathsf {C} \) has \(\mathtt {x}\) and its capability , for communication with the producer, but it does not have \(\mathtt {y}\) or for communication with the buffer. It receives \(\mathtt {y}\) from the producer, as part of , and \(\mathtt {y}\) is passed as a parameter to \(\mathsf {Consume} \). The capability is not a parameter of \(\mathsf {Consume} \), but it is received in a \(\mathsf {turn} \) message from the producer.

The complete system consists of the producer, the consumer and the buffer in parallel, with sessions \(s_1\) (roles and ) and \(s_2\) (roles and ) scoped to construct a closed process.

The session types involved in these processes are projections of the global type (Sect. 3). They specify how each role is expected to use its channel endpoint. The roles are for the buffer, for the combined role of the producer and the consumer as they interact with the buffer, for the producer, and for the consumer.

These types occur in the capabilities associated with each process. For example process has , process has has .

Fig. 9.
figure 9

Typing derivation for \(\mathsf {Produce} \).

Full size image
Fig. 10.
figure 10

Typing derivation for \(\mathsf {P} \).

Full size image

To illustrate the typing rules, we show the typing derivation for the producer, i.e. processes \(\mathsf {Produce} \) (Fig. 9) and \(\mathsf {P} \) (Fig. 10). Full derivations for all of the processes are in the technical report. The derivations use the following definitions.

Scenarios with multiple producers/consumers can be represented in a similar way, the capabilities acting as a form of lock for the resource being shared. The full typing derivation for producer consumer case study can be found in the extended version of this paper [33].

5 Technical Results

Following standard practice in the MPST literature, we show type safety and hence communication safety by proving a subject reduction theorem (Theorem 1). In the usual way, session types evolve during reduction—in our system, this is seen in both the environment and the capability set .

Definition 10 (Typing context reduction)

The reduction is:

figure fp

Following [28] our Definition 10 also accommodates subtyping () and our iso-recursive type equivalence (hence, unfolds types explicitly).

Theorem 1 (Subject reduction)

If  and , then there exist and such that and .

The proof is by induction on the derivation of \(P \,\longrightarrow \,P'\), with an analysis of the derivation of . A key case is , which requires preservation of the condition in that is consistent. This is because a communication reduction consumes matching prefixes from a pair of dual partial session types, which therefore remain dual. The full proof is in the extended version of this paper [33].

6 Related Work, Conclusion and Future Work

From the beginning of session types, channel endpoints were treated as linear resources so that each role in a protocol could be implemented by a unique agent. This approach is reinforced by several connections between session types and other linear type theories: the encodings of binary session types and multiparty session types into linear \(\pi \)-calculus types [12, 28]; the Curry-Howard correspondence between binary session types and linear logic [6, 34]; the connection between multiparty session types and linear logic [7, 8].

Some session type systems generalise linearity. Vasconcelos [32] allows a session type to become non-linear, and sharable, when it reaches a state that is invariant with every subsequent message. Mostrous and Vasconcelos [24] define affine session types, in which each endpoint must be used at most once and can be discarded with an explicit operator. In Fowler et al.’s [15] implementation of session types for the Links web programming language, affine typing allows sessions to be cancelled when exceptions (including dropped connections) occur. Caires and Pérez [5] use monadic types to describe cancellation (i.e. affine sessions) and non-determinism. Pruiksma and Pfenning [27] use adjoint logic to describe session cancellation and other behaviours including multicast and replication.

Usually linearity spreads, because a data structure containing linear values must also be linear. In the standard \(\pi \)-calculus, exceptions to this nature of linearity have been studied by Kobayashi in his work on deadlock-freedom Padovani [25] extends the linear \(\pi \)-calculus with composite regular types in such a way that data containing linear values can be shared among several processes. However, this sharing can occur only if there is no overlapping access to such values, which differs from our work where we have full sharing of values. On the other hand, we work directly with (multiparty) session types, whereas Padovani works with linear \(\pi \)-calculus and obtains his results via the encoding of session types into linear \(\pi \)-types [12].

Session types are related to the concept of typestate [29], especially in the work of Kouzapas et al. [21, 22] which defines a typestate system for Java based on multiparty session types. Typestate systems require linear typing or some other form of alias control, to avoid conflicting state changes via multiple references. Approaches include the permission-based systems used in the Plural and Plaid languages [4, 30] and the fine-grained approach of Militão et al. [23]. Crafa and Padovani [10] develop a “chemical” approach to concurrent typestate oriented programming, allowing objects to be accessed and modified concurrently by several processes, each potentially changing only part of their state. Our approach is partly inspired by Fähndrich and DeLine’s “adoption and focus” system [14], in which a shared stateful resource (in our case, a session channel) is separated from the linear key (capability, in our system) that enables it to be used. In this way the state changes of channels follow the standard session operations, channels can be shared (for example, stored in shared data structures), and access can be controlled by passing the capability around the system.

Balzer et al. [2, 3] support sharing of binary session channels by allowing locks to be acquired and released at points that are explicitly specified in the session type. Our approach with multiparty sessions is not based on locks, so it doesn’t require runtime mechanisms for managing blocked processes and notifying them when locks are released.

We have presented a new system of multiparty session types with capabilities, which allows sharing of resources in a way that generalises the strictly linear or affine access control typical of session type systems. The key technical idea is to separate a channel from the capability of using the channel. This allows channels to be shared, while capabilities are linearly controlled. We use a form of existential typing to maintain the link between a channel and its capability, while both are transmitted in messages. We have proved communication safety, formulated as a subject reduction theorem (Theorem 1). An area of future work is to prove progress and deadlock-freedom properties along the lines of, for example, Coppo et al. [9]. Another possibility is to apply our techniques to functional languages with session types [17].