Giovanni Fabbretti

Ivan Lanese

Jean-Bernard Stefani

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

Keywords: formal calculi, distributed systems, concurrency, failures, recoveries

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.

Une théorie comportementale des défaillances et des reprise en style Erlang dans les systèmes distribués.

Résumé : 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) noeuds et liens dynamiques ; iv) pannes avec récupération ; v) noeuds 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.

Mots-clés : calcul formel, systèmes distribués, concurrence, défaillances, reprises

Introduction

A key characteristic of distributed computer systems is the occurrence of partial failures, which can affect part of a system, e.g. failures of the system nodes (computers and the processes they support) or failures of the connections between them. The model of crash failures with recovery, where a node can fail by ceasing to operate entirely, and later on recover its operation (typically, after some administrator intervention) is an important model of failure to consider because of its relevance in practice. However the correct design of systems in this model is far from trivial, as the recent study on bugs affecting crash recovery in distributed systems demonstrates [START_REF] Gao | An empirical study on crash recovery bugs in large-scale distributed systems[END_REF]. Developing a process calculus analysis of the behavior of distributed systems with crash failures and recovery can help in this respect for it can reveal subtle phenomena in the behavior of such systems, and it can be leveraged for the development of analysis tools, such as verifiers and debuggers. Unfortunately, to the best of our knowledge, the literature contains precious few examples of process calculi accounting for crash failures with recovery, notably [START_REF] Fournet | A calculus of mobile agents[END_REF][START_REF] Amadio | An asynchronous model of locality, failure and process mobility[END_REF][START_REF] Berger | The two-phase commitment protocol in an extended pi-calculus[END_REF][START_REF] Bocchi | A model of actors and grey failures[END_REF], and none account simultaneously for the following features which we deem essential to faithfully model actual distributed systems:

1. Asynchronous communication: interaction between processes proceeds not by rendez-vous but by an asynchronous exchange of messages, which can possibly be lost or reordered while transiting to their destination.

2. Unique location for receivers: each communication targets a single location, either local or remote. This would not be the case, e.g., if communication were via channels, and receivers for a same channel could reside on different locations. This feature ensures that the complexity of message exchange is commensurate with that of simple asynchronous communication used in the Internet, and that no hidden cost, due for instance to leader election or routing protocols, is implied for the implementation of a simple message exchange (see e.g. [START_REF] Fournet | The reflexive CHAM and the join-calculus[END_REF] for a discussion).

3. Dynamic nodes and links: the number of nodes in a system, and of communication links between them, is not fixed and may vary. During execution, new nodes and links can be established, existing nodes and links can be removed, either because of failures or by design. This feature is necessary to account for actual distributed systems whose configurations may vary at run-time, notably because of failure management and of performance management (e.g. scaling decisions in cloud systems). The explicit presence of links is important because partial connections often affect large distributed systems and because introducing link failures leads to a different behavioral theory than dealing with node failures only, as noted in [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF].

4. Crash failures: when a node or a link fails, it does so silently, by ceasing execution. This is a simplifying assumption on the failure model of actual distributed systems, but one which, barring malicious faults, can be relatively well approximated in practice, as with the let it fail policy in Erlang.

5.

Recovery: when a node or link has failed, it can be revived to resume its execution or function. This may imply external intervention (e.g. by a human administrator) and may not be under the control of the running system. Note that we place no strong requirement on the resume operation, just that a recovered node be able to perform some computation: e.g. it need not guarantee that a recovered node operates exactly as prior to its crash. This weak recovery model is consistent e.g. with node recovery in Erlang, or the node failure model adopted in the Verdi framework for distributed systems verification [START_REF] Wilcox | Verdi: a framework for implementing and formally verifying distributed systems[END_REF]. Inria 6. Imperfect knowledge: in general, in a distributed system, a node has only a partial and imperfect knowledge of the overall state of the system. We call local view the belief a node entertains of the status of its neighbors (nodes it assumes it is connected to). Local views are explicitly maintained by distributed programming language runtimes such as that of Erlang [START_REF] Armstrong | Programming Erlang -Software for a Concurrent World[END_REF] and Elixir [START_REF] Juric | Elixir in Action[END_REF]. They play an essential part of key distributed algorithms, such as failure detection [START_REF] Gupta | On scalable and efficient distributed failure detectors[END_REF], membership management [START_REF] Das | SWIM: scalable weakly-consistent infection-style process group membership protocol[END_REF], checkpoint-rollback recovery schemes [START_REF] Elnozahy | A survey of rollbackrecovery protocols in message-passing systems[END_REF], or gossip-based peer sampling [START_REF] Jelasity | Gossip-based peer sampling[END_REF].

The two works dealing with crash failures and recovery that come closest to meeting these modeling requirements are [START_REF] Berger | The two-phase commitment protocol in an extended pi-calculus[END_REF] and the recent [START_REF] Bocchi | A model of actors and grey failures[END_REF]. However, they only consider a fixed number of nodes, and to model recovery they rely on timers and checkpointing constructs (their save primitives). Checkpointing primitives are powerful mechanisms that do not match our weak requirements to account for recovery. For instance, recovery in Erlang systems can take place without relying on checkpointing, just by restarting failed nodes and processes in a predefined state, possibly relying on persistence mechanisms for preserving data across node failures.

The goal of this paper, then, is to introduce a process calculus exhibiting all the above features, with no recourse to timers, perfect failure detection or a built-in checkpointing primitive. We have two additional requirements for this calculus. On the one hand, it has to stay close to the behavior of Erlang; on the other hand it has to stay as close as possible to the work by Francalanza and Hennessy [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF]. The Erlang programming language and its environment are representative of modern distributed programming facilities. It is a functional, concurrent and distributed language based on the actor model, and it is used in several large distributed projects [12]. It is well known for its "let it fail" policy, whereby a service that is not working as expected is killed as soon as the faulty behavior is detected, if not dead already, and restarted by its supervisor. Staying close to Erlang ensures our modeling remains faithful to actual distributed systems. The work by Francalanza and Hennessy [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF] constitutes a good benchmark for comparison. While not tackling recovery and relying on perfect failure detection, it contains several of the features mentioned above, and develops a behavioral theory with node and link failures. Staying close to it allows us to compare our behavioral theory with an established one, when restricting our attention to systems without recovery.

The rest of this paper is organized as follows. Section 2 introduces a motivating example, which serves also as an introduction to our calculus. Section 3 presents the calculus, its reduction semantics, and discusses key design choices. Section 4 equips our calculus with a notion of barbed congruence and characterizes it by a notion of bisimilarity to obtain a proof technique for checking system equivalence. Section 5 shows our calculus can encode constructs similar to Erlang primitives to build systems with hierarchical failure management. Moreover, we show that our behavioral theory agrees with the one in [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF] on key examples withour recovery. Finally, Section 6 discusses related work and concludes. Details of proofs and complementary material are available in the Appendix.

Crash and Recovery: Motivating Example

Before presenting our calculus, we discuss a motivating example which serves as an informal introduction (for the time being, we omit some details). An Erlang implementation of the example is discussed in Appendix B. Consider the following system:

servD = ν n r , n b , r 1 , r 2 , b. ∆ [ I ] ni [ R ] nr [ B ] n b

RR n°9511

where:

I = req(y, z).spawn n r .r 1 y, z R = (r 1 (y, z).spawn n b .b y, z ) | (r 2 (y, z).spawn n i .z y ) B = b(y, z).spawn n r .r 2 z, w y
System servD depicts a distributed server running on a network ∆. The network, ∆, whose formal definition we omit for the moment, can be graphically represented as follows,

•

n i • nr • n b
where • represents an alive location and the arrow represents a live bidirectional communication link between locations. A location in our calculus represents a locus of computation. It can represent a hardware node in a distributed system, or a virtual machine or a container running on a hardware node. A location constitutes also a unit of crash failure: when a location fails, all processes inside the location cease to function. Located processes take the form [ P ]

n , where P denotes a process and where n is the location name. There can be several processes located at the same location: for instance,

[ P ] n [ Q ]
n denotes two processes P and Q running in parallel inside the same location n.

The (admittedly simplistic) system servD behaves as follows. The interface process I, running on n i , awaits a single request from the environment on channel req. Once received, the elements of the request (a parameter y, and a return channel z) are routed to location n b , which runs the backend process B, through location n r , which hosts the router process R, as there is no direct link between n i and n b . The router awaits for the elements of the request on a private channel r 1 and forwards them by spawning a message b y, z on n b , where b is a private channel. Message sending in our calculus can only occur locally. For two remote locations to communicate, like for n i and n r , it is necessary for one to asynchronously spawn the message on the other one. The backend handles the information y and returns the answer w y to the interface, again by routing it through n r . Finally, the interface emits the answer on z for the client to consume it.

The following is a possible client for servD

[ spawn n i .(req h, z | z(w).Q) ] c
It sends a request to the interface n i by spawning it on n i . It also spawns a process on n i to handle the response, which will take the form of a message on channel z located on n i . Now, consider the following system:

servDF = ν n r , n b , n c , r 1 , r 2 , b, retry. ∆ [ J ] ni [ R ] nr [ kill ] nr [ !B ] n b [ !C ] nc where: J = req(y, z).((spawn n r .r 1 y, z ) | retry.spawn n r .r 1 y, z ) C = create n r .(R | spawn n i .retry)
Here, ∆ could be graphically represented like ∆ only with an extra link between n r and n c . System servDF represents a distributed server where location n r may be subject to one failure, modeled by the primitive kill. The system has a recovery mechanism in place to deal with that potential failure: the controller [ !C ] nc is a location that keeps trying, through the apposite primitive create, to recreate n r (the ! operator is akin to the π-calculus operator for replication), together with a message to restart the handling of the request. The interface is more sophisticated as it can now send a second request when asked to retry if something goes wrong with the first one. If n r fails, the controller can create another router with a message retry for the interface which will start the second attempt.

Inria

At first glance, servDF seems to correctly handle the failure scenario, but that is not the case. Indeed, consider an execution where the failure happens after the request has already been handled. In such case, the request would be processed again and another response sent back by the interface, a behavior that cannot be exhibited by servD. If one considers servD as the specification to meet, servDF does not satisfy it.

The following system correctly handles recovery, in that it meets the servD specification: In system servDFR the response from the backend is not directly sent to the client, but goes through a private channel c on which the interface listens only once. This mechanism prevents emitting the answer to the request twice. System servDFR can be understood as a masking 1-fault tolerant system, equivalent to the ideal one servD. We develop in Section 4 a behavioral theory able to tell apart servD from servDF, and able to prove equivalent servD and servDFR.

servDFR = ν n r , n b , n c , r 1 , r 2 , b, c, retry. ∆ [ K ] ni [ R ] nr [ kill ] nr [ !B ] n b [ !C ]

The Calculus

Names and notations

We assume given mutually disjoint infinite denumerable sets C, N and I. C is the set of channel names, N is the set of location names, and I is the set of incarnation variables. We use the set of integers Z as the set of incarnation numbers. An incarnation number is paired with a location name for recovery purposes, to distinguish the current instance of a location from its past failed instances. We denote by N the set N ∪ { }, where ∈ N. As in the π-calculus, channel names can be free or bound in terms. The same holds for location names. Incarnation variables can be bound, but not incarnation numbers. We denote by ũ a finite (possibly empty) tuple of elements. We write T {ṽ/ũ} for the usual capture-avoiding substitution of elements of ũ by elements of ṽ in term T , assuming tuples ũ and ṽ have the same arity. We write u, ṽ or ṽ, u for the tuple ṽ extended with element u as first or last element. Abusing notation, we sometimes identify a tuple ũ with the set of its elements. We denote by N + the set of strictly positive integers (by definition 0 ∈ N + ), and by N the set of positive integers (0 ∈ N). We denote by 0 the function 0 : N → Z that maps any n ∈ N to 0 and to 1.

Syntax

Systems in our calculus are defined through three levels of syntax, one for processes, one for configurations, one for systems.

The syntax of processes is defined as follows:

P, Q ::= 0 x ũ .P x(ṽ).P !x(ṽ).P ν w.P if r = s then P else Q P | Q node(n, λ).P remove n.P spawn n.P kill create n.P link n.P unlink n.P where:

ũ, r, s ⊂ C ∪ N ∪ I ∪ Z ṽ ⊂ C ∪ N ∪ I w ∈ C ∪ N x ∈ C n ∈ N λ ∈ I
Terms of the form x(ũ).P , ν w.P , and node(n, λ).P are binding constructs for their arguments ũ, w and n, λ, respectively.

The syntax of processes is that of the π-calculus with matching [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF] and replicated receivers (first line of productions), extended with primitives for distributed computing inspired from the Erlang programming language (second line of productions), and three primitives to activate locations, establish and remove links (third line of productions). 0 is the null process which can take no action. Processes can communicate by emitting a message x ṽ .P which can be received by some receiver process of the form x(ũ).Q residing on the same location. We write x ũ for x ṽ .0, and just x when ũ is empty. We assume the calculus is well-sorted, so that the arity of receivers always matches that of received messages. The construct !x(ũ).P is the replicated input construct, which replicates itself when receiving a message on channel x. Note that we use in our examples (as we did in the previous Section) the short-hand !P for ν c.(c | !c.(P | c)). The construct ν w.P is the standard restriction construct, which creates a fresh location or channel name. If ũ is a (possibly empty) tuple of names, we write ν ũ.P for ν u 1 . . . . ν u n .P if ũ = (u 1 , . . . , u n ). If ũ is empty, ν ũ.P is just P . The construct if r = s then P else Q tests the equality of names r and s and continues as P if the names match and as Q otherwise. The construct P | Q is the standard parallel composition for processes. Primitive node(n, λ).P substitutes n with the name of the current location, λ with the current incarnation number, and continues as P . Primitive remove n.P removes the location with name n from the local view of the current location and continues as P . Primitive spawn n.P launches process P at the location named n, if the latter is accessible. Primitive kill stops the current location in its current incarnation: no process can execute on a killed location; kill also models the crash of a location. Primitive create n.P creates a new location n, or reactivates a killed location with a new incarnation number, and launches process P on it. Primitive link n.P creates a connection between the current location and n and continues as P , while, unlink n.P breaks the link between the current location and n and continues as P ; unlink also models the failure of a link.

