Manifestly Phased Communication via Shared Session Types

Abstract

Session types denote message protocols between concurrent processes, allowing a type-safe expression of inter-process communication. Although previous work demonstrate a well-defined notion of subtyping where processes have different perceptions of the protocol, these formulations were limited to linear session types where each channel of communication has a unique provider and client. In this paper, we extend subtyping to shared session types where channels can now have multiple clients instead of a single client. We demonstrate that this generalization can statically capture protocol requirements that span multiple phases of interactions of a client with a shared service provider, something not possible in prior proposals. Moreover, the phases are manifest in the type of the client.

1 Introduction

Session types prescribe bidirectional communication protocols between concurrent processes [15, 16]. Variations of this type system were later given logical correspondences with intuitionistic [4] and classical [22] linear logic where proofs correspond to programs and cut reduction to communication. This correspondence mainly provided an interpretation of linear session types, which denote sessions with exactly one client and one provider. Shared session types, which encode communication between multiple clients and one provider, were proposed with a sharing semantics interpretation in a prior work [2]. Clients communicating along a shared channel follow an acquire-release discipline where they must first acquire exclusive access to the provider, communicate linearly, and then finally release the exclusive access, allowing other clients to acquire.

However, not all protocols that follow this acquire-release paradigm are safe; if a client that successfully acquires some shared channel of type A releases it at an unrelated type B, other clients that are blocked while trying to acquire will still see the channel as type A while the provider will see the channel as type B. To resolve this, we require an additional constraint that clients must release at the same type at which it acquired. This was formally expressed in [2] as the equi-synchronizing constraint, which statically verifies that session types encode communication which does not release at the wrong type. Although shared session types serve an important role in making session typed process calculi theory applicable to practical scenarios, we previously [19] showed that shared session types cannot express phases, or protocols across successive acquire-release cycles, due to the equi-synchronizing constraint being too restrictive (see Sect. 5).

We demonstrate that subtyping, first formalized in the session-typed process calculi setting by Gay and Hole [11], and its behavior across the two linear and shared modalities provide the groundwork for an elegant relaxation of the equi-synchronizing constraint, allowing for phases to be manifest in the session type. In message passing concurrency, subtyping allows a client and provider to safely maintain their own local views on the session type (or protocol) associated with a particular channel. Although previous papers [1, 11] investigate subtyping in the purely linear session type setting, we found that extending these results to the linear and shared session type setting as in [2] yields very powerful results with both practical and theoretical significance.

In this paper, we build upon past results on subtyping and propose a formulation of subtyping compatible with shared session types. We in particular introduce the subsynchronizing constraint, a relaxation of the equi-synchronizing constraint.

The main contributions of this paper include:

• A full formalization of a subtyping relation for shared session types and their meta theory.

• The introduction of the subsynchronizing constraint, a relaxation of the equi-synchronizing constraint.

• Illustrations of practical examples in this richer type system, further bridging the gap between session-typed process calculi and practical programming languages.

The rest of the paper will proceed as follows: Sect. 2 provides a brief introduction to linear and shared session-typed message-passing concurrency. Section 3 demonstrates the inability for prior systems to express phasing and motivates our approach. Section 4 provides an introduction to linear subtyping along with an attempt to extend the relation to the shared setting. Section 5 introduces the notion of phasing and the subsynchronizing judgment. Section 6 presents a message passing concurrent system using our typesystem and the corresponding progress and preservation statements. Section 7 discusses related work. Section 8 concludes the paper with some points of discussion and future work.

An extended version of this paper is available as a technical report [20], containing detailed proofs, a complete formalization of the system, and more complex examples. This paper will focus on our advancements to the type system and key ideas while treating the syntax of the language and the operational interpretation informally.

2 Background

2.1 Linear Session Types

Based on the correspondence established between intuitionistic linear logic and the session-typed $\pi$-calculus [4, 21] we can interpret a intuitionistic linear sequent

$$A_1, A_2, \ldots , A_n \vdash B$$

as the typing judgment for a process P by annotating the linear propositions with channel names:

$$\underbrace{a_1:A_1, a_2:A_2, \ldots , a_n:A_n}_\varDelta \vdash P \,::\, (b:B)$$

Interpreted as a typing judgment, we say that process P provides a session of type B along channel b while using channels $a_1, \ldots , a_n$ with session types $A_1, \ldots , A_n,$ respectively. Interpreted as a sequent, we say that P is a proof of some proposition B with hypotheses $A_1, \ldots , A_n$. Following linear logic, the context $\varDelta$ is restricted and rejects contraction and weakening. Programatically, this means that linear channels cannot be aliased nor freely deleted – they must be fully consumed exactly once.

