Fair Termination of Asynchronous Binary Sessions

Session type systems [32, 33, 35] have become a widespread formalism for ensuring a variety of safety and liveness properties of communicating processes through static analysis. Session types specify the sequences of messages that can be sent over a channel, and the type system makes sure that (1) well-typed processes comply with this protocol specification and that (2) the peer endpoints of the channel are used according to compatible protocols.

Many session type systems are defined for a synchronous calculus or language even if the actual underlying communication model is meant to be asynchronous. The point is that synchronous theories of session types are simpler and easier to work with and most if not all properties of a synchronous session type system hold even if the actual communication model is asynchronous. However, awareness of the communication model can help relaxing the type system and thus enlarging the family of well-typed processes. This observation has led to the study of asynchronous subtyping relations for session types [40, 39, 11] allowing processes to anticipate output messages with respect to the protocol specification they are expected to comply with, provided that anticipated outputs do not depend on incoming messages. This apparent violation of the protocol specification enabled by asynchronous subtyping is harmless precisely because output actions are non-blocking in an asynchronous setting.

The available session type systems based on asynchronous subtyping focus on the enforcement of safety properties but struggle at ensuring liveness properties of many simple communication patterns. As an illustration of such patterns consider a server that, in order to fulfill a request received from a session $x$, splits the request into an arbitrary number of tasks handled by a separate worker and then gathers the partial results to answer the client. We might be interested in establishing whether the client eventually receives a response.

To be more concrete, let us model the server as the term

which indicates the input of the request followed by the spawning of a $\mathrm{𝑆𝑝𝑙𝑖𝑡}$ process and of a $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$ process connected by a new session $y$.

The $\mathrm{𝑆𝑝𝑙𝑖𝑡}$ process is modeled by the following definitions:

according to which the server sends to the worker a non-deterministically chosen number of $\mathrm{𝗍𝖺𝗌𝗄}$s followed by a $\mathrm{𝗌𝗍𝗈𝗉}$ on session $y$, it then gathers from the worker an arbitrary number of $\mathrm{𝗋𝖾𝗌}$ults followed by a $\mathrm{𝗌𝗍𝗈𝗉}$, and finally sends back to the client a $\mathrm{𝗋𝖾𝗌𝗉}$onse on session $x$.

One possible modeling of the worker process is according to the definition

so that the worker sends a $\mathrm{𝗋𝖾𝗌}$ult for each $\mathrm{𝗍𝖺𝗌𝗄}$ it receives. The eye-catching aspect of $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$ is that it does not interact according to the “complementary” protocol implemented on the server side, at least not in the sense that is usually intended in (synchronous) session type theories. Indeed, while the server first sends all the $\mathrm{𝗍𝖺𝗌𝗄}$s and then gathers all the $\mathrm{𝗋𝖾𝗌}$ults, the worker eagerly sends one $\mathrm{𝗋𝖾𝗌}$ult after receiving each $\mathrm{𝗍𝖺𝗌𝗄}$.

In an asynchronous setting, the fact that $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$ sends some messages earlier than expected is not an issue since output actions are non-blocking. However, we would like to be sure that these early $\mathrm{𝗋𝖾𝗌}$ults do not keep accumulating and are eventually consumed by $\mathrm{𝐺𝑎𝑡ℎ𝑒𝑟}$. There is nothing in the modeling of $\mathrm{𝑆𝑝𝑙𝑖𝑡}$, $\mathrm{𝐺𝑎𝑡ℎ𝑒𝑟}$ and $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$ that prevents this from happening, but we can prove the eventual consumption of every $\mathrm{𝗋𝖾𝗌}$ult only under the assumption that sooner or later $\mathrm{𝑆𝑝𝑙𝑖𝑡}$ will send $\mathrm{𝗌𝗍𝗈𝗉}$ to $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$. If we broaden our viewpoint, we see that the same assumption is necessary to prove that the client interacting with the server does not starve. While the server is running, the client is awaiting for a $\mathrm{𝗋𝖾𝗌𝗉}$onse from session $x$. In order to prove that the client will eventually receive a $\mathrm{𝗋𝖾𝗌𝗉}$onse, we have to assume that $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$ will terminate the session $y$, which in turn requires the assumption that $\mathrm{𝑆𝑝𝑙𝑖𝑡}$ will eventually send $\mathrm{𝗌𝗍𝗈𝗉}$ to $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$. In general, the proof of any non-trivial liveness property that concerns the eventual production or consumption of a message on a certain session may require the assumption that every other session eventually terminates. For this reason, ensuring the eventual termination of sessions should be a primary goal of any session type system aimed at enforcing liveness properties. As we have seen in the discussion above, proving the eventual termination of a session may require some fairness assumptions like the fact that $\mathrm{𝑆𝑝𝑙𝑖𝑡}$ will eventually stop sending $\mathrm{𝗍𝖺𝗌𝗄}$s. For this reason, in the literature such eventual termination property is referred to as fair termination [30, 26, 2].

