Unreliability in Practical Subclasses of Communicating Systems

Asynchronous processes that communicate using First In First Out (FIFO) channels [11], henceforth referred to as FIFO systems, are widely used to model distributed protocols, but their verification is known to be computationally challenging. The model is Turing-powerful for even just two processes communicating via two unidirectional FIFO channels [11].

To address this challenge, several efforts have focused on identifying practical yet decidable subclasses – those expressive enough to model a wide range of distributed protocols, while ensuring that verification problems such as reachability and model checking remain decidable. Most FIFO systems assume perfect channels, which is too restrictive to model the real-world distributed phenomena where system failures often happen. This paper investigates whether two practical decidable subclasses of communicating systems, Realisable with Synchronous Communication (rsc) [18] and $k$-Multiparty Compatibility ($k$-mc) [35], are resilient when integrated with two different kinds of failures. These failure models were originally introduced in the contexts of contracts [37] and session types [3, 6]. We say a system is resilient under a given failure model if (i) the inclusion remains decidable, and (ii) the verification properties of interest remain decidable under that failure model.

For a finite set $\mathrm{\Sigma }$, we denote by ${\mathrm{\Sigma }}^{\ast }$ the set of finite words over $\mathrm{\Sigma }$, and the empty word with $\epsilon$. We use $|w|$ to denote the length of the word $w$, and $w_1\cdot w_2$ indicates the concatenation of two words $w_1,w_2\in {\mathrm{\Sigma }}^{\ast }$. Given a (non-deterministic) finite-state automaton $𝒜$, we denote by $ℒ(𝒜)$ the language accepted by $𝒜$. Consider a finite set of processes $\mathbb{P}$ (ranged over by $𝗉,𝗊,𝗋,\mathrm{\dots }$ or occasionally by ${𝗋}_{\mathrm{𝟣}},{𝗋}_{\mathrm{𝟤}},\mathrm{\dots }$) and a set of messages $\mathrm{\Sigma }$. In this paper, we consider the peer-to-peer communication model; i.e., there is a pair of unidirectional FIFO channels between each pair of processes, one for each direction of communication. In our model, processes act either by point-to-point communication or by internal actions (actions local to a single process). Moreover, in this setting, we consider messages to be atomic, akin to letters of an alphabet.

Let $\mathrm{𝐶ℎ}$ $=\{\mathrm{𝗉𝗊}\mid 𝗉\ne 𝗊\text{ and }𝗉,𝗊\in \mathbb{P}\}$ be a set of channels that stand for point-to-point links. Since we are considering the peer-to-peer model of communication, there is a unique process that can send a message to (or dually, receive a message from) a particular channel. An action $a=(\mathrm{𝗉𝗊},!,\text{m})\in \mathrm{𝖠𝖼𝗍}$ indicates that a process $𝗉$ sends a message m on the channel $\mathrm{𝗉𝗊}$. Similarly, $a=(\mathrm{𝗊𝗉},\mathrm{?},\text{m})\in \mathrm{𝖠𝖼𝗍}$ indicates that $𝗉$ receives a message m on the channel $\mathrm{𝗊𝗉}$. We henceforth denote an action $a=(\mathrm{𝗉𝗊},†,\text{m})\in \mathrm{𝖠𝖼𝗍}$, where $†\in \{!,\mathrm{?}\}$, in a simplified form as $\mathrm{𝗉𝗊}†\text{m}$. An internal action $c_{𝗉}$ means that process $𝗉$ performs the action $c$. We define a finite set of actions as $\mathrm{𝖠𝖼𝗍}\subseteq (\mathrm{𝐶ℎ}\times \{!,\mathrm{?}\}\times \mathrm{\Sigma })\cup {\mathrm{𝖠𝖼𝗍}}_{\tau }$ where ${\mathrm{𝖠𝖼𝗍}}_{\tau }$ is the set of all internal actions.

Note that in this model, there are no final or accepting states.

The set of outgoing channels of process $𝗉$ is represented by ${\mathrm{𝐶ℎ}}_{\text{o},𝗉}=\{\mathrm{𝗉𝗊}\mid 𝗊\in \mathbb{P}\setminus 𝗉\}$. Similarly, ${\mathrm{𝐶ℎ}}_{\text{i},𝗉}=\{\mathrm{𝗊𝗉}\mid 𝗊\in \mathbb{P}\setminus 𝗉\}$ is the set of incoming channels of process $𝗉$.

Given an action $a$, an active process, denoted by $\mathrm{𝗉𝗋𝗈𝖼}(a)$, is defined as: $\mathrm{𝗉𝗋𝗈𝖼}(\mathrm{𝗉𝗊}!m)=𝗉$ and $\mathrm{𝗉𝗋𝗈𝖼}(\mathrm{𝗉𝗊}\mathrm{?}m)=𝗊$. Similarly, $\mathrm{𝖼𝗁}(\mathrm{𝗉𝗊}!m)=\mathrm{𝖼𝗁}(\mathrm{𝗉𝗊}\mathrm{?}m)=\mathrm{𝗉𝗊}$.