The syntax of configurations is defined as follows:

L, M, N ::= 0 [ P ] n λ is a process P running on location (n, λ), where n is the name of the location and λ is an incarnation number (used for recovery). In examples, we may drop incarnation numbers of located processes if they are not relevant. Note that the special name identifies a well-known location which we will assume to be un-killable. Location is used merely for technical purposes to ensure we can simply build appropriate contexts for running systems. Apart from being unkillable, location behaves just as any other locations. We denote by L the set of configurations.

The syntax of systems is defined as follows:

S, R ::= ∆ N | ν w.S where:

w ∈ N ∪ C
A system is the composition of a network ∆ with a configuration N , or a system under a name (channel or location) restriction. We denote by S the set of systems. A network ∆, is a tuple A, L, V where • A is a function A : N → Z such that A( ) = 1 and such that the set supp(A) def = {n ∈ N | A(n) = 0} is finite. Function A may record three types of information on locations. If A(n) = λ ∈ N + , then location n is alive and its current incarnation number is λ. If A(n) = -λ, λ ∈ N + then location n has been killed and its last incarnation number while alive was λ. If A(n) = 0, then there is no location n in the network, alive or not. Because Inria of the finiteness condition above, a network can only host a finite number of locations, alive or dead.

• L ⊆ N × N is the set of links between locations. L is a finite symmetric binary relation over location names such that dom(L)

def = {n ∈ N | ∃m, (n, m) ∈ L} is finite. • V : N → (N → N)
is a function that maps location names to their local view, which is such that the set supp(V)

def = {n ∈ N | V(n) = 0} is finite and supp(V) ⊆ supp(A). The local view of a location n is a function V(n) : N → N such that the set {m ∈ N | V(n)(m) = 0} is finite. If V(n)(m) = κ ∈ N + ,
then location m in its incarnation κ is believed by n to be alive. If V(n)(m) = 0, then location n holds no belief on the status of location m.

For convenience we use ∆ A , ∆ L , and ∆ V to denote the individual components of a network representation ∆, and we use the following notations for extracting information from ∆:

• ∆ n λ : alive if ∆ A (n) = λ and λ ∈ N + . • ∆ n : dead if ∆ A (n) ∈ N + • ∆ n ↔ m if (n, m) ∈ ∆ L • ∆ n λ m κ if (n, m) ∈ ∆ L , ∆ n λ :
alive and ∆ m κ : alive

We now define update operations over a network ∆.

Definition 1 (Network updates). Network update operations are defined as follows:

• ∆ ⊕ n ↔ m = ∆ A , ∆ L ∪ {(n, m), (m, n)}, ∆ V • ∆ n ↔ m = ∆ A , ∆ L \ {(n, m), (m, n)}, ∆ V • ∆ ⊕ (n, λ) = ∆ A [n → λ], ∆ L ∪ {(n, n)}, ∆ V [n → 0] • ∆ (n, λ) = ∆ A [n → -λ], ∆ L , ∆ V • ∆ ⊕ n (m, λ) = ∆ A , ∆ L , ∆ V [n → ∆ V (n)[m → λ]] , if n = m • ∆ n m = ∆ A , ∆ L , ∆ V [n → ∆ V (n)[m → 0]] , if n = m • ∆ n n = ∆ ⊕ n (n, λ) = ∆
∆ ⊕ n ↔ m and ∆ n ↔ m add and remove a link, respectively, between n and m. ∆ ⊕ (n, λ) activates location n with incarnation number λ, and sets its view to the empty one. ∆ (n, λ) kills a location in its incarnation λ. ∆ ⊕ n (m, λ) adds (m, λ) to the view of n, and ∆ n m removes any belief on location m from the view of n.

We use below the notion of closed systems. Closed systems are systems which do not have free incarnation variables. The definition of free variables in systems and that of free names in configurations is completely standard. The notion of free names in a system is slightly unconventional because of the presence of a network, but it can be defined straightforwardly (see Appendix A for details).

S =α R S ≡ R [S.Ctx] N ≡ M C[N ] ≡ C[M ] Figure 1: Structural Congruence Rules Assuming ∆ n λ : alive msg ∆ [ x ṽ .Q ] n λ [ x(ũ).P ] n λ -→ ∆ [ Q ] n λ [ P {ṽ/ũ} ] n λ bang ∆ [ !x(ũ).P ] n λ -→ ∆ [ x(ũ).(P | !x(ũ).P ) ] n λ new ∆ [ ν u.P ] n λ -→ ν u.∆ [ P ] n λ u / ∈ fn(∆) ∪ {n, λ} fork ∆ [ P | Q ] n λ -→ ∆ [ P ] n λ [ Q ] n λ if-neq ∆ [ if r = s then P else Q ] n λ -→ ∆ [ Q ] n λ r = s node ∆ [ node(m, κ).P ] n λ -→ ∆ [ P {n, λ/m, κ} ] n λ if-eq ∆ [ if r = r then P else Q ] n λ -→ ∆ [ P ] n λ remove ∆ [ remove m.P ] n λ -→ ∆ n m [ P ] n λ

Reduction Semantics

The operational semantics of our calculus is defined via a reduction semantics given by a binary relation -→ ⊆ S × S between closed systems, and a structural congruence relation ≡ ⊆ S 2 ∪ L 2 , that is a binary equivalence relation between systems and between configurations. Evaluation contexts are "systems with a hole •" defined by the following grammar:

C ::= ν w.∆ E E ::= • (N E) where: w ⊂ N ∪ C
Relation ≡ is the smallest equivalence relation defined by the rules in Fig. 1, where = α stands for equality up to alpha-conversion, M, N, L ∈ L, and S, R ∈ S. Most rules are mundane. Rule S.Ctx turns ≡ into a congruence for the parallel and restriction operators. Alpha-conversion on systems, which appears in Rule S.α, is slightly unusual but can be defined straightforwardly (see Appendix A for details).

The reduction relation -→ is defined by the rules in Fig. 2, 3 and 4. Fig. 2 depicts the local reduction rules, i.e., those rules that involve only a single location and that essentially do not modify the network. Rule msg defines the receipt of a message by an input process. Rule bang defines the expansion of a replicated input process. Rule new performs the scope extrusion of a name from a process to a system. We introduced this rule as a computational step instead of a structural congruence rule for it simplifies our proofs. Rule fork turns a parallel composition into parallel threads in the same location. Rules if-eq, if-neq define the semantics of the branching construct. Rule node gets hold of the current location name and its incarnation number for further processing. Finally, rule remove deletes from the local view of the current location the belief it may hold about a given location m.

Fig. 3 depicts the distributed rules, i.e., rules that involve several locations or modify the network. Rule spawn-s defines a successful spawn, conditional upon the fact that a link exists between the spawning and target locations, and that the spawning location rightly believes the target location, with the incarnation recorded in its view, to be alive, or has no belief on the target location in its local view. This last constraint is captured by the side condition ∆ n (m) = κ, which we formally define as follow:

Inria spawn-s ∆ [ spawn m.P ] n λ -→ ∆ ⊕ m (n, λ) [ P ] m κ ∆n(m) = κ ∆ n λ mκ spawn-f ∆ [ spawn m.P ] n λ -→ ∆ n m 0 ∆n(m) = κ ∆ n λ mκ create-s ∆ [ create m.P ] n λ -→ ∆ ⊕ (m, κ + 1) [ P ] m κ+1 ∆ m : dead ∆ A (m) = -κ create-f ∆ [ create m.P ] n λ -→ ∆ 0 ∆ m : dead kill ∆ [ kill ] n λ -→ ∆ (n, λ) 0 n = link ∆ [ link m.P ] n λ -→ ∆ ⊕ n ↔ m [ P ] n λ ∆ n ↔ m unlink ∆ [ unlink m.P ] n λ -→ ∆ n ↔ m [ P ] n λ ∆ n ↔ m
∆ n (m) =          κ if n = m and ∆ A (n) = κ κ if n = m and ∆ V (n)(m) = κ κ if n = m and ∆ V (n)(m) = 0 and ∆ A (m) = κ 0 otherwise
Note that a successful spawn updates the target local view with the belief that the spawning location is alive with the incarnation number it had when it initiated the spawn. Rule spawnf defines a failed spawn, which may fail due to a wrong view, to a missing link between the two locations, or because the remote location is not alive. The view of the sender is updated by removing the belief on the target. This behavior is inspired by Erlang whose runtime, in a manner transparent to the user, updates the view of the spawning location if it receives no acknowledgement from the target as part of its distributed protocol. Rules link and unlink define respectively the establishment of a link and the removal of a link. Rule create-s defines the successful creation or reactivation of a location, provided it did not already exist in the network or was crashed. The newly activated location has an incarnation number that is the successor of the previous one (0 by convention if the location was not present in the network). Note that we do not require the existence of an alive link between the current location and the one to be activated since we want this operation to also model the possibility of interventions external to the system, such as those performed by human administrators. Note also that a location cannot be created anew each time, otherwise it would be impossible to resume the execution of a service under a well-known name. The use of incarnation numbers provides support for recovery schemes (see the discussion below in Section 3.4). Rule create-f defines

par ∆ N -→ ν ũ.∆ N ũ ∩ fn(M ) = ∅ ∆ N M -→ ν ũ.∆ N M res S -→ S ν u.S -→ ν u.S str S ≡ S S -→ R R ≡ R S -→ R Figure 4: Contextual rules
the failure of a create operation, which can fail because the location to activate may already be alive. Rule kill defines the killing of a location. Fig. 4 shows the contextual rules of our calculus. Rules par, and res are the rules respectively for parallel execution, and execution under restriction. Rule par is slightly unconventional in its use of restriction. When we consider the case where ũ is empty in rule par, we obtain a more standard-looking contextual rule for the parallel operator. However, we also have to consider cases when the active branch in the composition promotes a restriction at system level (via an application of rule new). In this case we have to avoid name capture by the idle branch in the composition. This way of proceeeding, coupled with the systematic presence of the distinguished location in any network, spares us the need to introduce parallel composition between systems. The intuition is that we can always extend a system with a process located on (to ensure it is alive) performing the desired changes on the public part of the network. This intuition is formalized in Appendix C.

Discussion

Communication. In our calculus, communication is local. Remote communication is obtained using the spawn operation (very similar to the go operation in [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF]) to send to a target node a process performing an output of a message. As a result remote communication is asynchronous (since the spawn is so), and there is a single location where the receiver can reside (since such location is specified in the spawn). This avoids the need of using a type system to ensure that possible receivers are located on a same node, differently from calculi based on channel-based remote communication such as [START_REF] Amadio | An asynchronous model of locality, failure and process mobility[END_REF].

Incarnation numbers. Incarnation numbers are called creation numbers in Erlang [11]. We introduce them in our calculus for two main reasons. On the one hand, this ensures we are faithful to Erlang and to the behavior Erlang systems exhibit in presence of failures (more details are provided in Appendix B). On the other hand, this ensures we have basic support in place for encoding different recovery schemes. Incarnation numbers ensure that a message issued by a previous incarnation of a location can safely be dropped, avoiding message duplication across different incarnations of the same location. They are present, under various names such as incarnation or epoch numbers, in several rollback-recovery schemes surveyed in [START_REF] Elnozahy | A survey of rollbackrecovery protocols in message-passing systems[END_REF], such as optimistic recovery [START_REF] Strom | Optimistic recovery in distributed systems[END_REF][START_REF] Om | Optimistic recovery in multi-threaded distributed systems[END_REF] or causal logging schemes [START_REF] Elnozahy | Manetho: Transparent rollback-recovery with low overhead, limited rollback, and fast output commit[END_REF]. They are also used for scalable distributed failure detection schemes [START_REF] Gupta | On scalable and efficient distributed failure detectors[END_REF] and in the SWIM protocol combining failure detection and membership management [START_REF] Das | SWIM: scalable weakly-consistent infection-style process group membership protocol[END_REF].

Imperfect knowledge. In distributed systems, the only way for locations to know something about the context that surrounds them is to communicate. If a location n receives a message from a remote one then n learns something on the context, namely that at some point in time the remote location was alive and working since it sent a message to n. Nonetheless, n cannot infer anything on the current status of the remote location or the status of the connection. Indeed, it could have stopped right after sending the message or the link could have broken right after the message was received or both. Erlang systems, like many others, have an optimistic approach: after a first two-way interaction two locations establish a mutual knowledge of their respective Inria incarnations, typically by means of a shared socket connection. From that point on, they keep using that shared connection until their view changes, rather than setting up a new connection for each message exchange. Reflecting this in our calculus plays a role in the semantics of our spawn primitive whenever the view of the locality is not in sync with the real state of the system. This in turn plays a role in our behavioral theory, as the following example illustrates.

Consider a variant servDFV of our running example where n c is linked to n i instead of n r , the network is such that the router n r is in its incarnation κ and the local view of the interface location n i contains n r → κ. The controller process running on n c is defined as follows:

C = create n r .R | spawn n i .retry
Now, servDFV is not equivalent to servD due to the fact that, in case of failure of n r , it is the controller informing the interface to restart the request and not the router n r , thus failing to update n i 's local view with the knowledge of n r 's new incarnation. A message from the interface at this point would fail as its local view contains the previous incarnation of n r . If not for the imperfect knowledge of the context, servDFV would have been equivalent to servD. In Appendix B we discuss an implementation of this system and we show that this behavior arises in reality too.