In this work we study a theory of asynchronous session types and an associated session type system ensuring that well-typed processes are fairly terminating under a suitable fairness assumption. The fair termination of processes entails the fair termination of the sessions they operate on, hence that all messages produced – including those sent earlier than expected – are eventually consumed and that all processes waiting for a message eventually receive one. In other words, the very same type system prevents process starvation and ensures the absence of orphan messages. Related works achieve these goals only partially:

• $\mathrm{■}$

  The theories of asynchronous session types developed by Mostrous et al. [40, 39], Chen et al. [11] and Ghilezan et al. [29] require that every output can be only anticipated with respect to finitely many inputs. Since there is no finite upper bound to the number of $\mathrm{𝗍𝖺𝗌𝗄}$s that $\mathrm{𝑆𝑝𝑙𝑖𝑡}$ can produce, each early $\mathrm{𝗋𝖾𝗌}$ produced by $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$ anticipates an unbounded number of inputs leaving $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$ out of reach for the aforementioned theories.

• $\mathrm{■}$

  Bravetti, Lange and Zavattaro [8] study an asynchronous subtyping relation for session types that allows early outputs to anticipate an unbounded number of inputs. However, their subtyping relation disallows any covariance of outputs, which is needed to account for the fact that the behavior of $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$ is more deterministic than the behavior expected by $\mathrm{𝐺𝑎𝑡ℎ𝑒𝑟}$. Indeed, while $\mathrm{𝐺𝑎𝑡ℎ𝑒𝑟}$ expects to receive an arbitrary number of $\mathrm{𝗋𝖾𝗌}$ults, $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$ produces exactly as many $\mathrm{𝗋𝖾𝗌}$ults as the number of $\mathrm{𝗍𝖺𝗌𝗄}$s it receives from $\mathrm{𝑆𝑝𝑙𝑖𝑡}$.

• $\mathrm{■}$

  None of the aforementioned works provides guarantees on the eventual fulfillment of the client’s request, either because they do not make sure that every session eventually terminates [11, 29] or because they do not take multiple sessions into account [29, 8].

• $\mathrm{■}$

  Ciccone, Dagnino and Padovani [14, 16, 13] study session type systems ensuring the fair termination of sessions, but their works are based on synchronous communication models that do not support any form of output anticipation like the one exemplified by $\mathrm{𝑊𝑜𝑟𝑘𝑒𝑟}$.

The theory of asynchronous session types that we propose in this paper addresses all these limitations. In addition, we also make the following technical contributions:

• $\mathrm{■}$

  We define a fair asynchronous subtyping relation for session types that is coarser than those in the literature for the family of eventually terminating session types. Unlike many existing fair/asynchronous subtyping relations [39, 14, 13, 8] our subtyping relation is closed under duality. This property is key for proving the type system sound.

• $\mathrm{■}$

  We give the first fair asynchronous semantics of session types using a labelled transition system (LTS) defined by bounded coinduction [1, 18]. The adoption of this semantics allows us to characterize fair asynchronous subtyping in a way that is structurally the same as the one for the well-known synchronous subtyping defined by Gay and Hole [28].

• $\mathrm{■}$

  Our theory of asynchronous session types with fair asynchronous subtyping is the first one where the process model and the type system are rooted in linear logic [45, 10, 37]. We incorporate fair asynchronous subtyping in the type system as generalized forms of the cut and linear logic axiom thanks to the aforementioned closure under duality. Also, instead of introducing explicit message buffers, we model asynchronous communications by means of suitable commuting conversions and deep cut reductions in linear logic proofs.

