Michel Raynal

Julien Stainer

Round-based Synchrony Weakened by Message Adversaries vs Asynchrony Enriched with Failure Detectors

Keywords: Asynchronous system, Distributed computability, Failure detector, Fair link, Message adversary, Message-passing model, Model equivalence, Ω, Process crash, Quorum, Read/write model, Round, Σ, Simulation, Source, Synchronous system, Task, Tournament, Wait-freedom

A message adversary is a daemon that suppresses messages in round-based message-passing synchronous systems in which no process crashes. A property imposed on a message adversary defines a subset of messages that cannot be eliminated by the adversary. It has recently been shown that when a message adversary is constrained by a property denoted TOUR (for tournament), the corresponding synchronous system and the asynchronous crash-prone read/write system have the same computability power for task solvability.

This paper introduces new message adversary properties (denoted SOURCE and QUORUM), and shows that the synchronous round-based systems whose adversaries are constrained by these properties are characterizations of classical asynchronous crashprone systems (1) whose communication is through atomic read/write registers or point-to-point message-passing, and (2) enriched with failure detectors such as Ω and Σ. Hence these properties characterize maximal adversaries, in the sense that they define strongest message adversaries equating classical asynchronous crash-prone systems. They consequently provide strong relations linking round-based synchrony weakened by message adversaries with asynchrony enriched with failure detectors. This not only enriches our understanding of the synchrony/asynchrony duality, but also allows for the establishment of a meaningful hierarchy of property-constrained message adversaries.

Systèmes synchrones affaiblis par des suppresseurs de messages vs systèmes asynchrones renforcés par des détecteurs de fautes Résumé : Un suppresseur de messages est une entité qui retire des messages dans un système synchrone à passage de messages dans lequel aucune défaillance ne survient. Les propriétés contraignant les suppresseurs de messages définissent les sous-ensembles de messages pouvant être retirés. Il a été récemment prouvé qu'un système synchrone dans lequel le suppresseur de messages est contraint par une propriété notée TOUR (pour tournoi) a la même puissance de calcul vis-à-vis des tâches qu'un système asynchrone sujet à des défaillances dans lequel les processus partagent de la mémoire.

Ce rapport introduit de nouvelles propriétés pour contraindre les suppresseurs de messages (notées SOURCE et QUORUM), et montre que les systèmes asynchrones dans lesquels les suppresseurs de messages suivent ces propriétés sont des caractérisations des systèmes asynchrones (1) communicant par mémoire partagée ou par passage de message, (2) enrichis avec des detecteurs de fautes tels que Σ ou Ω. Ces propriétés enrichissent notre compréhension de la dualité synchrone/asynchrone mais permettent également l'établissement d'une hiérarchie au sein des propriétés caractérisant les suppresseurs de messages.

Mots clés : systèmes asynchrones, calculabilité distribuée, détecteur de fautes, lien équitable, suppresseur de messages, modèle à passage de messages, équivalence de modèles, Ω, défaillances, quorum, mémoire partagée, ronde, Σ, simulation, source, système synchrone, tâche, tournoi, sans attente

Introduction

Message adversaries for synchronous message-passing systems In a round-based message-passing synchronous system, processes communicate by exchanging messages at every round, and the synchrony assumption provided by the model guarantees that the messages sent at the beginning a round are received by their destination processes by the end of the corresponding round. Assuming that no process is faulty, the notion of a message adversary has been introduced in [START_REF] Santoro | Time is not a healer[END_REF] (where it is called mobile transmission failures) to model messages losses and study their impact on the computability power of synchronous systems [START_REF] Santoro | Time is not a healer[END_REF][START_REF] Santoro | Agreement in synchronous networks with ubiquitous faults[END_REF].

Interestingly, the notion of constraining message deliveries has also been investigated in asynchronous systems, under distinct names, and in different contexts. As an example, asynchronous message patterns which allow failure detectors to be implemented despite asynchrony have been investigated in [START_REF] Anta | From an asynchronous intermittent rotating star to an eventual leader[END_REF][START_REF] Mourgaya | Asynchronous implementation of failure detectors[END_REF]. The view of failure detectors as being schedulers which encapsulate fairness assumptions can also be related to this approach [START_REF] Cornejo | Failure Detectors as Schedulers (Brief Announcement)[END_REF][START_REF] Pike | Failure detectors encapsulate fairness[END_REF]. Recently, assumptions on message deliveries and message exchange patterns have been used to define new asynchronous computation models and study their computability power [START_REF] Charron-Bost | The heard-of model: computing in distributed systems with benign faults[END_REF][START_REF] Kuhn | Distributed computation in dynamic networks[END_REF][START_REF] Rajsbaum | The iterated restricted immediate snapshot model[END_REF][START_REF] Schmid | Impossibility results and lower bounds for consensus under link failures[END_REF]. The general idea, which underlies these works, consists in capturing the "weakest pattern of information exchange" that allows a family of problems to be solved despite failures.

Notation The notation SMP n [adv : AD] is used to denote a round-based synchronous system made up of n reliable sequential processes whose communications are under the control of the adversary AD. While, in every round, each process sends a message to each other process, the power of the adversary AD consists in suppressing some of these messages (which are consequently never received).

According to their power, several classes of adversaries can be defined. SMP n [adv : ∅] denotes a synchronous system in which the adversary has no power (it can suppress no message), while SMP n [adv : ∞] denotes the synchronous system in which the adversary can suppress all messages. It is easy to see that, from a message adversary and computability point of view, SMP n [adv : ∅] is the most powerful crash-free synchronous system, while SMP n [adv : ∞] is the weakest. More generally, the weaker the message adversary AD, the more powerful the system.

Asynchrony from synchrony Informally, a task is a one-shot distributed computing problem where each process has a private input, and each process has to compute a local output such that each output may depend on the whole vector of input values (this vector -initially unknown to each process -contains the input values of all the processes). The most famous and studied task is the consensus task.

Afek and Gafni addressed recently task solvability in synchronous message-passing systems weakened by message adversaries [START_REF] Afek | Asynchrony from synchrony[END_REF]. Let ARW n,n-1 [fd : ∅] denote the asynchronous read/write model where up to (n -1) processes may crash ("f d : ∅" stands for "no failure detector", see below; this is the classical read/write wait-free model [START_REF] Herlihy | Wait-free synchronization[END_REF]). Afek and Gafni's main results are the following ones.

• Their first result concerns the adversary TOUR (for tournament) whose behavior is the following one. For each pair of processes p i and p j , and in each synchronous round, TOUR is allowed to suppress either the message sent by p i to p j or the message sent by p j to p i , but not both. The important result attached to TOUR is that SMP n [adv : TOUR] and ARW n,n-1 [fd : ∅] have the same computability power for read/write wait-free solvable tasks. • In addition to TOUR, two more adversaries, denoted TP and PAIRS, are described and it is shown that the three adversarybased synchronous models SMP n [adv : TOUR], SMP n [adv : TP], and SMP n [adv : PAIRS] are equivalent for task solvability. Moreover, SMP n [adv : PAIRS] is used to show that, from a topology point of view, the protocol complex of PAIRS is a subdivided complex. This means that the message adversary PAIRS (and consequently also TOUR and TP) captures, in a very simple way, Herlihy and Shavit's condition equating the read/write wait-free model with a complex subdivision [START_REF] Herlihy | The topological structure of asynchronous computability[END_REF].

Failure detectors for asynchronous crash-prone systems Informally, a failure detector is a device that provides each process p i with information on failures [START_REF] Chandra | Unreliable failure detectors for reliable distributed systems[END_REF]. According to the quality and the type of information they provide, several classes of failure detectors can be defined (see [START_REF] Raynal | Failure detectors for asynchronous distributed systems: an introduction[END_REF] for an introductory survey). The failure detectors denoted Ω and Σ are among the most important failure detectors. This is due to the following reasons: (1) Ω is the weakest failure detector that allows consensus to be solved in ARW n,n-1 [fd : ∅] [4, 14]; (2) Σ is the weakest failure detector that allows an atomic register to be implemented on top of AMP n,n-1 [fd : ∅] [START_REF] Delporte-Gallet | Tight failure detection bounds on atomic object implementations[END_REF], where AMP n,n-1 [fd : ∅] denotes the classical asynchronous message-passing system where up to (n-1) processes may crash and every message is eventually received. "Weakest" means that any failure detector that allows to solve consensus (resp., implement a register) provides at least as much information on failures as the one provided by Ω (resp., Σ). Finally, the pair (Σ, Ω) is the weakest failure detector that allows consensus to be solved in AMP n,n-1 [fd : ∅] [START_REF] Chandra | The weakest failure detector for solving consensus[END_REF][START_REF] Delporte-Gallet | Tight failure detection bounds on atomic object implementations[END_REF].

Let FD denote a failure detector. ARW n,n-1 [fd : FD] denotes the asynchronous read/write model where up to (n-1) processes may crash, enriched with FD. Similarly, AMP n,n-1 [fd : FD] denotes AMP n,n-1 [fd : ∅] enriched with FD.

Content of the paper Following Afek and Gafni's seminal approach, the aim of this paper is to better understand and extend the message adversary approach, and capture its relations with asynchrony restricted by failure detectors. Considering the round-based synchronous message-passing model with reliable processes (SMP n [adv : ∅]) as core model, it has the following contributions, which concern (1) the crash-prone asynchronous read/write model, and (2) the crash-prone message-passing model, both enriched with failure detectors. Its contributions are described in the hierarchy depicted in Figure 1. A ≃ M B means that the computing model A can be simulated in the model B and vice-versa. A ≃ T B means that any task that can be solved in the model A, can be solved in the model B and vice-versa. An arrow from A to B means that the model A is stronger than the model B, but not vice-versa. These arrows follow from known results (e.g., ARW n,n-1 [fd : Ω] is stronger than both ARW n,n-1 [fd : ∅] and AMP n,n-1 [fd : Ω]). Let us observe that, as they are failure-free, the system models SMP n [adv : ∅], ARW n,0 [fd : ∅], and AMP n,0 [fd : ∅], are computationally equivalent (first line of the figure). [START_REF] Afek | Asynchrony from synchrony[END_REF] Section 5 Said differently, when considering tasks solvability in crash-prone asynchronous systems enriched with Ω, what allows going from "message-passing" communication to "read/write" communication is characterized by the property TOUR from a message adversary point of view in a synchronous system (vertical arrow on the right of Figure 1). As just indicated, the paper provides message adversary-based characterizations of failure detectors for both read/write and message-passing crash-prone asynchronous systems. The aim of these results is to enrich our understanding of both message adversaries used to weaken communication in synchronous systems and failure detectors used to enrich asynchronous crash-prone systems. They complement the results of [START_REF] Afek | Asynchrony from synchrony[END_REF] and exhibit strong intimate relations linking synchrony, message losses, and roundbased model, on the one side, with asynchrony, process crashes, and failure detectors, on the other side. Interestingly, this seems to show that SMP n [adv : ∅] (the base reliable synchronous round-based model) and the notion of a message adversary are central in the quest for a Grand Unified model of distributed computing.

