A Sound and Complete Characterization of
Fair Asynchronous Session Subtyping

Abstract models such as communicating finite-state machines [3] and asynchronous session types [18] are essential to reason about correctness of distributed systems whose components communicate with point-to-point fifo channels. A fundamental issue, which makes it possible to manage system correctness in a compositional way, is the development of techniques allowing a component to be refined independently of the others, without compromising the correctness of the whole system. In this respect, the notion of fair asynchronous refinement for session types introduced by Bravetti, Lange and Zavattaro [6] guarantees fair termination, i.e. successful termination under fairness assumption: execution traces that loop forever are deemed unrealistic/unimportant and are not considered. Such a notion implies all the desirable safety and liveness properties of communicating systems, including communication safety, deadlock freedom, absence of orphan messages, and lock freedom. However, while the semantic (à la testing) definition of such refinement is straightforward, its (coinductive) characterization (à la session subtyping) has proved to be quite challenging. In fact, Bravetti, Lange and Zavattaro [6] only provide a sound but not complete characterization.

With respect to previous notions of asynchronous session subtyping [22, 9] (which leverage asynchrony by allowing the refined component to anticipate message emissions, but only under certain conditions) fair asynchronous subtyping [6] makes it possible to encompass subtypes that occur naturally in communication protocols, e.g. where two parties simultaneously send each other a finite but unspecified amount of messages before consuming them from their buffers. We illustrate this scenario in Figure 1, which depicts the interaction between a spacecraft $S$ and a ground station $G$ that communicate via two unbounded asynchronous channels (one in each direction). For convenience, the protocols are represented as communicating finite-state machines [3], i.e. with a labeled transition system-like notation where “?” represents inputs, “!” represents outputs, and the initial state is indicated by an incoming arrow. Consider $T_S$ and $T_G$ first. Session type $T_S$ is the abstraction of the spacecraft, which may send a finite but unspecified number of telemetries $\mathrm{𝗍𝗆}$ (abstractly modeling a for loop), followed by a message $\mathrm{𝗈𝗏𝖾𝗋}$. In the second phase, the spacecraft receives a number of telecommands ($\mathrm{𝗍𝖼}$), followed by a message $\mathrm{𝖽𝗈𝗇𝖾}$. In principle, the ground station should behave as the type $T_G$ which is the dual of $T_S$ (denoted by $\overline{T_S}$) where outputs become inputs and vice-versa. However, since the flyby window may be short, it makes sense to implement the ground station so that it communicates with the satellite by anticipating the output of the commands. That is, the ground station follows the type $T_G^{\prime }$, which sends telecommands before receiving telemetries. In this way $T_G^{\prime }$ and $T_S$ interact in a symmetric manner: they first send all of their messages and then consume the messages sent from the other partner. No communication error can occur, and the communication protocol can always terminate successfully, with empty queues. In fact $T_G^{\prime }$ and $T_S$ also form a correct composition in the sense that every message that is sent by one participant is eventually received by the other. The session subtyping presented by Bravetti, Lange and Zavattaro [6], which is proved to be a sound characterization of fair asynchronous session refiment, makes it possible to actually prove that $T_G^{\prime }$ refines $T_G$.

Let us now consider, in Figure 2, a more complex scenario concerning a processing server $PS$ and its client $C$. Consider $T_{PS}$ and $T_C$ first. Session type $T_{PS}$ is the abstraction of a batch processing server and $T_C$ that of a client. Note that these types are respectively isomorphic to $T_G$ and $T_S$ of Figure 1: now the client $T_C$ sends generic requests $\mathrm{𝗋𝖾𝗊}$ (instead of specific telemetry data $\mathrm{𝗍𝗆}$) and, when it decides to stop sending via $\mathrm{𝗌𝗍𝗈𝗉}$, it keeps waiting for responses $\mathrm{𝗋𝖾𝗌𝗉}$ (instead of telecommand data $\mathrm{𝗍𝖼}$) until it receives $\mathrm{𝗌𝗍𝗈𝗉}$. As in the previous scenario, the client $T_C$ and the batch processing server $T_{PS}$ (which is its dual) obviously form a correct composition. Also here it is possible to consider a more efficient version of the processing server, i.e. a stream processing server $T_{PS}^{\prime }$ which immediately (and asynchronously) sends the response to each request it receives. In this scenario, it may be natural to send responses one at a time after each request. In fact also $T_{PS}^{\prime }$ and $T_C$ form a correct composition. Actually, we have that $T_{PS}^{\prime }$ is a fair asynchronous session refinement of $T_{PS}$, meaning that $T_{PS}^{\prime }$ is a good replacement of $T_{PS}$ in any possible context. However, the characterization provided by Bravetti, Lange and Zavattaro [6] is unable to capture this specific refinement.