In this section we present syntax and semantics of a calculus of asynchronous processes called CaP and we formulate the safety and liveness properties that our type system guarantees. At the surface level, CaP closely resembles other calculi of binary sessions based on linear logic such as CP [45] or $\mu$CP [37]. The main differences between CaP and these calculi are that CaP supports general recursion, it includes a non-deterministic choice operator and above all it models asynchronous communication by giving a non-blocking semantics to output actions, which essentially act like message buffers.

The syntax of processes is shown in Table 1 and makes use of an infinite set of channels ranged over by $x$, $y$ and $z$, a set $\mathrm{𝖳𝖺𝗀𝗌}$ of tags ranged over by $𝖺$, $𝖻$, $\mathrm{\dots }$ and a set of process names ranged over by $A$, $B$, etc. The terminated process, which performs no actions, is denoted by $\mathrm{𝖽𝗈𝗇𝖾}$. The term $A⟨\overline{x}⟩$, where $\overline{x}$ is a possibly empty sequence of channels, represents the invocation of the process named $A$. We assume that for each such invocation there exists a unique global definition of the form $A(\overline{x})=P$ that gives meaning to the name $A$. We also assume that all invocations occur guarded by a prefix or by a non-deterministic choice. The term $x\leftrightarrow y$ models a link, that is a process that forwards every message received from $x$ to $y$ and vice versa, effectively unifying the two channels. Links are typical of calculi based on linear logic since their typing rule correspond to the axiom of the logic. The terms $\mathrm{𝖼𝗅𝗈𝗌𝖾}x$ and $\mathrm{𝗐𝖺𝗂𝗍}x.P$ model processes that respectively send and receive a termination signal on $x$. Note that $\mathrm{𝖼𝗅𝗈𝗌𝖾}x$ has no continuation, as is the case in most calculi based on linear logic, whereas $\mathrm{𝗐𝖺𝗂𝗍}x.P$ continues as $P$. The term $x(y)[P].Q$ models a bifurcating session: it creates a new channel $y$, sends $y$ on $x$, forks a new process $P$ that uses $y$, and then continues as $Q$. The process $x(y).P$ waits for a channel $y$ from $x$ and then continues as $P$. The terms $x⊲𝖺.P$ and $x⊳{\{{𝖺}_i:P_i\}}_{i\in I}$ model processes that respectively send and receive a tag. The sender selects one particular tag $𝖺$ to send. The receiver continues as $P_i$ depending on the tag ${𝖺}_i$ that it receives. In the examples we sometimes use tags as an abstract representation of more complex messages, such as $\mathrm{𝗋𝖾𝗊}$uests or $\mathrm{𝗍𝖺𝗌𝗄}$s. The term $(x)(P|Q)$ models the parallel composition of two processes $P$ and $Q$ connected by the channel $x$. We often refer to this term as a cut, since its typing rule coincides with the cut rule of linear logic. Finally, the term $P\oplus Q$ models the non-deterministic choice between $P$ and $Q$.

It is known that links in conjunction with bifurcating sessions can be used to encode session delegation, whereby processes exchange an existing (rather than new) channel $z$ on $x$. This behavior can be modeled by a term of the form $x(y)[y\leftrightarrow z].P$. As we will see in Section 6, CaP links also act as explicit casts enabling useful forms of subsumption.

The notions of free and bound channels for processes are defined as expected with the proviso that a process of the form $x(y)[P].Q$ binds $y$ in $P$ but not in $Q$. We identify processes up to renaming of bound channels and we write $\mathrm{𝖿𝗇}(P)$ for the set of channels occurring free in $P$. Also, for every global definition $A(\overline{x})=P$ we assume $\mathrm{𝖿𝗇}(P)=\{\overline{x}\}$.