SMP n [adv : ∅] ≃ M AMP n,0 [fd : ∅] ≃ M ARW n,0 [fd : ∅] SMP n [adv : ∞] ≃ T AMP n,n-1 [fd : ∅] Section 6 Section 3 Section 2 Section 4 SMP n [adv : SOURCE] ≃ T AMP n,n-1 [fd : Ω] SMP n [adv : QUORUM] ≃ T AMP n,n-1 [fd : Σ] SMP n [adv : SOURCE, QUORUM] ≃ T AMP n,n-1 [fd : Σ, Ω] SMP n [adv : SOURCE, TOUR] ≃ T ARW n,n-1 [fd : Ω] SMP n [adv : TOUR] ≃ T ARW n,n-1 [fd : ∅]

Roadmap

The paper is composed of 7 sections. Section 2 presents base models, message adversaries, and failure detectors. Section 3 introduces the property SOURCE on message deliveries, and show that it characterizes the failure detector Ω in read/write systems. Section 4 shows that, taken alone, the property SOURCE characterizes the failure detector Ω in asynchronous messagepassing systems. Section 5 and Section 6 introduce the property QUORUM and show that it characterizes the failure detector Σ. Finally, Section 7 concludes the paper.

2 Models, Adversaries, Failure Detectors, Tasks

Base computation models

The base computation models relevant to this paper have been presented in the introduction. They are (1) the reliable round-based synchronous model SMP n [adv : ∅] possibly weakened with a message adversary AD, and (b) the crash-prone asynchronous models ARW n,n-1 [fd : ∅] (read/write wait-free model [START_REF] Herlihy | Wait-free synchronization[END_REF]) and AMP n,n-1 [fd : ∅], both possibly enriched with a failure detector FD.

Message Adversary, Message Graphs, and Dynamic Graphs in Synchronous Systems

Message adversary Given a run of a synchronous system, a message adversary suppresses messages sent by processes. A property associated with a message adversary restricts its power by specifying messages which cannot be suppressed. A message adversary is consequently defined by a set of properties which constrain its behavior.

Message graphs associated with each round of a synchronous system Given a message adversary AD, and a round r of a run of a synchronous system, let G r be the directed graph (as defined in [START_REF] Afek | Asynchrony from synchrony[END_REF]), whose vertices are the process identities, and such that there is an edge from i to j iff the adversary AD does not suppress the message sent by p i to p j at round r. We consider the following definition associated with each graph G r .

• i r -→ j means that the directed edge (i, j) belongs to G r (at round r, the message from p i to p j is not removed by the adversary).

The property TOUR As indicated in the introduction, the property TOUR [START_REF] Afek | Asynchrony from synchrony[END_REF] restricts the behavior of a message adversary as follows. For any r, and any pair of processes (p i , p j ), G r contains the directed edge (i, j) or the directed edge (j, i) or both. This means that, at every round, the adversary cannot suppress both the messages sent to each other by two processes. Hence, the graphs G r associated with the rounds r of a run in SMP n [adv : TOUR] are such that:

∀r ≥ 1 : ∀ (i, j) : (i r -→ j) ∨ (j r -→ i).
Strongly/weakly correct processes in a synchronous run The aim of this section is to introduce the notion of a strongly correct process which captures the processes whose an infinite number of messages are received (directly or indirectly) by any other process [START_REF] Raynal | Increasing the power of the iterated immediate snapshot model with failure detectors[END_REF]. Such a notion is defined as follows.

• i ≥r j means that there is a directed path starting from p i and leading to p j in a dynamically defined sequence of message graphs starting at a round ≥ r. More formally,

∃k ≥ 0, ∃r 1 < • • • < r k , ∃λ 0 , λ 1 , . . . , λ k ∈ {1, . . . , n} : (r 1 ≥ r) ∧ (λ 0 = i ∧ λ k = j) ∧ (∀m ∈ {1, . . . , k} : λ m-1 rm -→ λ m ).
• i ∞ j def = ∀r > 0 : i ≥r j . Hence, i ∞ j means that, whatever r, there is eventually a directed path starting at p i at a round ≥ r and finishing at p j in the dynamically defined sequence of message graphs.

• (i ∞ j) ⇔ (i ∞ j ∧ j ∞ i).
Assuming each process always receive its own messages, this relation is reflexive, symmetric, and transitive. Hence, it is an equivalence relation.

Collection des Publications Internes de l'Irisa c IRISA

• Let G be the graph whose vertices are {1, ..., n} and directed edges are defined by the relation ∞ ; let SC(G) be the graph of its strongly connected components. If SC(G) has a single vertex X with no input edge, the processes in X are called strongly correct processes, while the processes in {1, ..., n} \ X are called weakly correct. If X is not unique, all processes are weakly correct.

Let SC denote the (possibly empty) set of strongly correct processes in a synchronous round-based system under the control of a message adversary.

Failure Detectors in Asynchronous Systems

While a message adversary weakens a synchronous round-based system (made up of reliable processes) by suppressing messages, a failure detector enriches an asynchronous system where no message is lost but where processes may suffer crash failures. Informally, a failure detector is a device that provides each process p i with a read-only local variable xx i containing (possibly unreliable) information on process crashes [START_REF] Chandra | Unreliable failure detectors for reliable distributed systems[END_REF]. This paper considers two failure detectors. Let τ denote any time instant; xx τ i denotes the value of xx i at time τ . This time notion, which is used in the definition of a failure detector, is not accessible to the processes. The identity of a process p i is i. Given a run, a process that crashes is said to be faulty in that run, otherwise it is correct. Let C denote the sets of identities of the correct processes.

• Ω is called an eventual leader failure detector [START_REF] Chandra | The weakest failure detector for solving consensus[END_REF]. In the system models ARW n,n-1

[fd : Ω] or AMP n,n-1 [fd : Ω],
each process p i is endowed with a local variable xx i = leader i that always contains a (possibly changing) process identity. Moreover, there is an unknown but finite time τ and a process identity ℓ ∈ C such that ∀τ ′ ≥ τ :

(i ∈ C) ⇒ (leader τ ′ i = ℓ).
• Σ is called a quorum failure detector [START_REF] Delporte-Gallet | Tight failure detection bounds on atomic object implementations[END_REF]. In the system model AMP n,n-1 [fd : Σ], each process p i is endowed with a local variable xx i = qr i that always contains a non-empty set of process identities and is such that (1) ∀τ, τ ′ , ∀i, j: qr τ i ∩ qr τ ′ j = ∅ (intersection property), and (2) ∀i ∈ C : ∃τ : ∀τ ′ ≥ τ : qr τ ′ i ⊆ C (liveness property).

Tasks

A task is a one-shot computation problem specified in terms of an input/output relation ∆. Each process starts with a private input value and must eventually computes a private output value. From an external observer point of view, an input vector I[1.

.n] specifies the input value I[i] = v i of each process p i . Similarly, an output vector O[1.

.n] specifies a result value O[j] for each process p j . A task is defined by a set of input vectors and a relation ∆ which describes which output vectors are correct for each input vector I. More precisely, for each valid input vector I, the values computed by the processes must be such that there is an output vector O ∈ ∆(I) such that, for each j, O[j] is the value computed by p j ; moreover, if no value is computed by p j , it is because p j has crashed during the computation. (A formal introduction to tasks can be found in [START_REF] Herlihy | The topological structure of asynchronous computability[END_REF].)

Theorem 1 A task T can be solved in SMP n [adv : ∞] iff it can be solved in AMP n,n-1 [fd : ∅].
Proof Let us observe that if T can be solved in SMP n [adv : ∞], it is a purely local task (each process can compute its result from its own input only [START_REF] Delporte-Gallet | The minimum information about failures for solving non-local tasks in message-passing systems[END_REF] 2 ). It is possible to simulate on AMP n,n-1 [fd : ∅] an algorithm A solving a task T in SMP n [adv : ∞], by sending no message. It follows that each process in AMP n,n-1 [fd : ∅] which computes a result behaves as in SMP n [adv : ∞] when the adversary removes all messages. As at least the correct processes of AMP n,n-1 [fd : ∅] computes a result, it follows that the task T is solved in

AMP n,n-1 [fd : ∅].
If T can be solved in AMP n,n-1 [fd : ∅], it can be solved if all except one process crashed initially. From a process point of view, this cannot be distinguished from the case where messages are arbitrarily delayed. It follows from this observation and the fact that a process has to eventually computes a result that T can be solved without communication. Hence, it can be solved in

SMP n [adv : ∞]. ✷ T heorem 1 3 SOURCE + TOUR is a Characterization of Ω in ARW n,n-1 [fd : ∅]
This section shows that the computing models SMP n [adv : SOURCE, TOUR] and ARW n,n-1 [fd : Ω] have the same computational power for tasks.

initialization:

(1) r i ← 0;

(2) ls_state i ← initial state of the local simulated algorithm;

(3) msgs_to_send i [1.

.n] ← initial messages to send to each process; (4) ∀r > 0 :

MEM [i][r][1..n] init to [⊥, ..., ⊥]. repeat forever (5) r i ← r i + 1; (6) repeat leader_val i ← MEM [leader i ][r i ][i] (7) until (leader_val i = ⊥) ∨ (leader i = i) (8) end repeat; (9) MEM [i][r i ] ← msgs_to_send i ; (10) rec_msgs i [1..n] ← MEM [1..n][r i ][i]; (11) (msgs_to_send i , ls_state i ) ← simulate(ls_state i , rec_msgs i ) end repeat.