Behavioral Theory

Weak Barbed Congruence

We define a standard notion of contextual equivalence called weak barbed congruence, originally proposed in [START_REF] Milner | Barbed bisimulation[END_REF]. We denote by =⇒ the reflexive and transitive closure of the reduction relation -→ . We rely on a notion of observables on systems, called barbs, formally defined as follows:

Definition 2 (Barb). A system S exhibits a barb on channel x at location n in its incarnation λ, in symbols S↓ x@n λ , iff S ≡ ν ũ.∆ [ x ṽ .P ] n λ N , for some x, n, λ, ũ, ṽ, P, N , where x, n / ∈ ũ, and ∆ n λ : alive. Also, S⇓ x@n λ iff S ⇒ S and S ↓ x@n λ .

We now define standard properties expected for a contextual equivalence.

Definition 3 (System congruence). An equivalence relation R over closed systems is a system congruence iff, whenever ν ũ.∆ 1 N R ν ṽ.∆ 2 M , for any names w and for any configuration L such that f n(L) ∩ ũ = f n(L) ∩ ṽ = ∅, we have:

ν w.ν ũ.∆ 1 N L R ν w.ν ṽ.∆ 2 M L Definition 4 (Weak Barb-preserving relation). A relation R over closed systems is weak barb- preserving iff whenever S R R and S↓ x@n then R⇓ x@n . Definition 5 (Weak reduction-closed relation). A relation R over closed systems is weak reduction-closed iff whenever S R R and S -→ S then R =⇒ R for some R such that S R R .
Definition 6 (Weak barbed congruence). Weak barbed congruence, noted ≈, is the largest weak barb-preserving, reduction-closed, system congruence.

As a first result, we can check that structural congruence is included in weak barbed congruence: Proof. Structural congruence is a barb-preserving system-congruence by definition. The fact that structural congruence is weak reduction-closed follows from propositions 5 and 6 in Appendix E. Much as in [START_REF] De | Basic observables for a calculus for global computing[END_REF], a simpler kind of barbs gives rise to the same barbed congruence. The interested reader can find a discussion in Appendix D. We keep the more detailed observables ↓ x@n λ for convenience, to simplify certain arguments in our proofs.

Assuming ∆ n λ : alive l-in ∆ [ x(ṽ).P ] n λ x(ũ)@n λ --------→ ∆ [ P {ũ/ṽ} ] n λ l-out ∆ [ x ṽ .P ] n λ x ṽ @n λ --------→ ∆ [ P ] n λ

A Labeled Transition Semantics

In this section we present a labeled transition semantics for our calculus in order to have a coinductive characterization of weak barbed congruence. Labels α in our LTS semantics take the following forms:

α ::= τ ν w.x ũ @n λ x(ũ)@n λ kill(n, λ) create(n, λ) ⊕ n λ → m n λ → m n λ m
The first three labels are classical: silent action, output action (possibly with restricted names), and input action. Transitions relations α --→ in our LTS semantics are defined inductively by several sets of inference rules. The first set of rules, not shown here, contains the equivalent of all the local rules of the reduction relation in Figure 2, except for rule msg. Fig. 5 depicts part of the the rules for concurrent and distributed primitives. Rules l-in and l-out are as in the standard early instantation-style LTS for the π-calculus [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]. Rules which are not shown contain the equivalent of local rules in Fig. 3. Rules which are not shown are derived from Figures 2 and3 by replacing -→ by τ --→ (see Appendix A for the full list of rules). Fig. 6 depicts the rules modeling the possible interactions of a context on the public part of the network. In particular the creation of a new location (l-create-ext), the killing of a location (l-kill-ext), the linking of two locations (l-link-ext) or the unlinking of two locations (l-unlink-ext). Finally, rule l-view imposes equality of views of locations for two equivalent systems. Fig. 7 depicts composition rules for the labeled transition semantics. Rules l-parL and l-syncL have symmetric rules l-parR and l-syncR, which are not shown. Most rules are mundane, we only discuss the non standard ones. Rules l-parL is the standard rule for parallel composition allowing independent evolution of one branch of the composition. The side condition on the idle What is unusual is that there is no corresponding close rule in our LTS semantics, because rule l-res O operates at the system level, and we have no operation for composing systems. Rule l-res O is a way to signal that a system is ready to send a message at a given address, possibly bearing private names in its payload.

Inria l-create-ext ∆ N create(n,κ+1) -----------→ ∆ ⊕ (n, κ + 1) N ∆ n : dead ∆ A (n) = -κ l-kill-ext ∆ N kill(n,λ) -------→ ∆ (n, λ) N ∆ n λ : alive l-unlink-ext ∆ N n λ →m --------→ ∆ n ↔ m N ∆ n λ : alive ∆ n ↔ m l-link-ext ∆ N ⊕n λ →m --------→ ∆ ⊕ n ↔ m N ∆ n λ : alive ∆ n ↔ m l-view ∆ N n λ m ------→ ∆ N ∆ n λ : alive and (∆ A (m) = ∆n(m) = 0 or ∆n(m) = 0) Figure 6: Net Rules l-parL ∆ N α ---→ ν ũ.∆ N ũ ∩ fn(M ) = ∅ ∆ N M α ---→ ν ũ.∆ N M l-syncL ∆ N x ũ @n λ --------→ ∆ N ∆ M x(ũ)@n λ --------→ ∆ M ∆ N M τ ---→ ∆ N M l-resO S ν ṽ.x ũ @n λ -----------→ S w ∈ ũ \ ṽ, x, n ν w.S ν w.ν ṽ.x ũ @n λ -------------→ S l-res S α ---→ S u / ∈ fn(α) ν u.S α ---→ ν u.S

Full Abstraction

Before presenting the main result of the paper we introduce the definition of weak bisimilarity. Our main result states that weak bisimilarity fully characterizes weak barbed congruence.

Theorem 1 (Full Abstraction). S ≈ R iff S ≈ R.
Proof. Details of the proof can be found in Appendix E.

A few comments are in order. A consequence of our result is that the public part of the network (i.e. those nodes and links whose names are not restricted) of two weak barbed congruent systems must coincide. This is visible directly from the rules in Fig. 6. In particular, incarnation numbers of public nodes must coincide. This may seem to be overly discriminative but in fact it is warranted: recovery protocols or failure handling protocols such as SWIM [START_REF] Das | SWIM: scalable weakly-consistent infection-style process group membership protocol[END_REF], which rely on incarnation numbers, would operate differently in dissimilar systems.

Examples

Deriving Erlang's Like Constructs

This sub-section shows how to implement several Erlang primitives using the ones provided by our calculus. Let us begin with the ping definition, which is used to test for accessibility of a remote location (m) by the current one (n). If the ping succeeds the view of n is updated with the knowledge of m and vice-versa, moreover the ping evaluates to an atom pong to signal success. If it fails n removes any belief it may had about the m and evaluates to pang.

Since in our calculus we do not have atoms we encode a slight variation of the ping that branches according to the result of the test. The successful one mimics the evaluation to pong and the negative to pang. ping m.P else Q def = ν x, t, f.node(u, λ).

x f | spawn m.(spawn u.x t ) | x(y).if y = t then P else remove m.Q

Primitive monitor repeatedly tests for a remote location accessibility and continues as P when the accessibility test fails. Since the ping can nondeterministically fail at any point the monitor too can nondeterministically fail. We encode it as follows.

monitor(m).P

def = ν x.(Q |!x.Q) where Q = ping m.x else P
Primitive start creates a new location l, provided that it does not exist already. Location l is said a slave node and the creator location is said the master node. The slave dies when its master dies, hence we need a monitoring process to implement this behavior. We encode it as follows.

start(l)

Behavioral Theory In Action

We begin this section by applying our behavioral theory to the motivating example in Section 2.

Example 1 (servD and servDFR are bisimilar.). To prove servD ≈ servDFR it suffices to show a candidate bisimulation relation and then play the bisimulation game to its elements. Consider relation R = {(servD, servDFR)} ∪ S 0 ∪ S 1 ∪ S 2 where

S 0 = {(servD, R 0 ) | servDFR τ ==⇒ R 0 } S 1 = {(S 1 , R 1 ) | (S 0 , R 0 ) ∈ S 0 , S 0 req(x,y)@ni =========⇒ S 1 ∧ R 0 req(x,y)@ni =========⇒ R 1 } S 2 = {(S 2 , R 2 ) | (S 1 , R 1 ) ∈ S 1 , S 1 z w λ @ni = ======= ⇒ S 1 ∧ R 1 z w λ @ni = ======= ⇒ R 2 }
Intuitively, from an external perspective, servD only inputs the request and exhibits the answer; hence, we need to prove that servDFR is able to match those two actions. The proof is available in Appendix F. ♦

We now present two examples inspired from [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF] to show that our behavioral theory agrees with the one they present in absence of recovery.

Example 2 (Synchronous moves). This example declines [16, Example 10] into a version that can nondeterministically fail w.r.t. the original one, due to the fact that we do not have a perfect failure detector. Consider the construct move m.P else Q which attempts to migrate P to m from the current location and if it fails, launches Q locally.

Assuming ∆ (n, λ) : alive, the behavior could be defined as We now show that in our setting, as in [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF], the primitive move is not observationally equivalent to mv. To prove this we take advantage of the contextuality property of ≈ and show that

move ∆ [ move m.P else Q ] n λ → ∆ [ P ] m λ ∆n(m) = λ ∆ n λ m λ nmove ∆ [ move m.P else Q ] n λ → ∆ [ Q ] n
ν ũ.∆ [ move m.P else Q ] n λ [ unlink n ] m κ ≈ ν ũ.∆ [ mv m.P else Q ] n λ [ unlink n ] m κ where ∆ = {n → λ, m → κ}, {n ↔ m)}, {n → 0, m → 0}
The intuition is that the right-hand side system can reach a point where b.P reached successfully m while spawn u.a.(spawn m.b)) manages to go back to n and also synchronizes on a. Now, if at this point the unlink reduces we get to a point where n and m cannot synchronize on b hence the two locations are alive but both P and Q are blocked. Due to the atomicity of the move the same state cannot be achieved on the left-hand side. ♦ Example 3 (Distributed Server). Here, we rephrase [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF]Example 11], where Francalanza and Hennessy show that the behavioral theory they present is able to distinguish a distributed server only able to reach its backend by a direct connection and one that, in addition to the direct connection, has also an indirect connection that goes through a third locality. The two systems are the following. Now, servD and sFHD2Rt, like in [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF], can be distinguished by the following context

C ≡ • [ unlink n ] n [ req z, h ] n
as servD would stop working after the break reduces, while servD2Rt would keep working correctly since it could route the request through m. ♦

Related work and conclusion

We have presented in this paper a distributed π-calculus with location and link crash failures and recoveries. The calculus basic constructs, including incarnation numbers to distinguish different versions of the same location across recoveries and local imperfect knowledge, were inspired mainly by the Erlang programing language and environment. To the best of our knowledge, this is the first work that combines these different features, and the first to deal with recovery without relying on some form of checkpointing (as in Erlang-style systems).

As mentioned in the Introduction, there are only a few works in the literature proposing a process calculus analysis of distributed systems with crash failures and recoveries. We discussed the work by Berger and Honda [START_REF] Berger | The two-phase commitment protocol in an extended pi-calculus[END_REF] and by Bocchi et al. [START_REF] Bocchi | A model of actors and grey failures[END_REF] in the Introduction. The work by Fournet et al. on the join calculus [START_REF] Fournet | A calculus of mobile agents[END_REF] shows how to extend the join calculus with primitives for crash failures and recoveries but does not take into account links and link failures and does not present a behavioral theory for these extensions of the join calculus. The work by Amadio [START_REF] Amadio | An asynchronous model of locality, failure and process mobility[END_REF] on the π 1l -calculus presents an asynchronous π-calculus with unique receivers, located processes, and location failures. It develops a behavioral theory for this calculus by translation of the π 1lcalculus into the π 1 calculus (an asynchronous π-calculus with unique receivers), but it relies on perfect failure detectors, does not support links and link failures, and recovery just consists in restarting a stopped process in its exact state at the moment of failure. In its discussion of weaker failure detectors, it does indicate how an extension could support a local view (of failed locations) but it does not elaborate the corresponding calculus and behavioral theory.

Our main inspiration for this paper was the work by Francalanza and Hennessy [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF] for their handling of node and link failures, and their behavioral theory. Apart from dealing with recovery, which they do not consider, our development is markedly different from theirs. We have opted for a simpler handling of scope extrusion, with simpler labels in our LTS semantics (just names instead of complex information about the network, including links and liveness of locations), Inria and no need to make explicit the partial view of a network available to an observer. In effect, we have opted for the alternative design choice they discussed when contrasting their work to that of De Nicola et al. [START_REF] De | Basic observables for a calculus for global computing[END_REF]: keep simple labels in the LTS and opt for a classical handling of scope extrusion, possibly at the expense of larger bisimulation relations. We believe the gain in simplicity of exposition and understanding, coupled with the simple handling of recovery our approach allows, is well worth it. Also, we Introduce explicit local views, which correspond to the belief that a location has of its neighbours and their current incarnation. Our local views are handled similarly as in Erlang -in particular they may not reflect the current state of the network -, and they have no equivalent in [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF]. The notion of partial views for observers in [START_REF] Francalanza | A theory of system behaviour in the presence of node and link failure[END_REF] is different: it is a way to filter out information contained in their complex labels so as to obtain full abstraction, and it plays no role in the operational semantics of their model.