Technically speaking, the coinductive characterization of subtyping given by Bravetti, Lange and Zavattaro [6] is not complete because it does not support output covariance, that is the possibility for a subtype to remove branches in output choices, corresponding to a reduced internal nondeterminism. This feature is needed to relate $T_{PS}^{\prime }$ and $T_{PS}$ of Figure 2 because the state $1$ (resp. $2$) of $T_{PS}^{\prime }$, in which the forced internal choice of emitting $!\mathrm{𝗋𝖾𝗌𝗉}$ (resp. $!\mathrm{𝗌𝗍𝗈𝗉}$) is taken, has a unique corresponding state in $T_{PS}$, namely state $1$, where two possible choices are present (either $!\mathrm{𝗋𝖾𝗌𝗉}$ or $!\mathrm{𝗌𝗍𝗈𝗉}$ can be sent).

In this paper we close the open problem of finding a sound and complete characterization of asynchronous fair refinement for session types. The characterization we present is crucially based on a novel asynchronous semantics for session types that: (i) expresses their asynchronous behavior without explicit modeling of FIFO buffers (as in the original paper of Bravetti, Lange and Zavattaro [6]), and (ii) allows us to adapt, to the asynchronous case, the approach introduced by Ciccone and Padovani [23, 12] for providing complete characterizations of fair session subtyping in the synchronous case. Being complete, our new subtyping allows us to prove that the stream processing server $T_{PS}^{\prime }$ is a refinement of the batch processing server $T_{PS}$.

We start by recalling the syntax and asynchronous semantics of session types as well as the notion of fair refinement given by Bravetti, Lange and Zavattaro [6]. In the definition of the syntax, instead of using the $\oplus$, , and the $\mathrm{𝑟𝑒𝑐}$ operators, we consider an equivalent process algebraic notation with choice and prefix [20] and a coinductive syntax to deal with possibly infinite session types. Following Bravetti, Lange and Zavattaro [6] we restrict to first-order session types, i.e. session types in which send/receive operations are used to exchange only messages of elementary singleton type. Considering higher-order types, where send/receive operations can be used to exchange also sessions, would not modify significantly the proofs of our results.

We assume the existence of a set of singleton types ranged over by $𝖺$, $𝖻$, $\mathrm{\dots }$ that we use to label branches in session types. The only value of type $𝖺$ is called tag and is denoted by the same symbol $𝖺$. Pre-session types are the possibly infinite trees coinductively generated by the productions below:

The polarities $\mathrm{?}$ and $!$ are used to distinguish input actions from output actions. A session type is a pre-session type that satisfies the following well-formedness conditions:

1. 1.

   in every subtree of the form ${\sum }_{i\in I}p{𝖺}_i.S_i$, $I$ is a non-empty finite set and if $I$ contains more than one element, then the message types ${𝖺}_i$ are pairwise distinct tags;

2. 2.

   the tree is regular, namely it is made of finitely many distinct subtrees ${\sum }_{i\in I}p{𝖺}_i.S_i$. Courcelle [13] established that every such tree can be expressed as the unique solution of a finite system of equations ${\{S_i=T_i\}}_{i\in I}$ where each metavariable $S_i$ may occur (guarded) in the $T_j$’s;

3. 3.

   every subtree ${\sum }_{i\in I}p{𝖺}_i.S_i$ contains a leaf of the form $\mathrm{𝖾𝗇𝖽}$.

A session type $\mathrm{𝖾𝗇𝖽}$ describes a terminated session (i.e. the corresponding channel is no longer usable). A branching session type ${\sum }_{i\in I}p{𝖺}_i.S_i$ describes a channel used for sending or receiving a message of type ${𝖺}_i$ and then according to $S_i$. The well-formedness condition (1) above requires that message types must be pairwise distinct tags if there is more than one branch. Sometimes we write $p{𝖺}_1.S_1+\mathrm{\cdots }+p{𝖺}_n.S_n$ for ${\sum }_{i=1}^{n}p{𝖺}_i.S_i$. Note that the polarity $p$ is the same in every branch, i.e. mixed choices are disallowed as usual.

The well-formedness condition (2) guarantees that we deal only with session types representing trees consisting of finitely many distinct subtrees as those that can be represented with a finite syntax and the $\mathrm{𝑟𝑒𝑐}$ operator [13].

The well-formedness condition (3) ensures that session types describe protocols that can always terminate. This assumption is not usually present in other session type syntax definitions where it is possible to also express non-terminating protocols. As we will see in the following (Definition 3), non-terminating protocols are not inhabited in our theory. In particular, we consider a notion of correct type composition such that, whatever sequence of interactions is performed, such sequence can always be extended to reach successful session termination where both types become $\mathrm{𝖾𝗇𝖽}$. In conclusion, ruling out non-terminating protocols in the syntax of session types does not affect the family of protocols we are interested in modeling and at the same time simplifies the technical development.