We have anticipated that CaP adopts an asynchronous communication model. In practice this would be implemented by FIFO buffers storing messages that have been produced but not consumed. In CaP, we model asynchrony giving a non-blocking semantics to the output actions $x(y)[Q].P$ and $x⊲𝖺.P$. That is, we allow the continuation $P$ to reduce and/or interact with other sub-processes even if the prefix has not been consumed. In a sense, we consider the prefixes $x(y)[Q]$ and $x⊲𝖺$ as floating messages or parts of a buffer associated with channel $x$. In general, we call buffer any term generated by the following grammar:

A buffer is either empty, represented by a hole $[]$, or a tag $𝖺$ sent on $x$ followed by a buffer for $x$, or a fresh channel $y$ (with associated process $P$) sent on $x$ and followed by a buffer for $x$. Note that the annotation $x$ in the metavariable ${ℬ}_x$ is meant to bind the channel on which the messages in the buffer have been sent. Therefore, having at our disposal a buffer ${ℬ}_x$, we can write ${ℬ}_y$ for the buffer that has the same structure as ${ℬ}_x$ but where $x$ has been replaced by $y$. Buffers vaguely resemble reduction contexts, except that they allow us to place a hole behind output prefixes since these are meant to be non-blocking. Hereafter we write ${ℬ}_x[P]$ for the process obtained by replacing the hole in ${ℬ}_x$ with $P$.

The operational semantics of CaP is given by a structural pre-congruence relation $⊒$ and a reduction relation $\to$, both defined in Table 2. In simple words, structural pre-congruence relates processes that are essentially equivalent except for the order of independent actions, while reduction describes communications and the resolution of non-deterministic choices.

We can roughly classify the rules for structural pre-congruence in four groups. The first group contains [s-call], [s-link] and [s-comm], which capture expected properties of process invocations, links and parallel compositions: a process invocation $A⟨\overline{x}⟩$ is indistinguishable from $P$ if $A(\overline{x})=P$; a link $x\leftrightarrow y$ is indistinguishable from $y\leftrightarrow x$; a cut $(x)(P|Q)$ is indistinguishable from $(x)(Q|P)$, that is parallel composition is commutative.

The second group of rules contains [s-wait], [s-case] and [s-join]. These rules allow an input action on some channel $y$ to be extruded from a cut on $x$ when $x\ne y$. The purpose of these transformations is to move inputs on $y$ close to outputs on $y$, so as to enable interactions in the session $y$. These transformations correspond to well-known rearrangements of linear logic proofs (for example, they are sometimes referred to as external reductions [3, 25]), except that in CaP we allow the input prefix to be found within an arbitrary buffer ${ℬ}_x$, coherently with the intuition that (output) actions in a buffer are non-blocking. The side condition $z\notin \mathrm{𝖿𝗇}({ℬ}_x)$ in [s-join] makes sure that free occurrences of $z$ in ${ℬ}_x$ are not accidentally captured by the binding prefix. Since we consider processes (and buffers) modulo renaming of bound names and there is an infinite supply of names, the bound $z$ can always be renamed so as to enable this process transformation.

The third group of rules contains [s-pull-0], [s-pull-1] and [s-pull-2]. These rules are similar to those of the second group, except that they allow whole buffers of messages on $y$ to float through cuts on $x$ when $x\ne y$. [s-pull-2] is simple and speaks for itself while [s-pull-1] deals with the case in which the name $x$ bound by the cut occurs in the process $P$ associated with a fresh channel $z$ sent on $y\ne x$. In this case the cut as a whole becomes associated with $z$. In principle we should also specify the side condition $x\notin \mathrm{𝖿𝗇}(Q)$, but this condition holds for well-typed processes when $x\in \mathrm{𝖿𝗇}(P)$. The rule [s-pull-0] covers a somewhat peculiar case of [s-pull-2], whereby a buffer ${ℬ}_x$ can be extruded from the cut on $x$ because there is a link $x\leftrightarrow y$ that acts as a forwarder from $x$ to $y$. Note that the extruded buffer ${ℬ}_x$ turns into ${ℬ}_y$, so as to reflect the forwarding effect of the link.

The fourth and final group of rules contains [s-pull-3] and [s-pull-4]. These rules allow buffers for different channels to be permuted. Again [s-pull-3] deals with the special case in which a channel $x$ occurs in the process $P$ associated with a fresh channel $z$.