We say a control state $q\in Q_{𝗉}$ is a sending state (resp. receiving state) if all its outgoing transitions are labelled by send (resp. receive) actions. If a control state is neither a sending nor receiving state, i.e., it either has both send and receive actions or neither, then we call it a mixed state. We say a sending (resp. receiving) state is directed if all the send (resp. receive) actions from that control state are to the same process. Like for finite-state automata, we say that a FIFO automaton ${𝒜}_{𝗉}=(Q_{𝗉},{\delta }_{𝗉},q_{0𝗉})$ is deterministic if for all transitions $(q,a,q^{\prime }),(q,a^{\prime },q^{\prime \prime })\in {\delta }_{𝗉}$, $a=a^{\prime }⟹q^{\prime }=q^{\prime \prime }$. We write $q_1\stackrel{a_1\mathrm{\cdots }{a}_n}{\to }{q}_{n+1}$ for $(q_1,a_1,q_2)\mathrm{\cdots }(q_n,a_n,q_{n+1})\in {\delta }_{𝗉}$. Unless specified otherwise, we consider non-deterministic automata, allowing mixed states, and all states do not have to be directed.

The initial configuration of $𝒮$ is ${\gamma }_0=(\overrightarrow{q_0};\overrightarrow{\epsilon })$ where $\overrightarrow{q_0}={(q_{0𝗉})}_{𝗉\in \mathbb{P}}$ and we write $\overrightarrow{\epsilon }$ for the $|\mathrm{𝐶ℎ}|$-tuple $(\epsilon ,\mathrm{\dots },\epsilon )$. We let ${𝒜}_{𝗉}=(Q_{𝗉},{\delta }_{𝗉},q_{0𝗉})$ be a FIFO automaton. Let $𝒮={({𝒜}_{𝗉})}_{𝗉\in \mathbb{P}}$ be the system whose initial configuration is ${\gamma }_0$. The FIFO automaton $\mathrm{𝗉𝗋𝗈𝖽𝗎𝖼𝗍}(𝒮)$ associated with $𝒮$ is the standard asynchronous product automaton: $\mathrm{𝗉𝗋𝗈𝖽𝗎𝖼𝗍}(𝒮)=(Q,\delta ,\overrightarrow{q_0})$ where $Q={\prod }_{𝗉\in \mathbb{P}}{Q}_{𝗉}$, $\overrightarrow{q_0}={(q_{0𝗉})}_{𝗉\in \mathbb{P}}$, and $\delta$ is the set of triples $(\overrightarrow{q_1},a,\overrightarrow{q_2})$ for which there exists $𝗉\in \mathbb{P}$ such that $(q_1^{}{}_{𝗉}{}^{},a,q_2^{}{}_{𝗉}{}^{})\in {\delta }_{𝗉}$ and $q_1^{}{}_{𝗋}{}^{}=q_2^{}{}_{𝗋}{}^{}$ for all $𝗋\in \mathbb{P}\setminus \{𝗉\}$. An execution $e=a_1\cdot a_2\mathrm{\cdots }{a}_n\in {\mathrm{𝖠𝖼𝗍}}^{\ast }$ is an arbitrary finite sequence of actions. We write $\mathrm{𝖾𝗑𝖾𝖼𝗎𝗍𝗂𝗈𝗇𝗌}(𝒮)$ for $\{e\in {\mathrm{𝖠𝖼𝗍}}^{\ast }\mid {\gamma }_0\stackrel{𝑒}{\to }\gamma \text{ for some configuration }\gamma \}$. Given $e=a_1\cdot a_2\mathrm{\cdots }{a}_n$, we write $\mathrm{𝖠𝖼𝗍}(e)=\{a_1,a_2,\mathrm{\dots },a_n\}$. Moreover, we say two systems are trace-equivalent if they produce the same set of executions, i.e. $𝒮\approx {𝒮}^{\prime }$ is as follows: $\forall \varphi ,\varphi \in \mathrm{𝖾𝗑𝖾𝖼𝗎𝗍𝗂𝗈𝗇𝗌}(𝒮)\iff \varphi \in \mathrm{𝖾𝗑𝖾𝖼𝗎𝗍𝗂𝗈𝗇𝗌}({𝒮}^{\prime })$.

We first extend the definitions of synchrony in systems from [18] to consider possible interferences. The main extension relates to the definition of matching pairs. Intuitively, matching pairs refer to a send action and the corresponding receive action in a given execution. In the presence of interferences, it is not necessary that the same message that is sent is received (due to corruption), or that the $k$-th send action corresponds to the $k$-th receive action (due to lossiness or out-of-order). Hence we extend the definition of matching pairs.