It is worth to mention that Bravetti, Lange and Zavattaro [6] do not consider the well formedness condition (3), hence allowing for the specification of non-terminating types. In the comparison with the related literature in Section 5 we discuss the impact of the absence of this condition on the definition of the fair asynchronous subtyping reported in that paper.

We write $\overline{S}$ for the dual of $S$, which is the session type corecursively defined by the equations

where $\overline{p}$ is the dual of the polarity $p$ so that $\overline{\mathrm{?}}=!$ and $\overline{!}=\mathrm{?}$. As usual, duality affects the direction of messages but not message types.

We now define the transition system that we use to formalize the notion of correct session type composition and the induced notion of refinement [6].

The transition system makes use of explicit FIFO queues of messages that have been sent asynchronously. A configuration is a term $[S,{\omega }_S]|[T,{\omega }_T]$ where $S$ and $T$ are session types equipped with two queues ${\omega }_S$ and ${\omega }_T$ of incoming messages. We write $ϵ$ for the empty queue and we use $s$, $s^{\prime }$, etc. to range over configurations.

Intuitively, the composition of the two types $S$ and $T$ in Example 2 is incorrect because it can lead to a deadlocked configuration $[\mathrm{?}𝖻.\mathrm{𝖾𝗇𝖽},𝖺]|[\mathrm{?}𝖺.\mathrm{𝖾𝗇𝖽},𝖻]$ discussed therein. Following Bravetti, Lange and Zavattaro [6] we formalize the correct composition of two types as a compliance relation.

We can now formally state that the types $S$ and $T$ of Example 2 are not compliant because of the sequence of transitions discussed at the end of Example 2: $[S,ϵ]|[T,ϵ]\to [S,𝖺]|[\mathrm{?}𝖺.\mathrm{𝖾𝗇𝖽},ϵ]\to [\mathrm{?}𝖻.\mathrm{𝖾𝗇𝖽},𝖺]|[\mathrm{?}𝖺.\mathrm{𝖾𝗇𝖽},𝖻]$ leading to a configuration different from the successfully terminated computation $[\mathrm{𝖾𝗇𝖽},ϵ]|[\mathrm{𝖾𝗇𝖽},ϵ]$, and without outgoing transitions.

Compliance induces a semantic notion of type refinement, as follows.

In words, this definition says that a process behaving as $T$ can be “safely” replaced by a process behaving as $S$ when $S$ is a refinement of $T$. Indeed, the peer process, which is assumed to behave according to some session type $R$ such that $R$ and $T$ are compliant, will still interact correctly after the substitution has taken place. We quote “safely” above since we want to stress that the notion of session correctness being preserved here is not merely a safety property, but rather a combination of a safety property (if the interaction gets stuck, then it has successfully terminated) and a liveness property (the interaction can always successfully terminate).

Because of the universal quantification on the type $R$, Definition 4 provides few insights about what it means for $S$ to be a refinement of $T$. For this reason, it is important to provide alternative (but equivalent) characterizations of type refinement. Bravetti, Lange and Zavattaro [6] present a characterization of refinement defined coinductively à la session subtyping [16], hence called fair asynchronous subtyping, which can be used to prove some interesting and non trivial relations as those discussed in Section 1.

The coinductive subtyping in [6] is a sound but not complete characterization of fair asynchronous refinement. In particular, it is uncapable of establishing relations $S⪯T$ where $S$ describes a more deterministic protocol than $T$ (output covariance). We have seen an instance of this case in Section 1 when discussing the stream and batch processing servers. Liveness-preserving refinements are difficult to characterize because they are intrinsically non-local: the removal of an output action in a region of a session type may compromise the successful termination of the protocol along a branch that is “far away” from the location where the output was removed. In our case this phenomenon is further aggravated by the presence of asynchrony, which allows output actions to be anticipated and therefore to be moved around.

In order to provide a complete characterization of refinement, we use an alternative, queue-less semantics of asynchronous session types that we introduce in the next section.

The first step towards our characterization of fair refinement is the definition of a novel asynchronous semantics for session types that does not make use of explicit queues. This alternative semantics will allow us to adapt the complete characterization of fair synchronous subtyping for session types [23, 12] to the asynchronous case.

We now introduce a labelled transition system to describe the sequences of input/output actions that are allowed by a session type. A label is a pair made of a polarity and a tag $𝖺$:

We will refer to the dual of a label $\alpha$ with the notation $\overline{\alpha }$, where $\overline{p𝖺}\stackrel{\text{def}}{=}\overline{p}𝖺$.

The labelled transition system (LTS) of asychronous session types is coinductively defined thus:

