Abstract Subtyping for
Asynchronous Multiparty Sessions

The undecidability of MAS is unfortunate, as safety-preserving substitutions are most valuable in the asynchronous setting to check the validity of performance optimisations, namely sending messages earlier or postponing receives [38]. A MAS subtyping checker would encourage developers to experiment with communication structures, providing a litmus test for checking the correctness of an optimisation. While polynomial checking algorithms do exist [36], they do not support optimisation even for the simpler binary case. A potential solution lies in abstract interpretation, previously applied to binary subtyping, where sets of words model asynchronicity [3]. This addresses undecidability with systematic (lattice-theoretic) approximation. To apply abstract interpretation to multiparty interaction, we reformulate MAS as subtyping on sets of session trees, and make the following contributions:

• $\mathrm{■}$

  We introduce an equivalent but more tractable formulation of MAS [27], based on a new lite refinement preorder. MAS [27] is defined using nested quantification over infinite structures. One of the challenges of checking MAS is that it requires a check for inclusion of the actions being postponed over infinite structures. Lite refinement provides a way to automation by reducing the inclusion check to a simple, local check.

• $\mathrm{■}$

  Abstraction has been applied to binary subtyping by adapting subtyping to sets of words and then representing these sets with regular expressions [3]. MAS is formulated in terms of session trees, and likewise we generalise subtyping to sets of session trees. To derive continuations after performing an action, we adapt the Brzozowski derivative [10] from regular expressions to session trees, and further extend it to sets of session trees. This provides a semantic foundation for subtyping, similar to a collecting semantics [17], ready for abstract interpretation and the deployment of an abstract domain.

• $\mathrm{■}$

  We provide a new abstract domain for representing sets of session trees based on type graphs [43] and provide new domain operations for send and receive. Since the abstract domain is not finite, we show how widening can be applied to derive a terminating MAS algorithm founded on lite refinement.

Overall, we show how the theoretical formulation of MAS [27] can be distilled into an algorithm for checking subtyping. Moreover, our algorithm yields a certificate (enabling subtyping to be double-checked by a third-party without consideration of low-level algorithmic details). We complement our theoretical contribution by evaluating our algorithm on some challenging problems and show it can prove subtyping more often than existing methods, whilst being an order of magnitude faster than the state-of-the-art binary algorithm [3].

Let $\mathbb{P}$ denote a finite set of roles and $\mathrm{\Sigma }$ denote a finite alphabet of communication labels. Let ${𝔸}^{!}=\{p!a\mid p\in \mathbb{P},a\in \mathrm{\Sigma }\}$, ${𝔸}^{\mathrm{?}}=\{p\mathrm{?}a\mid p\in \mathbb{P},a\in \mathrm{\Sigma }\}$ and $𝔸={𝔸}^{!}\cup {𝔸}^{\mathrm{?}}$. The syntactic category of session types, $𝕊$, is inductively defined by:

where $I$ is drawn from the category of (finite) index sets $𝕀$. Session type ${\oplus }_{i\in I}p!a_i.{𝕊}_i$ is for selection/send: the role selects one label in ${\{a_i\}}_{i\in I}$, sends it to role $p$, and continues as the corresponding ${𝕊}_i$. Session type is a branching/receive action, where the role receives a label from $p$. $\mathrm{𝖾𝗇𝖽}$ is for termination, $\mu 𝚝.𝕊$ for recursion, and $𝚝$ is a type variable used for recursive call.

Asynchronous multiparty subtyping [27] is based on a co-inductive representation of session types called session trees. The category $𝕋$ for session trees is defined co-inductively below. Subtyping is defined using three sub-classes of session trees called single-output (SO) trees $𝕌$, single-input (SI) trees $𝕍$, and single-input-single-output (SISO) trees $𝕎$, also defined co-inductively below:

We let $S$, $T$, $U$, $V$ and $W$ denote typical members $𝕊$, $𝕋$, $𝕌$, $𝕍$ and $𝕎$, respectively.