The Property SOURCE

This property is defined as follows:

∃s ∈ {1, . . . , n} :

∃r 0 ≥ 1 : ∀r ≥ r 0 : ∀ i ∈ {1, . . . , n} : (s r -→ i).
This statement means that, in each run of SMP n [adv : SOURCE], there are a process p s and a round r 0 , such that, at every round r ≥ r 0 , the adversary does not suppress the message sent by p s to the other processes.

From ARW

n,n-1 [fd : Ω] to SMP n [adv : SOURCE, TOUR]
This section presents a simulation of SMP n [adv : SOURCE, TOUR] on top of ARW n,n-1 [fd : Ω] such that, any task that can be solved in

ARW n,n-1 [fd : Ω] can be solved in SMP n [adv : SOURCE, TOUR].
Global and local variables of the simulation The simulation uses a shared variable

MEM [1..n][1..][1..n] where MEM [i][r][j]
is an atomic read/write register written by p i and read by p j . This register contains the message sent by p i to p j in round r of the simulation of SMP n [adv : SOURCE, TOUR]; ⊥ is a default value used to indicate that no message has yet been written or the corresponding message has been suppressed by the adversary. The local variable r i simulates the current round number of SMP n [adv : SOURCE, TOUR], while ls_state i represents the local simulation state. The local variable msgs_to_send i [1..n] contains the messages that p i will send to each other process during the next simulated round (msgs_to_send i [j] contains the message for p j ). leader i is the read-only local variable containing the current local output of Ω.

The simulation is locally defined by the function simulate() which takes as input parameters the current local state of the simulation and the messages received from the other processes at the current round. It modifies accordingly the local simulation state and computes the messages that will be sent to the other processes during the next round.

The simulation algorithm The local simulation algorithm is described in Figure 2. The local simulator of process p i first proceeds to the next round (line 5) and waits until its current leader has sent it a message (MEM

[leader i ][r i ][i] = ⊥)
or it is its own leader (lines 6-8). When this occurs, the simulator writes in MEM [i][r i ] the messages sent by p i at the current round (line 9). Then, p i consumes messages (line 10), and uses them to modify its local simulation state and compute the message it will send during the next round (line 11).

Lemma 1 If a task can be solved in SMP n [adv : SOURCE, TOUR], it can be solved in ARW n,n-1 [fd : Ω].
Proof Let us consider a simulated process p i (i.e., p i executes in SMP n [adv : SOURCE, TOUR]). When there is no ambiguity, we use the same identifier p i , for a simulated process and its simulator.

Let us first observe that no correct simulator p i can block forever in the loop of lines 6-8. This is an immediate consequence of the eventual leadership property of Ω (the eventually elected process p ℓ cannot block forever), and the fact that it writes its messages in MEM

[ℓ][r][1..n].
Let us show that the tournament property TOUR is satisfied at every round. Let us consider two processes that terminates a round r ≥ 0. It follows from lines 9-10 that (1) p i has written a message into

MEM [i][r][j] and then read MEM [j][r][i], while (2) p j has Collection des Publications Internes de l'Irisa c IRISA written a message in MEM [j][r][i] and then read MEM [i][r][j].
As registers are atomic, it follows that either p i has written into

MEM [i][r][j] before p j has written into MEM [j][r][i],
or the opposite. Whatever the case, as each process writes before reading, at least one of them reads the message from the other, and consequently G r contains (i, j) or (j, i). Let us now consider a process p j whose simulator crashes during the execution. From the point of view of any process p i whose simulator is correct, everything appears as if, after the simulator of p j has crashed, the simulated adversary removes all the messages sent by p j to p i and keeps the messages sent by p i to p j . Hence, if p j crashes after round r, we have (i, j) ∈ G r ′ at any round r ′ > r.

Finally, let us consider a time after which all the correct simulators have forever the same correct leader p ℓ and no more simulator crashes. It follows from lines 6-8, that there is a round r such that, at any round r ′ ≥ r, any correct process p i receives the message sent by p ℓ . Moreover, crashed processes receive implicitly all messages sent by p ℓ . It follows that we have (ℓ, i) ∈ G r ′ which establishes the SOURCE property of the adversary.

It follows from the previous arguments that, if the task can be solved in SMP n [adv : SOURCE, TOUR], it can be solved in ARW n,n-1 [fd : Ω]. A process with a correct simulator behaves the same way in both models, and a process with a faulty simulator either computes a correct output value or crashes before it has computed an output value (in this case, its entry in the output vector contains ⊥).

✷

v into MEM [i] is denoted write i (v).
As in the previous simulation, the procedure simulate() is used to locally simulate the behavior of p i from its current step until its next invocation of a communication operation (i.e., a read or a write of the simulated shared memory). The simulation stops just before this invocation. It takes as input parameters the current local state of p i (ls_state i ) and the last value read from the shared memory by p i . This value, saved in read_value i (and initialized to ⊥), is meaningless if the operation is a write. The local variable next_op i contains p i 's next read or write operation to be simulated.

The local variable view i contains all the read/write operations issued by the processes and known by p i . Such an operation is represented by a triple (j, seq_nb, next_op). The simulation algorithm is a full information algorithm and consequently the set view i increases forever.

The local variable informed i contains the set of processes which, to p i knowledge, know the last read/write operation it is currently simulating. Finally, the set missed i (from which Ω is built) contains pairs (k, r) whose meaning is the following: ((k, r) ∈ missed i ) ⇒ there is at least one process that, during round r of the simulation, has not received and delivered the message sent by (the simulator of) p k during that round.

The simulation algorithm The simulation algorithm is described in Figure 3. When it starts a new round, the simulator of p i sends its control local state, i.e., the triple (i, view i , missed i ) to each other process (line 5). Then (lines 6-10), it considers all the messages it has received during the current round r, and updates accordingly rec_msg i and missed i .

Lines 11-12 locally implement Ω (see below). The variable informed i is then updated to take into account what has been learned from the messages just received. Let us notice (line 13) that it follows from TOUR that (j / ∈ rec_from i ) ⇒ p j has received p i 's round r message.

Then (the simulator of) p i executes rounds in SMP n [adv : SOURCE, TOUR] until it learns that (the simulators of) all the processes know its last read/write operation (line 15). Then, (line 16) it invokes simulate(ls_state i , read_value i ). If its (simulated) shared memory operation is a read, the value read_value i is the value obtained by this read operation. Otherwise (the simulated operation is a write of p i ), read_value i is useless. As already indicated, the invocation of simulate(ls_state i , read_value i ) simulates then the behavior of p i until its next read/write operation.