Since the session type associated with a channel denotes a bidirectional protocol, each connective has two operational interpretations – one from the perspective of the provider and one from the client. This operationally dual interpretation results in a schema where for any connective, either the client or provider will send while the other will receive as summarized in Table 1.

For example, a channel of type $A \otimes 1$ requires that the provider sends a channel of type A and proceeds as type 1 while the client receives a channel of type A and proceeds as 1. The multiplicative unit 1 denotes the end of the protocol – the provider must terminate and close its channel while a client must wait for the channel to be closed. A channel of type $\oplus \{{\overline{l:A}}\}$ (n-nary internal choice) requires the provider to choose and send a label i in $\overline{l}$ and proceed as $A_i$ while the client must receive and branch on some label i and proceed as $A_i$. Similarly, a channel of type requires the client to choose and send a label and the provider to receive and branch on a label. The continuation type of some session type refers to the type after a message exchange; for example, B would be the continuation type of $A \otimes B$ and similarly $A_i$ of $\oplus \{{\overline{l:A}}\}$ for some i in $\overline{l}$. The unit 1 does not have a continuation type since it marks the end of communication.

Table 1. A summary of the linear connectives and their operational interpretations

We consider a session type denoting the interaction with a provider of a queue of integers, which we will develop throughout the paper:

$$ \begin{aligned} \mathbf{queue} = \& \{ enqueue :&\text {int} \supset \mathbf{queue} , \\ dequeue :&\oplus \{{ some : \text {int} \wedge \mathbf{queue} , none : \mathbf{queue} }\} \} \end{aligned}$$

where we informally adopt value input and output $\supset$ and $\wedge$ [21] as value analogues to channel input and output $\multimap$ and $\otimes$, respectively, which are orthogonal to the advancements in this work. Following this protocol, a client must send a label $enqueue$ or $dequeue$. If it chooses $enqueue$, it must send an int and then recur, and on the other hand, if it chooses $dequeue$, it will receive either some int as indicated by the $some$ branch of the internal choice or nothing as indicated by the $none$ branch. In either case, we let the queue recur¹. Dually, a server must first receive a label $enqueue$ or $dequeue$ from the client. If it receives an $enqueue$, it will receive an int and then recur. If it receives a $dequeue$ instead, it must either send a $some$ label followed by the appropriate int and then recur or send a $none$ label and then recur.

We adopt an equi-recursive [8] interpretation which requires that recursive session types be contractive [11], guaranteeing that there are no messages associated with the unfolding of a recursive type. This in particular requires that we reason about session types coinductively.

We now attempt to encode a protocol representing an auction based on [9]. An auction transitions between the bidding phase where clients are allowed to place bids and the collecting phase where a winner is given the item while all the losers are refunded their respective bids.

$$ \begin{aligned} \mathbf{bidding} = \& \{ bid :&\oplus \{ ok : \text {id} \supset \text {money} \supset \mathbf{bidding} , \\&collecting : \mathbf{collecting} \}\} \\ \mathbf{collecting} = \& \{ collect : \text {id}\supset&\oplus \{ prize : \text {item} \wedge \mathbf{bidding} , \\&\quad refund : \text {money} \wedge \mathbf{bidding} , \\&\quad bidding : \mathbf{bidding} \}\} \end{aligned}$$

In this example, we make the bidding phase and collecting phase explicit by separating the protocol into bidding and collecting. Beginning with bidding, a client must send a $bid$ label². The provider will either respond with an $ok$, allowing the client to make a bid by sending its id, money, and then recursing back to bidding, or a $collecting$, indicating that the auction is in the collecting phase and thereby making the client transition to collecting.

For collecting, the client must send a $collect$ label. For ease of presentation, we require the client to also send its id immediately, giving enough information to the provider to know if the client should receive a $prize$ or a $refund ,$ along with $bidding$ if the client is in the wrong phase. The $prize$ branch covers the case where the client won the previous bid, the $refund$ branch covers the case where the client lost the bid, and the $bidding$ branch informs the client that the auction is currently in the bidding phase.

Because linear channels have exactly one provider and one client, what we have described so far only encodes a single participant auction. One can assert that the provider is actually a broker to an auction of multiple participants, but that does not solve the fundamental problem, that is, encoding shared communication with multiple clients.

2.2 Shared Session Types