In the definition of structural pre-congruence there are some glaring omissions (e.g. associativity of parallel composition) and very few rules are invertible. This is not because the missing rules would be unsound, but because they turn out to be unnecessary for proving that well-typed processes are deadlock free and fairly terminating.

Base reductions consist of [r-choice], [r-close], [r-select] and [r-fork] which respectively model the reduction of a non-deterministic process, the termination of the session $x$ and the consumption of tags and channels sent on channel $x$. The rules are almost standard, except that [r-select] and [r-fork] allow input actions on $x$ to operate from within arbitrary buffers for $x$. The buffers represent asynchronously sent messages that do not block subsequent actions. At the logical level, these interactions correspond to deep cut reductions in a sense that resembles deep inference [31], whereby logical rules can be applied deep within a context. Unlike [r-select] and [r-fork], there is no buffer around $\mathrm{𝗐𝖺𝗂𝗍}x.P$ in [r-close]. This rule implies that a session cannot be closed unless all the messages (asynchronously) produced therein have also been consumed. Note that this property is enforced by the type system and is not meant to be checked at runtime. Rules [r-cut], [r-buffer] and [r-str] propagate reductions across cuts and buffers and close them by structural pre-congruence.

Hereafter we write ${\to }^{\ast }$ for the reflexive, transitive closure of $\to$. We write $P\to$ if $P\to Q$ for some $Q$ and $P/\to$ if not $P\to$.

We can now formally define the safety and liveness properties we are interested in.

Deadlock freedom is an instance of safety property. A deadlock-free process either reduces or it is (structurally pre-congruent to) $\mathrm{𝖽𝗈𝗇𝖾}$. For example, the process $\mathrm{\Omega }()=\mathrm{\Omega }⟨⟩\oplus \mathrm{\Omega }⟨⟩$ is deadlock free (we have $\mathrm{\Omega }⟨⟩\to \mathrm{\Omega }⟨⟩$) whereas $(x)(\mathrm{𝖼𝗅𝗈𝗌𝖾}y|\mathrm{𝗐𝖺𝗂𝗍}x.\mathrm{𝖽𝗈𝗇𝖾})$ is deadlocked. When a deadlock-free process stops reducing, it contains no pending actions and all of its sessions have been closed. In particular, all the messages in buffers have been consumed.

The liveness properties we are interested in are related to termination, of which there exist several variants. A reduction sequence of $P$ is a sequence $(P_0,P_1,\mathrm{\dots })$ such that $P_0=P$ and $P_i\to P_{i+1}$ whenever $i+1$ is not greater than the length of the sequence. A run is a maximal reduction sequence, in the sense that either it is infinite or the last process in the sequence (say $P_n$) does not reduce (that is, $P_n/\to$). We say that $P$ is weakly terminating if it has a finite run, that $P$ is terminating if every run of $P$ is finite, and that $P$ is diverging if every run of $P$ is infinite. For example, $\mathrm{\Omega }⟨⟩\oplus \mathrm{𝖽𝗈𝗇𝖾}$ is weakly terminating but not terminating, $\mathrm{𝖽𝗈𝗇𝖾}\oplus \mathrm{𝖽𝗈𝗇𝖾}$ is terminating, and $\mathrm{\Omega }⟨⟩$ is diverging. Note that here we call “termination” the mere inability to reduce further and not the fact that a process has become $\mathrm{𝖽𝗈𝗇𝖾}$. For example, $\mathrm{𝖽𝗈𝗇𝖾}$, $\mathrm{𝖼𝗅𝗈𝗌𝖾}x$ and $(x)(\mathrm{𝖼𝗅𝗈𝗌𝖾}y|\mathrm{𝗐𝖺𝗂𝗍}x.\mathrm{𝖽𝗈𝗇𝖾})$ are all terminated (they do not reduce), but only $\mathrm{𝖽𝗈𝗇𝖾}$ is also deadlock free. So it really is the combination of deadlock freedom (Definition 1) and some termination property that we wish to enforce with our type system.