Formal models for distributed systems with failures can also be found in recent verification tools for distributed algorithms and distributed systems such as Disel [START_REF] Sergey | Programming and proving with distributed protocols[END_REF], Gobra [START_REF] Wolf | Gobra: Modular specification and verification of go programs[END_REF], Perennial [START_REF] Chajed | Verifying concurrent, crash-safe systems with perennial[END_REF], Psync [START_REF] Dragoi | Psync: a partially synchronous language for fault-tolerant distributed algorithms[END_REF], TLC [START_REF] Griffin | TLC: temporal logic of distributed components[END_REF], Verdi [START_REF] Wilcox | Verdi: a framework for implementing and formally verifying distributed systems[END_REF]. They can either rely on a specific language (such as Gobra, for Go programs), or domain specific languages for formally specifying algorithms (such as PSync or Disel), or be more general purpose, relying on a mixture of logic and more operational models (such as Perennial, Verdi or TLC). Verdi in particular is interesting for it supports a variety of failure models, including a model of crash failures and recoveries which is quite close to ours, and makes use of simulation relations in its proof techniques. However, to the best of our knowledge, they (Verdi included) do not provide as we do a compositional theory of system equivalence in presence of crash failures and recoveries.

The calculus presented in this paper provides us with a basis for further studies. It would certainly be interesting to further expand it to cater for other failure models, including the kinds of grey failures tackled by Bocchi et al. [START_REF] Bocchi | A model of actors and grey failures[END_REF], probably making it parametric in failure models along the lines of Verdi [START_REF] Wilcox | Verdi: a framework for implementing and formally verifying distributed systems[END_REF]. In its current form, we think it is close enough to the behavior of Erlang systems, and its primitives sufficient to account for a significant subset of Erlang failure handling constructs, to allow us to study reversible debugging for distributed Erlang systems with failures and recoveries, building on the substantial amount of work developed in the past ten years around reversibility and reversible debugging in Erlang [START_REF] Lanese | A theory of reversibility for Erlang[END_REF][START_REF] Lanese | Causal-consistent replay reversible semantics for message passing concurrent programs[END_REF].

A Notations and rules

For ease of reference, we gather in this section all the notations and inference rules used in the paper.

A.1 Notations

We assume given mutually disjoint infinite denumerable sets C, N and I. C is the set of channel names, N is the set of location names, and I is the set of incarnation number variables. We use the set of integers Z as the set of incarnation numbers. An incarnation number is paired with a location name for recovery purposes, to distinguish the current instance of a location from its past failed instances. We denote by N the set N ∪ { }, where ∈ N. As in the π-calculus, channel names can be free or bound in terms. The same holds for location names. Incarnation variables can be bound, but not incarnation numbers. We denote by ũ a finite (possibly empty) tuple of elements. We write T {ṽ/ũ} for the usual capture-avoiding substitution of elements of ũ by elements of ṽ in term T , assuming tuples ũ and ṽ have the same arity. We write u, ṽ or ṽ, u for the tuple ṽ extended with element u as first or last element. Abusing notation, we sometimes identify a tuple ũ with the set of its elements. We denote by N + the set of strictly positive integers (by definition 0 ∈ N + ), and by N the set of positive integers (0 ∈ N). We denote by 0 the function 0 : N → Z that maps any n ∈ N to 0 and to 1.

A.2 Calculus syntax and alpha-conversion on systems

P, Q ::= 0 x ũ .P x(ṽ).P !x(ṽ).P ν w.P if r = s then P else Q P | Q node(n, λ).P remove n.P spawn n.P kill ũ, r, s

⊂ C ∪ N ∪ I ∪ Z ṽ ⊂ C ∪ N ∪ I w ∈ C ∪ N x ∈ C n ∈ N λ ∈ I
Free names in processes and configurations are defined inductively as follows:

fn(0) = ∅ fn(x ũ .P ) = ũ ∪ {x} ∪ fn(P )
fn(x(ṽ).P ) = {x} ∪ fn(P ) \ ṽ fn(!x(ṽ).P ) = {x} ∪ fn(P ) \ ṽ fn(ν w.P ) = fn(P ) \ {w} L denotes the set of configurations. S denotes the set of systems. A network ∆ is a tuple A, L, V where:

fn(if r = s then P else Q) = fn(P ) ∪ fn(Q) ∪
• A is a function A : N → Z such that A( ) = 1 and such that the set supp(A) def = {n ∈ N | A(n) = 0} is finite. Function A records three types of information on locations. If A(n) = λ ∈ N + , then location n is alive and its current incarnation number is λ. If A(n) = -λ, λ ∈ N + then location n has been killed and its last incarnation number while alive was λ. If A(n) = 0, then there is no location n in the network, alive or not.

• L ⊆ N × N is the set of links between locations. L is a finite symmetric binary relation over location names such that dom(L)

def = {n ∈ N | ∃m, (n, m) ∈ L} is finite. • V : N → (N → N)
is a function that maps location names to their local view which is such that the set supp(V)

def = {n ∈ N | V(n) = 0} is finite and supp(V) ⊆ supp(A). The local view of a location n is a function V(n) : N → N such that the set {m ∈ N | V(n)(m) = 0} is finite. If V(n)(m) = κ ∈ N + ,
then location m in its incarnation κ is believed by n to be alive. If V(n)(m) = 0, then location n holds no belief on the status of location m.

∆ A , ∆ L , and ∆ V denote the components of a network representation ∆. Notations for extracting information from ∆:

• ∆ n λ : alive if ∆ A (n) = λ and λ ∈ N + . • ∆ n : dead if ∆ A (n) ∈ N + • ∆ n ↔ m if (n, m) ∈ ∆ L • ∆ n λ m κ if (n, m) ∈ ∆ L , ∆ n λ :
alive and ∆ m κ : alive Update operations over a network ∆:

• ∆ ⊕ n ↔ m = ∆ A , ∆ L ∪ {(n, m), (m, n)}, ∆ V • ∆ n ↔ m = ∆ A , ∆ L \ {(n, m), (m, n)}, ∆ V • ∆ ⊕ (n, λ) = ∆ A [n → λ], ∆ L ∪ {(n, n)}, ∆ V [n → 0] • ∆ (n, λ) = ∆ A [n → -λ], ∆ L , ∆ V • ∆ ⊕ n (m, λ) = ∆ A , ∆ L , ∆ V [n → ∆ V (n)[m → λ]] , if n = m • ∆ n m = ∆ A , ∆ L , ∆ V [n → ∆ V (n)[m → 0]] , if n = m • ∆ n n = ∆ ⊕ n (n, λ) = ∆
Free names of networks and systems are defined inductively as follows:

fn(∆) = supp(∆ A ) ∪ dom(∆ L ) fn(∆ N ) = fn(∆) ∪ fn(N ) fn(ν ũ.S) = fn(S) \ ũ Inria [S.Par.C] N M ≡ M N [S.Par.A] (L M ) N ≡ L (M N ) [S.Par.N] (N 0) ≡ N [S.Res.C] ν u.ν v.S ≡ ν v.ν u.S [S.Res.Nil] ν u.S ≡ S u / ∈ fn(S) [S.α] S =α R S ≡ R [S.Ctx] N ≡ M C[N ] ≡ C[M ]

A.4 LTS semantics

Labels α in our LTS semantics take the following forms:

α ::= τ ν w.x ũ @n λ x(ũ)@n λ kill(n, λ) create(n, λ) ⊕ n λ → m n λ → m n λ m
Free names in labels are defined as follows:

fn(τ ) = ∅ fn(ν w.x ũ @n λ ) = (ũ ∪ {x, n}) \ w fn(x(ũ)@n λ ) = ũ ∪ {x, n} fn(kill(n, λ)) = {n} fn(create(n, λ)) = {n} fn(⊕n λ → m) = {n, m} fn( n λ → m) = {n, m} fn(n λ m) = {n, m}
Labelled transition relations α --→ of our LTS semantics are defined by the rules in Fig. 10 and11.

Inria msg ∆ [ x ṽ .Q ] n λ [ x(ũ).P ] n λ -→ ∆ [ P {ṽ/ũ} ] n λ [ Q ] n λ bang ∆ [ !x(ũ).P ] n λ -→ ∆ [ x(ũ).(P | !x(ũ).P ) ] n λ new ∆ [ ν u.P ] n λ -→ ν u.∆ [ P ] n λ u / ∈ fn(∆) ∪ {n, λ} fork ∆ [ P | Q ] n λ -→ ∆ [ P ] n λ [ Q ] n λ if-neq ∆ [ if r = s then P else Q ] n λ -→ ∆ [ Q ] n λ r = s node ∆ [ node(m, κ).P ] n λ -→ ∆ [ P {m, κ/n, λ} ] n λ if-eq ∆ [ if r = r then P else Q ] n λ -→ ∆ [ P ] n λ remove ∆ [ remove m.P ] n λ -→ ∆ n m [ P ] n λ spawn-s ∆n(m) = κ ∆ n λ mκ ∆ [ spawn m.P ] n λ -→ ∆ ⊕ m (n, λ) [ P ] m κ link ∆ n ↔ m ∆ [ link m.P ] n λ -→ ∆ ⊕ n ↔ m [ P ] n λ spawn-f ∆n(m) = κ ∆ n λ mκ ∆ [ spawn m.P ] n λ -→ ∆ n m 0 unlink ∆ n ↔ m ∆ [ unlink m.P ] n λ -→ ∆ n λ ↔ m [ P ] n λ create-s ∆ m : dead ∆ A (m) = -κ ∆ [ create m.P ] n λ -→ ∆ ⊕ (m, κ + 1) [ P ] m κ+1 kill n = ∆ [ kill ] n λ -→ ∆ (n, λ) 0 create-f ∆ m : dead ∆ [ create m.P ] n λ -→ ∆ 0 par ∆ N -→ ν ũ.∆ N ũ ∩ fn(M ) = ∅ ∆ N M -→ ν ũ.∆ N M res S -→ S ν u.S -→ ν u.S str S ≡ S S -→ R R ≡ R S -→ R Figure 9: Reduction Rules Assuming ∆ n λ : alive l-bang ∆ [ !x(ũ).P ] n λ τ ---→ ∆ [ x(ũ).(P | !x(ũ).P ) ] n λ l-fork ∆ [ P | Q ] n λ τ ---→ ∆ [ P ] n λ [ Q ] n λ l-new u / ∈ fn(∆) ∪ {n, λ} ∆ [ ν u.P ] n λ τ ---→ ν u.∆ [ P ] n λ l-node ∆ [ node(m, κ).P ] n λ τ ---→ ∆ [ P {m, κ/n, λ} ] n λ l-if-neq r = s ∆ [ if r = s then P else Q ] n λ τ ---→ ∆ [ Q ] n λ l-remove ∆ [ remove m.P ] n λ τ ---→ ∆ n m [ P ] n λ l-if-eq ∆ [ if r = r then P else Q ] n λ τ ---→ ∆ [ P ] n λ kill n = ∆ [ kill ] n λ τ ---→ ∆ (n, λ) 0 l-in ∆ [ x(ṽ).P ] n λ x(ũ)@n λ --------→ ∆ [ P {ũ/ṽ} ] n λ l-out ∆ [ x ṽ .P ] n λ x ṽ @n λ --------→ ∆ [ P ] n λ l-spawn-s ∆n(m) = κ ∆ n λ mκ ∆ [ spawn m.P ] n λ τ ---→ ∆ ⊕ m (n, λ) [ P ] m κ l-link ∆ n ↔ m ∆ [ link m.P ] n λ τ ---→ ∆ ⊕ n ↔ m [ P ] n λ l-spawn-f ∆n(m) = κ ∆ n λ mκ ∆ [ spawn m.P ] n λ τ ---→ ∆ n m 0 l-unlink ∆ n ↔ m ∆ [ unlink m.P ] n λ τ ---→ ∆ n ↔ m [ P ] n λ l-create-s ∆ m : dead ∆ A (m) = -κ ∆ [ create m.P ] n λ τ ---→ ∆ ⊕ (m, κ + 1) [ P ] m κ+1 l-create-f ∆ m : dead ∆ [ create m.P ] n λ τ ---→ ∆ 0 Figure 10: LTS Rules (1) Inria l-create-ext ∆ n : dead ∆ A (n) = -κ ∆ N create(n,κ+1) -----------→ ∆ ⊕ (n, κ + 1) N l-kill-ext ∆ n λ : alive ∆ N kill(n,λ) -------→ ∆ (n, λ) N l-unlink-ext ∆ n λ : alive ∆ n ↔ m ∆ N n λ →m --------→ ∆ n ↔ m N l-link-ext ∆ n λ : alive ∆ n ↔ m ∆ N ⊕n λ →m --------→ ∆ ⊕ n ↔ m N l-view ∆ n λ : alive and (∆ A (m) = ∆n(m) = 0 or ∆n(m) = 0) ∆ N n λ m ------→ ∆ N l-res S α ---→ S u / ∈ fn(α) ν u.S α ---→ ν u.S l-parL ∆ N α ---→ ν ũ.∆ N ũ ∩ fn(M ) = ∅ ∆ N M α ---→ ν ũ.∆ N M l-parR ∆ N α ---→ ν ũ.∆ N ũ ∩ fn(M ) = ∅ ∆ M N α ---→ ν ũ.∆ M N l-syncL ∆ N x ũ @n λ --------→ ∆ N ∆ M x(ũ)@n λ --------→ ∆ M ∆ N M τ ---→ ∆ N M
l-resO S ν ṽ.x ũ @n λ -----------→ S w ∈ ũ \ ṽ, x, n ν w.S ν w.ν ṽ.x ṽ @n λ -------------→ ν S.

l-syncR

∆ N x ũ @n λ --------→ ∆ N ∆ M x(ũ)@n λ --------→ ∆ M ∆ M N τ ---→ ∆ M N l-α S =α T T α ---→ T T =α S S α ---→ S

B Erlang

B.1 Experiments on Erlang's Semantics

In this section we will show a typical distributed Erlang behaviors. To simulate a distributed environment Erlang nodes will be running on dockers' container connected through a network.