Note that if $m=m^{\prime }$ and $k=k^{\prime }$, we are back to the original definition of matching pairs in [17, Section 2], which we shall refer to henceforth as perfect matching pairs. When we refer to a matching pair, we mean either a perfect or $i$-matching pair. Moreover, our formalism allows for a single message to have more than one kind of interference, e.g. the same message can be corrupted and received out-of-order.

We now modify the definition of interactions from [17] as follows.

Given $e=a_1\mathrm{\cdots }{a}_n$, a set of interactions $\nu$ is called a valid communication of $e$ if for every index $j\in \{1,\mathrm{\dots },n\}$, there exists exactly one interaction $\chi \in \nu$ such that $j\in \chi$. I.e., we need to ensure that every action in $e$ belongs to exactly one interaction in the valid communication. We denote by $\text{Comm}(e)$ the set of all valid communications associated to $e$.

For the rest of this section, when we refer to an execution, we are referring to a tuple $(e,\nu )$ such that $\nu \in \text{Comm}(e)$. We say that two actions $a_1$, $a_2$ commute if $\mathrm{𝗉𝗋𝗈𝖼}(a_1)\ne \mathrm{𝗉𝗋𝗈𝖼}(a_2)$ and they do not form a matching pair.

Given an execution $(e,\nu )$ such that $e=a_1\mathrm{\dots }{a}_n$ and $\nu \in \text{Comm}(e)$, we say that $j{\prec }_{e,\nu }{j}^{\prime }$ if (1) and (2) $a_j$, $a_{j^{\prime }}$ do not commute in $\nu$. We now graphically characterise causally equivalent executions, using the notion of a conflict graph. This allows us to establish equivalences between different executions in which actions can be interchanged.

The conflict graph corresponding to Example 10, $\mathrm{𝖼𝗀𝗋𝖺𝗉𝗁}(e,{\nu }_1)$, is:

Two executions $(e,\nu )$ and $(e^{\prime },{\nu }^{\prime })$ are causally equivalent, denoted by $(e,\nu )\sim (e^{\prime },{\nu }^{\prime })$, if their conflict graphs are isomorphic.

We are now ready to define $i$-rsc systems, which is the extension of rsc to include interferences. Intuitively, $i$-rsc executions can be reordered to mimic rendezvous (or synchronous) communication. In the case with interference, we enforce that every valid communication is equivalent to a RSC execution.

This is the strictest version, however, this can be adapted to include only one communication by assuming a single instance of $\nu$ instead of all. We formalise our observation about non-$i$-rsc behaviours from Example 13, and show that $i$-rsc still maintains the good properties of the conflict graph as in [17].

A borderline violation for interferences defined below is a key concept for the decidability of rsc systems. Intuitively, it provides a “minimal counter-example” for non-rsc behaviour.

Following the same approach as in [17], we show that inclusion into the $i$-rsc class is decidable. For simplicity, we construct the following sets: ${\mathrm{𝖠𝖼𝗍}}_{nr}=\{𝖼!\mathrm{?}m\mid 𝖼!m\in \mathrm{𝖠𝖼𝗍},𝖼\mathrm{?}{m}^{\prime }\in \mathrm{𝖠𝖼𝗍}\}\cup \{𝖼!m\mid 𝖼!m\in \mathrm{𝖠𝖼𝗍}\}$ and ${\mathrm{𝖠𝖼𝗍}}_{\mathrm{?}}=\{𝖼\mathrm{?}m\mid 𝖼\mathrm{?}m\in \mathrm{𝖠𝖼𝗍}\}$. Note that $𝖼!\mathrm{?}m$ could include a send-receive pair where the message sent is different from the one received. This ensures inclusion of matching pairs due to corruption. An $i$-rsc execution can be represented by a word in ${\mathrm{𝖠𝖼𝗍}}_{nr}^{\ast }$ and a borderline violation by a word in ${\mathrm{𝖠𝖼𝗍}}_{nr}^{\ast }.{\mathrm{𝖠𝖼𝗍}}_{\mathrm{?}}$. We first show that the set of borderline violations is regular.

Next we show that the subset of executions $\mathrm{𝖾𝗑𝖾𝖼𝗎𝗍𝗂𝗈𝗇𝗌}(𝒮)$ that begin with an $i$-rsc prefix and terminate with a reception is regular. The construction of the automaton ${𝒜}_{\mathrm{𝑟𝑠𝑐}}$ recognising such a language mimics the $i$-rsc executions of the original system $𝒮$, storing only the information on non-empty buffers, guessing which is the send message that will be matched by the final reception.