The rule [l-sync] simply expresses the fact that a session type allows the input/output action described by its topmost prefix, as expected. The rule [l-async] is concerned with asynchrony and lifts input actions that are enabled deep in a session type, provided that such actions are only prefixed by output actions. The rationale for such “asynchronous transitions” is that the topmost outputs allowed by a session type may have been performed asynchronously, so that the underlying input is enabled even if the output messages have not been consumed yet. For example, the session type $!𝖺.\mathrm{?}𝖻.S$ may evolve either as

The first transition sequence is the expected one and describes an evolution in which the order of actions is consistent with the syntactic structure of the session type. The second transition sequence is peculiar to the asynchronous setting and describes an evolution in which the input $\mathrm{?}𝖻$ is performed before the output $!𝖺$. Asynchronous transitions seem to clash with the very nature of session types, whose purpose is to impose an order on the actions performed by a process on a channel. To better understand them, we find it useful to appeal to the usual interpretation of labelled transition systems as descriptions of those actions that trigger interactions with the environment: a process that behaves according to the session type $!𝖺.\mathrm{?}𝖻.S$ is still required to send $𝖺$ before it starts waiting for $𝖻$. However, it will be capable of receiving $𝖻$ before $𝖺$ has been consumed by the party with which it is interacting, because $𝖺$ may have been queued. In this sense, we see the queue as an entity associated with the process and not really part of the environment in which the process executes.

It is useful to introduce some additional notation related to actions and transitions of session types. We let $\phi$ and $\psi$ range over strings of labels and use $\epsilon$ to denote the empty string. We write $\stackrel{{\alpha }_1\mathrm{\cdots }{\alpha }_n}{\to }$ for the composition $\stackrel{{\alpha }_1}{⟶}\mathrm{\cdots }\stackrel{{\alpha }_n}{⟶}$, we write $S\stackrel{\phi }{⟶}$ if $S\stackrel{\phi }{⟶}T$ for some $T$ and we write $S/\stackrel{\phi }{⟶}$ if not $S\stackrel{\phi }{⟶}$.

Two subtle aspects of the LTS deserve further comments. First of all, asynchronous transitions are possible only provided that they are enabled along every branch of a session type. For example, if $S=!𝖺.\mathrm{?}𝖼.S_1+!𝖻.(\mathrm{?}𝖼.S_2+\mathrm{?}𝖽.S_3)$, then we have

The $\mathrm{?}𝖼$-labelled transition is enabled because that input action is available regardless of the message (either $𝖺$ or $𝖻$) that has been sent. On the contrary, the $\mathrm{?}𝖽$-labelled transition is initially disabled because the input of $𝖽$ is possible only if $𝖻$ has been sent. So, the peer interacting with a process that follows the session type $S$ must necessarily consume either $𝖺$ or $𝖻$ in order to understand whether or not it can send $𝖽$.

Finally, we have to motivate the coinductive definition of the LTS. This aspect is related to both asynchrony and fairness. Consider a session type $S$ such that $S=!𝖺.S+!𝖻.\mathrm{?}𝖼.T$. The question is whether or not the $\mathrm{?}𝖼$-labelled transition should be enabled from $S$. In principle, $S$ allows the output of an infinite sequence of $𝖺$ messages and so the $\mathrm{?}𝖼$-labelled transition should be disabled. In this work, however, we make the assumption that this behavior is unrealistic or unfair, therefore we want the $\mathrm{?}𝖼$-labelled transition to be enabled. From a technical standpoint, the only derivation that allows us to express an $\mathrm{?}𝖼$-labelled transition for $S$ is the following one

where $S^{\prime }=!𝖺.S^{\prime }+!𝖻.T$. This infinite derivation is legal only if the LTS is coinductively defined.

Technically, concerning our fairness assumption, remember that in this paper we take the viewpoint that sessions are meant to eventually terminate so that neverending communication protocols are excluded. This is reflected both in the notion of session correctness (definition 3) from which refinement is derived (definition 4), as well as in the definition of the asynchronous LTS (rule [l-async]). Concerning the nature of our fairness assumption, it turns out to be an instance of what van Glabbeek and Höfner [25] call full fairness where the property being preserved is the reachability of the $[\mathrm{𝖾𝗇𝖽},ϵ]|[\mathrm{𝖾𝗇𝖽},ϵ]$ configuration.

The coinductive definition of the LTS may cast doubts on the significance of the labels of transitions, in the sense that some (input) transitions could be coinductively derivable for a given session type $S$ even if they do not correspond to actions that are actually described within $S$. For example, for the pre-session type $S=!𝖺.S$ it would be possible to derive every transition of the form $S\stackrel{\mathrm{?}𝖻}{⟶}T$ by using infinitely many applications of [l-async]. The following result rules out this possibility. The key element of the proof is the fact that, because of the well-formedness condition (3), every subtree of a session type contains a leaf of the form $\mathrm{𝖾𝗇𝖽}$.

After looking at the transition sequences in (1), the reader may also wonder whether the LTS always satisfies the diamond property when a session type simultaneously enables both input and output actions. Crucially, this is the case.