Although linear session types and their corresponding process calculi give a system with strong guarantees such as session fidelity (preservation) and deadlock freedom (progress), as we show in the previous section while attemping to encode an auction, they are not expressive enough to model systems with shared resources. Since multiple clients cannot simultaneously communicate to a single provider in an unrestricted manner, we adopt an acquire-release paradigm. The only action a client can perform on a shared channel is to send an acquire request, which the provider must accept. After successfully acquiring, the client is guaranteed to have exclusive access to the provider and therefore can communicate linearly until the client releases its exclusive access.

Instead of treating the acquire and release operations as mere operational primitives, in prior work [2] we extend the type system such that the acquire and release points are manifest in the type by stratifying session types into shared and linear types. Unlike linear channels, shared channels are unrestricted in that they can be freely aliased or deleted. In the remaining sections, we will make the distinction between linear and shared explicit by marking channel names and session type meta-variables with subscripts L and S respectively where appropriate. For example, a linear channel is marked $a_{\scriptscriptstyle L}$, while a shared channel is marked $b_{\scriptscriptstyle S}$.

Since shared channels represent unrestricted channels that must first be acquired, we introduce the modal upshift operator ${\uparrow _L^S}A_{\scriptscriptstyle L}$ for some $A_{\scriptscriptstyle L}$ which requires clients to acquire and then proceed linearly as prescribed by $A_{\scriptscriptstyle L}$. Similarly, the modal downshift operator ${\downarrow _L^S}B_{\scriptscriptstyle S}$ for some $B_{\scriptscriptstyle S}$ requires clients to release and proceed as a shared type. Type theoretically, these modal shifts mark transitions between shared to linear and vice versa. In summary, we have:

$$ \begin{aligned}&\text {(Shared Layer)}&A_{\scriptscriptstyle S} \; \,::= \;&{\uparrow _L^S}A_{\scriptscriptstyle L} \\&\text {(Linear Layer)}&A_{\scriptscriptstyle L}, B_{\scriptscriptstyle L} \; \,::= \;&{\downarrow _L^S}A_{\scriptscriptstyle S} \; | \;1 \; | \;A_{\scriptscriptstyle L}\otimes B_{\scriptscriptstyle L} \; | \;A_{\scriptscriptstyle L}\multimap B_{\scriptscriptstyle L} \; | \; \& \{{\overline{l {:} A_{\scriptscriptstyle L}}}\} \; | \;\oplus \{{\overline{l {:} A_{\scriptscriptstyle L}}}\} \end{aligned}$$

where we emphasize that the previously defined (linear) type operators such as $\otimes$ remain only at the linear layer – a shared session type can only be constructed by a modal upshift ${\uparrow _L^S}$ of some linear session type $A_{\scriptscriptstyle L}$.

As initially introduced, clients of shared channels follow an acquire-release pattern – they must first acquire exclusive access to the channel, proceed linearly, and then finally release the exclusive access that they had, allowing other clients of the same shared channel to potentially acquire exclusive access. The middle linear section can also be viewed as a critical region since the client is guaranteed unique access to a shared provider process. Therefore, this system naturally supports atomic operations on shared resources.

Using shared channels, we can encode a shared queue, where there can be multiple clients interacting with the same data:

A client of such a channel must first send an acquire message, being blocked until the acquisition is successful. Upon acquisition, the client must then proceed linearly as in the previously defined linear queue. The only difference is that before recursing, the client must release its exclusive access, allowing other blocked clients to successfully acquire.

3 Equi-Synchronizing Rules Out Phasing

We can also attempt to salvage the previous attempt of encoding (multi-participant) auctions by “wrapping” the previous purely linear protocol between ${\uparrow _L^S}$ and ${\downarrow _L^S}$.

A client to bidding must first acquire exclusive access as indicated by ${\uparrow _L^S}$, proceed linearly, and then eventually release at either bidding (in the $ok$ branch) or collecting (in the $collecting$ branch). Similarly, a client to collecting must first acquire exclusive access, proceed linearly, and then eventually release at bidding since all branches lead to bidding.

Unfortunately, as formulated so far, this protocol is not sound. For example, consider two auction participants P and Q that are both in the collecting phase and blocked trying to acquire. Suppose P successfully acquires, in which case it follows the protocol linearly and eventually releases at bidding. Then, if Q successfully acquires, we have a situation where Q rightfully believes that it acquired at collecting but since P previously released at type bidding, the auctioneer believes that it currently accepted a connection from bidding. The subsequent label sent by the client, $collect$ is not an available option for the provider; session fidelity has been violated.