By using docker facilities we will simulate failure and changes in the network structure. The code of this examples can be found at [13].

Pinging a reincarnation of a previous known location

Description. In this scenario l 2 successfully contacts l 1 , thus establishing a connection. Then, l 1 fails and recovers. Finally, l 2 , before detecting that the incarnation of l 1 to which it was connected has failed, tests again its accessibility. Graphically, the network could be represented as follow.

•

l 1 • l 1
The following commands set up the configuration and attach a remote shell to l 2 .

gfa bb r et @u b un t u :~/ $ docker -compose up -d gfa bb r et @u b un t u :~/ $ docker exec -it l2 . com erl -name test@l2 . com -setcookie cookie -remsh app@l2 . com -hidden

Then, to establish a connection between the two locations in the Erlang console we can ping the remote location.

( app@l2 . com )2 > net_adm : ping ( ' app@l1 . com '). pong

To induce the fault and make it seem like a genuine interruption of services, without third parties being notified, we detach the container from all the networks, restart it, and reconnect it to the networks it was connected to. The disconnection is required as otherwise the other containers would be notified of the restart. Detaching and re-attaching the container to the network takes few milliseconds, hence not enough for the Erlang system to detect it. To do so we get the container and network ids through the docker commands and we feed them to the restart script. Finally we attempt to ping the remote location after the restarting.

... ( app@l2 . com )3 > spawn ( ' app@l1 . com ' , fun () -> self () end ). <0.107.0 > ( app@l2 . com )4 > = WARNING REPORT ==== 2 -May -2 0 2 3 : : 1 5 : 1 6 : 0 2 . 1 7 4 3 0 8 === ** Can not start erlang : apply ,[# Fun < erl_eval .43.3316493 > ,[]] on ' app@l1 . com ' **

The test for spawn failed even if there is a live running instance of l 1 . The reason why is that l 2 attempted to spawn on the instance of l 2 that it knew already (in terms of our calculus, location l 2 at incarnation λ), which was stored in its view, and not the one currently alive (location l 2 at Inria incarnation λ + 1). If we had given l 2 enough time it would have detected that the incarnation of l 2 it knew was dead since it would not feel its heartbeat and in that case the spawn would have succeeded since l 1 would have initiated a new connection.

An example of the corresponding system in our calculus is the following one:

∆ [ ping l 1 ] l2 κ [ spawn l 1 .t ] l2 κ [ kill ] l1 λ [ create l 1 .0 ] where ∆ = {l 1 → λ, l 2 → κ)}, {l 1 ↔ n 2 }, {l 2 → 0} B.

Running Example in Erlang

In this section we discuss how to reproduce the experiments showing the behaviors of the three servers presented in Section 2. Actually, for simplicity as bugged behavior we show servDFV from Section 3.4.

All the code of the examples can be found at [13] (including servDF).

We begin by servD.

The procedure to set up the three nodes is as above.

Then, we can connect to the interface.

gfabbret@ub un t u :~/ $ docker exec -it interface . com erl -name t est@in terfac e . com -setcookie cookie -remsh app@interface . com -hidden

Then, we can invoke the interface process which will send the request and observe the outcome.

( app@interface . com )1 > servD : interface ().

Initiating request Response received

As expected, everything went well. Now, let us discuss the more interesting servDFV, where the misbehavior is due to a spawn that fails because of a wrong view.

The procedure to set up the system is as before, nonetheless this time two remote consoles are required: one on the interface to start the process and one on the controller to restart the router. The commands to attach the remote consoles are as above, but for replacing the name of the container. Now, we can initiate the request from the interface.

( app@interface . com )1 > servDFV : interface ().

Initiating request

The process gets stuck because the (bugged) router drops the message. Now, we can simulate a failure of the router container by means of gfabbret@ub un t u :~/ $ ./ restart servdf_net1 router . com Then, right after, before the interface node detects the absence of the router because of the lack of its heartbeat we can restore the service from the controller console. where the spawn has failed due to wrong view. Finally, let us discuss servDFR. To set up the scenario and attach consoles to the interface and the controller we proceed as above.

Then we start the request ( app@interface . com )1 > servDFR : interface ().

Initiating request

The process gets stuck like it did in servDFV. As in servDFV we restart the router and we create a new router through the controller process. In this implementation though is the router to send a retry message to the interface, hence its view is correctly updated and the following expected behavior is shown.

Retrying request Response received ok

Inria

C Modifying networks

We formalize in this section the intuition that we can modify, in essentially arbitrary ways, the observable part of networks in our systems. To transform A into A we need to remove all the elements that are in A but not in A and we need to add all those elements that are in A but not in A. To remove the nodes it suffices to build the following context

L - A = n∈supp(A)\supp(A ) [ kill ] n λ
Then, to add the nodes it suffices to build the following context

L + A = n∈supp(A )\supp(A) [ create n.0 ]
To change L in to L we need to perform the same operations as above. To remove the links it suffices to build the following context

L - L = (n,m)∈L\L [ unlink m.0 ] n
Then, to add the links it suffices to build the following context

L + L = (n,m)∈L \L [ link m.0 ] n Finally, we obtain as L = L - A L + A L - L L +
L . Note that we did not mention incarnation numbers for new nodes in supp(A ) \ supp(A). If a particular incarnation number λ > 1 is required for location n, it suffices to repeatedly kill and (re-)create location n in L + A until the correct incarnation number is reached. In the above proposition views updates are not mentioned because there are some limits in extending them. In particular consider the network ∆

{( , 1), (n, λ), (n , λ )}, {n ↔ n }, {(n , {(n, λ o )})} (1)
where n = n , λ o < λ and the following network

∆ {( , 1), (n, λ), (n , λ )}, {n ↔ n }, {(n , {(n, λ o )}), (n, {(n , λ )})} (2)
Then ∆ cannot be modified by context into ∆ . The problem lies in the fact that any primitive that adds a location to another location's view requires for the remote location to be in its view. In the above example, n view is not aligned with the reality, since n believes to be connected to (n, λ o ) while (n, λ o ) is dead and now (n, λ), a newer incarnation, is up and running.

D Barb alternative

This section shows that it is possible to simplify our notion of barb, a result akin to that put forward by De Nicola et al. in [START_REF] De | Basic observables for a calculus for global computing[END_REF]. The alternate definition of barb we consider in this section is one where a barb just displays the location of messages.

Definition 8 (Location Barb). We say that a system S exhibits a barb at location n, in symbols S↓ n , iff S ≡ ν ũ.∆ [ x ṽ .P ] n λ N , for some x, n, λ, ũ, ṽ, P, N , where x, n / ∈ ũ, and ∆ (n, λ) : alive. Also, S⇓ n if S ⇒ S and S ↓ n . We denote by ≈l the weak barbed congruence obtained by considering only barbs at locations. Now the two weak barbed congruences ≈ and ≈l coincide

Proposition 3. ≈l = ≈ Proof.
In what follows we use the following notation : if U ≡ ν ũ.∆ N , and L is such that fn(L) ∩ ũ = ∅, then U L denotes the system ν ũ.∆ N L.

That ≈ ⊆ ≈l is clear. We show the converse. Let closed systems S and T be such that S ≈l T and S↓ x@n λ . By definition of full barbs, we have S ≡ ν ũ.∆ [ x ṽ .P ] n λ N for some x, n, λ, ũ, ṽ, P, N . By definition of location barbs, we have S↓ n . Since S ≈l T , we must have T =⇒ T 1 ↓ n for some T 1 . Assume for the sake of contradiction that ¬(T ⇓ x@n λ ), and consider the systems S L and T L, where:

L = [ create k.link n.spawn n.(x(ỹ).spawn k.t) ] 1 k, t / ∈ fn(S) ∪ fn(T )
Since ≈l is a system congruence, we must have S L ≈l T L. Now, by construction, we have

S L =⇒ ν ũ.∆ N [ t ] k 1
and S↓ k But since ¬(T ⇓ x@n λ ), and t, k are fresh for T , there can be no T such that T L =⇒ T and T ⇓ k , contradicting the fact that S ≈l T .

Inria

E Full Abstraction

E.1 Soundness

Definition 9 (Strong Simulation). A binary relation S ⊆ S × S over closed systems is a strong simulation iff whenever (P, Q) ∈ S,

• P α --→ P implies Q α --→ Q for some Q with (P , Q ) ∈ S
Definition 10 (Strong Bisimulation). A relation S is a strong bisimulation if both S and S -1 are strong simulations.

Definition 11 (Strong Bisimilarity). Strong bisimilarity, denoted by ∼, is the largest srong bisimulation over systems.

The fact ∼ is an equivalence relation is a standard result for any labelled transition system. We start with a simple lemma on the preservation of free names by labelled transitions. If α is a label from our LTS semantics, we define pi(α) and po(α) as follows:

po(α) = ũ \ w if α = ν w.x ũ @n λ ∅ otherwise pi(α) = ũ if α = x(ũ)@n λ ∅ otherwise Lemma 1. Let S, S be closed systems such that S α --→ S . Then fn(S ) ⊆ fn(S) ∪ pi(α).
Proof. By induction on the derivation of S α --→ S .

We now prove two lemmas relating labelled transitions in the calculus LTS semantics and the structure of systems. In the remainder, we extend ≡ to output actions, and identify equivalent output actions, setting:

ν v.ν w.x ũ @n λ ≡ ν w.ν v.x ũ @n λ ν w.α ≡ ν w.ω if α ≡ ω
Lemma 2 (Input/output actions and systems). Let S, S be closed systems such that S α --→ S . The following properties hold:

1. if α = ν ṽ.x ũ @n λ then S ≡ ν w.∆ [ x ũ .P ] n λ
N for some ∆, w, P, N with x, n / ∈ w, ṽ ⊆ w, ∆ n λ : alive

2. if α = x(ũ)@n λ then S ≡ ν w.∆ [ x(ũ).P ] n λ
N for some ∆, ṽ, w, P, N with ũ, x, n ∩ w = ∅, ∆ n λ : alive

Proof. We show the first assertion, the second one is handled similarly. We reason by induction on the derivation of S α --→ S , where α = ν ṽ.x ũ @n λ , considering the last rule used in the proof tree:

• Rule l-out: in this case, we have S = ∆ [ x ũ .P ] n λ , ∆ n λ : alive, as required.

• Rule l-parL: in this case, we have S = ∆ N M , α = x ũ @n λ , with ∆ N

RR n°9511

• Rule l-parR: same as l-parL.

• Rule l-res: in this case we have S = ν z.S with S α --→ S , for some S , S , and v / ∈ fn(α). By induction assumption, we have S ≡ ν w.∆ [ x s .P ]

n λ N , with ∆ n λ : alive, x, n / ∈ w, ṽ ⊆ w. Thus S ≡ ν z, w.∆ [ x s .P ] n λ
N , with ∆ n λ : alive, and x, n / ∈ v, w, ṽ ⊆ z, w as required.

• Rule l-resO: in this case, we have S = ν z.T with T ω --→ T , z ∈ ũ \ x, n, α = ν z.ω. By induction assumption, we have

T ≡ ν w.∆ [ x r .P ] n λ
N for some ∆, ũ, w, P, N with x, n / ∈ w, ṽ\{z} ⊆ w, ∆ n λ : alive Hence, we have

S ≡ ν z, w.∆ [ x r .P ] n λ
N for some ∆, ũ, w, P, N with x, n / ∈ z, w, ṽ ⊆ z, w, ∆ n λ : alive as required.

Lemma 3 (Silent actions and systems). Let S, S be closed systems such that S τ --→ S . Then one of the following properties hold, for some ũ, w, u, n, m, λ, P, Q, N with ∆ (n, λ) : alive:

S ≡ ν w.∆ [ !x(ũ).P ] n λ N (3)
S ≡ ν w.∆ [ ν u.P ] n λ N (4)
S ≡ ν w.∆ [ if r = s then P else Q ] n λ N (5)
S ≡ ν w.∆ [ P | Q ] n λ N (6)
S ≡ ν w.∆ [ x ũ .P ] n λ [ x(ũ).Q ] n λ N (13)
Proof. We reason by induction on the derivation of S τ --→ S , considering the last rule used in the derivation.

• Rule l-res: In this case, we have S = ν u.T and S = ν u.T , with T τ --→ T . Applying the induction assumption, we have T ≡ ν w.∆ L N , where L is one of the located processes listed in the lemma assertions ([ !x(ũ).P ] n λ , [ ν u.P ] n λ , etc.). Hence S ≡ ν u, w.∆ L N , as required.

• Rule l-syncL: In this case, we have

S = ∆ N M with ∆ N x ũ @n λ -------→ ∆ N and ∆ M x(ũ)@n λ -------→ ∆ M . Applying Lemma2 we have N ≡ [ x ũ .P ] n λ
U for some P, U with ∆ n λ : alive, and

M ≡ [ x(ũ).Q ] n λ V for some Q, V . Hence we have S ≡ ∆ [ x ũ .P ] n λ [ x(ũ).Q ] n λ
U V , one of the possible forms required.

• Rule l-syncR is handled similarly as rule l-syncL.

Inria

• Rule l-parL: In this case we have S = ∆ N M , with ∆ N τ --→ ν ũ.∆ N , and fn(M ) ∩ ũ = ∅. By induction assumption, we have N ≡ L U , where L is one of the located processes listed in the lemma assertions. Hence S ≡ ∆ L U M , as required.

• Rule l-parR is handled similarly as rule l-parL.

• Rules with τ --→ conclusion in Fig. 10: All these rules conclusion are of the form ∆ L τ --→ U , where L is one of the single located processes listed in the lemma assertions. In these cases, we just have S = ∆ L, as required.

Proposition 4 (Structural congruence is a strong bisimulation). We have ≡ ⊆ ∼.