If a sequence $W$ contains the action $p\diamond a$ where $\diamond \in \{!,\mathrm{?}\}$, we write $p\diamond a\in W$. Given the sets ${\mathbb{Q}}^{!}=\{p!\mid p\in \mathbb{P}\}$, ${\mathbb{Q}}^{\mathrm{?}}=\{p\mathrm{?}\mid p\in \mathbb{P}\}$ and $\mathbb{Q}={\mathbb{Q}}^{!}\cup {\mathbb{Q}}^{\mathrm{?}}$ we define the mapping $act:𝔸\to \mathbb{Q}$ where $act(p\diamond a)=p\diamond$. Given a set of actions $A\subseteq 𝔸$ and a sequence of actions $W\in 𝕎$, we define $act(A)=\{act(p\diamond a)\mid p\diamond a\in A\}$ and $act(W)=\{act(p\diamond a)\mid p\diamond a\in W\}$.

MAS [27] is formulated in terms of two classes of sequence of actions, ${𝒜}^p$ and ${ℬ}^p$, which are parameterised by a participant $p$. Classes ${𝒜}^p$ and ${ℬ}^p$ embed the principles of swapability encoded into MAS. These finite sequences are inductively defined as follows:

${𝒜}^p$ defines the sequences of actions that can be anticipated before a receive action from $p$ (namely any receive action that is not from $p$), whereas ${ℬ}^p$ defines the sequences of actions that can be anticipated before a send action to $p$ (namely any receive action – outputs can always be done before inputs – and any send action that is not to $p$). Note in particular that $p\mathrm{?}a\notin {𝒜}^p$ and $p!a\notin {ℬ}^p$. Using ${𝒜}^p$ and ${ℬ}^p$, we can now define refinement for SISO trees:

SISO-tree refinement provides an elegant vehicle for expressing swapability over the sequences of actions. However, a session type is not a sequence of actions, but rather a tree with selection and branching points. Definition 5 decomposes session trees in sets of SI- and SO- trees so as to express the co- and contra-variance of selection and branching.

The intuition is that SO-tree decomposition removes the selection points in a session tree and expresses them using sets of single-output sequences, and dually for SI-trees. The maps ${⟦\cdot ⟧}_{\mathrm{𝖲𝖮}}$ and ${⟦\cdot ⟧}_{\mathrm{𝖲𝖨}}$ lift to a set of session trees $𝒯\in \mathrm{\wp }(𝕋)$ by, respectively, ${⟦𝒯⟧}_{\mathrm{𝖲𝖮}}={\cup }_{T\in 𝒯}{⟦T⟧}_{\mathrm{𝖲𝖮}}$ and ${⟦𝒯⟧}_{\mathrm{𝖲𝖨}}={\cup }_{T\in 𝒯}{⟦T⟧}_{\mathrm{𝖲𝖨}}$.

Multiparty Asynchronous Subtyping (MAS) is formally defined as a binary relation on session trees in a forall-exists construction. Covariance and contravariance are encoded as a forall requirement on the SO-trees (resp. SI-trees) of the subtype (resp. supertype). The problem is then reduced to checking SISO-tree refinement:

Derivatives differ depending on whether they look for receive or send actions. A receive derivative is calculated using a depth bound derived using the ${\mathrm{𝖺𝗅𝗐𝖺𝗒𝗌}}_{p\mathrm{?}}$ predicate:

Lemma 14 asserts that the absence of a bound $k$ implies the absence of subtyping. Lemma 15 asserts that there exists at most one $k$ for which ${\mathrm{𝖺𝗅𝗐𝖺𝗒𝗌}}_{p\mathrm{?}}(T^{\prime },k)$ holds. The receive derivative, which follows, is then defined in terms of the bound.

Following MAS, a receive action from $p$ can only be found immediately (first rule) or after other receive actions from other roles (second rule). The second rule can be applied non-deterministically for any $j\in I$ and derives at least $|I|$ distinct derivatives (which ${\delta }_{p\mathrm{?}a}(T)$ returns as a set). We write $q\mathrm{?}{a}_j.D_j$ for the concatenation of $q\mathrm{?}a$, the action preceding $p\mathrm{?}a$, with a subtree $D_j$ that was the continuation of $p\mathrm{?}a$ in that path. The receive derivative is well-defined because there exists at most one $k$ such that ${\mathrm{𝖺𝗅𝗐𝖺𝗒𝗌}}_{p\mathrm{?}}(T^{\prime },k)$ holds.