Having established these basic facts about the LTS of session types, we introduce some more notation. If $\phi ={\alpha }_1\mathrm{\cdots }{\alpha }_n$, we write $\phi .S$ for ${\alpha }_1\mathrm{\dots }{\alpha }_n.S$. Note that $\epsilon .S=S$. Then, we define a notion of partial derivative for session types that resembles Brzozowski’s derivative for regular expressions [8]. In particular, if $S\stackrel{\phi }{⟶}T$ we say that $T$ is the derivative of $S$ after $\phi$ and we write $S(\phi )$ for $T$. Note that $S(\phi )$ is uniquely defined because of the well-formedness condition (1). We define the inputs and outputs of a session type as $\mathrm{𝗂𝗇𝗉}(S)\stackrel{\text{def}}{=}\{𝖺\mid S\stackrel{\mathrm{?}𝖺}{⟶}\}$ and $\mathrm{𝗈𝗎𝗍}(S)\stackrel{\text{def}}{=}\{𝖺\mid S\stackrel{!𝖺}{⟶}\}$. Note that $\mathrm{𝗂𝗇𝗉}(\mathrm{𝖾𝗇𝖽})=\mathrm{𝗈𝗎𝗍}(\mathrm{𝖾𝗇𝖽})=\mathrm{\varnothing }$. Occasionally we use $\mathrm{𝗈𝗎𝗍}(\cdot )$ also as a predicate so that $\mathrm{𝗈𝗎𝗍}(S)$ holds if and only if $\mathrm{𝗈𝗎𝗍}(S)\ne \mathrm{\varnothing }$. Finally, the set of traces of a session type is defined as $\mathrm{𝗍𝗋}(S)\stackrel{\text{def}}{=}\{\phi \mid S\stackrel{\phi }{⟶}\mathrm{𝖾𝗇𝖽}\}$.

We now define a notion of correctness that adapts, to the new semantics, the notion of correct composition used in Definition 3. A session composition is a pair $S\parallel T$ of session types. Session compositions reduce according to the following rule:

Notice that we overload $\to$ and ${\to }^{\ast }$, which were previously used to denote the transitions over session configurations in Definition 1. Their actual meaning is made clear by the context. Moreover, note that a session composition is stuck (i.e. it does not reduce) if one of the two session types in the composition enables an output for which the corresponding input is disabled in the other session type.

The definition of correct session composition is the same as Definition 3 adapted to the new asynchronous semantics of types. Intuitively, in a correct session composition $S\parallel T$, the only state that is allowed to be stuck is the final one, where both session types have reduced to $\mathrm{𝖾𝗇𝖽}$ meaning that the session has successfully terminated. Moreover, every intermediate state $S^{\prime }\parallel T^{\prime }$ that is reachable from $S\parallel T$ must itself be on a path that leads to successful termination of the session.

A simple example of correct session composition is $!𝖺.\mathrm{?}𝖻.\mathrm{𝖾𝗇𝖽}\parallel \mathrm{?}𝖺.!𝖻.\mathrm{𝖾𝗇𝖽}$, which admits only one reduction sequence

where every intermediate state can reduce further towards successful termination. Note that a $\mathrm{?}𝖻$-labelled transition is immediately enabled by the session type on the left hand side of the initial composition, but the matching $!𝖻$-labelled transition becomes enabled only after the first reduction. More interestingly, also the composition $!𝖺.\mathrm{?}𝖻.\mathrm{𝖾𝗇𝖽}\parallel !𝖻.\mathrm{?}𝖺.\mathrm{𝖾𝗇𝖽}$ is correct. In this case the composition may evolve non-deterministically in two ways, depending on which output message is consumed first:

In synchronous theories of (binary) session types duality implies correctness, to the point that in most cases session correctness is expressed in terms of duality. This does not hold for the notion of correctness given by Bravetti, Lange and Zavattaro [6] because they do not consider the well-formedness condition (3). In fact, every type without $\mathrm{𝖾𝗇𝖽}$ cannot be correctly composed with any other type, including its dual. We now show that by restricting to types satisfying also the well-formedness condition (3) we recover this property which also plays a key role in the alternative characterization of subtyping discussed in the next section.

As discussed in Example 9, the presence of FIFO message queues in Definition 1 allows types starting with outputs to emit messages and store them in the queues without performing any check about the possibility for the receiver to consume these messages. On the contrary, the new reduction semantics of session composition (2) checks that all outputs can be consumed by the partner. Despite this difference, the two semantics can be proved “equivalent”. More specifically, we will prove the following correspondence result: two session types $S$ and $T$ are compliant (according to Definition 3) if and only if $S⨝T$ (according to Definition 10).