Previous work [2] addresses this problem by introducing an additional requirement that if a channel was acquired at some type $A_{\scriptscriptstyle S}$, all possible future releases (by looking at the continuation types) must release at $A_{\scriptscriptstyle S}$. This is formulated as the equi-synchronizing constraint, defined coinductively on the structure of session types. In particular, neither bidding nor collecting are equi-synchronizing because they do not always release at the same type at which it was acquired. For bidding, the $collecting$ branch causes a release at a different type, and for collecting, all branches lead to a release at a different type.

A solution to the auction scenario is to unify the two phases into one:

The type auction is indeed equi-synchronizing because all possible release points are at auction.

This presentation of the auction however loses the explicit denotation of the two phases; although the previous linear single participant version of the auction protocol can make explicit the bidding and collecting phases in the session type, the equi-synchronizing requirement forces the two phases to merge into one in the case of shared session types. In general, the requirement that all release points are equivalent prevents shared session types to encode protocols across multiple acquire-release cycles since information is necessarily “lost” after a particular acquire-release cycle.

4 Subtyping

So far, there is an implicit requirement that given a particular channel, both its provider and clients agree on its protocol or type. A relaxation of this requirement in the context of linear session types have been investigated by Gay and Hole [11], and in this section, we present subtyping in the context of both linear session types and shared session types.

If $A \le B$, then a provider viewing its offering channel as type A can safely communicate with a client viewing the same channel as type B. This perspective reveals a notion of substitutability, where a process providing a channel of type A can be replaced by a process providing $A'$ such that $A' \le A$ and dually, a client to some channel of type B can be replaced by another process using the same channel as some type $B'$ such that $B \le B'$. The following subtyping rules, interpreted coinductively, formalize the subtyping relation between session types:

One of the notable consequences of adopting subtyping is that internal and external choices allow one side to have more labels or branches. For internal choice, since the provider sends some label, there is no harm in a client to be prepared to handle additional labels that it will never receive and vice versa for external choice. Another observation is that subtyping of session types is covariant in their continuations; following this paradigm, we can immediately define subtyping for the new type connectives ${\uparrow _L^S}$ and ${\downarrow _L^S}$:

Remark 1

The subtyping relation $\le$ is a partial order.

A key principle governing subtyping of session types is that ignorance is bliss; neither the client nor the provider need to know the precise protocol that the other party is following, as supported by our extended report [20] which proves the same progress and preservation theorems in an implementation of session typed process calculus with shared channels [2] in a system with subtyping.

Let us revisit the shared queue example:

Instead of allowing all clients to freely enqueue and dequeue, suppose we only allow certain clients to enqueue and certain clients to dequeue. With subtyping, we first fix the provider’s type to be shared_queue. Next, we restrict writer clients by removing the dequeue label and similarly restrict reader clients by removing the enqueue label:

where it is indeed the case that $\mathbf{shared}\_queue \le \mathbf{producer}$ and $\mathbf{shared}\_queue \le \mathbf{consumer}$, justifying both the writer and reader clients’ views on the type of the channel.

We will defer the detailed discussion of the subtle interactions that occur between the notion of equi-synchronizing constraint and subtyping to Sect. 5.1. For this example however, the fact that all three types shared_queue, producer, and consumer are independently equi-synchronizing is a strong justification of its soundness.

5 Phasing

One of the most common patterns when encoding data structures and protocols via session types is to begin the linear type with an external choice. When these types recur, we are met with another external choice. A notion of phasing emerges from this pattern, where a single phase spans from the initial external choice to the recursion.

We introduced an auction protocol, which in its linear form can make explicit the two distinct phases, yet in its shared form cannot due to the equi-synchronizing constraint. With subtyping however, this seems to no longer be a problem; the auctioneer can view the protocol as auction whereas the clients can independently view the protocol as bidding or collecting depending on their current phase since $\mathbf{auction} \le \mathbf{bidding}$ and $\mathbf{auction} \le \mathbf{collecting}$.

Unfortunately, there is a critical issue with this solution. Since shared channels can be aliased, a client in the collecting phase can alias the channel, follow the protocol, and then ignore the released type (bidding phase) – it can then use the previously aliased channel to communicate as if in the collecting phase. In general, the strategy of encoding phases in shared communication through a shared supertype allows malicious clients to re-enter previously encountered phases since they may internally store aliases. Thus, what we require is a subtyping relation across shared and linear modes since linear channels are restricted and in particular cannot be aliased.