Unfortunately, Lemma 14 does not help us define a send derivative on supertypes as we no longer rely on a known bound $k$. Hence, the definition of ${\mathrm{\Delta }}_{p!a}^k$ is parametric in $k$.

The $k$-th derivative is defined to be the set of derivatives ${𝒟}^{\mathrm{\ell }}$ for which ${𝒟}^{\mathrm{\ell }}\ne \mathrm{\varnothing }$, the degree $\mathrm{\ell }$ is maximal and $\mathrm{\ell }\le k$. If ${𝒟}^{\mathrm{\ell }}=\mathrm{\varnothing }$ for all $0\le \mathrm{\ell }\le k$ then the $k$-th derivative is itself null. Following MAS, in a supertype, a send action can be found immediately (first rule), after receive actions (e.g., the subtype may have anticipated the output), or after other send actions from different roles (third rule). Condition $k_i$ maximal means: ${\forall }_{i\in I}:{\mathrm{\Delta }}_{p!a}^{k_i^{\ast }}(T_i^{\prime },D_i^{\ast })\Rightarrow k_i^{\ast }\le k_i$. The third rule derives at least one derivative equipped with $|J|$ branches $q!a_j.D_j$, where the $D_j$ are again selected to maximise their degree $k_i$.

To apply one derivative after another in a chain of actions, receive and send derivatives are lifted to operators on sets of supertypes as follows:

The use of $\uplus$ in ${\mathrm{\Delta }}_{p!a}^k({𝒯}^{\prime })$ reflects covariance over sends: the $p!a$ action of the subtype must be supported by all session-trees $T^{\prime }\in {𝒯}^{\prime }$. Conversely, the use of $\cup$ in ${\delta }_{p\mathrm{?}a}({𝒯}^{\prime })$ models contravariance over receives: the $p\mathrm{?}a$ of the subtype does not need to be found in all $T^{\prime }\in {𝒯}^{\prime }$.

The ternary subtyping relation is defined using an environment $\mathrm{\Gamma }$, a partial map $𝕋\rightharpoonup \mathrm{\wp }(\mathbb{Q})$, that records the actions performed by $T$ before $T$ is encountered again as a sub-tree. This device assumes that session trees are regular [40, Section 21.7.2] (aka rational [16]). $T$ is regular iff its set of distinct subtrees, $\mathrm{𝗌𝗎𝖻}(T)$, is finite. This is not limiting since session types correspond to regular session trees. The premises of $\mathrm{𝖱𝖾𝖿𝖨𝗇𝖠}$ and $\mathrm{𝖱𝖾𝖿𝖮𝗎𝗍𝖡}$ are partitioned by the dotted lines into: (bottom) requirements based on the syntax of the subtype $T$ that decompose the problem onto sub-problems of the form ${\mathrm{\Gamma }}_i⊢T_i\le {𝒟}_i$ and ensure a progress condition, and (top) subtyping requirements based on derivatives. In both rules, the premise $T\mapsto Q\in \mathrm{\Gamma }\Rightarrow Q\supseteq act(hd({𝒯}^{\prime }))$ stipulates that the actions at the head of ${𝒯}^{\prime }$ must be performed within one cycle of $T$, that is, before $T$ is revisited while traversing the subtype. This progress condition [15] ensures that a head action of ${𝒯}^{\prime }$ is not postponed indefinitely.²²2 Binary subtyping [3, 5, 6, 13] makes use of a check that tests for cycles of send actions in the candidate subtype. We reframed these checks here as a more intuitive and simple progress condition, which amounts to no more than a set inclusion test that discharges a requirement on swapability.

