Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unreliability in Practical Subclasses of Communicating Systems

Amrita Suresh, Nobuko Yoshida

TL;DR

The paper addresses resilience of practical decidable FIFO-subclasses, notably $\textsc{rsc}$ and $k$-mc, under realistic failures including interferences and crash-stop. It introduces $i$-rsc and $k$-wmc to capture interferences while preserving decidability and extends the model to crash-handling FIFO systems, proving decidability for $\textsc{rsc}$ and $k$-wmc under crash-stop failures, plus a trace-preserving MPST-to-crash-handling translation. It validates the approach by extending verification tools to support interferences and by evaluating representative protocols, illustrating practical robustness of these subclasses. Overall, the results establish that key verification properties remain decidable with comparable complexity in the presence of realistic channel and process failures, enabling more reliable analysis of distributed protocols.

Abstract

Systems of communicating automata are prominent models for peer-to-peer message-passing over unbounded channels, but in the general scenario, most verification properties are undecidable. To address this issue, two decidable subclasses, Realisable with Synchronous Communication (RSC) and k-Multiparty Compatibility} (k-MC), were proposed in the literature, with corresponding verification tools developed and applied in practice. Unfortunately, both RSC and k-MC are not resilient under failures: (1) their decidability relies on the assumption of perfect channels and (2) most standard protocols do not satisfy RSC or k-MC under failures. To address these limitations, this paper studies the resilience of RSC and k-MC under two distinct failure models: interference and crash-stop failures. For interference, we relax the conditions of RSC and k-MC and prove that the inclusions of these relaxed properties remain decidable under interference, preserving their known complexity bounds. We then propose a novel crash-handling communicating system that captures wider behaviours than existing multiparty session types (MPST) with crash-stop failures. We study a translation of MPST with crash-stop failures into this system integrating RSC and k-MC properties, and establish their decidability results. Finally, by verifying representative protocols from the literature using RSC and k-MC tools extended to interferences, we evaluate the relaxed systems and demonstrate their resilience.

Unreliability in Practical Subclasses of Communicating Systems

TL;DR

The paper addresses resilience of practical decidable FIFO-subclasses, notably and -mc, under realistic failures including interferences and crash-stop. It introduces -rsc and -wmc to capture interferences while preserving decidability and extends the model to crash-handling FIFO systems, proving decidability for and -wmc under crash-stop failures, plus a trace-preserving MPST-to-crash-handling translation. It validates the approach by extending verification tools to support interferences and by evaluating representative protocols, illustrating practical robustness of these subclasses. Overall, the results establish that key verification properties remain decidable with comparable complexity in the presence of realistic channel and process failures, enabling more reliable analysis of distributed protocols.

Abstract

Systems of communicating automata are prominent models for peer-to-peer message-passing over unbounded channels, but in the general scenario, most verification properties are undecidable. To address this issue, two decidable subclasses, Realisable with Synchronous Communication (RSC) and k-Multiparty Compatibility} (k-MC), were proposed in the literature, with corresponding verification tools developed and applied in practice. Unfortunately, both RSC and k-MC are not resilient under failures: (1) their decidability relies on the assumption of perfect channels and (2) most standard protocols do not satisfy RSC or k-MC under failures. To address these limitations, this paper studies the resilience of RSC and k-MC under two distinct failure models: interference and crash-stop failures. For interference, we relax the conditions of RSC and k-MC and prove that the inclusions of these relaxed properties remain decidable under interference, preserving their known complexity bounds. We then propose a novel crash-handling communicating system that captures wider behaviours than existing multiparty session types (MPST) with crash-stop failures. We study a translation of MPST with crash-stop failures into this system integrating RSC and k-MC properties, and establish their decidability results. Finally, by verifying representative protocols from the literature using RSC and k-MC tools extended to interferences, we evaluate the relaxed systems and demonstrate their resilience.

Paper Structure

This paper contains 4 sections, 5 theorems, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. RSC systems with interferences
  4. $k$-Multiparty Compatibility with interferences

Key Result

Lemma 13

An execution $(e, \nu)$ is causally equivalent to an $\textsc{$i$-rsc}$ execution iff the associated conflict graph $\mathsf{cgraph}(e, \nu)$ is acyclic.

Figures (2)

  • Figure 1: Classes of communication systems (since the $\dagger$-marked definitions are introduced in the context of CSA (Def \ref{['def:csa']}), we restrict them accordingly).
  • Figure 2: The above system $\mathcal{S}$ is half-duplex in the absence of errors. However, in case of (any or multiple) errors, it is no longer half-duplex.

Theorems & Definitions (21)

  • Example 1
  • Definition 2: FIFO automaton
  • Definition 3: FIFO system
  • Definition 4: Interference model
  • Definition 5: Successor configuration under interference
  • Example 6
  • Definition 7: Matching pair with interference
  • Example 8
  • Definition 9: Interaction
  • Example 10
  • ...and 11 more