The termination property we target in this work is called fair termination [30, 26, 2]. Fair termination consists of those processes such that all of their infinite runs are considered to be unrealistic or unfair and therefore can be ignored insofar termination is concerned. We could say that these processes may diverge in principle, but they terminate in practice. Clearly, fair termination depends on a fairness notion that discriminates fair runs from unfair ones. Among all fairness notions, here we consider a particular instance of full fairness [44].

Remember that a run is a maximal reduction sequence of a process. So, along a fair run the process only has finitely many chances to terminate. This can happen either because the run is finite (the process eventually terminates) or because the run contains a diverging process (at some point termination is no longer possible). For example, the infinite run $(\mathrm{\Omega }⟨⟩\oplus \mathrm{𝖽𝗈𝗇𝖾},\mathrm{\Omega }⟨⟩,\mathrm{\dots })$ is fair because only the first process in it is weakly terminating. We find it useful to also look at the negation of the notion of fair run: an unfair run is necessarily infinite and contains infinitely many weakly terminating processes. In other words, an unfair run describes a computation along which termination is always reachable, but it is never reached as if the process is avoiding it on purpose. For example, if $A()=A⟨⟩\oplus \mathrm{𝖽𝗈𝗇𝖾}$ then the infinite run $(A⟨⟩,A⟨⟩,\mathrm{\dots })$ is unfair because $\mathrm{𝖽𝗈𝗇𝖾}$ is always reachable but never reached.

For example, $A()=A⟨⟩\oplus \mathrm{𝖽𝗈𝗇𝖾}$ is fairly terminating whereas $\mathrm{\Omega }⟨⟩\oplus \mathrm{𝖽𝗈𝗇𝖾}$ is not because it has an infinite fair run. There are two reasons why full fairness is a suitable fairness assumption in our setting. First, full fairness has been shown to be the strongest conceivable fairness assumption [44], which means that it allows us to target the largest family of fairly terminating processes. Second, it has been observed [12] that this family admits the following alternative characterization which does not mention fair runs at all.

The relevance of this characterization rests in the fact that it provides the key proof method for the soundness of our type system. Indeed, suppose that the type system ensures that well-typed processes weakly terminate. We expect the type system to also enjoy subject redution, namely the property that well-typed processes always reduce to well-typed processes. But then, using the right-to-left implication in Theorem 4, the very same type system also ensures that well-typed processes fairly terminate.

We define the subtyping relation for asynchronous session types in three steps. First of all, we formalize what we mean by correct asynchronous composition between the session types describing the protocols implemented by two processes using the two endpoints of a session. In many session type systems, this notion coincides with session type duality. Since we have to take asynchrony into account, duality alone is too strict so we need a notion of correct composition using the LTS defined in Section 3. Once this notion is in place, asynchronous subtyping can be defined as the relation that preserves correct asynchronous composition. This relation is “sound” by definition, but its properties can be intrinsically difficult to grasp. The final step will be to provide a precise (i.e. sound and complete) alternative characterization of asynchronous subtyping that sheds light on its properties.

The definition of correct asynchronous composition is given below.

In words, Items 2, 3, 4, and 5 state that $(S,T)$ forms a correct composition if, whenever one of the two types performs a (possibly early) output transition $!\sigma$, the other type is able to respond with a (possibly late) compatible input transition $\mathrm{?}\tau$ and the continuations remain correct. In general this is not enough to guarantee progress because early outputs are only allowed but not mandatory. For example, the types and satisfy Items 2 and 3, but two processes strictly adhering to these protocols (i.e. without performing early outputs) would starve. Item 1 requires that at least one of the two types is positive, namely that at least on one side of the session the outputs are guaranteed to be immediate. This is enough to ensure progress. For example, we have as well as .

It is easy to see that $⨝$ is symmetric and that duality implies correctness:

Other properties of $⨝$ are more surprising. For example, if and $R=\oplus \{𝖺:R\}$, we have that $S⨝R$ does not hold because of the early output transition $S\stackrel{!𝖼}{⟶}$ to which $R$ is unable to respond. The lack of compatibility between $S$ and $R$ is due to the fact that (the process behaving as) $S$ makes a fairness assumption on the behavior of the process it is interacting with. More precisely, a process complying with $S$ assumes that sooner or later a $𝖻$ message will be received, finally enabling the output of $𝖼$. In anticipation of this, the process may decide to perform an early output of $𝖼$, but in doing so it would generate an orphan message when interacting with another process adhering to $R$, which is not honoring this fairness assumption. It is also easy to see that $\mathrm{𝟎}⨝S$ holds for every $S$ and that $\top ⨝S$ implies $S=\mathrm{𝟎}$. These properties of $\mathrm{𝟎}$ and $\top$ follow directly from the [may-$\oplus$] and [may-$\&$] rules that we have commented in Section 3.