We first add two new linear connectives ${\uparrow _L^L}$ and ${\downarrow _L^L}$ that, like ${\uparrow _L^S}$ and ${\downarrow _L^S}$, have operationally an acquire-release semantics but enforce a linear treatment of the associated channels. Prior work [14] has already explored such intra-layer shifts, albeit for the purpose of enforcing synchronization in an asynchronous message-passing system. Thus for example, the protocol denoted by ${\uparrow _L^L}A_{\scriptscriptstyle L}$ requires the client to “acquire” as in the shared case. If the provider happens to provide a linear channel ${\uparrow _L^L}A_{\scriptscriptstyle L}$, then this merely adds a synchronization point in the communication. The more interesting case is when the provider is actually providing a shared channel, some ${\uparrow _L^S}A_{\scriptscriptstyle L}$; a client should be able to view the session type as ${\uparrow _L^L}A_{\scriptscriptstyle L}$ without any trouble. We formalize this idea to the following additional subtyping relations:

Using the new connectives, we can complete the auction protocol where the two phases are manifest in the session type; a client must actually view the auction protocol linearly!

where $\mathbf{auction} \le \mathbf{bidding}$ and $\mathbf{auction} \le \mathbf{collecting}$. Compared to the initially presented linear auction protocol, this version inserts the purely linear shifts ${\uparrow _L^L}$ and ${\downarrow _L^L}$ where appropriate such that the protocol is compatible with the shared auction protocol that the auctioneer provides. Therefore, the addition of ${\uparrow _L^L}$ and ${\downarrow _L^L}$ to our system allows a natural subtyping relation between shared session types and linear session types, where they serve as a means to safely bridge between shared and linear modalities.

Remark 2

A protocol spanning multiple phases can also be interpreted as a deterministic finite autonomata (DFA) where nodes represent the phase or the state of the protocol and edges represent choice branches. The previous auction protocol can be encoded as a two state DFA as shown in Fig. 1.

Fig. 1.

A DFA representation of the two phases in the auction protocol. Multiple labels enclosed in brackets as in $\{ prize , refund , bidding \}$ mean that any of those labels can be selected.

5.1 Subsynchronizing Constraint

We note in Sect. 2.2 that in previous work [2], we require session types to be equi-synchronizing, which requires that processes following the protocol are released at the exact type at which it was acquired. This constraint guarantees that clients do not acquire at a type that they do not expect. With the introduction of subtyping however, there are two major relaxations that we propose on this constraint.

Releasing At a Subtype. A client P using some channel as some type $a_{\scriptscriptstyle S} {:} A_{\scriptscriptstyle S}$ can safely communicate with any (shared) process offering a channel of type $a_{\scriptscriptstyle S} {:} A'_{\scriptscriptstyle S}$ such that $A'_{\scriptscriptstyle S} \le A_{\scriptscriptstyle S}$ due to subtyping. If another client acquires $a_{\scriptscriptstyle S}$ and releases it at some $A''_{\scriptscriptstyle S}$ such that $A''_{\scriptscriptstyle S} \le A'_{\scriptscriptstyle S}$, then P can still safely communicate along $a_{\scriptscriptstyle S}$ since $A''_{\scriptscriptstyle S} \le A_{\scriptscriptstyle S}$ by transitivity. Thus, one reasonable relaxation to the equi-synchronizing constraint is that processes do not need to be released at the same exact type but instead a subtype.

Branches That Never Occur. A major consequence of subtyping is that providers and clients can wait on some branches in the internal and external choices which in fact never will be sent by the other party. For example, suppose a provider P provides a channel of type $A_{\scriptscriptstyle S} = {{\uparrow _L^S} \& \{{a:{\downarrow _L^S}A_{\scriptscriptstyle S}, b:{\downarrow _L^S}B_{\scriptscriptstyle S}}\}}$. Assuming some unrelated $B_{\scriptscriptstyle S}$, we can see that $A_{\scriptscriptstyle S}$ is not equi-synchronizing because the b branch can lead to releasing at a different type. However, suppose some client C views the channel as ${{\uparrow _L^S} \& \{{a:{\downarrow _L^S}A_{\scriptscriptstyle S}}\}}$ – in this case, P can only receive a, and the b branch can safely be ignored since C will never send the b label. This points to the necessity of using both the provider and client types to more finely verify the synchronizing constraint. Of course, if there is another client D that views the channel in a way that the b branch can be taken, then the entire setup is not synchronizing. Thus, we must verify the synchronization constraint for all pairs of providers and clients.