For the following result, we let the size $|𝒜|$ of an automaton $𝒜=(Q,\delta ,q_0)$ be $|Q|+|\delta |$. Moreover, the size $|𝒮|$ of a system $𝒮={({𝒜}_{𝗉})}_{𝗉\in \mathbb{P}}$ = ${\sum }_{𝗉\in \mathbb{P}}|{𝒜}_{𝗉}|$.

Using the above lemmas, we derive the following main theorem in this section, which states that the inclusion of an $i$-rsc system is decidable; and the complexity is comparable to that of checking inclusion to rsc[17, Theorem 12].

We extend our analyses to consider $k$-multiparty compatibility ($k$-mc) which was introduced in [35] for a subset of FIFO systems, called communicating session automata (CSA). CSA strictly include systems corresponding to asynchronous multiparty session types [15].

In this section, we only consider communicating session automata. We begin by recalling the definition of $k$-mc which is composed of two properties, $k$-safety and $k$-exhaustivity.

The $k$-safety condition is composed of two properties, the first being eventual reception ($k$-er) which ensures that every message sent to a channel is eventually received. The other property is progress ($k$-pg) where the system is not “stuck” at any receiving state.

A system is $k$-exhaustive if for all $k$-reachable configurations, whenever a send action is enabled, it can be fired within a $k$-bounded execution.

Example 23 shows that the reachability set of $k$-mc is not necessarily regular, unlike the binary half-duplex systems [14].

We prove that $k$-mc in the absence of errors, for a large class of systems the $k$-safety property subsumes $k$-exhaustivity.

Session types [46, 27, 28] are a type discipline to ensure communication safety for message passing systems. Most session types assume a scenario where participants operate reliably, i.e. communication happens without failures. To model systems closer to the real world, Barwell et al. [6, 3] introduced session types with crash-stop failures. In this section, we consider the same notion for communicating systems which we define as crash-handling.

This section shows that the crash-handling system strictly subsumes the crash-stop systems in [3, 5], preserving the semantics. We recall the crash-stop semantics for local types defined in [3] where the major additions are (1) a special local type $\mathrm{𝗌𝗍𝗈𝗉}$ to denote crashed processes; and (2) a crash-handling branch (catch) in one of branches of an external choice.

The syntax of the local types ($S,T,\mathrm{\dots }$) are given as:

An external choice (branching) (resp., an internal choice (selection)), denoted by $𝗉\mathrm{?}{\{m_i.T_i\}}_{i\in I}$ (resp., $𝗉!{\{m_i.T_i\}}_{i\in I}$) indicates that the current role is to receive from (or send to) the process $𝗉$. We require pairwise-distinct, non-empty labels and the crash-handling label (catch) not appear in internal choices; and that singleton crash-handling labels not permitted in external choices. The type $\mathrm{𝖾𝗇𝖽}$ indicates a successful termination (omitted where unambiguous), and recursive types are assumed guarded, i.e., $\mu 𝐭.𝐭$ is not allowed, and recursive variables are unique. A runtime type $\mathrm{𝗌𝗍𝗈𝗉}$ denotes crashes.

We point out here that while this is a bottom-up view of the crash-handling behaviour introduced in [3], we have taken a purely type-based approach here. For a calculus based approach, we refer the reader to [4].

We define the LTS over local types and extend the notions to communicating systems. We use the same labels as the ones for communicating systems.

Rules [LR1] and [LR2] are standard output/input and recursion rules, respectively; rule [LR3] accommodates for the crash of a process; rule [LR4] is the main rule for crash-handling where the reception of crash information leads the process to a crash-handling branch; and rule [LR5] allows any dangling crash information messages to be read in the sink states.

The LTS over a set of local types is defined as in Definition 3, where a configuration $\gamma =(\overrightarrow{T};\overrightarrow{w})$ of a system is a pair with $\overrightarrow{T}={\{T_{𝗉}\}}_{𝗉\in \mathbb{P}}$ and $\overrightarrow{w}={(w_{\mathrm{𝗉𝗊}})}_{\mathrm{𝗉𝗊}\in \mathrm{𝐶ℎ}}$ with $w_{\mathrm{𝗉𝗊}}\in {\mathrm{\Sigma }}^{\ast }$.

Next we algorithmically translate from local types to FIFO automata preserving the trace semantics. Below we write $\mu \overrightarrow{𝐭}.T$ for $\mu {𝐭}_1.\mu {𝐭}_2\mathrm{\dots }\mu {𝐭}_n.T$ with $n\ge 0$.

In order to construct the FIFO automata, we first need to define the set of states. Intuitively, this is the set of types which result from any continuation of the initial local type. Below we define a type occurring in another type (based on the definition in [47]).

And now, we are ready to define the FIFO automata.

We now prove that the automata generated from a local type can be composed into communicating session automata, and this translation preserves the semantics.

By Lemma 39, we derive that the resulting systems belong to the class of crash-handling systems, and the problem of checking rsc and $k$-wmc is decidable for this class.