We can now define fair asynchronous subtyping semantically using Liskov’s substitution principle [38] where the property being preserved is session correctness (Definition 8).

Paraphrasing, this definition says that a process using a channel $x$ according to $T$ can be safely replaced by a process using $x$ according to $S$ when $S$ is a subtype of $T$. Indeed, the peer process, which is assumed to use the same channel $x$ according to some session type $R$ such that $R⨝T$, will still interact correctly after the substitution has taken place.

A few subtyping relations are easy to figure out. For example, we have $\mathrm{𝟎}⩽S$ and $S⩽\top$ for every $S$ because of the properties of $\mathrm{𝟎}$ and $\top$ that we have pointed out above. It is also easy to see that holds in an asynchronous setting. After all, the process that behaves according to is sending a tag $𝖺$ that also the process that behaves according to may anticipate. Note that the inverse relation does not hold, despite the fact that and perform exactly the same transitions, because forms a correct asynchronous composition with but not with (Item 1 of Definition 8 is violated).

The above notion of subtyping is sound “by definition”, but provides little information concerning the shape of related session types. To compensate for this problem, we also give a sound and complete coinductive characterization of $⩽$, which relates directly to Definition 8.

Items 2, 3, 4, and 5 of Definition 12 specify the expected requirements for a session subtyping relation: every input transition of the supertype $T$ must be matched by an input transition of the subtype $S$ and the corresponding continuations should still be related by subtyping; dually, every output transition of the subtype $S$ must be matched by an output transition of the supertype $T$ and the corresponding continuations should still be related by subtyping. Interestingly, these items are essentially the same found in analogous characterizations of synchronous subtyping for session types [28], modulo the different orientation of $⩽$ due to our viewpoint based on the substitution of processes rather than on the substitution of channels.¹¹1The interested reader may refer to Gay [27] for a comparison of the two viewpoints. However, the clauses of Definition 12 are not mutually exclusive, because the same session type may perform both input and output transitions. Also, session types related by subtyping need not start with the same type constructor. In this respect, Item 1 makes sure that the smaller session type can only anticipate (and not postpone) outputs, as argued above.

Definition 12 is a sound and complete characterization of $⩽$.

Using Definitions 12 and 13 we can prove some significant properties of $⩽$:

• $\mathrm{■}$

  (input contravariance) if $J\subseteq I$ by Item 2;

• $\mathrm{■}$

  (output covariance) $\oplus {\{{𝖺}_i:S_i\}}_{i\in I}⩽\oplus {\{{𝖺}_i:S_i\}}_{i\in J}$ if $I\subseteq J$ by Item 3;

• $\mathrm{■}$

  (output anticipation) . Note that the inverse relation does not hold, despite these two session types have exactly the same transitions, because of Item 1.

There are exceptions to output covariance and input contravariance when one of the two types specifies a non-terminating protocol. The next example illustrates one of such cases.

The cases in which co/contra variance does not hold have no impact on the typeability of CaP processes: since our type system ensures the fair termination of well-typed processes, protocols like $T$ in Example 14 are not inhabited. We will see in Section 7 that $⩽$ includes other subtyping relations supporting full co/contra variance for the family of fairly terminating session types, those that always allow the protocol to end.

We now list a few properties of $⩽$. First of all, we establish that $⩽$ is closed by duality.

In this section we describe the type system for CaP ensuring that well-typed processes weakly terminate, besides being free from communication errors and deadlocks. Theorem 4 then allows us to conclude that the very same type system also ensures fair termination when we make the fairness assumption stated in Definition 2. The type system is based on the proof rules of MALL but also includes typing rules for the non-logical process forms, namely termination, process invocation and non-deterministic choice.