Rule $\mathrm{𝖱𝖾𝖿𝖨𝗇𝖠}$ lifts $\mathrm{𝖱𝖾𝖿𝖨𝗇}$ and $\mathrm{𝖱𝖾𝖿𝖠}$ of lite refinement (Definition 9) to sets of session trees. The first premise of $\mathrm{𝖱𝖾𝖿𝖨𝗇𝖠}$ (top) is a coverage condition which ensures that for every $T^{\prime }\in {𝒯}^{\prime }$ a receive derivative ${\delta }_{p\mathrm{?}{a}_i}(T^{\prime })$ is defined for least one $i\in I$. This guarantees that the selection of receive actions offered by $T$ cover those occurring in ${𝒯}^{\prime }$.

Rule $\mathrm{𝖱𝖾𝖿𝖮𝗎𝗍𝖡}$ lifts $\mathrm{𝖱𝖾𝖿𝖮𝗎𝗍}$ and $\mathrm{𝖱𝖾𝖿𝖡}$ (Definition 9) to session trees by applying the send derivative. Note $\mathrm{𝖱𝖾𝖿𝖨𝗇𝖠}$ permits a relaxation ${𝒟}_i$ to be used for ${\delta }_{p\mathrm{?}{a}_i}({𝒯}^{\prime })$; likewise a superset ${𝒟}_i$ is used for ${\mathrm{\Delta }}_{p!a_i}^{k_i}({𝒯}^{\prime })$ in $\mathrm{𝖱𝖾𝖿𝖮𝗎𝗍𝖡}$. Observe $k$ is not fixed upfront: it can vary with ${𝒯}^{\prime }$.

Operations on type graphs can be designed to mimic those on sets of session trees. In particular, to faithfully mimic the derivatives, it is both necessary to detect the absence of a derivative and preserve the derivation in a relaxation. The following definition formulates these requires and the proposition shows how they can be satisfied by lifting ${\mathrm{\Delta }}_{p!a}^k$ and ${\delta }_{p\mathrm{?}a}$:

An abstract receive derivative ${\pi }_{p\mathrm{?}a}:𝔾\to 𝔾$ can also be constructed using an environment $\mathrm{\Gamma }$.

An algorithm for checking subtyping follows from Figure 1 by substituting ${\mathrm{\Delta }}_{p!a}^k$ with ${\mathrm{\Pi }}_{p!a}^k$ and ${\delta }_{p\mathrm{?}a}$ with ${\pi }_{p\mathrm{?}a}$; thus operations on sets of session trees are simulated with operations on type graphs. We provide insight by first showing how widening can be applied to type graphs to create a co-inductive proof of subtyping, for a subtype that is linearly recursive.

Example 32 illustrates how widening can be applied to establish the existence of an infinite co-inductive proof for $T\le Q$. Algorithm 1 outlines an algorithm, which applies the same strategy for proving $T\le T^{\prime }$, but is applicable when $T$ is not linearly recursive. The key caveat for our algorithm is that $T$ is regular. This ensures $\mathrm{𝗌𝗎𝖻}(T)$ is finite. It follows there exists a finite set $wp\subseteq \mathrm{𝗌𝗎𝖻}(T)$ such that every cycle of $T$ crosses at least one sub-tree of $wp$. ($wp$ is inspired by the idea of widening points which are program locations [4] where widening is applied.)

In addition to $wp$, which is fixed throughout, our subtyping algorithm has a worklist $L$ and a partial map $𝒢:\mathrm{𝗌𝗎𝖻}(T)\rightharpoonup 𝔾$ as parameters. $𝒢$ mirrors the strategy used Example 32 which associates each sub-tree of $T$ with its own type graph. The algorithm is primed with $L=[⟨T,\mathrm{\Gamma }⟩]$ where $\mathrm{\Gamma }=\mathrm{\varnothing }$ and $𝒢=\{T\mapsto T^{\prime }\}$ (recall $𝕋\subseteq 𝔾$). The algorithm exits successfully at line (2) returning the certificate $𝒢$, and otherwise throws an exception at (8), (9), (14) or (15) indicating an inconclusive verdict. The body of Subtyping removes the first pair $⟨T,\mathrm{\Gamma }⟩$ from the worklist (if not empty), and checks whether the action at the root of $T$ is a receive, a send, or an $\mathrm{𝖾𝗇𝖽}$. In the latter case, if $𝔾(T)=\mathrm{𝖾𝗇𝖽}$ then rule $\mathrm{𝖱𝖾𝖿𝖤𝗇𝖽}$ of Figure 1 holds and processing continues, otherwise an exception is thrown.