Following previous work [2], we formulate constraints by extending the shared types: ${\hat{A} \; \,::= \;\bot \; | \;A_{\scriptscriptstyle S} \; | \;\top }$ where $\bot \le A_{\scriptscriptstyle S} \le \top$ for any $A_{\scriptscriptstyle S}$. Intuitively, $\top$ indicates a channel that has not been acquired yet (no constraints on a future release), $A_{\scriptscriptstyle S}$ indicates the previous presentation of shared channels, and $\bot$ indicates a channel that will never be available (hence, any client attempting to acquire from this channel will never succeed and be blocked).

We are now ready to present the subsynchronizing judgment, interpreted coinductively, which is of the form $\vdash (A, B, \hat{D}) \; \text {ssync}$ for some A and B such that $A \le B$. It asserts that a provider providing a channel of type A and a client using that channel with type B is subsynchronizing with respect to some constraint $\hat{D}$. To verify a pair of types A and B to be subsynchronizing, we take $\top$ as its initial constraint (recall that $\top$ represents no constraint), that is, we say that A and B are subsynchronizing if $\vdash (A, B, \top ) \; \text {ssync}$.

The general progression of derivations to verify that two types are subsynchronizing is to first look for an upshift ${\uparrow _L^S}$ on the provider’s type, involving either $S{\uparrow _L^S}$ or $S{\uparrow _L^S}{\uparrow _L^L}$. After encountering a ${\uparrow _L^S}$, it “records” the provider’s type as the constraint and continues to look at the continuations of the types. When encountering internal and external choices, it only requires the continuations for the common branches to be subsynchronizing. When it encounters a downshift ${\downarrow _L^S}$ from the provider’s side, it checks if the release point as denoted by the continuation of ${\downarrow _L^S}$ is a subtype of the recorded constraint, in which case it continues with the derivation with the $\top$ constraint.

Remark 3

Subsynchronizing is a strictly weaker constraint than equi-synchronizing. In particular, if A is equi-synchronizing, then the pair A, A are subsynchronizing.

6 Metatheory

In this section we present the progress and preservation theorems in a synchronous message passing concurrent system implementing our type system. We defer many of the technical details of the system and the proofs to our extended report [20] which follows a similar style to the system in a previous work [2]. In particular, the two theorems are equally strong as the ones in [2], justifying our subtyping extension.

6.1 Process Typing

We take the typing judgment presented in Sect. 2.1 and extend it with shared channels as introduced in Sect. 2.2:

$$\begin{aligned} {\varGamma \vdash P \,::\, (a_{\scriptscriptstyle S} {:} A_{\scriptscriptstyle S})} \\ {\varGamma ;\varDelta \vdash Q \,::\, (a_{\scriptscriptstyle L} {:} A_{\scriptscriptstyle L})} \end{aligned}$$

where $\varGamma = {a_1}_{\scriptscriptstyle S} {:} \hat{A_1}, \ldots , {a_n}_{\scriptscriptstyle S} {:} \hat{A_n}$ is a structural context of shared channels and constraints ($\bot$ and $\top$) which can appear at runtime.

The first judgment asserts that P provides a shared channel $a_{\scriptscriptstyle S} {:} A_{\scriptscriptstyle S}$ while using shared channels in $\varGamma$; the lack of dependence on any linear channels $\varDelta$ is due to the independence principle presented in [2]. The second judgment asserts that Q provides a linear channel $a_{\scriptscriptstyle L} {:} A_{\scriptscriptstyle L}$ while using shared channels in $\varGamma$ and linear channels in $\varDelta$.

Forwarding is a fundamental operation that allows a process to identify its offering channel with a channel it uses if the types match.

The rules $ID_{\scriptscriptstyle L}$ and $ID_{\scriptscriptstyle S}$ require the offering channel to be a supertype of the channel it is being identified with. Since we syntactically distinguish shared channels and linear channels, we require an additional rule $ID_{\scriptscriptstyle {LS}}$ that allows linear channels to be forwarded with a shared channel provided the subtyping relation holds.

We also show the right rule of $\otimes$, which requires the provider to send a channel $y_{\scriptscriptstyle L}$ alongside its offering channel $x_{\scriptscriptstyle L}$:

Similar to the forwarding case, a shared channel can instead be sent if the appropriate subtyping relation holds:

One important observation is that typing judgments remain local in the presence of subtyping; the channels in $\varGamma$ and $\varDelta$ may be provided by processes at some subtype (maintained in the configuration; see Sect. 6.3) and need not match. We therefore do not adopt a general subsumption rule that allows arbitrary substitutions that preserve subtyping and instead precisely manage where subtyping occurs in the system.

6.2 Processes and Configuration