In order to state the correspondence result, it is convenient to introduce some additional notation allowing us to consider the configuration queues as sequences of input actions to be executed in order to consume the buffered messages. More precisely, given the queue $\omega ={𝖺}_1{𝖺}_2\mathrm{\dots }{𝖺}_n$, we write $\mathrm{?}\omega$ for the corresponding sequence $\mathrm{?}{𝖺}_1\mathrm{?}{𝖺}_2\mathrm{\dots }\mathrm{?}{𝖺}_n$ of input actions. We also use the notation $S\stackrel{\mathrm{?}\omega }{\to }{S}^{\prime }$ as a shortcut for $S\stackrel{\mathrm{?}{𝖺}_1\mathrm{?}{𝖺}_2\mathrm{\dots }\mathrm{?}{𝖺}_n}{\to }{S}^{\prime }$. Notice that the queue $\omega$ could be empty, i.e. $\omega =ϵ$, in which case $S\stackrel{\mathrm{?}\omega }{\to }S$.

In Example 2 we have seen a computation defined according to Definition 1 that cannot be mimicked by our reductions defined by rule (2). We now prove that the vice versa actually holds. More precisely we identify a way to relate session compositions to session configurations, and we prove that each reduction of a session compositions can be mimicked by a corresponding sequence of transitions of configurations. A session composition $S_1\parallel T_1$ corresponds to several configurations $[S,{\omega }_S]|[T,{\omega }_T]$ such that $S\stackrel{\mathrm{?}{\omega }_S}{\to }{S}_1$ and $T\stackrel{\mathrm{?}{\omega }_T}{\to }{T}_1$. That is, $S_1$ can be thought of as the residual of $S$ after all the messages in the queue ${\omega }_S$ of incoming messages have been consumed. Similarly for $T_1$ and $T$.

We now investigate the possibility for the reduction relation defined by rule (2) to mimick sequences of transitions of corresponding configurations. This is not true in general, as shown in Example 9. However, we can prove this result under the assumption that the initial session compositions, or the initial configurations, are correct. These two cases are considered in the next two lemmas, the first of which states that a correct session composition $S\parallel T$ can mimick all computations of the configuration $[S,ϵ]|[T,ϵ]$ and the reached compositions/configurations are related by the correspondence relation discussed above and used in Lemma 13.

A similar correspondence result holds also for initial correct configurations.

We can now conclude with the main result of this section, that is the correspondence between compliance (Definition 3) and correctness (Definition 10).

In this section we present the main contribution of the paper, namely a sound and complete characterization of the refinement relation defined by Bravetti, Lange and Zavattaro [6] recalled in Definition 4. In light of Theorem 16, such refinement can be alternatively defined using the new labelled transition system for asynchronous session types defined in Section 3 and the notion of correctness in Definition 10:

$S⪯T$ if and only if $R⨝T$ implies $R⨝S$ for every $R$

This definition corresponds to the definition of a subtyping relation for session following Liskov’s substitution principle [19], where the property to be preserved is session correctness.

We start the characterization of $⪯$ by introducing the following coiductive relation which, as we will see later, turns out to be an overapproximation of $⪯$.

The clauses of Definition 17 specify some expected requirements for a session subtyping relation: a terminated session type $\mathrm{𝖾𝗇𝖽}$ is in relation with itself only; every input action in a supertype $T$ should be matched by the same input action allowed in the subtype $S$ and the corresponding continuations should still be related by subtyping; dually, every output action allowed by a subtype $S$ should be matched by an output action allowed by the supertype $T$ and the corresponding continuations should still be related by subtyping.

Interestingly, these clauses are essentially those found in analogous characterizations of synchronous subtyping for session types [16], 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 [15] for a comparison of the two viewpoints. However, there are a couple of quirks that separate Definition 17 from sibling definitions. First of all, recall that transitions like $T\stackrel{\mathrm{?}𝖺}{⟶}{T}^{\prime }$ and $S\stackrel{\mathrm{?}𝖺}{⟶}{S}^{\prime }$ may concern “deep” input actions enabled by $T$ and $S$, even when $T$ and $S$ begin with output actions. Hence, clause (2) may allow pairs of session types to be related even if they do not start with the same kind of actions. A simple instance of this fact is given by the session types $!𝖺.\mathrm{?}𝖻.S$ and $\mathrm{?}𝖻.!𝖺.S$ discussed earlier, for which we have $!𝖺.\mathrm{?}𝖻.S\stackrel{\mathrm{?}𝖻}{⟶}!𝖺.S$ and $\mathrm{?}𝖻.!𝖺.S\stackrel{\mathrm{?}𝖻}{⟶}!𝖺.S$. Another novelty is that the clauses (2) and (3) are no longer mutually exclusive, since it may happen that $\mathrm{𝗈𝗎𝗍}(T)$ holds for a $T$ that also allows (deep) input transitions. For example, any asynchronous subtyping relation that includes the pair $(!𝖺.\mathrm{?}𝖻.S,!𝖺.\mathrm{?}𝖻.S)$ must also include the pair $(\mathrm{?}𝖻.S,\mathrm{?}𝖻.S)$ because of clause (3) as well as the pair $(!𝖺.S,!𝖺.S)$ because of clause (2).