If $T$ is a receive, the progress condition of $\mathrm{𝖱𝖾𝖿𝖨𝗇𝖠}$ is checked at (8). The coverage condition at (9) can be decided without recourse to $\gamma$ by an auxiliary predicate $\mathrm{𝖼𝗈𝗏𝖾𝗋}$ defined thus: $\mathrm{𝖼𝗈𝗏𝖾𝗋}(\mathrm{\varnothing })=true$, $\mathrm{𝖼𝗈𝗏𝖾𝗋}({\cup }_{j\in J}{G}_j)={\wedge }_{j\in J}\mathrm{𝖼𝗈𝗏𝖾𝗋}(G_j)$ and $\mathrm{𝖼𝗈𝗏𝖾𝗋}(G)=\exists i\in I:{\delta }_{p\mathrm{?}{a}_i}(G)\ne \mathrm{\varnothing }$ if $G\in 𝕋$. Then $\mathrm{𝖼𝗈𝗏𝖾𝗋}(𝒢(T))$ holds iff $\forall T^{\prime }\in \gamma (𝒢(T)):\exists i\in I:{\delta }_{p\mathrm{?}{a}_i}(T^{\prime })\ne \mathrm{\varnothing }$. Line (9) also checks $J\ne \mathrm{\varnothing }$. If these checks are passed, $𝒢$ is relaxed to ${𝒢}^{\prime }$ by updating $𝒢$ on the keys $\{T_j\mid j\in J\}$. If the sub-tree $T_j\in wp$ then widening is triggered and ${𝒢}^{\prime }(T_j)={𝒢}^{\prime }(T_j)\mathrm{▽}{\pi }_{p\mathrm{?}{a}_j}(𝒢(T))$. It follows $𝒢(T_j)⪯{𝒢}^{\prime }(T_j)$ and ${\pi }_{p\mathrm{?}{a}_j}(𝒢(T))⪯{𝒢}^{\prime }(T_j)$, both assuring soundness while ensuring that ${𝒢}^{\prime }(T_j)$ cannot be relaxed ad infinitum. If $T_j\notin wp$ then ${𝒢}^{\prime }(T_j)$ = ${𝒢}^{\prime }(T_j)\cup {\pi }_{p\mathrm{?}{a}_j}(𝒢(T))$, again yielding a sound relaxation. Widening at $wp$ is enough to ensure $𝒢$ is ultimately stable across all keys [4]: thus ${𝒢}^{\prime }=𝒢$ after a finite number of updates.

To demonstrate $\mathrm{𝖱𝖾𝖿𝖨𝗇𝖠}$ holds it remains to show $\mathrm{\Gamma }[T\mapsto \mathrm{\varnothing }]+p\mathrm{?}⊢T_j\le \gamma ({𝒢}^{\prime }(T_j))$ for all $j\in J$. This is achieved by the list comprehension at (11) which extends the worklist with the pair $⟨T_j,\mathrm{\Gamma }[T\mapsto \mathrm{\varnothing }]+p\mathrm{?}⟩$ for each $j\in J$ providing the pair actually needs to be considered, that is, if $\mathrm{\Gamma }(T_j)=\perp$ or $\neg ({𝒢}^{\prime }(T_j)⪯𝒢(T_j))$. Subtyping then reduces to invoking $\text{Subtype}(L^{\prime },wp,{𝒢}^{\prime })$. Observe $\mathrm{\Gamma }(T_j)\ne \perp$ on any subsequent visit to $T_j$, and eventually ${𝒢}^{\prime }(T_j)⪯𝒢(T_j)$ by virtue of widening. Termination thus follows.