If the operation at which the local simulation stopped is a read of MEM [ℓ] (line 17), the local simulator computes, and deposits in read_value i , the value that will be associated with this read (line [START_REF] Raynal | K-anti-Omega[END_REF][START_REF] Raynal | Failure detectors for asynchronous distributed systems: an introduction[END_REF][START_REF] Raynal | Increasing the power of the iterated immediate snapshot model with failure detectors[END_REF][START_REF] Santoro | Time is not a healer[END_REF][START_REF] Santoro | Agreement in synchronous networks with ubiquitous faults[END_REF]. If p ℓ has not issued a write, read_value i is set to the default value ⊥ (line 19). Otherwise, read_value i is set to the last value written by p ℓ (line 18-21). Then, whatever the next operation (read or write) of p i , the local simulator associates a sequence number with it and adds the triple (i, seq_nb i , next_op i ) to initialization:

(1) ls_state i ← initial state of the local simulated algorithm;

read_value i ← ⊥; (2) (next_op i , ls_state i ) ← simulate(local_sim_state i , read_value i ); (3) seq_nb i ← 1; informed i ← {i}; missed i ← ∅; (4) view i ← {(i, seq_nb i , next_op i )}. round r = 1, 2, • • • do:
(5) send(i, view i , missed i ) to each other process; (6) rec_msgs i ← set of triples (j, view j , missed j ) received during this round; [START_REF] Delporte-Gallet | Tight failure detection bounds on atomic object implementations[END_REF]

view i ← view i ∪
(j,view j ,missed j )∈rec_msgs i view j ; (8) missed i ← missed i ∪ (j,view j ,missed j )∈rec_msgs i missed j ; (9) rec_from i ← j ∈ {1, . . . , n} : ∃(j, view j , missed j ) ∈ rec_msgs i ∪ {i}; [START_REF] Herlihy | Wait-free synchronization[END_REF]

missed i ← missed i ∪ (k, r) : k ∈ {1, . . . , n} \ rec_from i ; (11) min_missed i ← min |{r : (j, r) ∈ missed i }|, j ∈ {1, . . . , n} ; (12) ℓd i ← min j : |{r : (j, r) ∈ missed i }| = min_missed i ; (13) informed i ← informed i ∪ ({1, . . . , n} \ rec_from i ) (14) ∪ j ∈ rec_from i : (i, seq_nq i , next_op i ) ∈ view j ; (15) if (informed i = {1, . . . , n}) then (16) (next_op i , ls_state i ) ← simulate(ls_state i , read_value i ); (17) if (next_op i = read i (ℓ)) then (18) if (∄(ℓ, -, write ℓ (-)) ∈ view i ) (19) then read_value i ← ⊥ (20) else max_snℓ i ← max{sn ℓ , (ℓ, sn ℓ , write ℓ (-)) ∈ view i }; (21) read_value i ← v ℓ : (ℓ, max_snℓ i , write ℓ (v ℓ )) ∈ view i (22) end if (23) end if; (24) seq_nb i ← seq_nb i + 1; informed i ← {i}; (25) view i ← view i ∪ {(i, seq_nb i , next_op i )} (26) end if.
when leader i is read: return (ℓd i ). view i (line 24-25). Moreover, as its scope is the simulation of next_op i , the set informed i is reset to {i}.

As previously indicated, the current value (kept in ℓd i ) of the read-only variable leader i , which locally implements Ω, is computed from the set missed i at lines 11-12. The simulator of p i (1) computes, for each p j , the set of rounds at which at least one simulator has not received the round r message sent by p j 's simulator (these are messages suppressed by the adversary); then (2) it associates with each p j the cardinality of the previous set; and finally, (3) it considers the process p ℓ for which the adversary has suppressed the less messages (if there are several such processes, ties are solved by using the total order on process identities). Part 1: the simulation is non-blocking. Given that the simulation algorithm is a full information algorithm, the "king in two tournaments" Theorem [START_REF] Afek | A king in two tournaments[END_REF] 3 states that at least one read/write operation issued by a simulated process p i is known by all simulators in two simulation rounds (i.e., there is a simulator p i such that, for any j, we have next_op i ∈ view j in at most two rounds).

Let us consider three consecutive simulation rounds r, r+1 and r+2, and p i a simulator whose message (i, view i , missed i ) sent at line 5 has reached (directly or indirectly) all the process simulators by the end of round r + 1. As (due to TOUR), G r+2 contains a tournament, we have one of the following for each j = i: (a) j r+2 -→ i and in that case, p i receives its own triple (i, seq_nb i , next_op i ) from p j and consequently it knows that p j knows its triple (i, seq_nq i , next_op i ) (line 14); or (b) ¬(j r+2 -→ i) and in that case, we necessarily have i r+2 -→ j and consequently p i knows that p j knows its triple. It follows that, at the end of the simulation round r + 2, p i terminates the simulation of its read or write operation next_op i (line 15-line 23). As there is a bounded number of processes, there is at least one process that eventually executes until it computes its local result. It follows that the simulation is non-blocking.

Part 2: correct and faulty processes in ARW n,n-1 [fd : Ω].

As each message graph G r contains a tournament, it follows that the relation ∞ (introduced in Section 2.2) defines a total order on the equivalence classes of the relation ∞ . Hence, there is a single set X of strongly correct process simulators (i.e., X has no input edge in SC(G)). This set X contains exactly all the process simulators whose messages sent at line 5 are always eventually received (at some round, directly or indirectly) by all other process simulators.

It follows from the previous reasoning (Part 1) on the fact that the simulation is non-blocking, and the condition inf omed i = {1, ...n} (line 15), that each process in X simulates any number of its operations. Hence, those processes are correct in ARW n,n-1 [fd : Ω]. Differently, for each process p j such that j ∈ {1, ..., n} \ X, there is a round from which the predicate inf ormed j = {1, ...n} is never satisfied, and consequently the simulation of the process p j stops progressing. Hence, each weakly correct simulator p j such that j ∈ {1, ..., n} \ X simulates a faulty process in ARW n,n-1 [fd : Ω].

Part 3: definition of the linearization of the read and write operations. A write operation is linearized at the first of the two following time instants: (1) τ 1 the end of the simulation of this write operation (i.e., when the condition line 15 is satisfied by the associated simulator), and (2) τ 2 the time instant just before the linearization point of the simulation of the first read operation returning the written value. If none of these two instants ever happen, then the write is never linearized and the corresponding simulated process appears as crashed.

The linearization of a read operation is close to but different from the one of a write operation. A read operation is linearized at the first of these two time instants: (1) τ 1 the end of this read operation simulation (when the condition line 15 is satisfied by the associated simulator), and (2) τ 2 the time instant just before the linearization point of the simulation of the first write operation which overwrites the read value. However, if the instant τ 1 never happen, then the read is never linearized (even if τ 2 exists) and the simulated process appears as crashed. (Remark that, thanks to the fact that a simulator selects the freshest value it knows to prepare the value returned by a simulated read operation, and to the fact that, at the instant of the linearization of a write (or read) operation, all processes have the corresponding written (or read) value in their views, the read value cannot have been effectively overwritten before the beginning of the read operation returning it.)

As the reading (resp. overwriting) of a written (read) value cannot occur neither before the start of the corresponding write (read) operation, the linearization point of this operation occurs after its the start of the operation. Moreover, the selection of the first among τ 1 and τ 2 for both types of operation implies that the linearization point occurs at the latest at end of its simulation, and that (a) a read is always linearized after the writing of the value it returns, (b) the overwriting of a value is always linearized after all read operations that return it. Part 4: the local variables leader i implement Ω. It follows from the property SOURCE that there is a process p s and a round r 0 such that, from r 0 , no message from p s is removed by the adversary. In particular, after some round r s ≥ r 0 , all the messages sent by (the simulator of) p s are received by all the strongly correct processes. Let S ⊆ X be the set of processes p s satisfying this property ( eventually all their messages are -directly-received by all the strongly correct processes). Let r S = max{r s : s ∈ S}. (Let us notice that an arbitrary number of messages from the processes in S to processes which are not strongly correct can be suppressed by the adversary.)

As, at any round r ≥ r S , no message from (the simulator of) a process in S to (the simulator of) a strongly correct process is suppressed, no simulator of a strongly correct process p i adds a pair (s, r), s ∈ S, to its set missed i (line 10).

Let us observe that: (a) the simulator of any process p i adds all the set missed it receives to its own set missed i (line 8); (b) due to the definition of "strongly correct" simulator, messages are eventually propagated (directly or indirectly) in each direction between each pair of strongly correct simulators; and (c) after some finite time, no strongly correct simulator receive message from a weakly correct simulator.

It follows from the previous observations that, for each s ∈ S, the values |{r : (r, s) ∈ missed i }| eventually stabilize at the same finite value at each strongly correct simulator p i , while, for each j ∈ {1, ..., n} \ S, the value |r : (r, j) ∈ missed i }| never stops increasing. Hence, the same eventual leader is elected at all strongly correct processes by the code of lines 11-12, and consequently the correct simulated processes inherits the same eventual leader. Moreover, as the process simulators in S are strongly correct, the elected leader is a process which is correct in ARW The algorithm described in Figure 4 presents a simulation (for tasks) of SMP n [adv : SOURCE] on top of AMP n,n-1 [fd : Ω]. Its principles are close to the ones of the simulation of Figure 2. The algorithm ensures that the eventual leader p ℓ satisfies the property SOURCE. Hence, there are strongly correct processes and the eventual leader is one of them. The aim of the simulation algorithm is then to eventually withdraw all the messages except the ones from the leader.

Local variables of the simulation As in the previous simulations, r i is the locally simulated round number; msgs_to_send i [j] (initialized to ⊥) contains the next simulated message to be sent to p j ; rec_msg i [r] contains the simulated messages received at round r; sim_rec_msgs i [x] contains the message received from the process p x currently considered as the leader by p i ; leader i is the read-only variable provided by Ω.

(1)

r i ← 0; sim_rec_msgs i [1, . . . , n] ← [⊥, . . . , ⊥]; (2) (msgs_to_send i [1, . . . , n], ls_state i ) ← simulate(sim_rec_msgs i ); (3) for each r > 0 do rec_msgs i [r][1, . . . , n] ← [⊥, . . . , ⊥] end for; (4) repeat forever (5) r←r i + 1; (6)
for each j ∈ {1, . . . , n} do send(r i , msgs_to_send i [j]) to p j end for; [START_REF] Delporte-Gallet | Tight failure detection bounds on atomic object implementations[END_REF] repeat cur_ℓd i ← leader i [START_REF] Delporte-Gallet | The minimum information about failures for solving non-local tasks in message-passing systems[END_REF] until

(cur_ℓd i = i ∨ rec_msgs i [r i ][cur_ℓd i ] = ⊥) (9)
end repeat; [START_REF] Herlihy | Wait-free synchronization[END_REF] The simulation algorithm The procedure simulate() takes as input parameter the simulated messages received by p i at the current round, and simulates the local algorithm until the next sending of messages by p i . This procedure returns the simulated messages to be sent at the beginning of the next round.