To reason about session types and process calculi, we must consider a collection of message passing processes, which is known as a configuration. In our system, we split the configuration into the shared fragment $\varLambda$ and the linear fragment $\varTheta$, where $\varLambda$ is a list of process predicates that offer shared channels and $\varTheta$ is similarly a list of process predicates that offer linear channels.

The most fundamental process predicate denotes a process term P that provides some channel a and is of form $\text {proc}(a, P)$. We also introduce the predicate $\text {unavail}(a_{\scriptscriptstyle S})$, which represents a shared process that is unavailable to be acquired, for example, due to it being acquired by another process, and $\text {connect}(a_{\scriptscriptstyle L}, b_{\scriptscriptstyle S})$, which provides a linear reference $a_{\scriptscriptstyle L}$ to a shared channel $b_{\scriptscriptstyle S}$, needed to express shared to linear subtyping.

We require the linear configuration $\varTheta$ to obey an ordering that processes can only depend on processes that appear to its right; $\text {proc}(a_{\scriptscriptstyle L}, P), \text {proc}(b_{\scriptscriptstyle L}, Q)$ would be ill-formed if P depends on $b_{\scriptscriptstyle L}$. On the other hand, $\varLambda$ has no ordering constraints. For the subsequent sections, we require that configurations are well-formed, which essentially requires that both shared and linear processes provide unique channel names thereby avoiding naming conflicts.

6.3 Configuration Typing

The configuration typing judgment asserts that a given configuration collectively provides a set of shared and linear channels; each fragment is checked separately as shown by the only typing rule for the combined configuration:

The shared context $\varGamma$ appears on both sides due to circularity; the appearance on the left side allows any processes to depend on a particular shared channel in $\varGamma$ while the appearance on the right side asserts that $\varLambda$ collectively provides $\varGamma$. In most cases, $\hat{A}$ is some shared session type $A_{\scriptscriptstyle S}$, but the maximal and minimal types $\bot$ and $\top$ can appear at runtime.

For the shared fragment, we check each process predicate independently; in particular, a configuration typing rule for some $\text {proc}(a_{\scriptscriptstyle S}, P)$ is shown below.

An important point is that $a_{\scriptscriptstyle S}$ is of type $A_{\scriptscriptstyle S}$ in $\varGamma$ and $A'_{\scriptscriptstyle S}$ is only local to the process typing judgment; thus, the provider P views the channel $a_{\scriptscriptstyle S}$ at type $A'_{\scriptscriptstyle S}$ while all clients view the channel $a_{\scriptscriptstyle S}$ at type $A_{\scriptscriptstyle S}$. The subtyping relation $A'_{\scriptscriptstyle S} \le A_{\scriptscriptstyle S}$ is subsumed by the subsynchronizing judgment $\vdash (A'_{\scriptscriptstyle S}, A_{\scriptscriptstyle S}, \top ) \; \text {ssync}$ which guarantees that the pair $(A'_{\scriptscriptstyle S}, A_{\scriptscriptstyle S})$ is subsynchronizing.

A configuration typing rule for some (linear) $\text {proc}(a_{\scriptscriptstyle L}, P), \varTheta '$ is shown below.

Since P may use some linear channels $\varDelta _a$, we split the offering channels of $\varTheta '$ to $\varDelta _a, \varDelta '$ and make explicit that P will consume $\varDelta _a$. Similar to the shared case, the process typing judgment (third premise) locally assumes $a_{\scriptscriptstyle L}$ is of type $A'_{\scriptscriptstyle L}$ such that $A'_{\scriptscriptstyle L} \le A_{\scriptscriptstyle L}$ (again, subsumed by the subsynchronizing judgment), guaranteeing that a client of $a_{\scriptscriptstyle L}$ view the channel as type $A_{\scriptscriptstyle L}$.

6.4 Dynamics

The operational semantics of the system is formulated through multiset rewriting rules [5], which is of form ${S_1, \ldots , S_n \rightarrow T_1, \ldots , T_m}$, where each $S_i$ and $T_j$ corresponds to a process predicate. Each rule captures a transition in a subset of the configuration; for example, the following is one of three rules that capture the semantics of forwarding:

Connect predicates are consumed if a process acquires linearly on a channel that is provided by a shared process. We first show how a shared process providing some $b_{\scriptscriptstyle S}$ can be acquired:

The rule says that a client can successfully acquire if there is a corresponding accept by the provider. In the following rule, a connect predicate “coordinates” the acquire/accept between different modes:

6.5 Theorems

So far, we have incompletely introduced the statics [20, Appendix D] and the dynamics [20, Appendix E] of the system, focusing on the interesting cases that depart from the system presented in [2].

The preservation theorem, or session fidelity, guarantees that well-typed configurations remain well-typed. In particular, this means that processes will always adhere to the protocol denoted by the session type.

Theorem 1 (Preservation)

If ${\varGamma \models \varLambda ;\varTheta \,::\, (\varGamma ;\varDelta )}$ for some $\varLambda , \varTheta , \varGamma ,$ and $\varDelta$, and $\varLambda ;\varTheta \rightarrow \varLambda ';\varTheta '$ for some $\varLambda ';\varTheta '$, then ${\varGamma '\models \varLambda ';\varTheta ' \,::\, (\varGamma ';\varDelta )}$ where $\varGamma ' \preceq \varGamma$.