We now present a first result relating $⪯$ and asynchronous subtyping. We have that $⪯$ satisfies the clauses of Definition 17 hence it is an asynchronous sbtyping relation.

As we have anticipated, the largest asynchronous subtyping relation contains pairs of types that are not in subtyping relation, as illustrated by the next example.

In general, a purely coinductive characterization based on the clauses of Definition 17 allows us to capture the safety-preserving properties of subtyping, those concerning the admissibility of interactions, because they are supported by an invariant argument. However, the very same clauses do not say anything about the liveness-preserving properties of subtyping, those concerning the reachability of successful termination, which must be supported by a well-foundedness argument. In order to find a sound characterization of subtyping, we have to resort to bounded coinduction [1, 14], a particular case of coinductive definition where we consider the largest relation that satisfies the clauses in Definition 17 and that is also included in an inductively defined relation that preserves the reachability of successful termination. We dub this inductive relation convergence and we denote it by $⊑$.

Before looking at the formal definition of $⊑$, let us try to acquire a rough understanding of convergence by recalling Example 21, in which we have identified two session types $S$ and $T$ that satisfy the clauses of Definition 17 but are not related by subtyping. In that example, we can see that the traces that lead $S$ to termination are a subset of the traces that lead $T$ to termination. This is a general property that holds every time $S$ describes a more deterministic (or “less demanding”) behavior compared to $T$. However, in the specific case of Example 21, the traces that lead $S$ to termination are too few, to the point that there exists a potential partner (described by $R$ in the example) that terminates solely relying on those traces of $T$ that have disappeared in $S$. Contrast $S$ and $T$ those with $S^{\prime }=!𝖺.!𝖺.S^{\prime }+!𝖻.\mathrm{𝖾𝗇𝖽}$ and $T^{\prime }=!𝖺.T^{\prime }+!𝖻.\mathrm{𝖾𝗇𝖽}$. Also in this case $S^{\prime }$ is more deterministic than $T^{\prime }$ and some traces that lead $T^{\prime }$ to termination have disappeared in $S^{\prime }$. Specifically, every trace of the form $\phi =!{𝖺}^{2n+1}!𝖻$ is allowed by $T^{\prime }$ but not by $S^{\prime }$. However, it is also the case that for each of these traces we can find another trace $!{𝖺}^{2n}!𝖻$ that shares a common prefix with $\phi$ and that leads both $S^{\prime }$ and $T^{\prime }$ to termination after an output action $!𝖻$. Since the behavior described by $T^{\prime }$ is always able to autonomously veer the interaction towards termination after any number of $𝖺$ messages, any session type $R$ that can be correctly combined with $T^{\prime }$ must be prepared to receive this $𝖻$ message at any time, meaning that termination is preserved also if $R$ is combined with $S^{\prime }$.

Let us now define $⊑$ formally.

Intuitively, a derivation for the relation $S⊑T$ measures the “difference” between $S$ and $T$ in terms of allowed traces. When $\mathrm{𝗍𝗋}(T)\subseteq \mathrm{𝗍𝗋}(S)$ there is essentially no difference between $S$ and $T$, so the rule that defines $⊑$ has no premises and turns into an axiom. When $\mathrm{𝗍𝗋}(T)⊈\mathrm{𝗍𝗋}(S)$, then for every trace $\phi$ of actions allowed by $T$ but not by $S$ there is a prefix $\psi \le \phi$ shared by both $S$ and $T$ and followed by an output action $!𝖺$ that leads to a pair of session types $S(\psi !𝖺)$ and $T(\psi !𝖺)$ that are “slightly less different” from each other in terms of allowed traces. Indeed, the derivation for $S(\psi !𝖺)⊑T(\psi !𝖺)$ must be strictly smaller than that for $S⊑T$, or else $S⊑T$ would not be inductively derivable.

Note that $⊑$ is trivially reflexive, but apart from that it is generally difficult to understand when two session types are related by convergence because of the non-local flavor of the relation. However, it is easy to see that any two session types related by an asynchronous subtyping where at least one of them is finite are also related by convergence.

Gay and Hole [16] introduced the first notion of subtyping for synchronous session types. This subtyping supports variance on both inputs and outputs so that a subtype can have more external nondeterminism (by adding branches in input choices) and less internal nondeterminism (by removing branches in output choices). Padovani [23] studied a notion of fair subtyping for synchronous multi-party session types that preserves a notion of correctness similar to our Definition 3. One key difference between Padovani’s fair subtyping and Gay-Hole subtyping is that the variance of outputs must be limited in such a way that an output branch can be pruned only if it is not necessary to reach successful termination. Ciccone and Padovani [23, 11, 12] have presented sound and complete charcaterizations of fair subtyping in the synchronous case. These characterizations all combine a coinductively defined relation and an inductively defined relation (called “convergence”), which respectively capture the safety-preserving and the liveness-preserving aspects of subtyping.