Proof. Since ≡ is an equivalence relations, it suffices to prove that ≡ is a strong simulation, namely that for any closed systems S, R, if S α --→ S and S ≡ R, then there exists R such that R α --→ R and S ≡ R . We reason by induction on the derivation of S ≡ R, considering the last rule used in the proof tree: Rule s.res.c: In this case, S = ν u.ν v.T and R = ν v.ν u.T . Since S α --→ S , this can only have been obtained by applying rule l-res twice, rule l-resO twice, or a or a combination of rule l-res and rule l-rresO. We consider the four cases: Rule l-res followed by rule l-resO: Similar to the previous case.

Rule s.res.nil: In this case, S = ν u.R, u / ∈ fn(R). Since S α --→ S , this can only have been obtained by applying rule ress as the last rule. Hence, we have R

ω --→ R , S = ν u.R , α = ω{ * /u}, u ∈ fn(ω) \ po(ω). Now by Lemma 1, we have fn(R ) ⊆ fn(R) ∪ pi(ω). Since po(ω) ⊆ fn(R) and u ∈ fn(R), then u / ∈ po(ω), hence α = ω. In addition, since u / ∈ fn(ω), then u / ∈ pi(ω), hence u / ∈ fn(R ).
We can then apply rule s.res.nil to get S ≡ R , as required.

Case inferred by

if-neq Then S is ∆ [ if u = v.P else Q ] n ,

RR n°9511

Case l-syncR: In this case, we have S = ∆ N L, ∆ N x(ũ)@n λ -------→ ∆ N , ∆ L x ũ @n λ -------→ ∆ L , and S = ∆ N L , corresponding to assertion 4.

Case l-res: In this case, we have S = ν a.T , S = ν a.T , T τ --→ T . By induction hypothesis, we have for T one of the four cases 1 to 4 in the lemma. We consider only the cases l-parL and l-syncL, the other ones are handled similarly. If a ∈ ũ, then applying l-resO, we get ν a.ν s.∆ N ν a, w.x ũ @n λ -----------→ ν r.∆ N , with ũ ∩ r = ∅ and r = a, s \ a, w, as required. If a / ∈ ũ, then applying l-res we get ν a.ν s.∆ N ν w.x ũ @n λ ----------→ ν a.ν r.∆ N , with ũ ∩ a, r = ∅ and a, r = a, s \ w, as required.

Case α = ν w.x ũ @n λ : handled by induction on the derivation of S α --→ S with cases similar to the cases τ .l-parL, τ .l-parR and τ .l-res above.

Case α = x(ũ)@n λ : handled by induction on the derivation of S α --→ S with cases similar to the cases τ .l-parL, τ .l-parR and τ .l-res above.

Proposition 7 (Weak System Congruence). Weak bisimilarity is a weak system congruence; that is, if ν ũ.∆ N ≈ ν ṽ.∆ M then for all w, L, with fn(L) ∩ ũ, ṽ = ∅, we have ν w.ν ũ.∆ N L ≈ ν w.ν ṽ.∆ M L Proof. We prove that the relation

S def = { ν w.ν s.∆ S N S L, ν w.ν r.∆ R N R L | ν s.∆ S N S ≈ ν r.∆ R N R fn(L) ∩ (s ∪ r) = ∅ }
S = ν s.∆ S N S ν a.x ũ @n λ ---------→ ν z s .∆ S N S = S ∆ S L x(ũ)@n λ -------→ ∆ S L z s = s \ ã ũ ∩ zs = ∅ U = ν s.∆ S N S L Inria Since S ≈ R, we have R ν ã.x ũ @n λ =========⇒ ν w r .ν z r .∆ R N R = R for some wr , ∆ R , N R , with z r = r \ ã, and R ≈ S . Now, since R τ ==⇒ R 1 x ũ @n λ -------→ R 2 τ ==⇒ R , where R 1 = ν w 1 .ν z r .∆ 1 R N 1 R for some ∆ 1 R , N 1 R
, we are guaranteed that n λ is alive, and that ∆ 1 R L

x(ũ)@n λ -------→ ∆ 1 R L . Also, we have ũ ∩ z r = ∅. By repeated applications of rule l-parL and by one application of rule l-syncL, we obtain R L τ ==⇒ V , with V = ν w r .ν r.∆ R N R L and with fn(L ) ∩ w r = ∅ because of the conditions of rule l-parL. Summing up, we have:

U = ν ã.ν z s .∆ S N S L = ν ã.S V ≡ ν ã.ν w r .ν z r .∆ R N R L = ν ã.R S ≈ R fn(L ) ⊆ fn(L) ∪ ũ \ ã by Lemma 1 fn(L ) ∩ w r ũ ∩ z s = ũ ∩ z r = ∅
Hence we have fn(L ) ∩ z s = ∅ and fn(L ) ∩ ( w r ∪ z r ) = ∅, and S = ν z s .∆ S N S ≈ ν wr .ν z r .∆ R N R = R , which means that U, V ∈ S, as required. Case l-syncR Similar to the case l-syncL, but simpler. Case l-parL In this case, we have

S L τ --→ U , with S L = ∆ S N S L, U = ν s.∆ S N S L, S τ --→ ν s.∆ S N S , with fn(L) ∩ s = ∅. Since S ≈ R, we have R τ ==⇒ R with R ≈ S and R = ν r.∆ R N R . Now applying repeatedly rule l-parL, we get R L τ ==⇒ ν r.∆ R N R L = V , with fn(L) ∩ r = ∅ because
of the conditions of rules l-parL. Now we have U, V ∈ S, as required. Case l-parR Similar to the case l-parL, but simpler.

Case x(ũ)@n λ We consider the different cases listed in Lemma 4 for S L = ν s.∆ S N S L and S L x(ũ)@n λ -------→ U :

Case l-parL In that case, we have S = ν s.∆ S N S , S

x(ũ)@n λ -------→ S S = ν s.∆ S N S . Since S ≈ R, we have R x(ũ)@n λ = ====== ⇒ R , where R = ν z.ν r.∆ R N R . Now, by repeated application of rule l-parL, we get R L x(ũ)@n λ = ====== ⇒ ν w.ν r.∆ R N R L = V ,
with fn(L) ∩ ν z. = ∅ because of the conditions of rule l-parL. Since we also have fn(L) ∩ r = ∅ by definition, we have U, V ∈ S, as required. Case l-parR Similar to the case l-parL, but simpler. Case ν ã.x ũ @n λ We consider the different cases listed in Lemma 4 for

S L = ν s.∆ S N S L and S L ν ã.x ũ @n λ ---------→ U : Case l-parL In that case, we have S = ν s.∆ S N S , S ν ã.x ũ @n λ ---------→ S S = ν s a .∆ S N S , U = ν sa ∆ S . N S L, s a = s \ ã. Since S ≈ R, we have R ν ã.x ũ @n λ =========⇒ R , where R ≡ ν w.ν r a .∆ R N R , r a =
--→ ν w.V or R L ν w.α -----→ V .
In both cases, we have U, V ∈ S and ν w.U, ν w.V ∈ S (S is closed under restriction by construction), as required.

Proposition 8 (Soudness of weak bisimilarity). Weak bisimilarity is sound with respect to weak barbed congruence, i.e. ≈ ⊆ ≈.

Proof. Weak bisimilarity is weak barb-preserving thanks to Lemma 2. It is weak reduction-closed thanks to Proposition 6. It is a system congruence thanks to Proposition 7. Thus ≈ ⊆ ≈ by definition of weak barbed congruence as the largest of weak barb-preserving, reduction-closed, system congruence.

E.2 Completeness

In the remainder of this section, we use the following notation: if S = ν s.∆ N is a closed system, we write S M for the system ν s.∆N M provided fn(M ) ∩ s = ∅.

Lemma 5 (Inducing Network Changes).

• Suppose ∆ (n, λ) : alive --→ U l as a premise, with T l = ν x, l.U l , x, n / ∈ fn(α), and that for any such transition we have S α --→ T .

-S kill(n,λ) ------→ S implies S [ kill ] n λ -→ S -S [ kill ] n λ -→ S , where S ≡ ν ũ.∆ N , ∆ (n, λ) : alive implies S kill(n,λ) ------→ S • Suppose ∆ (n, λ) : alive -S create(n,λ) --------→ S implies S [ create n.P ) ] m κ -→ S [ P ] n λ -S [ create n.P ] m κ -→ S [ P ] n λ , where S ≡ ν ũ.∆ N , ∆ n λ : alive implies S create(n,λ) --------→ S • Suppose S = ν ũ∆.N and ∆ n ↔ m -S n λ →m -------→ S , where S ≡ ν ũ.∆ N implies S [ unlink m.P ] n λ -→ S [ P ]
Proposition 10. If we have S l [ x ] l λ ≈ R l [ x ] l λ with x, l fresh for S, R then S ≈ R. Proof. If S l [ x ] l λ ≈ R l [ x ]
l λ then by system congruence we also have Proof. To prove the statement it suffices to show that ≈ ∪ ≈ is a bisimulation up-to ≡. Take S ≈ R and suppose that S α --→ S ; we reason by case analysis on α.

ν x, l.S l [ x ] l λ ≈ ν x, l.R l [ x ]
• Case α = τ . Thanks to Proposition 5 and Proposition 6, the thesis follow by the reduction closure property.

• Case α = x ũ @n λ . Consider the context

L = [ x(ỹ).if ỹ = ũ then create l.(f ail | f ail.succ) ] n λ
with l, succ and f ail fresh and the reduction S L =⇒ T 1 , where T 1 ≡ S l [ succ ] l . Now, since S ≈ R, T 1 ↓ succ@l and T 1 ↓ f ail@l , we must have a transition R L =⇒ T 2 s.t. T 2 ↓ succ@l and T 2 ↓ f ail@l . We remark here that we have T 2 ↓ succ@l , with a strong barb, because the only way for R L to make disappear ↓ f ail@l is to have consumed it on the fresh location l, thereby showing ↓ succ@l .

The only way to obtain this is if R

x ũ @n λ = ====== ⇒ R , hence T 2 ≡ R l [ succ ] l . Now, since (S l [ succ ] l , R l [ succ ] l ) ∈ ≈,
by Proposition 10 we have (S , R ) ∈ ≈ as required.

• Case α = x(ũ)@n λ . Consider the context

L = [ x ũ .create l.(f ail | f ail.succ) ] n λ
with l, f ail, succ fresh and the reduction S L =⇒ T 1 , where T 1 ≡ S l [ succ ] l . Now, since S ≈ R, T 1 ↓ succ@l and T 1 ↓ f ail@l , we must have a transition R L =⇒ T 2 s.t. T 2 ↓ succ@l and T 2 ↓ f ail@l . The only way to obtain this is if R [ succ ] l . Now, since S ≈ R, T 1 ↓ succ@l and T 1 ↓ f ail@l , we must have a transition R L =⇒ T 2 s.t. T 2 ↓ succ@l and T 2 ↓ f ail@l . The only way to obtain this is

x(ũ)@n λ = ====== ⇒ R , hence T 2 ≡ R l [ succ ] l . Now, since (S l [ succ ] l , R l [ succ ] l ) ∈ ≈,
if R =⇒ R 1 [ link m.create l.(f ail | f ail.succ) ] n λ -→ R 1 [ create l.(f ail | f ail.succ) ] n =⇒ T 2 , where T 2 ≡ R l [ succ ] l .
Then, by Lemma 5 we know that R with l, f ail, succ 1 and succ 2 fresh. Now, since S ≈ R their public network must agree on aliveness of localities, links, and views. There are two cases to be considered: when the link n ↔ m is alive is S and when it is not. [ succ 1 ] l . Now, since S ≈ R and T 1 ↓ succ1@l and T 1 ↓ f ail@l we have a matching transition R L =⇒ T 2 s.t. T 2 ↓ succ1@l and T ↓ f ail@l . Hence we have T [ succ 2 ] l . Now, since S ≈ R and T 1 ↓ succ2@l and T 1 ↓ f ail@l we have a matching transition R L =⇒ T 2 s.t. T 2 ↓ succ2@l and T ↓ f ail@l . Hence we have

τ ==⇒ R i n λ →m -------→ R j τ ==⇒ R . Now, since (S l [ succ ] l , R l [ succ ] l ) ∈ ≈,

F Bisimulation Of Running Example

In this section we show that a bisimulation relating the example without failure and the example with recovery. We recall briefly the two systems. Now we analyze the moves of the various pairs to show that indeed R is a bisimulation.

• Pair (servD, servDFR). Now we proceed by case analysis on the possible transitions.

-Case x(y, z)@n i . * Case servD

x(y,z)@ni --------→ T 1 . Consider transition Case τ Here, any possible τ transition can be matched by the other system by doing nothing.

Case z w @n i Here there is only one possible system S that can perform the step z w @n i , that is

ν ũ.∆ [ z w ] n1
Now, there are an unbounded number of different system R 1 that can match the move, according to the state of the recovery. We only show the following example. Consider system

  nc where: K = req(y, z).((spawn n r .r 1 y, c ) | c(w).z w | retry.spawn n r .r 1 y, c )

  be the empty configuration 0, a located process [ P ] n λ or a parallel composition of configurations N M . A located process [ P ]

[

  S.Par.C] N M ≡ M N [S.Par.A] (L M ) N ≡ L (M N ) [S.Par.N] (N 0) ≡ N [S.Res.C] ν u.ν v.S ≡ ν v.ν u.S [S.Res.Nil]

Figure 2 :

 2 Figure 2: Local Rules

Figure 3 :

 3 Figure 3: Distributed Rules