sim_rec_msgs i [cur_ℓd i ] ← rec_msgs i [r i ][cur_ℓd i ]; (
After the initialization stage (lines 1-3), the local simulator of p i enters a loop whose each body execution simulates a round of the synchronous system. It first sends the messages that p i has to send at the current round (line 6). Then it waits until it has received a message from its current leader or it is its own leader (lines 7-9). When this occurs, it retrieves the message sent by its current leader (line 10) and invokes the procedure simulate() with this message as input parameter, before proceeding to the simulation of the next synchronous round. Proof Let us first show that no correct process remains blocked forever in the loop lines of 7-9. Indeed, there is a finite time τ after which an eventual leader (say p ℓ ) is elected by Ω at each process. It then follows from the first part of the predicate of line 8 that p ℓ cannot remain blocked at line 8, and consequently executes rounds forever. Moreover, as its messages are eventually received at Collection des Publications Internes de l'Irisa c IRISA each round by all correct processes, it follows that there is a time after which the second part of the predicate of line 8 is always satisfied by these processes. Consequently, none of them can remain blocked forever at line 8.

The previous reasoning shows also that the eventual leader elected by Ω behaves as a source, and consequently the property SOURCE is satisfied in the simulated synchronous system.

✷ Lemma 3 4.2 From SMP n [adv : SOURCE] to AMP n,n-1 [fd : Ω]
The simulation algorithm is described in Figure 5. It is similar to the algorithm of Figure 3 (which simulates ARW n,n-1 [fd : Ω] on top of SMP n [adv : SOURCE, TOUR]).

Local variables of the simulation The local variables ls_state i , view i , rec_f rom i , and missed i have the same meaning as in Figure 3. The local variable msgs_to_rec i contains messages to be consumed by the simulated process (it corresponds to read_value i in Figure 3). The variable msgs_to_send i contains the messages to be sent in the next simulation round (it corresponds to next_op i in Figure 3). The variable msgs_received i is a new variable containing the messages already received by the simulated process p i . Finally, ℓd i is the local variable containing current local value of Ω built by the algorithm.

The simulation algorithm As in the simulation of Figure 3, lines 1-4 are an initialization stage. Similarly to previous simulations, the procedure simulate() locally simulates the process p i . It takes messages to be consumed by p i as input parameter and returns the next set of messages to be sent. The simulation algorithm is a full information algorithm. During each simulation round r, the simulator of p i first sends its control local state to each other process, and waits for the same information from them (lines 5-6). Then, according to the messages it has received during the current round, it updates view i , missed i , and rec_f rom i (lines 7-10). As in Figure 3, it also computes the identity ℓd i of its current candidate to be the eventual leader (lines [START_REF] Herlihy | The topological structure of asynchronous computability[END_REF][START_REF] Kuhn | Distributed computation in dynamic networks[END_REF].

If a simulation message has been received from the process p ℓdi , the simulator of p i strives to make p i progress. It considers the last message sent by p ℓdi to p i (triple (ℓd i , i, m)), and adds it to the set msgs_to_rec i (lines [START_REF] Lo | Using failure detectors to solve consensus in asynchronous shared-memory systems[END_REF][START_REF] Mourgaya | Asynchronous implementation of failure detectors[END_REF]. Then, if the messages p i has to send are known by its current leader p ℓdi (line 16), the procedure simulate() is invoked to make p i progress (line 17), and the local control variables msgs_received i and view i are updated accordingly (line 18).

initialization:

(1) ls_state i ← initial state of the local simulated algorithm; [START_REF] Afek | A king in two tournaments[END_REF]

msgs_to_rec i ← ∅; msgs_received i ← ∅; (3) (msgs_to_send i , ls_state i ) ← simulate(ls_state i , msgs_to_rec i ); (4) view i ← msgs_to_send i ; missed i ← ∅; ℓd i ← i. round r = 1, 2, • • • do:
(5) send(i, view i , missed i ) to each other process; (6) rec_msgs i ← set of triples (j, view j , missed j ) received during this round; [START_REF] Delporte-Gallet | Tight failure detection bounds on atomic object implementations[END_REF]

view i ← view i ∪
(j,view j ,missed j )∈rec_msgs i view j ; (8) missed i ← missed i ∪ (j,view j ,missed j )∈rec_msgs i missed j ; (9) rec_from i ← j ∈ {1, . . . , n} : ∃(j, view j , missed j ) ∈ rec_msgs i ∪ {i}; [START_REF] Herlihy | Wait-free synchronization[END_REF]

missed i ← missed i ∪ (k, r) : k ∈ {1, . . . , n} \ rec_from i ; (11) min_missed i ← min |{r : (j, r) ∈ missed i }|, j ∈ {1, . . . , n} ; (12) ℓd i ← min j : |{r : (j, r) ∈ missed i }| = min_missed i ; (13) if (ℓd i ∈ rec_f rom i ) then (14) let view ℓd i be such that (ℓd i , view ℓd i , missed ℓd i ) ∈ rec_msgs i ; (15) msgs_to_rec i ← msgs_to_rec i ∪ {(ℓd i , i, m) : (ℓd i , i, m) ∈ view ℓd i }; (16) if (msgs_to_send i ⊆ view ℓd i ) then (17) (msgs_to_send i , ls_state i ) ← simulate(ls_state i , msgs_to_rec i \ msgs_received i ); (18) msgs_received i ← msgs_to_rec i ; view i ← view i ∪ msgs_to_send i (19) end if (20) end if.
when leader i is read: return (ℓd i ). Let S be the set of processes which satisfy the property SOURCE. As, by assumption there at least one source, we have S = ∅. Moreover, due the definition of the set SC of strongly correct simulators we have S ⊆ SC. Let S ′ be the set of processes which, albeit they are not necessarily source, appear as sources to all processes of SC. Hence we have S ⊆ S ′ ⊆ SC, and S ′ = ∅.

The variables leader i implement Ω. According to the definition of SC, there is a round r 0 after which no more message from a weakly correct simulator is received (directly or indirectly) by a strongly correct simulator. Let r 1 = max{r s , s ∈ S ′ } where r s is the first round after which no message sent by p s to a strongly correct simulator is eliminated. As, after r 1 , each strongly correct simulator receives at every round a message from each simulator in S ′ , it follows that none of them adds a pair (s, r), r ≥ r 1 , s ∈ S ′ in its variable missed i at line 10. After r 2 = max{r 0 , r 1 }, the only pairs (s, r), s ∈ S ′ (r < r 1 ) that are added by a strongly correct simulator in its variable missed i are those that have been added by other strongly correct simulators at line 8 or line 11 before r 2 . Since strongly correct simulators are infinitely often able to transmit (directly or not) messages to each other, there is a round r 3 ≥ r 2 such that any strongly correct simulator p i has received (directly or not) during a round rj ≥ r 2 the information contained in the variable missed j from each other strongly correct simulator p j . After r 3 , for any s ∈ S ′ , the number of pairs (s, r) in the variables missed i of all strongly correct simulators p i is the same and does not increase anymore.

For each simulator p i , i / ∈ S ′ , there is an infinite number of rounds r such that p i 's message is not received during round r by at least one of the strongly correct simulator p j , and accordingly, this simulator adds a pair (i, r) to its variable missed j during round r at line 10. As the strongly correct simulators communicate (directly or not) infinitely often with each other, all of them eventually add this pair to their variable missed during r (at line 10) or later (at line 8). Consequently, for each such simulator p i , i / ∈ S ′ , the number of pairs (i, r) in the variable missed j of every strongly simulator p j increases forever.

It follows from the previous discussion that the minimal number of rounds missed by a simulator (as calculated at line 12, and using simulator identity to do tie-breaking) eventually becomes and remains the same at each strongly correct simulator. Let ℓd denote this simulator identity. As it is the identity that is eventually always returned when leader i is read by any simulated process p i whose simulator is strongly correct, the unicity eventual property of Ω is ensured for these processes. The next paragraph shows that the set of strongly correct simulators corresponds exactly to the set of correct simulated processes. As p ℓd is strongly correct, the elected process is a correct process, which concludes the proof of Ω.

Correct and faulty (simulated) processes in AMP n,n-1 [fd : Ω]. It follows from the previous paragraphs that each strongly correct simulator p i is always eventually able to transmit (directly or not) a new message m to p ℓd , and then eventually receive (directly) a message from p ℓd containing m. Hence the conditions of line 13 and line 16 are fulfilled an infinite number of times and, consequently, the corresponding simulator can always issue enough steps (line 17) to progress in the simulated code.

Hence, the correct simulated processes and the faulty simulated processes are the ones simulated by the strongly correct and weakly correct simulators, respectively. It follows that Linearization of communication operations. Let us consider a simulated process p i that sends a message m to a simulated process p j . This operation is disseminated to each simulator by p i 's simulator at line 5. Then a simulator considers this simulated message m only at line 17 when the second input parameter of its invocation of simulate() contains the message m. (Let us observe, that this message m arrives at a simulator p k from its current leader ℓd k , lines 13 and 16).

Let τ 1 be the time of the first invocation of simulate() by a simulator such that m belongs to the second input parameter of this invocation, where τ 1 = ∞ if there is no such invocation. Let τ 2 be the time at which the simulator of p i starts the execution of simulate() (line 17) after it has disseminated m, where τ 2 = ∞ if there is no such invocation.

The send of m is linearized at time min(τ 1 , τ 2 ) (let us notice that the simulation of p i does not progress between the sending of m by p i and its linearization point). If min(τ 1 , τ 2 ) = ∞, the send of m is linearized after the receiver p j has computed its result.

The reception of m is linearized at the time of the invocation by p j of simulate() whose second input parameter contains the message m, or after p j has computed its result if there is no such invocation.

✷ Lemma 4 4.3 SOURCE is a characterization of Ω in AMP n,n-1 [fd : ∅] Theorem 3 A task can be solved in AMP n,n-1 [fd : Ω] iff it can be solved in SMP n [adv : SOURCE, FAIR].
Proof The proof follows directly from Lemma 3 and Lemma 4.

✷ T heorem 3
Collection des Publications Internes de l'Irisa c IRISA

5 QUORUM is a Characterization of Σ in AMP n,n-1 [fd : ∅]
This section shows that the computing models SMP n [adv : QUORUM] and AMP n,n-1 [fd : Σ] have the same computational power for tasks.

The Property QUORUM

Let us remember that SC is the set of strongly correct processes in the considered synchronous message-passing system (processes whose an infinite number of messages are received by each other process). The property QUORUM is defined as follows:

∀ i, j : ∀ r i , r j : ({k :

k ri -→ i} ∩ {k : k rj -→ j} = ∅) ∧ (SC = ∅).
This property is a statement of Σ suited to the context of round-based synchronous message-passing systems prone to message adversaries. Given any pair of processes p i and p j , its first part states that, whatever the synchronous rounds r i and r j executed by p i and p j , respectively, there is a process p k whose messages to p i at round r i and to p j at round r j are not eliminated by the adversary (intersection property). The second part states that there is at least one process whose messages are infinitely often received by each other process (liveness property). Theorem 4 will show that this formulation of Σ is correct for the equivalence of AMP n,n-1 [fd : Σ] and SMP n [adv : QUORUM] for task solvability.

From AMP

n,n-1 [fd : Σ] to SMP n [adv : QUORUM]
The simulation algorithm described in Figure 6. It has the same local variables as, and is very close to, the one of Figure 4. In addition to the local output of the failure detector Σ, which is denoted qr i , the only modifications are the lines 7-10 which differ in both algorithms. The simulator of p i waits until it has received a message from each process that appears in its current quorum qr i (lines 7-9). It then invokes the procedure simulate() with these messages as input (line 10).

The principle of this simulation is the following: after some time, the simulated message adversary suppresses all the messages sent by processes that do not belong to a quorum, but is prevented from suppressing the messages sent by processes belonging to quorums.

(1) r i ← 0; sim_rec_msgs i [1, . . Proof The proof that no simulator of a process p i remains forever blocked in a round r i follows directly from the fact that (1) each process simulator send a message to each other process simulator at every round (line 6), and (2) each quorum qr i eventually contains only correct simulators (liveness of Σ).

Let qr r i be the value of qr i that allows p i to exit the repeat loop during the simulation of round r (lines 7-9). It follows from line 8 and line 10 that qr r i = {k : k ri -→ i}. Moreover, it follows from the intersection property provided by Σ that ∀ i, j, r i , r j : qr ri i ∩ qr rj j = ∅. The first part of the property QUORUM, namely, ∀ i, j, r i , r j : ({k :

k ri -→ i} ∩ {k : k rj -→ j} = ∅), is consequently satisfied.
According to the previous discussion, a correct (resp., faulty) process in AMP n,n-1 [fd : Σ] is a process whose simulator is strongly (resp., weakly) correct. Proof The proof follows immediately from Lemma 5 and Lemma 6.

✷ T heorem 4

6 SOURCE + QUORUM Characterizes Σ + Ω in AMP n,n-1 [fd : ∅]
Let us notice that the properties SOURCE and QUORUM are independent of one another in the sense that none of them can be obtained from the other. It follows that the power provided by SOURCE and the power provided by QUORUM can be added. More specifically, we have the following:

• A merge of the simulation of SMP n [adv : SOURCE] in AMP n,n-1 [fd : Ω] (Figure 4) with the simulation of SMP n [adv : QUORUM] in AMP n,n-1 [fd : Σ] (Figure 6) provides a simulation SMP n [adv : SOURCE, QUORUM] in AMP n,n-1 [fd : Σ, Ω]. The difference between this simulation and the one of Figure 4 (or Figure 6) is at lines 7-10 which becomes [START_REF] Delporte-Gallet | Tight failure detection bounds on atomic object implementations[END_REF]

repeat cur_ℓd i ← leader i ; cur_qr i ← qr i (8) until [(∀j ∈ cur_qr i \ {i} : rec_msgs i [r i ][j] = ⊥) ∧ (cur_ℓd i = i ∨ rec_msgs i [r i ][cur_ℓd i ] = ⊥)] (9) end repeat; (10) for each j ∈ cur_qr i ∪ cur_ld i do sim_rec_msgs i [j] ← rec_msgs i [r i ][j] end for.
The proof is the same as in Lemma 5 augmented by the fact that the eventual leader elected by Ω verifies the property SOURCE as shown in Lemma 3.

• Similarly, adding the management of missed i and the procedure to query Ω (as done at lines 8-11 of Figure 5 The linearization points and the proof of the properties of Σ are the same as in Lemma 6, while the proof of the properties of Ω follows the one of Lemma 4. Let us finally notice that it follows directly from the properties SOURCE and QUORUM that a process verifying the SOURCE property appears eventually in all the simulated quorums.

Theorem 5 then follows:

Theorem 5 A task can be solved in SMP n [adv : SOURCE, QUORUM] iff it can be solved in AMP n,n-1 [fd : Σ, Ω].

Conclusion

Considering crash-free synchronous round-based systems, message adversaries have been designed as daemons that suppress messages. Failure detectors have been introduced to enrich crash-prone asynchronous (read/write or message-passing) systems. A previous work [START_REF] Afek | Asynchrony from synchrony[END_REF] has shown that, from a task solvability point of view, the message adversaries constrained by a property denoted TOUR (for tournament) characterizes the well-known wait-free read/write model. Considering task solvability, this paper has introduced relations linking failures detectors and message adversaries. More precisely, it has introduced two new properties, denoted SOURCE and QUORUM, which are restrictions on message adversaries, and has shown that • SOURCE + TOUR characterizes the wait-free read/write model enriched with Ω, Collection des Publications Internes de l'Irisa c IRISA

• SOURCE characterizes the crash-prone asynchronous message-passing model enriched with Ω, • QUORUM characterizes the crash-prone asynchronous message-passing model enriched with Σ, • SOURCE + QUORUM characterizes the crash-prone asynchronous message-passing model enriched with Σ + Ω.

Hence, when considering task solvability, these characterizations state "minimal properties" defining the strongest message adversaries for synchronous round-based message-passing systems equating classical asynchronous crash-prone systems. Interestingly, this allows for the establishment of a hierarchy on message adversaries (e.g., SMP n [adv : QUORUM] is stronger than SMP n [adv : TOUR] as shown on the left of Figure 1; this follows from the fact that the computability power of Σ is strictly stronger than read/write registers).

In our understanding of the foundations of distributed computing, a lot of issues remain still open. As examples, here are two interesting message adversary-related problems. Which is the weakest message adversary AD such that consensus can be solved in SMP n [adv : AD]? (The only thing we know is that SMP n [adv : CONS] is weaker than or equivalent to SMP n [adv : SOURCE, TOUR] and strictly stronger than SMP n [adv : TOUR]). Is the addition of the constraint |SC| ≥ nt to an adversary sufficient to characterize t-resilient asynchronous crash-prone read/write or message-passing systems?

A.3 SOURCE + TOUR, SOURCE tp +TP, and SOURCE pairs + PAIRS are Equivalent

The following theorem extends to the pairs SOURCE + TOUR, SOURCE tp + TP, and SOURCE pairs + PAIRS, the equivalence of the properties TOUR, TP, and PAIRS stated in [START_REF] Afek | Asynchrony from synchrony[END_REF]. While the structure of these simulations are based on the ones described in [START_REF] Afek | Asynchrony from synchrony[END_REF], some of their technical developments are different. This is due to the introduction of the source process which requires message patterns in consecutive rounds that are no longer fully independent.

Theorem 6 The the system model SMP n [adv : SOURCE, TOUR], the system model SMP n [adv : SOURCE tp , TP], and the system model SMP n [adv : SOURCE pairs , PAIRS] have the same computational power.

Proof To show that two system models are equivalent, the proof consists in simulating each of them on top of the other one. ). Then, it gathers all the messages it receives during a simulation round, and adds the union of all the sets they contain to its set of known messages M i . At the end of the simulation round 2n-3, the set of messages known by p i and addressed to itself is returned as the set of messages it receives during the simulated round of A in SMP n [adv : SOURCE, TOUR].

The simulated message graphs verify TOUR. Let M r i denote the value of the set M i of the messages known by a process p i at the end of the simulation round r (with M 0 i = {(i, msg i )}). Let K r i denote the set of processes which received msg i before the end of the simulation round r, namely, K r i = {j ∈ {1, . . . , n} : (i, msg i ) ∈ M r j }. Let i and j be two process identities and r ∈ {1, . . . , 2n -3} a simulation round number such that, at the beginning of round r, we have (j, msg j ) / ∈ M r-1 i and (i, msg i ) / ∈ M r-1 j (i.e., p i does not know msg j and p j does not know msg i ). According to property TP, G r preserves a path from p i to p j or from p j to p i : ∃k ≥ 1, ∃(π 1 , . . . , π k ) ∈ {1, . . . , n} k :

(∀l ∈ {1, . . . , k -1} : (π l , π l+1 ) ∈ G r ) ∧ ({π 1 , π k } = {i, j}) . If π 1 = i, then, as π 1 = i ∈ K r-1 i and π k = j / ∈ K r-1 i , it exists m ∈ {1, . . . , k -1} such that π m ∈ K r-1 i ∧ π m+1 / ∈ K r-1 i . Since a message goes from π m to π m+1 during round r, |K r i | > |K r-1 i |.
If π 1 = j, the same reasoning applies and we have then

|K r j | > |K r-1 j |. As initially |K 0 i | = |K 0 j | = 1, it follows that, for all r ∈ {1, . . . , 2n -3}, if i / ∈ K r-1 j and j / ∈ K r-1 i , then |K r i | + |K r j | ≥ 2 + r. Consequently: |K 2n-3 i ∩ K 2n-3 j | = |K 2n-3 i | + |K 2n-3 j | -|K 2n-3 i ∪ K 2n-3 j |, ≥ 2 + (2n -3) -|K 2n-3 i ∪ K 2n-3 j |, ≥ 2n -1 -n ≥ n -1,
and it follows that {i, j} ∩ K 2n-3 i ∩ K 2n-3 j = ∅, which proves that at least one simulated message between p i and p j is received during the 2n -3 simulation rounds. As the proof holds for any pair of processes, the proposed protocol simulates a round of SMP n [adv : SOURCE, TOUR] in 2n -3 rounds of SMP n [adv : SOURCE tp , TP] and this simulation satisfies the property TOUR. TOUR] is simulated using 2n -3 rounds (denoted with small r letters) of protocol described above. Let p s be a process such that, after the simulation round r 0 , for all r ′ ≥ r 0 , G r ′ is such that there are (message) paths from p s to any other process. Let r 1 = 1 + ⌈ r0-1 2n-3 ⌉ × (2n -3) be the first simulation round after r 0 such that the simulation of a new simulated round R 0 = 1 + ⌈ r0-1 2n-3 ⌉ of SMP n [adv : SOURCE, TOUR] begins. Hence, for all r ′ ≥ r 0 , the graphs G r ′ are such that there are paths (possibly changing at every round) from p s to any other process. It follows that the arguments used above hold with π 1 = s and π k = j.

Let r be a round such that r ≥ r 1 , and R = 1 + ⌊ r-1 2n-3 ⌋ be the round of SMP n [adv : SOURCE, TOUR] that is simulated during r (r ≥ r 1 ≥ r 0 hence, R ≥ R 0 ). Moreover, let r ′ = r -(R -1) × (2n -3) = ((r -1) mod (2n -3)) + 1 denote one of the 2n -3 simulation rounds simulating the round R. With the same notations as above, as s r j for any p j , the previous reasoning can be applied with π 1 = s and π k = j, namely, if j / ∈ |K r ′ -1

s | we have |K r ′ s | > |K r ′ -1 s |.
As this is true for any r ≥ r 1 , it is possible, similarly as before, to infer that if j / ∈ K r ′ -1 , then |K The simulated message graphs verify TOUR. As at least one of the two messages exchanged by p i and p j is preserved by SMP n [adv : SOURCE pairs , PAIRS] at this round r, and as each pair of processes is associated with one of the Cn2 rounds, it follows that, in the simulated round R of SMP n [adv : SOURCE, TOUR], at least one message is preserved on each link, thus G R satisfies TOUR.

The source of SMP n [adv : SOURCE pairs , PAIRS] simulates a source of SMP n [adv : SOURCE, TOUR]. According to definition of SOURCE, it exists a process p s and a round r 0 after which no message from p s is removed by the adversary in all the rounds associated with a pair containing p s . Let r 1 = 1 + ⌈ r0-1

Cn2 ⌉ × Cn2 be the first round after r 0 at which the simulation of a new round R 0 = 1 + ⌈ r0-1 Cn2 ⌉ of SMP n [adv : SOURCE, TOUR] begins. In all the simulated rounds starting from R 0 , all processes receive p s 's message. The source property of TOUR is then verified. Here again, it follows directly from the definitions of PAIRS and SOURCE + TOUR that a protocol which, for each simulated round R, suppresses all the messages except the ones sent by the processes of the pair associated (by PAIRS) with R, simulates a round of SMP n [adv : SOURCE pairs , PAIRS] (moreover, a simulated round R requires exactly one simulation round r). Moreover, as at least one message is preserved in each round on each link by TOUR, it follows that one of the two messages sent by the processes that belong to the pair associated with the round R is not removed. Thus the PAIRS property is verified by the simulated system. Beside that, by definition of SOURCE, it exists a process p s and a simulation round number r 0 such that all the messages sent by p s after r 0 are preserved. It follows that, after r 0 , all the messages sent by p s (during the simulation rounds associated with a pair to which it belongs) are preserved. Consequently, the property SOURCE pairs is verified, which concludes the proof of the computational equivalence between SMP n [adv : SOURCE, TOUR] and SMP n [adv : SOURCE pairs , PAIRS].

✷ T heorem 6

The next corollary follows from Theorem 2 and the previous theorem. B The Failure Detector Ω k

Definition Ω k (1 ≤ k ≤ n) is called an anti-omega-k failure detector [START_REF] Raynal | K-anti-Omega[END_REF][START_REF] Zieliński | Anti-Omega: the weakest failure detector for set agreement[END_REF]. It is a simple generalization of Ω (Ω 1 = Ω).

In the system model AMP n,n-1 [fd : Ω k ], each process p i is endowed with a local variable xx i = leaders i that always contains a (possibly changing) set of k process identities. Moreover, there is a time τ and a process identity ℓ ∈ C such that ∀τ ′ ≥ τ : (i ∈ C) ⇒ (leaders τ ′ i = ℓ).

Figure 1 :

 1 Figure 1: A message adversary hierarchy based on task equivalence and failure detectors

Figure 2 :

 2 Figure 2: From ARW n,n-1 [fd : Ω] to SMP n [adv : SOURCE, TOUR]

Figure 3 :

 3 Figure 3: Simulation of ARW n,n-1 [fd : Ω] in SMP n [adv : SOURCE, TOUR]

Lemma 2

 2 If a task can be solved in ARW n,n-1 [fd : Ω], it can be solved in SMP n [adv : SOURCE, TOUR]. Proof The proof consists of four parts: (1) the simulation is non-blocking; (2) the definition of which are the correct/faulty processes in ARW n,n-1 [fd : Ω]; (3) the definition of the linearization of the read and write operations; and (4) the fact that local variables leader i implement Ω.

  11) (msgs_to_send i [1, . . . , n], ls_state i ) ← simulate(sim_rec_msgs i ); (12) sim_rec_msgs i [1, . . . , n] ← [⊥, . . . , ⊥] (13) end repeat. when (r, m) received from p j : rec_msgs i [r][j] ← m.

Figure 4 :

 4 Figure 4: From AMP n,n-1 [fd : Ω] to SMP n [adv : SOURCE]

Lemma 3

 3 If a task can be solved in SMP n [adv : SOURCE], it can be solved in AMP n,n-1 [fd : Ω].

Figure 5 :

 5 Figure 5: Simulation of AMP n,n-1 [fd : Ω] in SMP n [adv : SOURCE]

Figure 6 :Lemma 5

 65 Figure 6: From AMP n,n-1 [fd : Σ] to SMP n [adv : QUORUM]

Part 2 :

 2 the local variables rec_f rom i implement Σ. The intersection property of Σ comes directly from the first predicate defining the property QUORUM. The liveness property of Σ is a consequence of Item (2) noticed above, and the fact that the correct processes in the simulated system AMP n,n-1 [fd : Σ] are exactly those whose simulators are strongly correct in SMP n [adv : QUORUM]. Part 3: The linearization points of the communication operations are defined the same way as in the proof of Lemma 4. ✷ Lemma 6 5.4 QUORUM is a Characterization of Σ in AMP n,n-1 [fd : ∅] Theorem 4 A task can be solved in SMP n [adv : QUORUM] iff it can be solved in AMP n,n-1 [fd : Σ].

  ) to the simulation of AMP n,n-1 [fd : Σ] in SMP n [adv : QUORUM] (Figure 7) provides a simulation of AMP n,n-1 [fd : Σ, Ω] in SMP n [adv : SOURCE, QUORUM].

3 s.

 3 r ′ s | ≥ 1 + r ′ (if j / ∈ K r ′ -1 s , then, for all 1 ≤ r ′′ ≤ r ′ , j / ∈ K r ′′ -1 s , consequently |K r ′′ s | > |K r ′′ -1 s |, moreover |K 0 s | = 1 then a simple induction allows to conclude). It follows that if r ′ ≥ n -1 then j ∈ K r ′s , in particular j ∈ K 2n-That implies that, in any simulated round R ≥ R 0 , the sets of received messages are such that all processes receive the messages sent by p s . The properties SOURCE + TOUR are consequently verified by the adversary (which is simulated by sequences of 2n -3 simulation rounds), which concludes the proof of the computational equivalence of the models SMP n [adv : SOURCE tp , TP] and SMP n [adv : SOURCE, TOUR]. Part 3 of the proof: simulation of SMP n [adv : SOURCE, TOUR] on top of SMP n [adv : SOURCE pairs , PAIRS]. The definitions of SOURCE + TOUR and SOURCE pairs + PAIRS imply directly that Cn2 consecutive rounds of SMP n [adv : SOURCE pairs , PAIRS] simulate a round of SMP n [adv : SOURCE, TOUR]. Indeed, to send a message m to a process p j in the currently simulated round R of SMP n [adv : SOURCE, TOUR], a process p i just sends m during the simulation round r associated with the pair {p i , p j }.

Part 4

 4 of the proof: simulation of SMP n [adv : SOURCE pairs , PAIRS] on top of SMP n [adv : SOURCE, TOUR].

Corollary 1 A

 1 task T can be solved in ARW n,n-1 [fd : Ω] iff it can be solved in any of the three following synchronous models: SMP n [adv : SOURCE, TOUR], or SMP n [adv : SOURCE tp , TP], or SMP n [adv : SOURCE pairs , PAIRS].

ARW n,n- 1

 1 [fd : Ω k ] ≃ T SMP n [adv : k -SOURCE, TOUR] It is possible to extend the Theorem 2 to the system model ARW n,n-1 [fd : Ω k ]. The corresponding adversary, denoted k-S-TOUR is defined as follows: ∃S ⊆ {1, . . . , n}, ∃r 0 > 0 : (|S| = k) ∧ (∀r ≥ r 0 : ∃s r ∈ S : ∀ i : s r r → i). The proof that a task is solvable in ARW n,n-1 [fd : Ω k ] iff it is solvable in SMP n [adv : k -SOURCE, TOUR] is a straightforward generalization of the previous one. It is left to the reader. Collection des Publications Internes de l'Irisa c IRISA

  1

  • Then Section 5 focuses on a new message delivery property denoted QUORUM, and shows that a message adversary constrained by this property captures in SMP • Finally, as a consequence of the previous results, Section 6 shows that the properties SOURCE + QUORUM characterize the pair of failure detectors Σ + Ω, i.e., SMP

n [adv : ∅] the same computability power (from a task point of view) as the one added by the failure detector Σ to AMP n,n-1 [fd : ∅]. To that end, it shows that SMP n [adv : QUORUM] ≃ T AMP n,n-1 [fd : Σ]. n [adv : SOURCE, QUORUM] ≃ T AMP n,n-1 [fd : Σ, Ω].

  Lemma 1 3.3 From SMP n [adv : SOURCE, TOUR] to ARW n,n-1 [fd : Ω]

This section presents a simulation of ARW n,n-1 [fd : Ω] on top of SMP n [adv : SOURCE, TOUR] such that, any task that can be solved in SMP n [adv : SOURCE, TOUR] can be solved in ARW n,n-1 [fd : Ω]. This simulation has the same structure as the simulation of ARW n,n-1 [fd : ∅] on top of SMP n [adv : ∅] described in

[START_REF] Afek | Asynchrony from synchrony[END_REF]

. Basically, it adds to it the management of the local variables missed i (defined below) from which Ω is extracted.

Global and local variables of the simulation

The shared memory of ARW n,n-1 [fd : Ω] is made up of an array of singlewriter/multi-reader atomic registers MEM [1.

.n] such that only p i can write MEM [i]. The simulation associates a sequence number with each read or write operation of a simulated process p i . To simplify notations, a read of MEM [ℓ] by p i is denoted read i (ℓ) and a write of

  Remark Let us remark that it is not possible to conclude from the previous theorem and the fact that Ω is the weakest failure detector to solve consensus in ARW n,n-1 [fd : ∅], that the property SOURCE + TOUR defines a weakest message adversary AD allowing consensus to be solved in SMP n [adv : AD]. It remains possible that a property AD weaker than SOURCE + TOUR allows consensus to be solved in SMP n [adv : AD]. Said differently nothing allows us to claim that the "granularity on the properties which can be defined to constrain message adversaries" is the same as the "granularity on the information on failures" provided by failure detectors.Let CONS be the minimal message adversary property that allows consensus to be solved in SMP n [adv : CONS]. As consensus is solvable in SMP n [adv : SOURCE, TOUR], it follows that SMP n [adv : SOURCE, TOUR] is at least as powerful as SMP n [adv : CONS]. On another side, as (1) a read/write register can be implemented from consensus, and (2) consensus cannot be solved in SMP n [adv : TOUR], it follows that SMP n [adv : CONS] is strictly more powerful than SMP n [adv : TOUR]. 4 SOURCE is a Characterization of Ω in AMP n,n-1 [fd : ∅] 4.1 From AMP n,n-1 [fd : Ω] to SMP n [adv : SOURCE]

	n,n-1 [fd : Ω].	✷ Lemma 2
	3.4 SOURCE + TOUR is a Characterization of Ω in ARW n,n-1 [fd : ∅]

Theorem 2 A task can be solved in SMP n [adv : SOURCE, TOUR] iff it can be solved in ARW n,n-1 [fd : Ω].

Proof The proof follows immediately from Lemma 1 and Lemma 2.

✷ T heorem 2

Collection des Publications Internes de l'Irisa c IRISA

  . , n] ← [⊥, . . . , ⊥]; (2) (msgs_to_send i [1, . . . , n], ls_state i ) ← simulate(sim_rec_msgs i ); (3) for each r > 0 do rec_msgs i [r][1, . . . , n] ← [⊥, . . . , ⊥] end for; for each j ∈ cur_qr i do sim_rec_msgs i [j] ← rec_msgs i [r i ][j] end for; (11) (msgs_to_send i [1, . . . , n], ls_state i ) ← simulate(sim_rec_msgs i ); (12) sim_rec_msgs i [1, . . . , n] ← [⊥, . . . , ⊥] (13) end repeat. when (r, m) received from p j : rec_msgs i [r][j] ← m.

	(4) repeat forever
	(5)	r←r i + 1;
	(6)	for each j ∈ {1, . . . , n} do send(r i , msgs_to_send i [j]) to p j end for;
	(7)	repeat cur_qr i ← qr i
	(8)	until (∀j ∈ cur_qr i \ {i} : rec_msgs i [r i ][j] = ⊥)
	(9)	end repeat;
	(10)

  The proof first shows that SMP n [adv : SOURCE, TOUR] and SMP n [adv : SOURCE tp , TP] are equivalent. It then shows that SMP n [adv : SOURCE, TOUR] and SMP n [adv : SOURCE pairs , PAIRS] are equivalent. It then follows by transitivity that SMP n [adv : SOURCE tp , TP] and SMP n [adv : SOURCE pairs , PAIRS] are equivalent. Part 1 of the proof: SOURCE + TOUR is a weaker adversary than SOURCE tp + TP. Since ∀i, j, ∀r > 0 : i =⇒ i r j, it follows directly from the property definitions that an adversary that respects the properties SOURCE and TOUR respects also the properties SOURCE tp and TP. Part 2 of the proof: simulation of SMP n [adv : SOURCE, TOUR] on top of SMP n [adv : SOURCE tp , TP]. Simulation protocol. Let A be an algorithm designed for SMP n [adv : SOURCE, TOUR]. The simulation consists in executing 2n -3 simulation rounds of a full information protocol in SMP n [adv : SOURCE tp , TP] in order to simulate each round of A. For each of these simulated rounds, each process p i does the following. It first sends a set M i containing all the messages it knows (initially it knows only the pair (i, msg i ) where msg i is the set of messages sent by p i in A during the currently simulated round in SMP

r -→ j n [adv : SOURCE, TOUR]

  The source of SMP n [adv : SOURCE pairs , PAIRS] simulates a source of SMP n [adv : SOURCE, TOUR]. Considering the previous protocol which simulates a round of SMP n [adv : SOURCE, TOUR] in 2n-3 rounds of SMP n [adv : SOURCE tp , TP], it is sufficient to show that, if SMP n [adv : SOURCE tp , TP] eventually always preserves paths starting from a process p s to any other process, then eventually all messages originating from s are preserved in the simulated rounds of SMP n [adv : SOURCE, TOUR]. Collection des Publications Internes de l'Irisa c IRISA Let us consider a simulation in SMP n [adv : SOURCE tp , TP] of a sequence of rounds of SMP n [adv : SOURCE, TOUR]. Each round R of SMP n [adv : SOURCE,

As shown in[START_REF] Afek | Asynchrony from synchrony[END_REF] with the properties TOUR, TP, and PAIRS, several properties can be equivalent (i.e., each one can be implemented in SMPn[adv : ∅] under the control of an adversary constrained by any other one). Hence, if a property P is the "weakest", so are the properties equivalent to P .Collection des Publications Internes de l'Irisa c IRISA

This corresponds to a weakening of the system model ARW n,n-1 [fd : ∅] such that, from an operational point of view, a process computes its own result from its input and what it read from the memory before writing its input in the shared memory.Collection des Publications Internes de l'Irisa c IRISA

Collection des Publications Internes de l'Irisa c IRISA

This theorem extends a theorem on graph tournament by Landau[START_REF] Landau | On dominance relations and the structure of animal societies, III: The condition for score structure[END_REF] to the case where consecutive tournaments can be different.Collection des Publications Internes de l'Irisa c IRISA

This definition of PAIRS is slightly different but equivalent to the one given in[START_REF] Afek | Asynchrony from synchrony[END_REF].Collection des Publications Internes de l'Irisa c IRISA

Acknowledgments

This work has been partially supported by the French ANR project DISPLEXITY devoted to computability and complexity in distributed computing. Special thanks to D. Imbs and S. Rajsbaum for interesting discussions on distributed computing models.

Let us now show that SC = ∅. To that end, let us first observe that it follows from the intersection property of Σ that ∀ i, j, ∀ r, ∃k(i, j, r) such that k(i, j, r) r -→ i ∧ k(i, j, r) r -→ j. As {k(i, j, r)} r>0 ⊆ {1, ..., n}, it follows that there is some k ′ (i, j) which appears infinitely often in the sequence k(i, j, 1), k(i, j, 2), ... Hence, we have k ′ (i, j) ∞ i ∧k ′ (i, j) ∞ j. As this is true for any pair (i, j), it follows that the graph G, whose set of vertices is {1, ..., n} and edges are defined by the relation ∞ , has a single strongly connected component without input edges. As this strongly connected component defines the set of strongly correct processes, this set is not empty, which concludes the proof of the lemma.

The simulation algorithm is described in Figure 7. It is very close to the simulation of AMP n,n-1 [fd : Ω] on top of SMP n [adv : SOURCE] presented in Figure 5. It has the same local variables, except the variable missed i which is now useless. The value returned when qr i is read by a simulated process p i is now the current value of the set rec_f rom i . The only other difference appears at lines 9-10. The simulation of the simulated process p i (invocation of the procedure simulate() at lines 11) is now constrained by the predicate of line 9 which states that the messages that p i wants to send (the messages saved in msg_to_send i ) must be known by at all the simulators defining the current quorum of p i (set rec_f rom i ). When this is satisfied, the set of messages to be received by p i in the next invocation of simulate() is redefined (line 11) to include the last simulated messages sent to p i by processes p j such that j ∈ rec_f rom i .

initialization:

(1) ls_state i ← initial state of the local simulated algorithm; [START_REF] Afek | A king in two tournaments[END_REF]

when qr i is read: return(rec_from i ). According to the definition of SC and to the second part of QUORUM property, we have SC = ∅ and ∀i ∈ SC, ∀j ∈ {1, . . . , n} : i ∞ j. Let p i be a simulated process p i whose simulator is strongly correct. As its messages are always received by every process, they are received by the processes in its local set rec_f rom i . Moreover, as the simulation algorithm is a full information algorithm, it eventually receives from each process in rec_f rom i the messages whose it is simulating the sending. The condition of line 9 becomes then satisfied, and the simulator of p i is allowed to progress in the simulation of p i (line 11). Hence, no strongly correct simulator can block forever in the simulation of its simulated process p i .

According to (1) the intersection property of QUORUM, and (2) the fact that SC = ∅ implies that ∃r : ∀r ′ ≥ r, ∀i ∈ SC : {k : k r ′ i} ⊆ SC, it follows that ∀r > 0, ∀i ∈ {1, . . . , n} : {k : k r i} ∩ SC = ∅ (A). Moreover, there is a round after which no message from a weakly correct process reaches a strongly correct process (B). Finally, (predicate at line 9) to progress in the simulation, a simulator has to receive from each simulator in its current set rec_f rom i a copy of the messages msgs_to_send i whose it is simulating the sending (C). It follows from A, B, and C that, eventually, the predicate at line 9 of any weakly correct process remains false forever (because its set msgs_to_send i is never received by a strongly correct process). Consequently, there is a finite time after which, all weakly correct simulators stop progressing in the simulation (while they forever execute rounds, they never execute lines 10-12).

Collection des Publications Internes de l'Irisa c IRISA

A The Properties TP and PAIRS and their Source Extensions

A.1 Definition

In addition to TOUR, Afek and Gafni have defined two more properties, denoted TP (for traversal path) and PAIRS [START_REF] Afek | Asynchrony from synchrony[END_REF], defined as follows from the graphs G r introduced in Section 2.2.

• The property TP is similar to TOUR. It differs in the replacement of the directed edge constraint i r -→ j by the directed path constraint i r j meaning that there is a directed path from p i to p j in G r (i.e., at round r there is a path from p i to p j on which no message is removed by the adversary). Formally, the graphs G r defined by TP are such that: ∀r ≥ 1 : ∀ (i, j) : (i r j) ∨ (j r i).

• Let Cn2 be the number of combinations of 2 elements in a set of n elements (binomial coefficient), and σ() be a bijection from {0, . . . , Cn2 -1} into {(i, j) ∈ {1, . . . , n} 2 : i < j)}. PAIRS is similar to TOUR except that a round of TOUR is decomposed into C(n, 2) rounds of PAIRS 4 . During a round of PAIRS, the adversary suppresses all messages but one or both of the messages sent by the pair of processes associated by σ() with the current round number. The messages graphs G r associated with PAIRS are formally defined as follows:

A main result of [START_REF] Afek | Asynchrony from synchrony[END_REF] A.2 Adding a source to TP and PAIRS While the property TOUR is, at each round, on each pair of processes, this is not the case of the properties TP and PAIRS. Hence, the property SOURCE has to be customized to be appropriately associated with TP or PAIRS. More specifically we have the following.

• The eventual source property associated with TP is denoted SOURCE tp . It considers a path instead of an edge. Formally, it is defined a s follows: ∃s ∈ {1, . . . , n} : ∃r 0 ≥ 1 : ∀r ≥ r 0 : ∀ i ∈ {1, . . . , n} : (s r i).

• Similarly the intermittent source property associated with PAIRS is denoted SOURCE pairs . It preserves messages sent by a source s in every round r such that σ(r) involved s. Formally: ∃s ∈ {1, . . . , n} : ∃r 0 ≥ 1 : ∀r ≥ r 0 : σ(r mod Cn2) ∈ {(s, i), (i, s)} ⇒ (s r -→ i).