Subtyping relations for asynchronous session types have been defined by Mostrous and Yoshida [21], Chen et al. [9] and Bravetti, Lange and Zavattaro [6]. In the asynchronous case a subtype can anticipate output actions w.r.t. its supertype because anticipated outputs can be stored in the communication queues without altering the overall interaction behaviour. The first proposal for asynchronous subtyping [21] allows a subtype to execute loops of anticipated outputs, thus delaying input actions indefinitely. This could leave orphan messages in the buffers. The subsequent work of Chen et al. [9] imposes restrictions on output anticipation so as to avoid orphan messages. Bravetti, Lange and Zavattaro [6] have defined the first fair (liveness-preserving) asynchronous session subtyping along the lines of Definition 4. However, they only provided a sound (but not complete) coinductive characterization.

In this paper we present the first complete characterization of the fair asynchronous subtyping relation defined by Bravetti, Lange and Zavattaro [6] using the techniques introduced by Ciccone and Padovani in the synchronous case [23, 11, 12]. In particular, we complement a coinductively defined subtyping relation with a notion of convergence. To do so, we leverage a novel “asynchronous” operational semantics of session types in which a type can perform an input transition even if such input is prefixed by outputs, under the assumption that such input is present along every initial sequence of outputs.

Another fair asynchronous subtyping relation that makes use of a similar operational semantics has been recently defined by Padovani and Zavattaro [24]. Unlike the relation defined by Bravetti, Lange and Zavattaro [6] and characterized in this paper, the subtyping relation of Padovani and Zavattaro [24] preserves a liveness property that is strictly weaker than successful session termination. For this reason, their operational semantics is completely symmetric with respect to the treatment of input and output actions and no inductively-defined convergence relation is necessary in order to obtain a sound and complete characterization of subtyping.

A notable difference between the paper of Bravetti, Lange and Zavattaro [6] and our own is the fact that we focus on those session types describing protocols that can always terminate, whereas Bravetti, Lange and Zavattaro make no such assumption. This choice affects the properties of the subtyping relation. In particular, Bravetti, Lange and Zavattaro [6] show that a supertype can have additional input branches provided that such branches are uncontrollable. A session type is uncontrollable if there are no session types that can be correctly composed with it. Our well-formedness condition (3) in the definition of types, guarantees that all session types are controllable. We argue that the characterization presented in this paper can be easily extended to the more general case where uncontrollable session types are allowed, following the approach considered by Padovani [23]. Basically, types that do not satisfy the well-formedness condition (3) can be normalized by pruning away the uncontrollable subtrees. The normalization yields session types that are semantically equivalent to the original ones and that satisfy the condition (3). At that point, our characterization can be used to establish whether or not they are related by subtyping.

We envision three lines of development of this work. One line is concerned with the study of algorithmic versions of our notions of correct composition, subtyping, and convergence. As for all the known subtypings for asychronous sessions, these notions turn out to be undecidable [7]. In the literature, sound (but not complete) algorithmic characterizations have been investigated for different variants of asynchronous session subtyping [4, 5, 2, 6]. We plan to investigate the possibility to adapt these approaches to our new formalization of fair asynchronous subtyping, possibly taking advantage of the novel operational semantics for asynchronous session types. Another line of future work concerns the application of fair asynchronous subtyping to the definition of type systems ensuring successful session termination of asynchronously communicating processes. Such type systems have been studied for synchronous communication by Ciccone, Dagnino and Padovani [11, 10]. A first proposal of such type system for asynchronous communication has been recently given by Padovani and Zavattaro [24]. However, as we have pointed out above, the subtyping relation used in their type system does not preserve successful session termination. As a consequence, their type system requires a substantial amount of additional annotations in types and in typing judgements in order to enforce successful termination. It may be the case that relying on a subtyping relation that provides stronger guarantees, like the one characterized in the present paper, could simplify the type system and possibly enlarge the family of typeable processes.

Finally, it may be worth investigating whether the characterization of fair asynchronous subtyping studied in this paper for binary session types extends smoothly to multiparty session types as well. In the synchronous setting, it is known that there are no substantial differences between the binary and the multiparty case, except for the presence of role names in session types [23, 11]. We conjecture that an asynchronous LTS for multiparty session types can be defined in a very natural way along the lines presented in this paper. However, the multiparty case grants additional out-of-order transitions compared to the binary case (see the unfair multiparty asynchronous subtyping defined by Ghilezan et al. [17]) and working out all of the resulting technicalities could be challenging.