Figure 5 :

 5 Figure 5: Concurrent and distributed Rules

  Output and input action mention the name and incarnation of the location performing the action. Labels kill(n, λ) and create(n, λ) indicate respectively the killing and activation of location n in incarnation λ. Labels ⊕n λ → m and n λ → m signal respectively the creation and destruction of a link between n and m, initiated by n at incarnation λ. Finally, n λ m signals that location n at incarnation λ holds the correct belief about location m. The transition relation labeled by α is denoted α --→ . We denote by τ ==⇒ the reflexive and transitive closure of τ --→ . For α = τ , we denote by α ==⇒ the relation τ ==⇒ α --→ τ ==⇒ .

Figure 7 :

 7 Figure 7: Composition Rules

Definition 7 (

 7 Weak Bisimilarity). A binary relation over closed systems S ⊆ S 2 is a weak simulation iff whenever (S, R) ∈ S and S α --→ S , then R α ==⇒ R for some R with (S , R ) ∈ S. A binary relation S over closed systems is a weak bisimulation if both S and S -1 are weak simulations. Weak bisimilarity, denoted by ≈, is the largest weak bisimulation.

  def = node(u, λ).create l.(monitor(u).kill) Primitive stop halts the execution of node m. We encode it as follows. stop(m) def = spawn m.kill Primitive disconnect removes m from the view of n and vice-versa. We encode it as follows. disconnect(m).P def = node(u, λ).remove m.(spawn m.(remove u)) Inria

λ

  Now one could try to implement the move primitive through the following macro mv m.P else Q def = ν a, b.node(u, λ).(spawn m.(b.P | spawn u.a.(spawn m.b)) | a | monitor a m.Q)The above code sends b.P to the target location and then goes back to signal the successful arrive of b.P , by synchronizing on the private channel a and eventually goes back to release P . The implementation uses mutual exclusion on a together with the macro monitor a m.Q, which is a slight variation of the one in Section 5.1. This macro acquires the resource a before testing and releases it after the success of the test whereas it releases Q if n is not accessible. It can be encoded as monitor a m.Q def = ν test.(test |!test.a.ping m.(test | a) else Q)

  servFHD ⇐ ν data, w y .∆ [ req(x, y).spawn n .data x, y ] n [ data(x, y).spawn n.x w y ] n sFHD2Rt ⇐ ν data, w y .∆ data sync, x | spawn n .spawn n .data sync, x | sync(x).y x , y). spawn n .x f (y) | spawn n .spawn n.x w y n

  create n.P link n.P unlink n.P L, M, N ::= 0 [ P ] ::= ∆ N | ν w.S where:

  {r, s} fn(P | Q) = fn(P ) ∪ fn(Q) fn(node(n, λ).P ) = fn(P ) \ {n} fn(remove n.P ) = fn(P ) ∪ {n} fn(spawn n.P ) = fn(P ) ∪ {n} fn(kill) = ∅ fn(create n.P ) = fn(P ) ∪ {n} fn(link n) = fn(unlink n) = {n} fn([ P ] n λ ) = fn(P ) ∪ {n} fn(N M ) = fn(N ) ∪ fn(M ) RR n°9511

Figure 8 :

 8 Figure 8: Structural Congruence Rules

Figure 11 :

 11 Figure 11: LTS Rules (2)