Proof

By induction on the dynamics and constructing a well-typed configuration for each case. See [20, Appendix F] for the detailed proof, covering all cases.

The $\varGamma ' \preceq \varGamma$ captures the idea that the configuration can gain additional shared processes and that the types of shared channels can become smaller. For example, if a process spawns an additional shared process, then the configuration will gain an additional channel in $\varGamma$ and if a shared channel is released to a smaller type, the type of the shared channel in $\varGamma$ can become smaller. Note that although it is indeed true that linear processes can be spawned, it will never appear in $\varDelta$ since the linear channel that the newly spawned process offers must be consumed by the process that spawned the channel, meaning $\varDelta$ is unchanged.

The progress theorem is as in [2], where we only allow configurations to be stuck due to failure of some client to acquire, for example, due to deadlock. A poised process [2, 17] is one that is currently trying to communicate across its offering channel and is analogous to the role of values in typical functional languages. Both shared and linear configurations are poised if and only if all its processes are trying to communicate across its offering channel.

Theorem 2 (Progress)

If ${\varGamma \models \varLambda ;\varTheta \,::\, (\varGamma ;\varDelta )}$ then either:

• 1. $\varLambda ;\varTheta \rightarrow \varLambda ';\varTheta$ for some $\varLambda '$ or

• 2. $\varLambda$ is poised and one of:

  • (a) $\varLambda ;\varTheta \rightarrow \varLambda ';\varTheta '$ or

  • (b) $\varTheta$ is poised or

  • (c) a linear process in $\varTheta$ is unable stuck and therefore unable to acquire

Proof

By induction on the typing of the configuration $\varLambda ; \varTheta$. We begin by induction on the typing of $\varLambda$ to prove either (1) or $\varLambda$ is poised. After, we prove (2) by induction on the typing of $\varTheta$ while assuming $\varLambda$ is poised. See [20, Appendix G] for the detailed proof.

Remark 4

Another paper [3] introduces additional static restrictions to allow a stronger and more common notion of progress, which are orthogonal to our results. Adopting this extension to the system we present here would give the usual notion of progress with deadlock freedom.

7 Related Work

Our paper serves as an extension to the manifest sharing system defined in [2] by introducing a notion of subtyping to the system which allows us to statically relax the equi-synchronizing constraint. Early glimpses of subtyping can be seen in the previous system with the introduction of $\bot$ and $\top$ as the minimal and maximal constraints, which happened to be compatible with our subtyping relation.

Subtyping for session types was first proposed by Gay and Hole [11], and a slightly modified style of session types guided from the correspondence with intuitionistic linear logic was given a subtyping extension [1]. Both these papers do not investigate the more recently discovered modal shifts, which is our contribution to the subtyping front.

There have also been many recent developments in subtyping in the context of multiparty session types [6, 7, 12, 13], which are a different class of type systems that describe protocols between an arbitrary number of participants from a neutral global point of view. Understanding the relation of our subtyping system to these systems is an interesting item for future work.

8 Conclusion

We propose a subtyping extension to a message passing concurrency programming language introduced in previous work [2] and showed examples highlighting the expressiveness that this new system provides. Throughout the paper, we follow two important principles, substitutability and ignorance is bliss, which gave a rich type system that in particular allows phases (in a shared setting) to be manifest in the type.

One immediate application of shared subtyping is that combined with refinement types [9, 10], it can encode finer specifications of protocols. For example in the auction scenario, we can statically show that each client that does not win a bid gets refunded precisely the exact amount of money it bid. Without shared to linear subtyping, specifications of shared communication across multiple acquire-release cycles were not possible.

A future work in a more theoretical platform is to extend the setting to adjoint logic [18], which provides a more general framework of reasoning about modal shifts in a message passing system. In particular, we found that affine session types, where contraction (aliasing) is rejected, have immediate applications.