A Behavioral Theory For Crash Failures and Erlang-style Recoveries In Distributed Systems

Distributed systems can be subject to various kinds of partial failures, and building fault-tolerance or failure mitigation mechanisms for distributed systems remains an important domain of research. In this paper, we present a calculus to formally model distributed systems subject to crash failures, and in which one can encode recovery mechanisms by leveraging a small set of lightweight (in terms of implementation cost) primitives. To the best of our knowledge, our calculus is the first one with support for all the following characteristics: i) asynchronous communication; ii) unique location for receivers; iii) dynamic nodes and links; iv) crash failures with recovery; v) nodes with imperfect knowledge of their context. We define a contextual equivalence for our calculus in the classical form of a barbed congruence, and a notion of bisimilarity which we prove fully abstract with respect to our barbed congruence. In addition, we show by means of examples that our calculus can support Erlang-style fault management and recovery, and that our behavioral theory agrees on key instances without recovery with previous work by Francalanza and Hennessy. This paper can be understood as a complete reworking and an extension to tackle recovery of Francalanza and Hennessy’s work.Les systèmes distribués peuvent être soumis à différents types de défaillances partielles, et l'élaboration de mécanismes de tolérance aux pannes ou d'atténuation des défaillances pour les systèmes distribués reste un domaine de recherche important. Dans cet article, nous présentons un calcul permettant de modéliser formellement les systèmes distribués soumis à des défaillances accidentelles, et dans lequel il est possible d'encoder des mécanismes de récupération en tirant parti d'un petit ensemble de primitives légères (en termes de coût d'implémentation). À notre connaissance, notre calcul est le premier à prendre en charge toutes les caractéristiques suivantes : i) communication asynchrone ; ii) emplacement unique pour les récepteurs ; iii) nœuds et liens dynamiques ; iv) pannes avec récupération ; v) nœuds ayant une connaissance imparfaite de leur contexte. Nous définissons une équivalence contextuelle pour notre calcul sous la forme classique d'une congruence barrée, ainsi qu'une notion de bisimilarité que nous prouvons totalement abstraite par rapport à notre congruence barrée. En outre, nous montrons à l'aide d'exemples que notre calcul peut prendre en charge la gestion et la récupération des fautes à la manière d'Erlang, et que notre théorie comportementale est en accord avec les travaux antérieurs de Francalanza et Hennessy en ce qui concerne les instances clés sans récupération. Cet article peut être considéré comme un remaniement complet et une extension du travail de Francalanza et Hennessy pour aborder la récupération.Traduit avec www.DeepL.com/Translator (version gratuite