(

  app@controller . com )1 > servDFV : controller (). ok and observe the following behavior on the interface = WARNING REPORT ==== 3 -May -2 0 2 3 : : 0 9 : 0 6 : 3 3 . 4 4 1 4 0 2 === ** Can not start erlang : apply ,[# Fun < servDF .1.93666681 > ,[]] on ' app@router . com ' **

Proposition 2 .

 2 Consider a system S = ν ũ.∆ N , where ∆ = A, L, V , a set of live locations A , such that ∀n ∈ supp(A)\supp(A ), n / ∈ ũ and a set of live links L s.t. ∀n, m, (n, m) ∈ L\L =⇒ n, m / ∈ ũ. Let ∆ = A , L , V , then, there exists a configuration L with f n(L) ∩ ũ = ∅ such that ν ũ.∆ N L =⇒ ν ũ.∆ N Proof. Assume to have ν ũ.∆ N , where ∆ = A, L, V , A and L .

α

  --→ ∆ N . By induction assumption, we have N ≡ [ x ũ .P ] n λ L for some L, with ∆ n λ : alive. Hence S ≡ ∆ [ x ũ .P ]

  n λ L M , ∆ n λ : alive, as required.

SSSSSS

  ≡ ν w.∆ [ node(m, κ).P ] ≡ ν w.∆ [ remove n.P ] ≡ ν w.∆ [ spawn m.P ] ≡ ν w.∆ [ create m.P ] ≡ ν w.∆ [ link m.P ] ≡ ν w.∆ [ unlink m.P ] n λ N

  Rule l-res applied twice: In this case, we have T ω --→ T , for some T , u, v / ∈ fn(α), ω = α, and S = ν u.ν v.T . Now applying rule l-res twice we get R α --→ ν v.ν u.T . Applying rule l-res twice, we get R ≡ S , as required. Rule l-resO applied twice: In this case, we have T ω --→ T for some T , v ∈ πω, u ∈ πω \ {v}, α = ν u.ν v.ω, and S = T . Applying rule l-resO twice we get: R α --→ T , hence we have R ≡ S , as required. Rule l-resO followed by rule l-res: In this case we have T ω --→ T for some T , v ∈ πω, u ∈ πω \ {v}, α = ν v.ω, and S = ν u.T . Applying rule l-resO we get: ν u.T ω --→ ν u.T . Applying l-resO we get: R = ν v.ν u.T α --→ ν u.T = R . Hence we have R ≡ S , as required.

  Rule s.α: In this case S = α R. By rule l-α we get directly R α --→ S . Hence we have found R = S , as required. Rule s.ctx: In this case, we have S = ν ũ.∆ L N and R = ν ũ.∆ L M with N ≡ M . We reason by induction on the structure of ũ: ũ = ∅: In this case, S α --→ S can only have been derived by an application of rule l-parL, rule l-parR, rule l-syncR, or rule l-syncL. We consider the four cases: Rule l-resO: In this case, we have T ω --→ T , v ∈ πω, α = ν v.ω, S = T . By the induction hypothesis, we have U ω --→ U for some U ≡ T . By rule l-resO we get R α --→ U = R . hence we have R ≡ S , as required. Proposition 5. If S -→ S then S τ --→ ≡ S . Proof. We proceed by induction on the inference S -→ S . Case inferred by if-eq Then S is ∆ [ if u = u.P else Q ] n λ , and the transition S τ --→ S follows by l-if-eq.

  where u = v, and the transition S τ --→ S follows by l-if-neq. Case inferred by bang Then S is ∆ [ !x(ũ.P ) ] n λ , and the transition S τ --→ S follows by l-bang. Case inferred by node Then S is ∆ [ node(m, κ).P ] n , and the transition S τ --→ S follows by l-node. Case inferred by msg Then S is ∆ [ x y ]

  S follows by l-out, l-in, and l-syncL. Case inferred by new Then S is ∆ [ ν x.P ] n λ , and the transition S τ --→ S follows by l-new. Case inferred by spawn-s Then S is ∆ [ spawn n.P ] n , and the transition S τ --→ S follows by l-spawn-s. Case inferred by spawn-f Then S is ∆ [ spawn n.P ] n , and the transition S τ --→ S follows by l-spawn-f. Case inferred by unlink Then S is ∆ [ unlink m.P ] n λ , and the transition S τ --→ S follows by l-break. Case inferred by link Then S is ∆ [ link m.P ] n λ , and the transition S τ --→ S follows by l-link. Case inferred by kill Then S is ∆ [ kill ] n λ , and the transition S τ --→ S follows by l-kill. Case inferred by remove Then S is ∆ [ remove m.P ] n λ , and the transition S τ --→ S follows by l-remove. Case inferred by create-s Then S is ∆ [ create m.P ] n λ , and the transition S τ --→ S follows by l-create-s. Case inferred by create-f Then S is ∆ [ create m.P ] n λ , and the transition S τ --→ S follows by l-create-f. Case inferred by par Then S is ν ũ.∆ N M , and the transition S τ --→ S follows by l-parL and the inductive hypothesis. Case inferred by res Then S is ν u.∆ N , and the transition S τ --→ S follows by l-ress and the inductive hypothesis.

Lemma 4 .

 4 Let S = ν s.∆ N L be a closed system. If S α --→ S , where α is a silent action, an output action or an input action, then one of the following assertions holds: 1. α = τ , ν s.∆ N τ --→ ν w.ν s.∆ N , and S ≡ ν w.ν s.∆ N L, with fn(L) ∩ w = ∅, and with rule l-parL the last rule used in the derivation of S α --→ S before possible applications of rule l-res.

2 .

 2 α = τ , ν s.∆ L τ --→ ν w.ν s.∆ L , and S ≡ ν w.ν s.∆ N L , with fn(N ) ∩ w = ∅, and with rule l-parR the last rule used in the derivation of S α --→ S before possible applications of rules l-res.

3 .

 3 α = τ , ν s.∆ N ν w.x ũ @n λ ----------→ ν r.∆ N , r = s\ w and ũ∩ r = ∅, ∆ L x(ũ)@n λ -------→ ∆ L ,and S ≡ ν s.∆ N L , with rule l-syncL the last rule used in the derivation of S α --→ S before possible applications of rules l-res.

  4. α = τ , ∆ N x(ũ)@n λ -------→ ∆ N , ν s.∆ L ν w.x ũ @n λ ----------→ ν r.∆ L , r = s \w and ũ∩ r = ∅, and S ≡ ν w.ν s.∆ N L , with rule l-syncR the last rule used in the derivation of S α --→ S before possible applications of rules l-res.

5 .

 5 α = ν w.x ũ@n λ , ν s.∆ N ν w.x ũ @n λ ----------→ ν r.∆ N , r = s \ w, ũ ∩ r = ∅, and S ≡ ν s.∆ NL with rule l-parL the last rule used in the derivation of S α --→ S before possible applications of rules l-res or l-resO.6. α = ν w.x ũ@n λ , ν s.∆ L ν w.x ũ @n λ ----------→ ν r.∆ L , r = s \ w, ũ ∩ r = ∅, and S ≡ ν s.∆ N L with rule l-parR the last rule used in the derivation of S α --→ S before possible applications of rules l-res or l-resO.

7 .

 7 α = x(ũ)@n λ , ν s.∆ N x(ũ)@n λ -------→ ν s.∆ N , S ≡ ν s.∆ N L, and ũ ∩ s = ∅, with rule l-parL the last rule used in the derivation of S α --→ S before possible applications of rule l-res.8. α = x(ũ)@n λ , ν s.∆ L x(ũ)@n λ -------→ ν s.∆ L , S ≡ ν s.∆ N L ,and ũ ∩ s = ∅, with rule l-parR the last rule used in the derivation of S α --→ S before possible applications of rule l-res. Proof. By case analysis on α. Case α = τ : in this case we reason by induction on the derivation of S τ --→ S , considering the last rule used in the proof tree: Case l-parL: In this case, we have S = ∆ N L, ∆ N τ --→ ν w.∆ N , and S = ∆ N τ --→ ν w.∆ N L, with fn(L) ∩ w = ∅, corresponding to assertion 1. Case l-parR: In this case, we have S ≡ ∆ N L, ∆ L τ --→ ν w.∆ L , and S = ∆ N τ --→ ν w.∆ N L , with fn(N ) ∩ w = ∅, corresponding to assertion 2. Case l-syncL: In this case, we have S = ∆ N L, ∆ N x ũ @n λ -------→ ∆ N , ∆ L x(ũ)@n λ -------→ ∆ L , and S = ∆ N L , corresponding to assertion 3.

  Rule l-parL: In this case we have T = ν s.∆ N L, T ≡ ν w.ν s.∆ N L, ν s.∆ N τ --→ ν w.ν s.∆ N , with fn(L) ∩ w = ∅. Applying rule l-res, we get S ≡ ν a.ν r.ν s.∆ N L ≡ ν a.ν r.ν s.∆ N L, ν a.ν s.∆ N τ --→ ν w.ν a.ν s.∆ N , with fn(L) ∩ w = ∅, corresponding to assertion 1. Rule l-syncL: In this case we have T= ν s.∆ N L, T ≡ ν s.∆ N L , ν s.∆ N ν w.x ũ @n λ ----------→ ν r.∆ N , ∆ L x(ũ)@n λ -------→ ∆ L ,with r = s\ w and ũ∩r = ∅. Applying rule l-res, we get S = ν w.ν s.∆ N L τ --→ ν w.ν s.∆ N L = S .

  is a weak bisimulation up to ≡. Since S is symmetric, it suffices to prove that S is a weak bisimulation up to ≡. DefineS = ν s.∆ S N S R = ν r.∆ R N R S L = ν w.ν s.∆ S N S L R L = ν w.ν r.∆ R N R Land consider a transition S L α --→ U . We proceed by induction on the structure of w: Case w = ∅: We proceed by case analysis on α: Case τ We consider the different cases listed in Lemma 4 for S L = ν s.∆ S N S L and S L τ --→ U : Case l-syncL In this case, we have:

  r \ ã, and S ≈ R . Now, by repeated application of rule l-parL, we get R L ν ã.x ũ @n λ =========⇒ ν z.ν r a .∆ R N R L = V , with fn(L) ∩ ν z. = ∅ because of the conditions of rule l-parL. Since we also have fn(L) ∩ r = ∅ by definition, we have U, V ∈ S, as required. Case l-parR Similar to the case l-parL, but simpler. Case create(n, λ) Easy since S L and S have the same network. Case kill(n, λ) Easy since S L and S have the same network. Case ⊕n → m Easy since S L and S have the same network. Case n → m Easy since S L and S have the same network. Case n m Easy since S L and S have the same network. Case w = w, z: Let ν w., ν z.S, ν w., ν z.R ∈ S. Then we have by construction ν z.S, ν z.R ∈ S. By induction hypothesis, if ν z.S α --→ U , then ν z.R α --→ V for some V with U, V ∈ S. Now using rule l-res or rule l-resO, we obtain either S L α --→ ν w.U or S L ν w. ν w.α -----→ U , which are matched respectively by R L α

-Proposition 9 .

 9 S [ unlink m.P ] n λ -→ S [ P ] n , where S ≡ ν ũ.∆ N , ∆ n ↔ m implies S n λ →m -------→ S • Suppose S = ν ũ∆.N and ∆ n ↔ m -S ⊕n λ →m -------→ S , where S ≡ ν ũ.∆ N implies S [ link m.P ] n λ -→ S [ P ] n λ Inria A Behavioral Theory For Crash Failures and Erlang-style Recoveries In Distributed Systems 45 -S [ link m.P ] n λ -→ S [ P ] n λ , where S ≡ ν ũ.∆ N , ∆ n ↔ m implies S ⊕n λ →m -------→ S Proof. The first clause for the action kill(n, λ) is proved by induction on the derivation S = ν ũ.∆ N kill(n,λ) ------→ ν ũ.∆ N = S . The second clause uses induction on the derivation of ν ũ.∆ N [ kill ] n λ -→ ν ũ.∆ N . The proof for the other clauses is similar. Given a system S ≡ ν ũ.∆ N and l s.t. l / ∈ f n(S) ∪ bn(S) we define S l as ν ũ.∆ ⊕ (l, 1) N . If S is a closed system and l, x / ∈ fn(S) then ν x, l.S l [ x ] l λ ∼ S. Proof. A direct proof that R = { ν x, l.S l [ x ] l λ , S | S ∈ S closed, x, l / ∈ fn(S)} is a strong bisimulation, noting that any transition ν x, l.S l [ x ] l λ α --→ T l must have been obtained by a derivation with S l α

  Proposition 9, Proposition 8, and transitivity of ≈ we have S ≈ R as required. Theorem 2 (Completeness of ≈ w.r.t. ≈). If S ≈ R then S ≈ R.

  by Proposition 10 we have (S , R ) ∈ ≈ as required. • Case α = ⊕n λ → m. By Lemma 5 we know that [ link m.P ] n λ induces the desired labeled action. Consider the context L = [ link m.create l.(f ail | f ail.succ) ] n λ with l, f ail, succ fresh and the reduction S L =⇒ T 1 , where T 1 ≡ S l

1 τ

 1 by Proposition 10 we have (S , R ) ∈ ≈ as required.• Case α = n λ → m. Consider the contextL = [ unlink m.create l.(f ail | f ail.succ) ] n λwith l, succ and f ail fresh. The reasoning is similar to above.• Case α = kill(n, λ). By Lemma 5 we know that [ kill ] n λ is the process that induces the reduction we are looking for. Consider the contextL = [ f ail ] n λ [ kill ] n λwith f ail fresh and reduction S L =⇒ T 1 . Now, since S ≈ R and T 1 ↓ f ail@n there is a matching move R L =⇒ T 2 s.t. T 2 ↓ f ail . Since f ail is fresh the only way to haveT 2 ↓ f ail@n is to have R L =⇒ R 1 [ f ail ] ==⇒ R . Now, we know that T 1 ≈ T 2 , where T 1 ≡ S [ f ail ] n λ and T 2 ≡ R [ f ail ] n λ . We know S [ f ail ] n λ ∼ S since n λ is not alive in S hence S [ f ail ]n λ ≈ S and by transitivity of ≈ we get S ≈ R [ f ail ] n λ . By using a similar reasoning we get (S , R ) ∈ ≈ as required. • Case α = create(n, λ). Consider the context L = [ create n.(create l.(f ail | f ail.succ)) ] with l, f ail and succ fresh; the reasoning is similar to above. • Case α = n λ m. Consider the context L = ν x. x | x.link m.(spawn m.(unlink n.create l.(f ail | f ail.succ 1 )) | x.spawn m.(create l.(f ail | f ail.succ 2 )) n λ

InriaA-

  Behavioral Theory For Crash Failures and Erlang-style Recoveries In Distributed Systems 47 Case n ↔ m. Consider the transition S L =⇒ T 1 ≡ ν x.S l [ x.spawnm.createl.f ail | f ail.succ ] n λ

  2 ≡ ν x.R l [ x.spawn m.create l.f ail | f ail.succ ] n λ [ succ 1 ] l (x is fresh in R). This is possible only if R n λ m = ===== ⇒ R . Now, ν x.S l [ x.spawn m.create l.f ail | f ail.succ ] n λ [ succ 1 ] l ∼ S l [ succ 1 ] l , because x / ∈ f n(S). By using a similar reasoning for T 2 and transitivity of ≈ we have(S l [ succ 1 ] l λ , R l [ succ 1 ] l λ ) ∈ ≈.Finally by Proposition 10 we have (S , R ) ∈ ≈ as required. -Case n ↔ m. Consider the transition S L =⇒ T 1 ≡ S l [ x.linkm.(spawnm.(unlinkn.createl.(f ail | f ail.succ 1 )) ] n λ

T 2 ≡

 2 R l [ x.link m.(spawn m.(unlink n.create l.(f ail | f ail.succ 1 )) ] n λ [ succ 2 ]l . Thisis possible only if R n λ m = ===== ⇒ R . Now, ν x.S l [ succ 2 ] l [ x.link m.(spawn m.(unlink n.create l.(f ail | f ail.succ 1 )) ] n λ ∼ S l [ succ 2 ] l , because x / ∈ f n(S).By using a similar reasoning for T 2 and transitivity of ≈ we have(S l [ succ 2 ] l , R l [ succ 2 ] l ) ∈ ≈.Finally by Proposition 10 we have (S , R ) ∈ ≈ as required.

C==⇒ R 0 }S 1 = 1 }S 2 =

 0112 servD = ν n r , n b , r 1 , r 2 , b.∆ [ I ] ni [ R ] nr [ B ] n b servDFR = ν n r , n b , n c , r 1 ,r 2 , b, c, retry. ∆ [ = ν c.(c |!c.(create n r .(R | spawn n i .retry) | c) I = req(y, z).spawn n r .r 1 y, z R = (r 1 (y, z).spawn n b .b y, z ) | (r 2 (y, z).spawn n i .z y ) B = b(y, z).spawn n r .r 2 z, w y K = req(y, z).((spawn n r .r 1 y, c ) | c(w).z w | retry.spawn n r .r 1 y, c ) Proposition 11. servD ≈ servDFR Proof. In the following, for simplicity reasons, we will omit in the action label the incarnation number of the location doing the action. Consider relation R = {(servD, servDFR)} ∪ S 0 ∪ S 1 ∪ S 2 whereS 0 = {(servD, R 0 ) | servDFR τ {(S 1 , R 1 ) | (S 0 , R 0 ) ∈ S 0 , S 0 req(x,y)@ni =========⇒ S 1 ∧ R 0 req(x,y)@ni =========⇒ R {(S 2 , R 2 ) | (S 1 , R 1 ) ∈ S 1 , S 1 z w @n1 = ====== ⇒ S 1 ∧ R 1 z w @n1 = ====== ⇒ R 2 }

[

  servD x(y,z)@ni --------→ T 1 ≡ ν n r , n b , r 1 , r 2 , b.∆ [ spawnn r .r 1 y, z ]The move can then be matched byservDFR x(y,z)@ni = ======= ⇒ T 2 ≡ ν n r , n b , n c , r 1 , r 2 , b, c, retry. ∆ [ (spawn n r .r 1 y, c ) | c(w).z w | retry.spawn n r .r 1 y, c ] nc and (T 1 , T 2 ) ∈ R.Inria A Behavioral Theory For Crash Failures and Erlang-style Recoveries In Distributed Systems 49 * Case servDFR x(y,z)@ni --------→ T 1 . Similar to above. -Case τ . * Consider transition servDFR τ --→ T 1 ≡ ν n b , n r , b, s, retry, n c , c.∆ [ c |!c.(create n r .(R | spawn n i .retry) | c) ] nc Then, the move can be matched by the other system by doing nothing, indeed (servD, T 1 ) ∈ R * Consider transition servDFR τ --→ T 1 ≡ ν n r , n b , a, b, s, retry, n c .∆ -(n b , λ b ) move can be matched by the other system by doing nothing, indeed (servD, T 1 ) ∈ R • Pairs (S 1 , R 1 ) ∈ S 1

R 1 ≡In R 1 [ r 1 [[ r 2 [[ r 2

 11122 ν n r , n b , n c , r 1 , r 2 , b, c, retry.∆ [ c(w).z w ] ni [ retry.spawn n r .r 1 y, c ] ni [ retry | R ] the failure has occurred (we omit dead locations) and the recovery process has RR n°9511 started already. By doing the following steps R can match the move. [ c(w).z w ] ni [ retry.spawn n r .r 1 y, c ]ν ũ.∆ [ c(w).z w ] ni [ spawn n r .r 1 y, c ] (y, z).spawn n b .b y, z ] nr [ r 2 (y, z).spawn n i .z y ] spawn n b .b y, c ] nr [ r 2 (y, z).spawn n i .z y ] ν ũ.∆ [ c(w).z w ] ni [ b y, c ] n b [ r 2 (y, z).spawn n i .z y ] ν ũ.∆ [ c(w).z w ] ni [ b y, c ] n b [ r 2 (y, z).spawn n i .z y ] nr [ kill ] nr [ b(y, z).(!B | spawn n r .r 2 z, w y ) ] ν ũ.∆ [ c(w).z w ] ni [ r 2 (y, z).spawn n i .z y ] nr [ kill ] nr [ !B | spawn n r .r 2 c, w y ) ] (y, z).spawn n i .z y ] spawn n r .r 2 c, w y ] (y, z).spawn n i .z y ] nc ) with (T 1 , T 2 ) ∈ R • Pairs S 2 × R 2Case τ Here there exist infinite R 2 that can perform a τ (the controller still attempting to recreate the location), anyway all the moves can matched by S 2 by doing nothing.InriaRESEARCH CENTRE GRENOBLE -RHÔNE-ALPESInovallée 655 avenue de l'Europe Montbonnot 38334 Saint Ismier Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

RR n°9511

To define alpha-conversion on systems, we define capture-avoiding substitution on networks. A capture avoiding substitution {v/u} on network ∆ is defined as follows: if ∆ = (A, L, V), then ∆{v/u} = (A{v/u}, L{v/u}, V{v/u}) where:

The effect of a capture avoiding substitution {v/u} on a system ∆ N is defined inductively as follows. We define the set occ of name occurrences of a system as follows:

Equality modulo alpha-conversion = α on systems is now defined as the smallest equivalence relation on systems defined by the following rules:

A.3 Reduction semantics

The operational semantics of our calculus is defined via a reduction semantics given by a binary relation -→ ⊆ S × S between closed systems, and a structural congruence relation ≡ ⊆ S 2 ∪ L 2 , that is a binary equivalence relation between systems and between configurations. Evaluation contexts are "systems with a hole •" defined by the following grammar:

Relation ≡ is the smallest equivalence relation defined by the rules in Fig. 8, where = α stands for equality up to alpha-conversion, M, N, L ∈ L, and S, R ∈ S.

Reduction relation -→ is defined by the rules in Fig. 9, where:

Rule l-parL: In this case, we have ∆ L α --→ ν ṽ.∆ L with ṽ ∩ fn(N ), and S = ν ṽ.∆ L N . Applying rule l-parL we get R α --→ ν ṽ.∆ L N = R , and by applying rule S.ctx we have R ≡ S , as required. Rule l-parR: In this case we have ∆ N α --→ ν ṽ.∆ N . We reason according to the last rule used to derive N ≡ M : Rule s.par.n: In this case, we have N = (M 0). Now, ∆ N α --→ ν ṽ.∆ N can only have been obtained via an application of rule l-parL, with ∆ M α --→ ν ṽ.∆ M , and N = M 0. But then applying l-parR we get: R α --→ ν ṽ.∆ L M = R . Since N ≡ M by rule s.par.n, we have by rule s.ctx S ≡ R , as required. Rule s.par.c: In this case, we have N = U

V and M = V U . Now the derivation ∆ N α --→ ν ṽ.∆ N can only have been obtained by the application of one of the rules l-parL, l-parR, l-syncL or l-syncR. We consider the different cases. Rule l-parL: In this case we have

Since we have S = ν ṽ.∆ L (U V ), and by rule s.par.c V U ≡ U V , and since ≡ is a congruence, we have by rule s.ctx S ≡ R , as required. The case of rule l-parR is handled similarly. Rule l-syncL: In this case, we have

where ω is an output action and ω is the matching input action. But then we can apply rule l-syncR to obtain ∆ M τ --→ ∆ M where M = V U , and then apply rule l-parR to get

U by rule s.par.c, and since ≡ is a congruence, we obtain by rule s.ctx S ≡ R , as required. The case of rule l-syncR is handled similarly. Rule s.par.a: this case is handled similarly to the case of rule s.par.c above. Case l-syncL Then S is ∆ N 1 N 2 , and we have

Now, by Lemma 2 we know the following:

Applying msg and str, we get S ≡ -→ S .

Case l-syncR Similar to case l-syncL.

Case l-parL Then S is ∆ N 1 N 2 , S is ν ṽ.∆ N 1 N 2 , where ∆ N 1 τ --→ ν ṽ.∆ N 1 , and ṽ ∩ fn(N 2 ) = ∅. Now, by using the inductive hypothesis and par we have ∆ N 1 N 2 -→ ν ṽ.∆ N 1 N 2 .

Case l-parR Similar to case l-parL.

Case l-res Then S is ν u.T , S is ν u.T , where T τ --→ T . Now by using the inductive hypothesis and res we get S = ν u.T -→ ν u.T = S .

Inria