1 Introduction

Two challenging adversaries: failures and anonymity Due to failures, concurrent processes have to deal not only with finite asynchrony (i.e., finite but arbitrary process speed), but also with infinite asynchrony (i.e., process crashes). In this context, mutex-based synchronization becomes inoperative, and pioneering works in fault-tolerant distributed computing, e.g., [27, 31], have instead promoted the design of “concurrent reading while writing” algorithms [25, 32, 37].

This new approach to synchronizing concurrent accesses has given rise to novel progress conditions; namely wait-freedom, non-blocking, and obstruction-freedom. Consider a concurrent object O. Wait-freedom means that any operation on O must terminate if the invoking process does not crash [22]. The non-blocking progress condition, also named lock-freedom, states that at least one process that does not crash returns from all its operations on O [26]. In the case of obstruction-freedom, a process should return from its operation on O if it executes solo during a long enough period of time [23].

On the other hand, anonymous systems are characterized by the fact that processes have no identity, execute the exact same code and the same initialization of their local variables. Hence, they are – in a strong sense – identical [3, 39], and may only differ from their local input values.

Considering the previous adversaries that are crashes as well as anonymity, a fundamental question is the following: “Given some concurrent object, is it possible to implement this object despite the failures of processes and their anonymity?” If the answer is “yes”, we are interested in doing it with a small number of multi-writer/multi-reader (MWMR) atomic registers.Footnote 1 In this paper, we address this fundamental question, where the concurrent object is k-set agreement, and the progress condition under consideration is obstruction-freedom.

Consensus and k -set agreement The k-set agreement problem is introduced in [12]. This problem generalizes consensus, which corresponds to the case where \(k=1\). In the following, we use the notation (nk)-set agreement to make explicit the fact that we consider a system of n processes. Every participating process proposes a value, and must decide a value if it does not crash (termination). On the safety side, a decided value must be a value that was proposed by some process (validity), and at most k different values can be decided (agreement).

The case for obstruction-freedom Designing a deterministic solution to the consensus problem in a non-anonymous and asynchronous system prone to even a single crash is not possible, be the communication medium a message-passing system [17], or read/write registers [29]. More generally, if k or more processes may crash, there is no deterministic read/write algorithm able to solve (nk)-set agreement [7, 24, 35]. These impossibility results remain true in anonymous systems.

As we are interested in the computing power of pure read/write asynchronous crash-prone anonymous systems, we neither want to enrich the underlying system with additional power (e.g., synchrony assumptions, random numbers, or failure detectors [6]), nor impose constraints on the input vector collectively proposed by the processes [19]. As a consequence, to sidestep the above impossibility results, instead of wait-freedom or non-blocking, we consider in this paper the obstruction-freedom progress condition [23]. For (nk)-set agreement, this property establishes that a process decides a value only if it executes solo during a “long enough” period of time without interruption. The notion of x-obstruction-freedom [38] extends this idea to any group of at most x processes. The practical interest of obstruction-freedom is discussed in [16]. An in-depth study of complexity issues of obstruction-free algorithms is presented in [4].

Content and contributions of this paper: an historical perspective In this paper, we present an obstruction-free algorithm solving the (nk)-set agreement problem in an asynchronous anonymous read/write system where any number of processes may crash. Our algorithm employs \((n-k+1)\) MWMR atomic registers, i.e., exactly n registers for consensus. In the case of (nk)-set agreement, the best lower bound known so far [15] is \(\varOmega (\sqrt{\frac{n}{k}-2})\). The anonymous obstruction-free (nk)-set agreement algorithms presented in [13, 15] requires \(2(n-k)+1\) MWMR registers. Hence our algorithm provides a gain of \((n-k)\) registers.

For consensus, an algorithm is sketched in [41], which (as ours) required n MWMR atomic registers. Always in the case of consensus, Gelashvili [20] recently proved that n / 20 registers are necessary, and Zhu proved a lower bound of \(n-1\) registers for non-anonymous consensus [42]. As a consequence, the algorithm we present in this paper is up to an additive factor of 1 close to the best known lower bound for non-anonymous consensus.

In the repeated version of the (nk)-set agreement problem, processes participate in a sequence of (nk)-set agreement instances. We further show that a simple modification of our base construction solves this problem without additional registers. The authors of [15] prove that \((n-k+1)\) atomic registers are necessary to solve the repeated (nk)-set agreement problem in an anonymous system. As a consequence, our solution is space optimal.

A technical perspective The algorithms proposed in this paper are round-based. They follow the pattern “snapshot; local computation; write”, where the snapshot and write operations occur on \((n-k+1)\) MWMR registers. This pattern is reminiscent of the one named “look; compute; move” found in robot algorithms [18, 36]. Interestingly, in our base solution and in the x-obstruction-free variation, processes do not maintain any local information between successive rounds. In this sense, the two algorithms are locally memoryless.

In our base algorithm, a register contains a quadruplet consisting of a round number, two control bits, and a proposed value. The algorithm exploits a partial order over the quadruplets. The way a process computes a new quadruplet is the key of this algorithm. The variation for the repeated (nk)-set agreement problem requires each register to store two additional fields, one of them being the sequence number of the corresponding instance, the other one containing the values decided in the previous (nk)-set agreement instances. In the x-obstruction-free algorithm, the last field of a quadruplet is a set of values, allowing up to x processes to concurrently progress.

The base algorithm we present hereafter applies a locally memoryless variation of the following pattern: Each process executes a sequence of asynchronous rounds, until it sees two “identical” consecutive rounds. When this occurs, the process can decide a value, and no other process will be able to decide a different value in the next rounds. Multiple wait-free consensus algorithm were proposed in the past that apply this pattern (see e.g., [5, 14, 32,33,34]). These algorithms cover anonymous as well as non-anonymous systems, binary and multivalued consensus. Some use an eventual leader failure detector \(\varOmega \) [11], while others rely on randomization.

A universality perspective In addition to the anonymous algorithms for consensus and k-set agreement, we also introduce in this paper a universal construction [22]. This construction works with the obstruction-freedom progress condition, and applies to concurrent objects that can be implemented in anonymous systems with any number of MWMR atomic registers. It requires only n such registers.

This universal construction tells us that, in the case of the obstruction-freedom progress condition, distributed objects implementable anonymously with any number of MWMR atomic registers require in fact only n registers.

Furthermore, in regard to colorless tasks [8], that is distributed problems which do not require some form of symmetry breaking, we show that identifiers do not bring more computational power. A similar result for colorless tasks was recently presented in [40]. While our approach is constructive, the one described in [40] is based on topology.

Roadmap Section 2 presents the computing model and the definitions used in this paper. Section 3 depicts an anonymous obstruction-free algorithm solving consensus. This algorithm captures the essence of our solution. Its correctness is proved in Sect. 4. Section 5 extends it to solve (nk)-set agreement. Then, the case where (nk)-set agreement is used repeatedly is addressed in Sect. 6. In Sect. 7, we consider the x-obstruction-freedom progress condition, and present a solution using \((n-k+x)\) registers. The reduction results on the power of repeated anonymous consensus (universal construction) are presented in Sect. 8. Finally, Sect. 9 closes the paper.

Fig. 1
figure 1

The function \(\mathsf{sup}()\)

2 Computing model and problem definition

2.1 Computing model

Process model The distributed system consists of n asynchronous processes \(\{p_1,\ldots , p_n\}\). When considering a process \(p_i\), the integer i is called its index. Indexes are used to ease the exposition from an external observer point of view. Processes do not have identities and execute the very same code. It is assumed that they know the value of n.

Let \(\mathbb {T}\) denote the increasing sequence of time instants (observable only from an external point of view). At each time instant, a unique process is activated to execute a step. A step consists in a read or a write to some register (access to the shared memory) possibly followed by a finite number of internal operations (on local variables).

Up to \((n-1)\) processes may crash. Before crashing a process executes correctly its algorithm. After it crashed (if it ever does), a process executes no more step. From a terminology point of view, and given an execution, a faulty process is a process that crashes, and a correct process is a process that does not crash. No process knows if it is correct or faulty (this is because, before crashing, a faulty process behaves as a correct one).

Communication model In addition to processes, the computing model includes a communication medium made up of m multi-writer/multi-reader (MWMR) atomic registers (let us notice that anonymity prevents processes from using single-writer/multi-reader registers). Registers are encapsulated in an array denoted \( REG [1..m]\). The registers are atomic. This means that read and write operations appear as if they have been executed sequentially, and this sequence (a) respects the real-time order of non-concurrent operations, and (b) is such that each read returns the value written by the closest preceding write operation (or the initial value of the register if there is no preceding write operation) [28]. When considering the set of concurrent objects defined from a sequential specification, atomicity is named linearizability [26], and the sequence of operations is called a linearization. Moreover, the time instant at which an operation appears as being executed is called its linearization point.

From atomic registers to a snapshot object At the upper layer, where consensus and (nk)-set agreement are solved, we use the array \( REG [1..m]\) to construct a snapshot object [1]. This object, denoted \( REG \) hereafter, provides processes with the operations \(\mathsf{write}()\) and \(\mathsf{snapshot}()\). When a process invokes \( REG .\mathsf{write}(x,v)\), it deposits the value v in \( REG [x]\). When it invokes \( REG .\mathsf{snapshot}()\) it obtains the content of the whole array. The snapshot object is linearizable, i.e., every invocation of \( REG .\mathsf{snapshot}()\) appears as instantaneous. For the \( REG \) object, a linearization is a sequence of write and snapshot operations.

An anonymous non-blocking (thus obstruction-free) implementation of a snapshot object is described in [21]. This implementation does not require additional atomic registers. In the following, we consider that the snapshot object \( REG \) is implemented using this algorithm.

2.2 Consensus and (nk)-set agreement

Obstruction-free consensus A consensus object is a one-shot object that provides each process with a single operation denoted \(\mathsf{propose}()\). “One-shot” means that a process invokes \(\mathsf{propose}()\) at most once. When a process invokes \(\mathsf{propose}(v)\), we say that it “proposes v”. When the invocation of \(\mathsf{propose}()\) returns value \(v^\prime \), we say that the invoking process “decides \(v^\prime \)”.

A process executes “solo” when it keeps on executing while the other processes have halted their execution (at any point of their algorithm). In the context of the obstruction-free progress condition (see below the OF-termination property), the consensus problem is defined by the following properties, that is, to be correct, any obstruction-free algorithm must satisfy such properties.

  • Validity. If a process decides a value, this value was proposed by a process.

  • Agreement. No two processes decide different values.

  • OF-termination. If there is a time after which a correct process executes solo, it decides a value.

  • SV-termination. If a single value is proposed, all correct processes decide.

Validity relates outputs to inputs. Agreement relates the outputs. Termination states the conditions under which a correct process must decide. There are two cases. The first is related to obstruction-freedom. The second one is independent of the concurrency and failure pattern; it is related to the input value pattern.Footnote 2

Obstruction-free (nk) -set agreement An obstruction-free (nk)-set agreement object is a one-shot object which has the same validity, OF-termination, and SV-termination properties as consensus, and for which we replace the agreement property with:

  • Agreement. At most k different values are decided.

Section 3, that follows, describes a base algorithm to solve the obstruction-free anonymous consensus problem. Further in the paper, this algorithm is extended twice: first in Sect. 5 to solve (nk)-set agreement, then in Sect. 7, to address the x-obstruction-freedom progress condition (in lieu of obstruction-freedom).

Fig. 2
figure 2

Anonymous obstruction-free consensus

3 Obstruction-free anonymous consensus algorithm

The obstruction-free anonymous consensus algorithm is presented in Fig. 2. This algorithm relies on the \(\mathsf{sup}()\) function detailed in Fig. 1. As indicated in the Introduction, from a data structure point of view, its essence is captured by quadruplets written in the MWMR atomic registers.

Shared memory The shared memory is made up of a snapshot object \( REG \), composed of n MWMR atomic registers. Initially, each of these registers contains a quadruplet \(\langle 0, \mathtt{down}, \mathtt{false}, \bot \rangle \). The meaning of these fields is the following.

  • The first field, denoted rd, is a round number.

  • The second field, denoted \( {\ell }v{\ell } \) (level), has a value in \(\{\mathtt{up},\mathtt{down}\}\), where \(\mathtt{up}> \mathtt{down}\).

  • The third field, denoted \( cf{\ell } \) (conflict), is a boolean (initially equals to \(\mathtt{false}\)). We assume \(\mathtt{true}> \mathtt{false}\).

  • The last field, denoted \( va{\ell } \) holds a value. It is initialized to \(\bot \), a default value that cannot be proposed. We assume that the set of proposed values is totally ordered, and that \(\bot \) is smaller than any proposed value.

When considering the lexicographical order, it is easy to see that the set of all the possible quadruplets \(\langle rd, {\ell }v{\ell } , cf{\ell } , va{\ell } \rangle \) is totally ordered. This total order, and its reflexive closure, are denoted “<” and “\(\le \)”, respectively.

Notion of conflict and the function \(\mathsf{sup}()\) In Fig. 1, we define the function \(\mathsf{sup}()\). This function plays a central role in the algorithm. It takes a non-empty set of quadruplets T as input parameter, and returns a quadruplet, which is the supremum of T, defined as follows.

Let \(\langle r, {\ell }eve{\ell } , conf{\ell }ict , v \rangle \) be the maximal element of T according to the lexicographical order (line S1), and let tuples(T) be the set of tuples in T associated with the maximal round number r (line S2). The set T is conflicting if either \( conf{\ell }ict \) is true, or the set tuples(T) contains more than one element (line S3).

Function \(\mathsf{sup}(T)\) first checks whether T is conflicting (lines S2–S3). Then, at line S4, the function returns the tuple \(\langle r, {\ell }eve{\ell } , conf{\ell }ict (T), v\rangle \), where the flag \( conf{\ell }ict (T)\) indicates if the input set T is conflicting. Let us notice that, since \(\mathtt{true}>\mathtt{false}\), the quadruplet returned by \(\mathsf{sup}(T)\) is always greater than, or equal to, the greatest element in T, i.e., \(\mathsf{sup}(T) \ge \mathsf{max}(T)\).

The algorithm Our base construction is pretty simple, and consists in an appropriate management of the snapshot object \( REG \), so that the n quadruplets it contains (a) never allow validity or agreement to be violated, and (b) eventually allow termination under good circumstances (which occur when obstruction-freedom is satisfied or when a single value is proposed).

In Fig. 2, when a process \(p_i\) invokes \(\mathsf{proposes}(v_i)\), it enters a loop that it will exit at line 03 (provided it terminates) with the statement \(\mathsf{return}( va{\ell } )\), where \( va{\ell } \) is the decided value. After entering the loop, a process issues a snapshot and assigns the returned array to its local variable view[1..n] (line 02). Then, there are two main cases according to the value stored in view.

  • Case 1 (lines 03–05). All the entries of \(view_i\) contain the same quadruplet \(\langle r, {\ell }eve{\ell } , conf{\ell }ict , va{\ell } \rangle \), and \(r > 0\). Then, there are three sub-cases to consider.

    • Case 1.1. If the level is \(\mathtt{up}\) and the conflict is \(\mathtt{false}\), the invoking process decides the value \( va{\ell } \) (line 03).

    • Case 1.2. If now the level is \(\mathtt{down}\) and the conflict field is \(\mathtt{false}\), process \(p_i\) enters the next round by writing \(\langle r+1,\mathtt{up}, \mathtt{false}, val\rangle \) in the first entry of \( REG \) (line 04).

    • Case 1.3. If there is a conflict, \(p_i\) enters the next round by writing \(\langle r+1,\mathtt{down}, \mathtt{false}, val\rangle \) in the first entry of \( REG \) (line 05).

  • Case 2 (lines 06–08). Not all the entries of \(view_i\) are equal or, possibly, one of them contains the quadruplet \(\langle 0,-,-,- \rangle \). In such a case, \(p_i\) first calls the function \(\mathsf{sup}(view[1],\cdots ,view[n],\langle 1,\mathtt{down}, \mathtt{false}, v_i\rangle )\) by executing line 06. This call returns a quadruplet X greater than all the input quadruplets, or equal to the greatest of them. As we have seen previously, this quadruplet X may inherit or discover a conflict. Moreover, as the quadruplet \(\langle 1,\mathtt{down},\mathtt{false}, v_i\rangle \) is an input parameter of \(\mathsf{sup}()\), \(X. va{\ell } \) cannot equal \(\bot \). Since none of the predicates at lines 03–05 is satisfied, at least one entry of view[1..n] is different than X. Then process \(p_i\) writes X into \( REG [z]\), where, from its point of view, z is the first entry of \( REG \) whose content differs from X (lines 07–08).

The underlying operational intuition As indicated in the Introduction, the intuition that underlies the algorithm presented at Fig. 2 is similar to the one used in some non-anonymous consensus algorithms (e.g., [5, 32, 34]), namely if a process executes two consecutive rounds (scans) returning the same values, it can safely decide.

To understand the above observation, let us first consider the very simple case where a unique process \(p_i\) executes the algorithm. With its initial call to \( REG .\mathsf{snapshot}()\) at line 02, this process obtains a view in which all the elements are equal to \(\langle 0,\mathtt{down},\mathtt{false},\bot \rangle \). Hence, \(p_i\) executes line 06, where the invocation of \(\mathsf{sup}()\) returns the quadruplet \(\langle 1,\mathtt{down}, \mathtt{false},v_i\rangle \), that is written into \( REG [1]\) at line 08. Then, during the second round, \(p_i\) computes with the help of function \(\mathsf{sup}()\) again the quadruplet. \(\langle 1,\mathtt{down}, \mathtt{false},v_i\rangle \). This quadruplet is written into \( REG [2]\). The above steps continue until \(p_i\) writes \(\langle 1,\mathtt{down}, \mathtt{false},v_i\rangle \) in all the registers of \( REG [1..n]\). When this occurs, \(p_i\) obtains at line 02 a view where all the elements equal \(\langle 1,\mathtt{down},\mathtt{false}, v_i\rangle \). It consequently executes line 04 and writes \(\langle 2,\mathtt{up}, \mathtt{false},v_i\rangle \) in \( REG [1]\). Then, during the following rounds, process \(p_i\) writes \(\langle 2,\mathtt{up}, \mathtt{false}, v_i\rangle \) in the other registers of \( REG \), by executing line 08. When this is done, \(p_i\) obtains a snapshot containing solely \(\langle 2,\mathtt{up},\mathtt{false}, v_i\rangle \). When this occurs, process \(p_i\) executes line 03 where it decides the value \(v_i\).

Let us now consider the case where, while \(p_i\) is executing, another process \(p_j\) invokes \(\mathsf{propose}(v_j)\) with \(v_j=v_i\). It is easy to see that, in such a case, \(p_i\) and \(p_j\) collaborate to fill in \( REG \) with the same quadruplet \(\langle 2,\mathtt{up}, \mathtt{false}, v_i\rangle \). If \(v_j\ne v_i\), depending on the concurrency pattern, a conflict may occur. For instance, it occurs if \( REG \) contains both \(\langle 1,\mathtt{down},\mathtt{false}, v_i\rangle \) and \(\langle 1,\mathtt{down}, \mathtt{false},v_j\rangle \). If a conflict appears, it will be propagated from round to round, until a process executes alone a higher round.

Remark 1

Let us first notice that no process needs to memorize in its local memory the values that it will use during the next rounds. Not only processes are anonymous, but their code is also memoryless (no persistent variables). The snapshot object \( REG \) constitutes the whole memory of the system. Hence, as defined in the Introduction, the algorithm is locally memoryless. In this sense, and from a locality point of view, it has a “functional” flavor.

Remark 2

Let us now assume the n-bounded concurrency model [2, 30]. This model is made up of an arbitrary number of processes, but, at any time, there are at most n processes executing steps. This allows processes to leave the system and other processes to join it as long as the concurrency degree does not exceed n.

The previous algorithm works without modification in such a model. A proposed value is now a value proposed by any of the N processes that participate in the algorithm. Hence, if \(N > n\), the number of proposed values can be greater than the upper bound n on the concurrency degree. This versatility dimension of the algorithm is a direct consequence of the previous locally memoryless property.

4 Proof of the algorithm

This section presents a correctness proof of the previous obstruction-free anonymous consensus algorithm. After a few definitions provided in Sect. 4.1, Sect. 4.2 shows that a relation “\(\sqsupseteq \)” defined over the quadruplets is a partial order. This relation is central to prove the key properties of the algorithm. Such properties are established in Sects. 4.3 and 4.4. Then, based on these properties, Sect. 4.5 shows that the algorithm is correct.

4.1 Definitions and notations

Let \(\mathcal {E}\) be the universal set of quadruplets that can be written in \( REG \). Given \(X \in \mathcal {E}\), its four fields are denoted X.rd, \(X. {\ell }v{\ell } \), \(X. cf{\ell } \) and \(X. va{\ell } \), respectively. Relations > and \(\ge \) refer to the lexicographical ordering over \(\mathcal {E}\). In addition, where appropriate, we consider that the array view[1..n] is the set \(\{view[1], \cdots , view[n]\}\).

Definition 1

Let \(X, Y \in \mathcal {E}\).

$$\begin{aligned} X \sqsupset Y~ \mathop {=}\limits ^{ def }~ (X>Y)\wedge [(X.rd > Y.rd)\vee (X. cf{\ell } )] \end{aligned}$$

We write \(X \sqsupset Y\) (X “dominates” Y) when (a) X is lexicographically greater than Y and (b) the round of X is greater than the round of Y, or X indicates a conflict (in this case, as \(X>Y\), we have \(X.rd = Y.rd\)).

At the operational level the algorithm ensures that the quadruplets it generates are totally ordered by relation >. Differently, the relation \(\sqsupset \) (which is a partial order on these quadruplets, see Sect. 4.2) captures the relevant part of this total order, and is consequently the key cornerstone on which the proof of the algorithm relies.

When \(X \sqsupset Y\) holds, we say “X strictly dominates Y”. Similarly, “X dominates Y”, denoted \(X \sqsupseteq Y\), means that \((X \sqsupset Y)\) or \((X=Y)\) holds. Relations \(\sqsubset \) and \(\sqsubseteq \) are defined in the natural way.

Definition 2

Given a set of quadruplets T, T is homogeneous if it contains a single element, say X. We then write it “T is \(\mathcal {H}(X)\)”.

Notation 1

The value of the local variable view of a process \(p_i\) at time \(\tau \), is denoted \(view_i^\tau \). Similarly the value of an atomic register \( REG [x]\) at time \(\tau \) is denoted \( REG ^\tau [x]\), and the value of \( REG \) at time \(\tau \) is denoted \( REG ^\tau \).

Notation 2

\(\mathcal {W}(x,X)\) denotes the writing of a quadruplet X in the register \( REG [x]\).

Definition 3

We say “a process \(p_j\) covers \( REG [x]\) at time \(\tau \)” when its next non-local step after time \(\tau \) is \(\mathcal {W}(x,X)\), where X is the quadruplet which is written. In this case we also say “\(\mathcal {W}(x,X)\) covers \( REG [x]\) at time \(\tau \)” or “\( REG [x]\) is covered by \(\mathcal {W}(x,X)\) at time \(\tau \)”.

Let us notice that if \(p_j\) covers \( REG [x]\) at time \(\tau \), then \(\tau \) necessarily lies between the last snapshot issued by \(p_j\) at line 02 and its planned write \(\mathcal {W}(x,X)\) that will occur at line 04, 05, or 08.

4.2 The relation \(\sqsupseteq \) is a partial order

Lemma 1

\(\sqsupseteq \) is a partial order.

Proof

The antisymmetry of relation \(\sqsupseteq \) follows from the fact that > is an order.

To prove transitivity, let us assume that \(X \sqsupseteq Y\) and \(Y \sqsupseteq Z\). We have to show that \(X \sqsupseteq Z\). If \(X=Y\) or \(Y=Z\), the claim follows trivially. Hence, assume that \(X \sqsupset Y\) and \(Y \sqsupset Z\) and let us prove that \(X \sqsupset Z\). Observe that, due to the definition of \(\sqsupset \), we have \(\big ((X \sqsupset Y) \wedge (Y \sqsupset Z)\big ) ~\Rightarrow ~ \big ((X> Y) \wedge (Y >Z)\big )\). As \((X> Y) \wedge (Y >Z)\), it follows by transitivity of > that \(X > Z\). To prove \(X \sqsupset Z\), it thus remains to show that \(\big ((X.rd > Z.rd) \vee (X. cf{\ell } )\big )\).

Let us observe that, due to the definition of \(\sqsupset \), we have \((X \sqsupset Y)~\Rightarrow ~~\big ((X.rd > Y.rd) \vee (X. cf{\ell } )\big )\). If \((X. cf{\ell } )\) then the claim follows trivially. So assume in following that \((X. cf{\ell } = \mathtt{false})\). Therefore, \((X.rd > Y.rd)\). But as \((Y > Z)\), we have \((Y.rd \ge Z.rd)\). By transitivity this yields to \((X.rd > Z.rd)\). This, combined with the fact that \(X > Z\) showed above, implies that \(X \sqsupset Z\). \(\square \)

4.3 Extracting the relations \(\sqsupset \) and \(\sqsupseteq \) from the algorithm

The definition of function \(\mathsf{sup}()\), which takes a non-empty set of quadruplets as input parameter was given in Fig. 1. The next lemma shows that the quadruplet returned by a call to \(\mathsf{sup}(T)\), dominates all the elements in T.

Lemma 2

Let T be a non-empty set of quadruplets. Then, \(\forall ~X \in T: \mathsf{sup}(T) \sqsupseteq X\).

Proof

Let \(X \in T\) and \(S=\mathsf{sup}(T)\). We have to prove that \(S \sqsupseteq X\). Let us first observe that, as \(S=\mathsf{sup}(T) \ge \mathsf{max}(T) \ge X\), we have \(S \ge X\). If \(S = X\) then the lemma follows immediately. So let us assume in the following that \(S > X\). To prove \(S \sqsupset X\) , we need to show that \(\big ((S. cf{\ell } ) \vee (S.rd > X.rd)\big )\). Assume that \((S. cf{\ell } = \mathtt{false})\) and let us prove that \((S.rd > X.rd)\).

As \((\mathsf{sup}(T). cf{\ell } = \mathtt{false})\), it follows from the code in Fig. 1 that \( conf{\ell }ict (T)=\mathtt{false}\) and \(\mathsf{sup}(T) = \mathsf{max}(T)\). Therefore, \(\mathsf{sup}(T)\) is the unique quadruplet of T associated with the round number \(\mathsf{sup}(T).rd\). All other elements of T if any have a strictly smaller round number. Therefore, \(S.rd > X.rd\). This establishes the claim. \(\square \)

Lemma 3

If \(p_i\) executes \(\mathcal {W}(-,Y)\) at time \(\tau \), then for every \(X \in view_i^{\tau }: Y \sqsupseteq X\).

Proof

We consider two cases according to the line at which the write occurs.

  • Y is written at line 04 or 05. It follows that \(Y.rd = (\mathsf{max}(view_i^\tau ).rd)+1\). Therefore, for every \(X \in view_i^{\tau }: Y.rd > X.rd\). Hence \(Y \sqsupset X\).

  • Y is written at line 08. In such a case, due to the call to function \(\mathsf{sup}()\) at line 06, the quadruplet Y written by \(p_i\) is equal to \(\mathsf{sup}(T)\) where T is defined as the set \(\{view_i^{\tau }[1],\cdots ,view_i^{\tau }[n],\langle 1,\mathtt{down}, \mathtt{false}, v_i \rangle \}\). Let us then apply Lemma 2. It follows that for every quadruplet X in \(view_i^{\tau }\), we have \(Y=\mathsf{sup}(T) \sqsupseteq X\).\(\square \)

Lemma 4

Let us assume that no process is covering the register \( REG [x]\) at time \(\tau \). For every write \(\mathcal {W}(-,X)\) that (a) occurs after \(\tau \) and (b) was not covering a register of \( REG \) at time \(\tau \), we have \(X \sqsupseteq REG ^{\tau }[x]\).

Proof

The proof is by contradiction. Let \(p_i\) be the first process that executes a write \(\mathcal {W}(-,X)\) contradicting the lemma. This means that \(\mathcal {W}(-,X)\) is not covering a register of \( REG \) at time \(\tau \) and \(X \not \sqsupseteq REG ^{\tau }[x]\). Let this write occur at time \(\tau _2 > \tau \). Thus, all writes that take place between time \(\tau \) and time \(\tau _2\) comply with the lemma. We derive a contradiction by showing that \(X \sqsupseteq REG ^{\tau }[x]\).

Let \(\tau _1 < \tau _2\) be the linearization time of the last snapshot taken by \(p_i\) (line 02) before executing \(\mathcal {W}(-,X)\). Since \(\mathcal {W}(-,X)\) was not covering a register of \( REG \) at time \(\tau \), the snapshot preceding this write was necessarily taken after \(\tau \). That is, \(\tau _1 > \tau \), and we have \(\tau _2> \tau _1 > \tau \).

According to Lemma 3, \(X \sqsupseteq view_i^{\tau _2}[x]\). But since the snapshot returning \(view_i^{\tau _2}\) is linearized at \(\tau _1\), it follows that \(view_i^{\tau _2}= REG ^{\tau _1}\). Therefore, we have \(X \sqsupseteq REG ^{\tau _1}[x]\) (let us call this assertion R).

In the following we show that \( REG ^{\tau _1}[x] \sqsupseteq REG ^{\tau }[x]\). If \( REG [x]\) was not updated between time \(\tau \) and time \(\tau _1\), then \( REG ^{\tau _1}[x] = REG ^{\tau }[x]\) and the claim follows. Otherwise, if \( REG [x]\) was updated between \(\tau \) and \(\tau _1\), the content of \( REG ^{\tau _1}[x]\), let it be Y, is the result of a write \(\mathcal {W}(x,Y)\) that occurred between \(\tau \) and \(\tau _1\) and that was not covering a register of \( REG \) at time \(\tau \) (let us remember that no write is covering \( REG [x]\) at time \(\tau \), which is crucial in the proof). We assumed above that \(\tau _2\) is the first time at which the lemma is contradicted. Hence the write \(\mathcal {W}(x,Y)\), which occurs before \(\tau _2\), complies with the requirements of the lemma. It follows that \(Y \sqsupseteq REG ^{\tau }[x]\), and we thus have \( REG ^{\tau _1}[x] \sqsupseteq REG ^{\tau }[x]\).

But it was shown above (see assertion R) that \(X \sqsupseteq REG ^{\tau _1}[x]\). Hence, due to the transitivity of the relation \(\sqsupseteq \) (Lemma 1), we obtain \(X \sqsupseteq REG ^{\tau }[x]\), a contradiction that concludes the proof of the lemma. \(\square \)

Lemma 5

Let \(\tau \) and \(\tau ^\prime \ge \tau \) be two time instants. If \( REG ^{\tau ^\prime }\) is \(\mathcal {H}(Y)\), then there exists \(X \in REG ^{\tau }\) such that \(Y \sqsupseteq X\).

Proof

If \( REG ^{\tau ^\prime }= REG ^{\tau }\), the lemma holds trivially. So let us assume in the following that \( REG ^{\tau ^\prime } \ne REG ^{\tau }\) which means that a write happens between \(\tau \) and \(\tau ^\prime \).

If \(\langle 0, \mathtt{down}, \mathtt{false}, \bot \rangle \in REG ^{\tau }\), as every quadruplet Y written in \( REG \) is such that \(Y.rd \ge 1\) (line 04,05, or lines 06–08), we have \(Y \sqsupset \langle 0, \mathtt{down}, \mathtt{false}, \bot \rangle \).

So, let us assume that \(\langle 0, \mathtt{down}, \mathtt{false}, \bot \rangle \not \in REG ^{\tau }\) and consider the last write in \( REG \) before \(\tau \). Assume this happens at \(\tau ^{-} \le \tau \) and let \(p_i\) be the writing process. Process \(p_i\) has no write covering a register of \( REG \) at time \(\tau ^{-}\). Consequently, at most \((n-1)\) processesFootnote 3 have a write covering a register of \( REG \) at time \(\tau ^{-}\). Hence, there exists \(x \in \{1, \ldots , n\}\) such that no write is covering \( REG [x]\) at time \(\tau ^{-}\). Let \(X= REG ^{\tau ^{-}}[x]= REG ^{\tau }[x]\). If \(X=Y\) then the claim of the lemma follows trivially. So assume in the following that \(X \ne Y\). Since \( REG ^{\tau ^{-}}[x]=X\), \( REG ^{\tau ^{\prime }}[x]=Y\) and \(Y \ne X\), there is necessarily a write \(\mathcal {W}(x,Y)\) that occurred between \(\tau ^-\) and \(\tau ^\prime \). As this write was not covering a register of \( REG \) at time \(\tau ^{-}\), it follows (according to Lemma 4) that \(Y \sqsupseteq X\), which proves the lemma. \(\square \)

The two following lemmas are corollaries of Lemma 5.

Lemma 6

If \( REG ^{\tau }\) is \(\mathcal {H}(X)\), \( REG ^{\tau ^\prime }\) is \(\mathcal {H}(Y)\), and \(\tau ^\prime \ge \tau \), then \(Y \sqsupseteq X\).

Lemma 7

If \( REG ^{\tau }\) is H(X), \( REG ^{\tau ^\prime }\) is \(\mathcal {H}(Y)\), \(\tau ^\prime \ge \tau \), \((Y.rd=X.rd)\) and \((\lnot Y. cf{\ell } )\) then \((Y. va{\ell } =X. va{\ell } )\).

Proof

According to Lemma 6, \(Y \sqsupseteq X\). If \(Y=X\) then the claim follows immediately. So let us assume \(Y \sqsupset X\). As \((Y.rd=X.rd)\) and \((\lnot Y. cf{\ell } )\), the definition of \(\sqsupseteq \) implies that \(Y. va{\ell } =X. va{\ell } \). \(\square \)

4.4 Exploiting homogeneous snapshots

Lemma 8

\([(X \in REG ^{\tau }) ~\wedge ~ (X. {\ell }v{\ell } =\mathtt{up})]\) \(\Rightarrow \) \((\exists \tau ^\prime < \tau :\) \(REG^{\tau ^\prime }\) is \(\mathcal {H}(Z) ~\wedge ~ Z=\langle X.rd-1, \mathtt{down}, \mathtt{false}, X. va{\ell } \rangle )\)

Proof

We first show the existence of some process that writes a tuple \(X^\prime = \langle X.rd, X. {\ell }v{\ell } , \mathtt{false}, X. va{\ell } \rangle \) into \( REG \). Depending on the value of \(X. cf{\ell } \), there are two cases to consider.

  • If \(X. cf{\ell } =\mathtt{false}\), then let \(X^\prime =X\). Since \(X. {\ell }v{\ell } =X^\prime . {\ell }v{\ell } =\mathtt{up}\), X was necessarily written into \( REG \) by some process (let us recall that the initial value of each register of \( REG \) is \(\langle 0, \mathtt{down}, \mathtt{false}, \bot \rangle \)).

  • If \(X. cf{\ell } = \mathtt{true}\), let us consider the time \(\tau _1\) at which X was written for the first time into \( REG \), say by \(p_i\). Since \(X. {\ell }v{\ell } =\mathtt{up}\), both \(\tau _1\) and \(p_i\) are well defined. This write of X happens necessarily at line 08 (If it was at line 04 or 05, we would have \(X. cf{\ell } = \mathtt{false}\)). Therefore, X was computed at line 06 by function \(\mathsf{sup}()\). Namely we have \(X=\mathsf{sup}(T)\), where the set T is equal to \(\{view^{\tau }[1],\cdots , view^{\tau }[n], \langle 1,\mathtt{down},\mathtt{false}, v_i\rangle \}\). Observe that \(X \not \in T\), otherwise X would not be written for the first time at \(\tau _1\). Let \(X^\prime =\mathsf{max}(T)\). Since \(X \not \in T\), it follows that \(X \ne X^\prime \). Due to line S4 of the function \(\mathsf{sup}()\), X and \(X^\prime \) differ only in their conflict field. Therefore, as \(X. cf{\ell } =\mathtt{true}\), it follows that \(X^\prime . cf{\ell } =\mathtt{false}\). Finally, as \(X^\prime . {\ell }v{\ell } =\mathtt{up}\) and all registers of \( REG \) are initialized to \(\langle 0, \mathtt{down}, \mathtt{false}, \bot \rangle \), it follows that \(X^\prime \) was necessarily written into \( REG \) by some process.

In both cases, there exists a time at which a process writes \(X^\prime = \langle X.rd, X. {\ell }v{\ell } , \mathtt{false}, X. va{\ell } \rangle \) into \( REG \). Let us consider the first process \(p_i\) that does so. This occurs at some time \(\tau _2 < \tau \). As \(X^\prime . {\ell }v{\ell } =\mathtt{up}\), this write can occur only at line 04 or line 08.

We first show that this write occurs necessarily at line 04. Assume for contradiction that the write of \(X^\prime \) into \( REG \) happens at line 08. In this case, the quadruplet \(X^\prime \) was computed at line 06. Therefore, \(X^\prime = \mathsf{sup}(T)\) where the set T is equal to \(\{view^{\tau _2}[1],\cdots , view^{\tau _2}[n], \langle 1,\mathtt{down},\mathtt{false}, v_i\rangle \}\). Observe that \(\mathsf{sup}(T)\) and \(\mathsf{max}(T)\) can differ only in their conflict field. As \(\mathsf{sup}(T). cf{\ell } =X^\prime . cf{\ell } =\mathtt{false}\), it follows that \(X^\prime = \mathsf{sup}(T)= \mathsf{max}(T)\). Consequently, \(X^\prime \in view^{\tau _2}\). That is, \(p_i\) is not the first process that writes \(X^\prime \) in \( REG \), contradiction. Therefore, the write necessarily happens at line 04.

From the precondition at line 04, \(view^{\tau _2}\) is \(\mathcal {H}(\langle X^\prime .rd-1, \mathtt{down}, \mathtt{false}, X^\prime . va{\ell } \rangle )\), and the lemma holds. \(\square \)

Lemma 9

\([( REG ^{\tau }\) is \(\mathcal {H}(X))\) \(\wedge \) \((X. {\ell }v{\ell } =\mathtt{up})\) \(\wedge \) \((\lnot X. cf{\ell } )\) \(\wedge \) \(( REG ^{\tau ^\prime }\) is \(\mathcal {H}(Y))\) \(\wedge \) \((Y.rd \ge X.rd)]\) \(\Rightarrow \) \((Y. va{\ell } =X. va{\ell } )\)

Proof

The proof is by induction on Y.rd. Let us first assume that \(Y.rd= X.rd\), for which we consider two cases.

  • (Case \(\tau \ge \tau ^\prime \))  Since \(X. cf{\ell } =\mathtt{false}\), it follows from Lemma 7 that \(Y. va{\ell } =X. va{\ell } \).

  • (Case \(\tau ^\prime > \tau \))  Lemma 6 tells us that \(Y \sqsupseteq X\). As \(Y.rd=X.rd\), it follows that \(Y. {\ell }v{\ell } \ge X. {\ell }v{\ell } =\mathtt{up}\), and consequently \(Y. {\ell }v{\ell } =\mathtt{up}\). Thus, \( REG ^{\tau ^\prime }\) is \(\mathcal {H}(Y)\), \(Y. {\ell }v{\ell } =\mathtt{up}\) and \(Y.rd=X.rd\). According to Lemma 8, this implies that there is \(\tau _1 < \tau \) and \(\tau _1^\prime <\tau ^\prime \) such that \(REG^{\tau _1}\) is \(\mathcal {H}(\langle X.rd-1, \mathtt{down}, \mathtt{false}, X. va{\ell } \rangle )\) and \(REG^{\tau _1^\prime }\) is \(\mathcal {H}(\langle Y.rd-1, \mathtt{down}, \mathtt{false}, Y. va{\ell } \rangle )\). From Lemma 6, we have

    • either \(\langle X.rd-1, \mathtt{down}, \mathtt{false}, X. va{\ell } \rangle \sqsupseteq \langle Y.rd-1, \mathtt{down}, \mathtt{false}, Y. va{\ell } \rangle \),

    • or symetrically \(\langle Y.rd-1, \mathtt{down}, \mathtt{false}, Y. va{\ell } \rangle \sqsupseteq \langle X.rd-1, \mathtt{down}, \mathtt{false}, X. va{\ell } \rangle \).

    Since by assumption \(X.rd=Y.rd\), we obtain \(X. va{\ell } =Y. va{\ell } \).

For the induction step, let assume that the lemma is true up to \(Y.rd=\rho \ge r\), and let us prove it for \(\rho +1\). To this end, we have to show that \(Y. va{\ell } =X. va{\ell } \) for every Y that is written in \( REG \) with \(Y.rd=\rho +1\). Let us assume by contradiction that \(Y. va{\ell } \ne X. va{\ell } \) and let \(p_i\) be the first process that writes \(\langle \rho +1, -,-, Y. va{\ell } \rangle \) into \( REG \). This happens at line 04 or 05. In all cases, this implies that, at this moment, \(view_j\) is \(\mathcal {H}(\langle \rho , -, -,Y. va{\ell } \rangle )\). But, according to the induction assumption, this implies \(Y. va{\ell } =X. va{\ell } \), a contradiction which completes the proof of the lemma. \(\square \)

4.5 Proof of the algorithm: using the previous lemmas

Lemma 10

No two processes decide different values.

Proof

Let r be the smallest round in which a process decides, \(p_i\) and \( va{\ell } \) being the deciding process and the decided value, respectively. There is a time \(\tau \) at which \(view_i^\tau \) is \(\mathcal {H}(\langle r, \mathtt{up},\mathtt{false}, va{\ell } \rangle )\). Due to Lemma 9, every homogeneous snapshot starting from round r is necessarily associated with the value \( va{\ell } \). Therefore, only this value can be decided in any round higher than r. Since r was assumed to be the smallest round in which a decision occurs, the consensus agreement property follows. \(\square \)

Lemma 11

For every quadruplet X that is written in \( REG \), \(X. va{\ell } \) is a value proposed by some process.

Proof

Let us assume by contradiction that \(X. va{\ell } =v\) was not proposed by a process, and let \(p_i\) be the first process that writes X into \( REG \). We consider two cases according to the line at which the write occurs.

Assume first that v is written to \( REG \) at either line 04 or line 05. In this case, \(p_i\) obtained a view of \( REG \) in which at least some register contains the value v. According to the predicate of these two lines, the round number associated with v is necessarily greater than 0 which implies that v was previously written into \( REG \) and was not there initially. But this means that \(p_i\) is not the first process which writes v into \( REG \), a contradiction.

Now, consider that v is written at line 08. In such a case, the quadruplet X, where \(X. va{\ell } =v\), was returned by a call to \(\mathsf{sup}(view[1],\cdots ,view[n], \langle 1,\mathtt{down},\mathtt{false}, v_i\rangle )\). It follows that v is either \(v_i\), the proposal of \(p_i\), or some value that was previously written by another process. But, by assumption, \(p_i\) is assumed to be the first process to write v. Hence, we know that \(v=v_i\). \(\square \)

Lemma 12

A decided value is a proposed value.

Proof

If a process decides a value v, it does it at line 03. Hence, according to the predicate of line 03, the round number associated with this value is greater than 0 which means that v was necessarily written into \( REG \) by some process. It then follows from Lemma 11, that v was proposed by a process, which establishes the claim. \(\square \)

Lemma 13

Let T be a non-empty set of quadruplets. For every \(T^\prime \subseteq T: \mathsf{sup}(T^\prime \cup \{\mathsf{sup}(T)\})=\mathsf{sup}(T)\).

Proof

Let \(S= \mathsf{sup}(T)\). Hence S.rd is the highest round number in T. Moreover, S is greater than, or equal to, any quadruplet in T. Hence, \(\mathsf{max}(T^\prime \cup \{S\})=S\). Therefore, combined with the the definition of \(\mathsf{sup}()\), we have: \(\mathsf{sup}(T^\prime \cup \{S\})= \langle S.rd, S. {\ell }v{\ell } , conf{\ell }ict (T^\prime \cup \{S\}) , S. va{\ell } \rangle \). Thus, in order to prove that \(\mathsf{sup}(T^\prime \cup \{S\})=S\), we need to show that \( conf{\ell }ict (T^\prime \cup \{S\}) =S. cf{\ell } \). Depending on the value of \(S. cf{\ell } \), there are two cases to consider.

  • (Case \(S. cf{\ell } = \mathtt{true}\))  As \(S = \mathsf{max}(T^\prime \cup \{S\})\) and due to the definition of \( conf{\ell }ict ()\) (line S3 in Fig. 1), \(S. cf{\ell } = \mathtt{true}\) implies that \( conf{\ell }ict (T^\prime \cup \{S\}) = \mathtt{true}\).

  • (Case \(S. cf{\ell } =\mathtt{false}\))  Since \(S=\mathsf{sup}(T)\), \(S. cf{\ell } =\mathtt{false}\) implies that \(|tuples(T)=1|\). It follows that S has a round number that is strictly greater than any other element of T. As \(T^\prime \subseteq T\), it follows that S is the only quadruplet in \(T^\prime \cup \{S\}\) with a round number equal to S.rd. Hence, \(|tuples(T^\prime \cup \{S\})=1|\). Since we assumed \(S. cf{\ell } =\mathtt{false}\) and \(S = \mathsf{max}(T^\prime \cup \{S\})\), it follows that \( conf{\ell }ict (T^\prime \cup \{S\}) = \mathtt{false}\).

From the above case analysis, we obtain that \( conf{\ell }ict (T^\prime \cup \{S\}) = S. cf{\ell } .\) \(\square \)

Lemma 14

If there is a time after which a process executes solo, it decides a value.

Proof

Assume that \(p_i\) eventually runs solo, we need to show that \(p_i\) decides. There exists a time \(\tau \), after which no other process than \(p_i\) writes into \( REG \). Let \(\tau ^\prime \ge \tau \) be the first time at which \(p_i\) takes a snapshot after \(\tau \). This snapshot is well defined, as \(p_i\) runs solo after \(\tau \) and the implementation of atomic snapshot is obstruction-free. Let \(S=\mathsf{sup}(view_i^{\tau ^\prime }[1],\cdots ,view_i^{\tau ^\prime }[n], \langle 1,\mathtt{down}, \mathtt{false}, v_i\rangle )\).

Let us first show that there is a time after \(\tau \) at which \( REG \) is \(\mathcal {H}(S)\).

  • If \( REG ^{\tau ^\prime }\) is \(\mathcal {H}(S)\), we are done.

  • If \( REG ^{\tau ^\prime }\) is not \(\mathcal {H}(S)\), \(p_i\) executes line 06 and computes S. Then it writes S in an entry of \( REG \) (containing a value different from S), and re-enters the loop. If \( REG \) is then \(\mathcal {H}(S)\), we are done. Otherwise, \(p_i\) executes again line 06 and, due to Lemma 13, the quadruplet computed by the function \(\mathsf{sup}()\) is equal to S. It follows that after a finite number of iterations of the loop, \( REG \) is \(\mathcal {H}(S)\).

When \( REG \) is \(\mathcal {H}(S)\), we have the following.

  • If \(S=\langle -, \mathtt{up}, \mathtt{false}, - \rangle \), \(p_i\) decides in line 03.

  • If \(S=\langle r, \mathtt{down}, \mathtt{false}, va{\ell } \rangle \), then \(p_i\) writes \(Y=\langle r+1, \mathtt{up}, \mathtt{false}, va{\ell } \rangle \) in line 04. Using the same argument as above, there is a time at which \( REG \) becomes \(\mathcal {H}(Y)\), and the previous case holds.

  • If \(S=\langle r, -, \mathtt{true}, va{\ell } \rangle \), then \(p_i\) writes \(Y=\langle r+1, \mathtt{down}, \mathtt{false}, va{\ell } \rangle \) in line 05. Then \(p_i\) keeps writing Y in the following iterations until \( REG \) becomes \(\mathcal {H}(Y)\), and the previous case holds.

Hence, in all cases \(p_i\) eventually decides. \(\square \)

Lemma 15

If a single value is proposed, all correct processes decide.

Proof

Let us assume that all processes propose the same value v. It follows that all the processes keep writing \(X= \langle 1, \mathtt{down}, \mathtt{false}, v \rangle \) until \( REG \) becomes \(\mathcal {H}(X)\). Then, once every register of \( REG \) has been updated at least once, the processes start writing \(Y= \langle 2, \mathtt{up}, \mathtt{false}, v \rangle \) until \( REG \) is \(\mathcal {H}(Y)\) and v. When this occurs, v is decided. \(\square \)

Theorem 1

The algorithm presented in Fig.  2 solves the obstruction-free consensus problem.

Proof

The proof follows directly from the conjunction of Lemma 10 (Agreement), Lemma 12 (Validity), Lemma 14 (OF-Termination), and Lemma 15 (SV-Termination). \(\square \)

5 From consensus to (nk)-set agreement

The algorithm Our previous obstruction-free consensus algorithm provides us “for free” with an obstruction-free solution to the (nk)-set agreement problem. The only difference lies in the size of the snapshot object \( REG \), which is now an array of \((n-k+1)\) MWMR atomic registers instead of an array of n MWMR atomic registers.

Theorem 2

Assuming an underlying snapshot object composed of \((n-k+1)\) MWMR atomic registers, the algorithm of Fig. 2 solves the obstruction-free (nk)-set agreement problem.

Proof

The arguments for the validity and liveness properties are the same as the ones of the consensus algorithm since they do not depend on the size of \( REG \).

As far as the k-set agreement property is concerned (no more than k different values are decided), we have to show that \((n-k+1)\) registers are sufficient. To this end, let us consider the \((k-1)\) first decided values, where the notion “first” is defined with respect to the linearization time of the snapshot invocation (line 02) that immediately precedes the invocation of the corresponding deciding statement (\(\mathsf{return}()\) at line 03). Let \(\tau \) be the time just after the linearization of these \((k-1)\) “deciding” snapshots. Starting from \(\tau \), at most \((n-(k-1))=(n-k+1)\) processes access the array \( REG \), which is made up of exactly \((n-k+1)\) registers. It follows that, after time \(\tau \), these \((n-k+1)\) processes execute the algorithm of Fig. 2, with the help of a snapshot object of size \((n-k+1)\). Hence, from \(\tau \), these at most \((n-k+1)\) processes execute actually an anonymous obstruction-free consensus algorithm, during which they can decide at most one more value. It follows that at most k values are decided by the n processes. \(\square \)

6 From one-shot to repeated (nk)-set agreement

6.1 The repeated (nk)-set agreement problem

In the repeated (nk)-set agreement problem, processes execute a sequence of (nk)-set agreements. More precisely, a process invokes sequentially the operation \(\mathsf{propose}(1,v)\), then \(\mathsf{propose}(2,v')\), etc., where \(1, 2, \ldots \) stands for the sequence number of the (nk)-set agreement instance, and \(v, v', \ldots \) is the value the process proposes to this instance.

It would be possible to associate a specific instance of the base algorithm described in Fig. 2 with each sequence number, but this would require \((n-k+1)\) atomic read/write registers per instance. The next section shows that in fact the repeated problem can be solved with only \((n-k+1)\) atomic registers. According to the complexity results of [15], it follows that this algorithm is optimal in regard to the number of atomic read/write registers it uses. This closes the discussion regarding the space complexity of the repeated form of the (nk)-set agreement problem.

6.2 Adapting the algorithm

From quadruplets to sextuplets Instead of a quadruplet, the registers of the snapshot object \( REG \) now contains a sextuplet \(X=\langle sn, rd, {\ell }v{\ell } , cf{\ell } , va{\ell } , dcd \rangle \). The four fields X.rd, \(X. {\ell }v{\ell } \), \(X. cf{\ell } \), and \(X. va{\ell } \) are the same as before. The additional field X.sn is a sequence number. The other additional field X.dcd is an initially empty list. From a rotational point of view, the jth element of this list is written X.dcd[j]; it contains a value decided at the jth instance of the repeated (nk)-set agreement problem.

Fig. 3
figure 3

Repeated anonymous obstruction-free consensus

The total order over the sextuplets “>” is as previously lexicographical but now applies to the six fields. In particular, given two lists dcd and \(dcd'\), the relation \(dcd > dcd'\) holds when there exists \(j \ge 1\) such that \(dcd[j] > dcd'[j]\) and for every \(1 \le k < j\), it is true that \(dcd[k] \ge dcd[k']\). Relation “\(\sqsupset \)” is defined as follows:

$$\begin{aligned} X \sqsupset Y~ \mathop {=}\limits ^{ def } (X>Y)&\wedge [(X.sn> Y.sn)\\&\vee (X.rd > Y.rd)\vee (X. cf{\ell } )]. \end{aligned}$$

Local variables Each process \(p_i\) now manages two local variables. The scope of these variables is the whole repeated (nk)-set agreement problem. (Hence, we do no longer have the locally memoryless property of the base obstruction-free algorithm presented in Fig. 2.)

  • The variable \(sn_i\), initialized to 0, is used by \(p_i\) to generate its sequence numbers. It is assumed that \(p_i\) increments \(sn_i\) before invoking \(\mathsf{propose}(sn_i,v_i)\).

  • The local list \(dcd_i\) is used by \(p_i\) to store the value it has decided during the previous instances of the (nk)-set agreement. Hence, \(dcd_i[sn]\) contains the value decided by \(p_i\) during the snth instance. These lists are exchanged by the processes, which allows the slower of them to catch up when they are in late.

The algorithm Figure 3 describes the algorithm executed at some process \(p_i\). The new parts, with respect to the base algorithm in Fig. 2, are underlined and in blue. To ease the understanding, both algorithms use the same line numbering. Figure 3 contains a single new line, marked with “N”. Suppressing all the underlined parts of the new algorithm leads to our base solution. In what follows, we detail the internals of our solution then establish its correctness.

  • Line 03. When all the entries of the view obtained by \(p_i\) contain only sextuplets whose first five fields are equal, \(p_i\) decide the value \( va{\ell } \). But before returning \( va{\ell } \), \(p_i\) writes \( va{\ell } \) in \(dcd_i[sn_i]\). The idea is that, when \(p_i\) will execute the next (nk)-set agreement instance (whose sequence number will be \(sn_i+1\)), it will be able to help processes with a sequence number smaller than \(sn_i\).

  • Line 04. Process \(p_i\) obtains a quadruplet of the form \(\langle sn_i, r,\mathtt{down},\mathtt{false}, va{\ell } , - \rangle \). In such a case, \(p_i\) writes \(\langle sn_i, r,\mathtt{down},\mathtt{false}, va{\ell } , dcd_i\rangle \) to \( REG [1]\). (Let us notice here that the write of \(dcd_i\) is to help other processes deciding (nk)-set agreement instances whose sequence number is smaller than \(sn_i\).)

  • Line 05. Similar to the previous case, except that a conflict now appears in the view computed by the process \(p_i\).

  • Lines 06–10. Process \(p_i\) computes the supremum of the snapshot view obtained at line 03, as well as the sextuplet \(\langle sn_i, 1,\mathtt{down},\mathtt{false}, va{\ell } , dcd_i\rangle \). We then consider the two following cases:

    • If the sequence number of the supremum is greater than \(sn_i\), process \(p_i\) benefit from the list of decisions stored in the supremum. More precisely, this help is obtained from the item \(dec[sn_i]\). Similarly to line 03, process \(p_i\) then writes this decision in \(dcd_i[sn_i]\) before returning from its call.

    • In the other case, the sequence number of the supremum is equal to \(sn_i\). Process \(p_i\) then executes the same operations as in the basic algorithm (lines 07–08).

6.3 Proof of the algorithm

This section first presents a simple technical lemma, and then shows that the algorithm described in Fig. 3 solves the repeated (nk)-set agreement problem.

Lemma 16

For any \(m \ge 1\), if X is written in \( REG \) and \(X.sn = m\), then for every \(1 \le k < m\), X.dcd[k] exists.

Proof

Let X be some sextuplet in \( REG \) for which \(X.sn = m\) holds. Name \(p_i\) the process that first writes X.

The operation of \(p_i\) might occur either at line 04, 05 or 08.

By definition of the repeated (nk)-set agreement, if \(p_i\) starts instance m of the problem, than it has already returned from the prior instances. As a consequence, if the write occurs at line 04 or 05, then the invariant holds.

Now in the case where the write takes place at line 08, the definition of function \(\mathsf{sup}()\) tells us that either some process wrote a quadruplet Y with \(Y.sn = m\) previously, or \(X=\langle sn_i, 1, \mathtt{down}, \mathtt{false}, v_i, dcd_i \rangle \). In the former case, we repeat our previous reasoning. In the later, we know that the invariant holds since \(p_i\) has already taken a decision in the instances prior to m. \(\square \)

Theorem 3

The algorithm in Fig. 3 is an obstruction-free solution to the repeated (nk)-set agreement problem.

Proof

Let us consider some execution \(\rho \) of the algorithm in Fig. 3. Let m be an instance that was executed in \(\rho \). We name \(U_m\) the set of decisions taken at instance m in \(\rho \). We also define \(V_m \subseteq U_m\) the decisions taken at instance m in \(\rho \) before a higher instance begins, that is before some sextuplet X with \(X.sn>m\) is observed by a process in \( REG \).

First of all, let us notice that, if no interleaving takes place between m and a higher instance, the algorithm of Fig. 3 boils down to our base algorithm. As a consequence, decisions in \(V_m\) are valid and \(|V_m| \le k\).

Let us now choose some decision \(u \in U_m\) taken by a process \(p_i\) in \(\rho \). Below, we show that \(u \in V_m\) holds.

  • If the decision takes place at line 03, then it occurs before an instance higher than m begins. Thus, by definition \(u \in V_m\) holds.

  • Let us now consider the case where process \(p_i\) decides at line N with \(inst>m\), choosing dec[m] as its decision. Lemma 16 tell us that this value is well-defined. In Fig. 3, we observe that a process \(p_j\) might update \(dcd_j[m]\) with value u only in the case where it decides u in instance m at line 03. Thus, u belongs to \(V_m\).

The previous reasoning shows that every instance is safe, in the sense that it satisfies both the validity and agreement properties of the (nk)-set agreement problem.

In Fig. 3, a process decides before a higher instance begins, or it decides immediately afterward. Consequently, the properties of OF-termination and SV-termination follow from the validity property and the fact that our base solution satisfies these two properties. \(\square \)

Theorem 3 tells us that solving repeated (nk)-set agreement in an anonymous system does not require more atomic read/write registers than the base non-repeated version. The additional cost lies only in the size of the atomic registers which contain two supplementary unbounded fields. As we pointed out at the beginning of this section, the lower bound established in [15] induces that the algorithm in Fig. 3 is space-optimal.

7 The case of x-obstruction-freedom

This section extends the base algorithm described in Fig. 2 to obtain a solution to the anonymous (nk)-set agreement problem with a stronger progress condition, namely x-obstruction-freedom. It first defines x-obstruction-freedom, then details the modifications to the base algorithm, and finally prove its correctness.

7.1 Problem statement

The notion of x-obstruction-freedom [38] guarantees that for every set of processes P, with \(|P|\le x\), every correct process in P returns from its operation invocation if no process outside of P takes a step for a “long enough” period of time. This progress property extends naturally obstruction-freedom, which corresponds to the case where \(x=1\). Moreover, x-obstruction-freedom and wait-freedom coincide in every n-process system where \(x \ge n\). In the case where \(x<n\), x-obstruction-freedom depends on the concurrency pattern, while wait-freedom does not.

Fig. 4
figure 4

Function \(\mathsf{sup}()\) suited to x-obstruction-freedom

The variant of the (nk)-set agreement problem that interests us is defined as follows. Its Validity, Agreement and SV-Termination properties remain the ones we stated in Sect. 2.2. Differently, OF-Termination is modified as follows:

  • x-OF-termination. If there is a time after which at most x correct processes take steps, each of these processes eventually decides a value.

Let observe that every x-obstruction-free solution to (nk)-set agreement is also a wait-free solution to \((k+1,k)\)-set agreement when \(x>k\). It then follows from [7, 24, 35] that there is no x-obstruction-free algorithm for \(x>k\). As a consequence, the rest of this section assumes \(x\le k\).

7.2 Algorithm

The shared memory Under x-obstruction-freedom, up to x processes may concurrently progress without preventing termination. As a consequence, in comparison to obstruction-freedom, solving k-set agreement in this setting requires to deal with more contention scenarios. To cope with these additional interleavings of processes, we increase the number of entries in \( REG \). More precisely, \( REG \) now contains \(m=(n-k+x)\) entries.

Ordering the quadruplets In the base algorithm, the four fields of some quadruplet X are the round number X.rd, the level \(X. {\ell }v{\ell } \), the conflict flag \(X.cf\ell \), and the value X.val. Coping with x-concurrency requires to replace the last field, which was initially a singleton, with a set of values. Hereafter, this new field is denoted \(X. valset \).

In line with the definitions of Sect. 4.1, let “>” denote the lexicographical order over the set of quadruplets, where the relation \(\sqsupset \) is generalized as follows to take into account the fact that the last field of a quadruplet is now a non-empty set of values:

$$\begin{aligned} X \sqsupset Y~ \mathop {=}\limits ^{ def }~ (X>Y) ~&\wedge ~ [(X.rd > Y.rd)\\ ~&\quad \vee ~ (X. cf{\ell } ) {~\vee ~ (X. valset \supseteq Y. valset )}] \end{aligned}$$

In comparison to the definition appearing in Sect. 4, the sole new case where the ordering \(X \sqsupset Y\) holds is \((X >Y) \wedge (X. valset \supseteq Y. valset )\). This case captures the fact that, as long as at most x input values are competing at some round, there is no conflict. If such a situation arises, we simply construct a quadruplet that aggregates the different input values.

Modifications to the \(\mathsf{sup}()\) function Figure 4 describes the new definition of function \(\mathsf{sup}()\). Compared with the original algorithm in Fig. 1, it introduces a few modifications (underlined and in blue). Those are detailed below.

  • Line S1. As pointed out previously, the last field of a quadruplet is now a set of values. The lexicographical ordering over such sets is as follows: sets are ordered first according to their size, and second using some arbitrary order over their elements. By abuse of notation, this order is also written <. For instance, we have \(\{10, 8,2\} < \{10, 4,3\}\) and \(\{10, 4,3\} < \{15,12\}\). It is assumed that for any set of values S, \(S < \bot \) holds.

  • Line S2. This line does not change.

  • Lines S3 and S4. This variant extends the definition of a conflict. Namely, it considers as a conflict the case where more than x distinct tuples are competing at round r, and also the additional case where more than x distinct values are competing at round r.

  • Lines S5 and S6. Compared to Fig. 1, function \(\mathsf{sup}()\) returns a quadruplet that may contain additional input values. This comes from the fact that the function aggregates the x greatest values competing at round r.

Fig. 5
figure 5

Anonymous x-obstruction-free (nk)-set agreement

Solving (nk) -set agreement under x -obstruction-freedom Figure 5 presents the modified algorithm solving the (nk)-set agreement problem, in which the progress condition is x-obstruction-freedom. Let us notice that it is also locally memoryless.

In Fig. 5, the differences between the two algorithms are underlined and in blue. These differences come from the fact that, as detailed previously, each quadruplet now contains a set of input values in its last field. The main difference is at line 03.

  • Line 03. When deciding, a process must pick one of the values provided in the snapshot taken from \( REG \).

7.3 Correctness proof

This section proves that Fig. 5 describes a correct solution to the (nk)-set agreement problem, when considering x-obstruction-freedom as the progress condition. The proof scheme is similar to the one used in Sect. 4.

Theorem 4

The algorithm in Fig. 5 is a solution to the x-obstruction-free (nk)-set agreement problem.

Proof

Validity and SV-Termination follow from a reasoning identical to the one conducted for the base algorithm.

As far as the Agreement property is concerned, let us first observe that the relation \(\sqsupset \) remains a partial order. Then, considering some non-empty set of quadruplets T and some \(X \in T\), the rewriting of function \(\mathsf{sup}()\) maintains that the relation \(\mathsf{sup}(T) \sqsupseteq X\) holds. Indeed, we have \(\mathsf{sup}(T) \ge \mathsf{max}(T)\) and either (i) \(X.rd < \mathsf{sup}(T).rd\), or (ii) there is a conflict leading to \(\mathsf{sup}(T). cf{\ell } = \mathtt{true}\), or alternatively (iii) since \(|values(T)| \le x\), we have \(X. valset \subseteq \mathsf{sup}(T). valset \).

Then, let us consider a run where at most \((n-k+x)\) processes take steps. From what precedes, we may conclude that (excluding Lemmas 7 and 9) Lemmas 38 hold for the algorithm in Fig. 5. The reformulations of Lemmas 7 and 9 as well as their respective correctness proofs are stated below. \(\square \)

Lemma 17

If \( REG ^{\tau }\) is \(\mathcal {H}(X)\), \( REG ^{\tau ^\prime }\) is \(\mathcal {H}(Y)\), \(\tau ^\prime \ge \tau \), \((Y.rd=X.rd)\) and \((\lnot Y. cf{\ell } )\) then \((Y. valset \supseteq X. valset )\).

Proof

According to Lemma 6, we have \(Y \sqsupseteq X\). If \(Y=X\), then the claim follows immediately. On the other hand, if \(Y \sqsupset X\) holds, since we know that \((Y.rd=X.rd)\) and \((\lnot Y. cf{\ell } )\), the definition of relation \(\sqsupseteq \) implies that we have \(Y. valset \supseteq X. valset \). \(\square \)

Lemma 18

\([( REG ^{\tau }\) is \(\mathcal {H}(X))\) \(\wedge \) \((X. {\ell }v{\ell } =\mathtt{up})\) \(\wedge \) \((\lnot X. cf{\ell } )\) \(\wedge \) \(( REG ^{\tau ^\prime }\) is \(\mathcal {H}(Y))\) \(\wedge \) \((Y.rd \ge X.rd)]\) \(\Rightarrow \) \((Y. valset \supseteq X. valset \vee X. valset \supseteq Y. valset )\).

Proof

The proof is by induction on Y.rd. Let us first assume \(Y.rd = X.rd\). There are two cases.

  • (Case \(\tau \ge \tau '\)) As \(X. cf{\ell } \) equals \(\mathtt{false}\), Lemma 17 implies that \(X. valset \supseteq Y. valset \).

  • (Case \(\tau ' > \tau \)). From Lemma 6, we know that \(Y \sqsupseteq X\). As \(Y.rd = X.rd\), it follows that \(Y. {\ell }v{\ell } \ge X. {\ell }v{\ell } = \mathtt{up}\). Applying Lemma 8, we obtain the existence of two quadruplets \(Z_X = \langle X.rd-1, \mathtt{down}, \mathtt{false}, X. valset \rangle \) and \(Z_Y = \langle X.rd-1, \mathtt{down}, \mathtt{false}, Y. valset \rangle \) such that \( REG \) is \(\mathcal {H}(Z_X)\) and \(\mathcal {H}(Z_Y)\) at some points in time. From Lemma 17, we deduce that \(X. valset \supseteq Y. valset \), or the converse, holds.

For the cases where \(Y.rd > X.rd\), let us consider that our induction hypothesis holds up to some round r. Then, let \(p_i\) be the first process that writes at round \(r +1\) some quadruplet \(\langle r+1, -, -, Y. valset \rangle \) into \( REG \). This happens at either line 04, or line 05 in Fig. 5. In both cases, our induction hypothesis implies that \(X. valset \supseteq Y. valset \) or the converse holds. \(\square \)

Lemma 19

At most x values are decided.

Proof

Let V be the set of decided values. Since each decision takes place at line 03, there exists a set \((X_v)_{v \in V}\) of tuples such that some process observes an homogeneous snapshot \(\mathcal {H}(X_v)\) with \(X_v. cf{\ell } = \mathtt{false}\), \(X_v. {\ell }v{\ell } = \mathtt{up}\) and \(v \in X_v. valset \).

For a tuple \(X_v\), since \(X_v. cf{\ell } = \mathtt{false}\), \(|X_v. valset | \le x\) holds. From Lemma 18, we deduce that for any two values \(v, w \in V\), either \(X_v. valset \subseteq X_w. valset \), or the converse, holds. The conjunction of the above two observations implies that \(|V| \le x\). \(\square \)

Applying the reasoning of Sect. 5, Lemma 19 implies that the algorithm described in Fig. 5 satisfies the Agreement property of (nk)-set agreement: \(n-(n-k+x)\) processes may decide up to \((k-x)\) values, and the \((n-k+x)\) remaining processes decide at most x values.

The next lemmas establish that the x-OF-termination property holds. To this end, and in line with the definition of x-OF-termination, we will consider some set of processes \(P_x\), with \(|P_X| \le x\), and a run \(\lambda \) of the algorithm in Fig. 5 satisfying \(\lambda =\lambda _1\lambda _2\), and only the processes of \(P_x\) take steps during \(\lambda _2\). If \(x=1\), then the algorithm in Fig. 5 boils down to our base solution. As a consequence, we assume hereafter \(x \ge 2\).

Lemma 20

All the correct processes decide in \(\lambda \), or for every round r, every entry of \( REG \) contains eventually some tuple X with \(X.rd > r\).

Proof

We proceed by contradiction.

Let \(P=\{p_1, \ldots , p_m\}\) be the largest set of processes that never decide. Consider a point in time \(\tau _0\) where only the processes in P take steps. At time \(\tau +1 > \tau _0\) and for every process \(p_i \in P\),

  • if \(p_i\) modifies \(view_i\), then this corresponds to the value of \( REG ^{\tau }\) (line 02); and

  • if \(p_i\) writes some tuple X in \( REG \), then we have \(X \ge \mathsf{sup}(view_i^{\tau })\) (lines 04, 05 and 08).

We note \(S^{\tau } = \{\mathsf{sup}(view_1^{\tau }), \ldots , \mathsf{sup}(view_m^{\tau }), \mathsf{sup}( REG ^{\tau })\}\) and \(m^{\tau } = min(S^{\tau })\). The above observation tells us that the sequence \((m^{\tau })_{\tau \ge \tau _0}\) is growing.

By hypothesis, there exists some round r and an entry \( REG [i]\) such that \( REG [i]\) never contains a tuple X with \(X.rd > r\). At the light of the code in Fig. 5, every entry \( REG [j]\) should satisfy \( REG [j].rd \le r\) at all time.

From what precedes, the sequence \((m^{\tau })_{\tau \ge \tau _0}\) is upper bounded and converges toward some value m.

Note \(\tau _1\) the time at which the convergence takes places, that is \(m^{\tau } = m\) is true for every \(\tau \ge \tau _1\). After time \(\tau _1\), every new write \(\mathcal {W}(-,X)\) to \( REG \) is such that \(X \ge m\). As a consequence, m can be written to an entry of \( REG \) at most |P| times after time \(\tau _1\) (see lines 07 and 08 in Fig. 5).

It follows that eventually it is true forever that \(\mathsf{sup}( REG ^{\tau }) > m\) holds, or that all the entries of \( REG \) contains m. Both cases leads to a contradiction: The former case is not possible, since m is the limit of \((m^{\tau })_{\tau \ge \tau _0}\). In the later, a process eventually observes an homogeneous snapshot for m. Since this process cannot decide, it executes line 04 or 05, writing some tuple X in \( REG \) with \(X.rd = m.rd+1\). \(\square \)

Lemma 21

All the processes of \(P_x\) decides in \(\lambda \).

Proof

Execution \(\lambda \) is such that \(\lambda =\lambda _1\lambda _2\) and only the processes of \(P_x\) take steps in \(\lambda _2\). Lemma 20 tells us that either all the processes in \(P_x\) decide, or \(\lambda _2\) contains an unbounded amount of rounds, starting from some round \(r_0\). Let us consider the later case, assuming without lack of generality, that none of the processes in \(P_x\) decide in \(\lambda _2\).

For some round r, we note \(\mathcal {X}_r\) the set \(\{ X : \exists p_i, \tau : view_i^{\tau }~\text {is}~\mathcal {H}(X) \wedge X.rd = r \}\). We also define \(V_r\) as \(min(\{V : \exists X \in \mathcal {X}_r ~\wedge ~ X. valset = V\})\). In what follows, we state several claims regarding the sequence \((V_r)_{r > r_0}\). \(\square \)

C1. :

\(\forall X,r : (\exists \tau ,j : REG ^{\tau }[j] = X \wedge X.rd = r+1) \implies X. valset \ge V_r\).

Proof

The above equation is true initially, as for any i, \( REG ^{0}[i] = \langle 0, \mathtt{down}, \mathtt{false}, \bot \rangle \). Then, consider that it holds up to time \(\tau \), and assume that a process \(p_i\) writes a tuples X in \( REG \) with \(X.rd = r+1\) at time \(\tau +1\). If \(p_i\) executes line 04 or 05, then there exists \(Y \in \mathcal {X}_r\) with \(X. valset = Y. valset \ge V_r\). Otherwise \(p_i\) executes line 08 and in such a case \(X=\mathsf{sup}(view_i^{\tau })\). Observe that for any \(Z \in view_i^{\tau }\) satisfying \(Z.rd = r+1\), line S5 in function \(\mathsf{sup}()\) implies that \(X. valset \ge Z. valset \), and from our induction hypothesis, \(Z. valset \ge V_r\). Thus, \(X. valset \ge V_r\) holds. \(\square \)

C2. :

\(\forall X,r : (\exists \tau ,j : REG ^{\tau }[j] = X \wedge X.rd = r+1 \wedge X. valset = V_r) \implies X. cf{\ell } = \mathtt{false}\).

Proof

The above equation is initially true. In what follows, we consider that it holds up to time \(\tau \), and assume that at time \(\tau +1\) a process \(p_i\) writes some tuple X in \( REG \) with \(X.rd = r+1~\wedge ~ X. valset = V_r\).

For the sake of contradiction, consider that \(X. cf{\ell } = \mathtt{true}\). In Fig. 5, a write to \( REG \) might occur either at line 04, 05 or 08. Since \(X. cf{\ell } = \mathtt{true}\) holds, \(p_i\) executes line 08 at time \(\tau +1\) with \(X=\mathsf{sup}(view_i^{\tau })\).

Define \(M=max(T)\), with \(T=\{Z \in view_i^{\tau } : Z.rd = r+1\}\). From the code at lines S5 and S6 in Fig. 4, \(M.rd = X.rd = r+1\) and \(X. valset \ge M. valset \) are both true. Claim C1 implies that \(M. valset \ge V_r\).

As \(X. valset \ge M. valset \) and \(X. valset = V_r\), necessarily \(M. valset = V_r\). Then, applying our induction hypothesis, we deduce that \(M. cf{\ell } = \mathtt{false}\). Since \(X. cf{\ell } = \mathtt{true}\), either \(|tuple(T)| > x\) or \(|values(T)| > x\) holds. Below, we explore each of these two cases.

  • \((|values(T)| > x)\) For every \(Z \in T\), \(|Z. valset | \le x\) holds. Hence, there exist \(Y, Z \in T\) with \(Y. valset \ne Z. valset \). By C1, \(Z. valset \ge V_r\) and \(Y. valset \ge V_r\) are true. It follows, that \(X. valset \ge M. valset \ge max(Y. valset ,Z. valset ) > V_r\). Contradiction.

  • \((|tuple(T)| > x)\) Choose \(Z \in T\). If \(Z. valset = V_r\), our induction hypothesis implies that \(Z. cf{\ell } = \mathtt{false}\) holds. Thus, there are at most two tuples in T of the form \(\langle r+1, -, \mathtt{false}, V_r \rangle \). As \(x \ge 2\), T contains at least three elements. It follow from C1 that there exists some \(Z \in T\) with \(Z. valset > V_r\). From which, we deduce that \(M. valset > V_r\). Contradiction.\(\square \)

C3. :

\(\forall r > r_0 : V_r < V_{r+2}\).

Proof

Claim C1 implies that \(V_r \le V_{r+1} \le V_{r+2}\). Consider that for some round r, the assertion \(V_r = V_{r+1} = V_{r+2}\) holds.

Choose X and Y respectively in \(\mathcal {X}_{r+1}\) and \(\mathcal {X}_{r+2}\), with \(X. valset = Y. valset = V_r\). From claim C2, \(X. cf{\ell } = \mathtt{false}\) holds. Applying C1, a short induction tells us that every tuple Z with \((Z. valset = V_r \wedge Z.rd = r+2)\) satisfies \(Z. {\ell }v{\ell } = \mathtt{up}\). This implies that \(Y. {\ell }v{\ell } = \mathtt{up}\) is true. Since C2 holds also for the tuple Y, \(Y. cf{\ell } = \mathtt{false}\) holds. As a consequence, some process decides at round \(r+2\). This contradicts that \(r+2 > r_0\) is true. \(\square \)

If the number of rounds is not bounded, then the claim C3 implies that \((V_r)_{r > r_0}\) diverges. However, any element in this sequence is a subset of the values proposed at round \(r_0\), contradicting such an assumption. \(\square \)

Lemmas 19 and 21 induce that Fig. 5 depicts an x-obstruction-free solution to the (nk)-set agreement problem. \(\square \)

8 On the power of repeated anonymous consensus

8.1 Universality of n MWMR registers

Let us first turn our attention to non-anonymous systems made up of n asynchronous processes communicating with SWMR read/write registers. Let us first notice that, if an object can be implemented with an arbitrary number of SWMR atomic read/write registers, it can be implemented with only n SWMR atomic read/write registers, one per process. This follows from the observation that, for every writer \(p_i\), we can glue together all the SWMR atomic read/write registers that \(p_i\) accesses into an array stored in a single register. At the light of this result, we raise the question whether a similar result exists in the context of anonymous systems. This section answers positively this question, showing that what can be obstruction-free computed by n anonymous processes with an arbitrary number of MWMR atomic registers, can also be obstruction-free computed by n anonymous processes with no more than n MWMR atomic registers.

Theorem 5

Let O be an object that can be obstruction-free implemented by n anonymous processes and any number of MWMR atomic read/write registers. O can be obstruction-free implemented by n anonymous processes and n MWMR atomic read/write registers.

Proof

The proof consists in building a simple universal construction whose core is the obstruction-free anonymous repeated consensus algorithm presented in Sect. 6. Let (a) \(p_1\), ..., \(p_n\) be the application processes, (b) R1, R2, etc., be the MWMR atomic read/write registers they share (there registers implement object O), and (c) \(in_1\), ..., \(in_n\) be the individual inputs of the n processes. Let \(q_1\), ..., \(q_n\) be a set of n anonymous simulators.

Each simulator \(q_i\) is assigned exactly one process \(p_i\). Moreover, the local memory of each simulator contains a copy of all the registers R1, R2, etc. The memory shared by the simulators contains only the snapshot object on which is built the obstruction-free anonymous repeated consensus algorithm. Hence, it is made up of n atomic read/write registers.

Each application process executes a sequence of steps, that is a sequence of read and write operations on the registers R1, R2, etc.

The simulation is a sequence of repeated consensus, and proceeds as follows.

  • First consensus. Each simulator \(q_i\) proposes the value \(prop_i=\)“step of process with input \(in_i\) is: read register Rx” (or “‘step of process with input \(in_i\) is: write v in register Ry”), where “read register Rx” or “ write v in register Ry” is the first step of \(p_i\). Let dec be the value decided by this first consensus instance. There are two cases.

    • If \(dec=prop_i\), \(q_i\) applies locally the operation “read register Rx” (or “write v in register Ry”), and prepares (for the next consensus instance) a new proposal \(prop_i\) according to next step of \(p_i\) as defined by its code, namely, \(prop_i\) is “step of process with input \(in_i\) is: ...”.

    • If \(dec\ne prop_i\), \(q_i\) keeps its proposal \(prop_i\) for the next consensus instance, but modifies its local copy of Ry if dec is “write v in register Ry”.

  • Second consensus. Each simulator \(q_i\) proposes the value \(prop_i\) it computed after it terminated the first consensus instance, and proposes it to the second consensus instance.

  • And so on.

Let us observe that, as several processes can have the same input and anonymous processes have the same code, it is possible that several simulators propose the same value prop to a consensus instance, where prop is “step of process with input \(in_i\) is read register Rx” (or “step of process with input \(in_i\) is write v register Ry”. If such a prop is decided by the corresponding consensus instance, and the decided value is “write v in register Ry”, only one write is applied to Ry by each simulator. This does not create a problem, as this write of v in \(R_y\) can be seen as a digest of the corresponding number of consecutive writes of v in \(R_y\), each one overwriting the previous one.

It follows from the sequence of repeated consensus that all simulators see the same sequence of steps issued by the processes, which is a linearization of the operations issued by the processes. In addition, each process \(p_i\) inherits the progress of its simulator \(q_i\). Hence, if a simulator \(q_i\) executes alone a long enough period of time to compute an output, so does the corresponding simulated process \(p_i\), which concludes the proof of the theorem. \(\square \)

8.2 Anonymity, tasks, and colorless tasks

The previous theorem showed that, in an anonymous system, n registers are sufficient to obstruction-free implement any object O implemented with more registers. An interesting follow-up question is to know which distributed tasks (see below), usually considered in a non-anonymous system, can be solved in an anonymous setting. As we shall see below, this set contains at least all colorless tasks, i.e., the distributed tasks that do not involve some kind of symmetry breaking argument.

Distributed tasks A distributed task T is defined by a set \(\mathcal {I}\) of input n-vectors, a set \(\mathcal {O}\) of output n-vectors and a map \(\varDelta \) from \(\mathcal {I}\) to \(2^{\mathcal {O}}\). If the input value of a process p in \(I \in \mathcal {I}\) is \(\bot \), we say that p does not participate to the input vector I. Similarly if O[p] equals \(\bot \), process p does not decide in O. For every distributed task \(T=(\varDelta ,\mathcal {I},\mathcal {O})\), we require that (i) a process may not decide (\((\forall p: O'[p] \in \{O[p], \bot \} \wedge (I,O) \in \varDelta ) \implies (I,O') \in \varDelta \)), and that (ii) a process that does not participate, does not decide (\((I[p]=\bot \wedge (I,O) \in \varDelta ) \implies O[p]=\bot \)).

The notion of interval linearizability (which generalizes linearizability [26]) is introduced in [10], where it is shown that tasks and one-shot concurrent objects are in a precise sense equivalent (Theorem 3 in [10]). It follows that the proof of the previous theorem remains correct if we consider a distributed task instead of an object O. We have consequently the following theorem.

Theorem 6

If a distributed task T is obstruction-free solvable by n anonymous processes and any number of MWMR atomic read/write registers, then T is obstruction-free solvable by n anonymous processes with no more than n MWMR atomic read/write registers.

The case of colorless tasks Let us note \({ val }(U)\) the set of non-null values in some vector U. Following [8], a task \(T=(\varDelta ,\mathcal {I},\mathcal {O})\) is colorless when in a solution to T, a process is free to adopt the input and output value of any other participating process. Formally, (\(({ val }(I) \subseteq { val }(I') \wedge { val }(O') \subseteq { val }(O) \wedge (\forall p : I'[p] = \bot \implies O'[p] = \bot ) \wedge (I,O) \in \varDelta ) \implies (I',O') \in \varDelta \)). This class of distributed tasks includes notably the k-set agreement problem. The next theorem shows that anonymity is enough when a task is colorless and obstruction-free -solvable.

Theorem 7

Let us consider a colorless task \(T=(\varDelta ,\mathcal {I},\mathcal {O})\) that is obstruction-free solvable in a non-anonymous system using any number of SWMR registers. Then, T is also obstruction-free solvable in an anonymous system with n MWMR atomic registers.

Proof

Let us consider an obstruction-free algorithm A, that solves T in a non-anonymous system. As n registers are sufficient in such a setting, we assume (without lack of generality) that A uses n registers only. In what follows, we present a construction to simulate a run of A in an anonymous system, and then proves its correctness.

  • Construction. In a first step, each anonymous process p proposes (0, v) to consensus, where v is its input value. Upon deciding some tuple (iw), if \(w=v\), then process p considers that it holds identifier i; otherwise p computes \(i' = i+1\) and proposes \((i',v)\) to the next consensus instance. This process repeats until p holds some identifier. Then, process p executes algorithm A with input v and identifier i. As in the proof of Theorem 5, all the processes holding identifier i agree on simulating the next step of process i with the help of anonymous consensus. During this simulation, we note that registers are SWMR and in particular that process i writes only to register R[i]. Process p decides the value the simulation of process i outputs.

Let us now show that this construction is correct. To this end, consider some input vector \(I \in \mathcal {I}\) and a run \(\rho \) following the above algorithm.

  • If no decision occurs in \(\rho \), the output vector O that contains \(\bot \) everywhere satisfies \((I,O) \in \varDelta \).

  • Assume now that a process p proposes a value u and decides some value v. Before process p decides, it must have chosen some identifier i. At the light of the above construction, all the processes that have identifier i propose and decide the same value. Hence, in run \(\rho \), the simulated process i proposes u and decides v. Generalizing this reasoning, let us note \(I'\) and \(O'\) respectively, the simulated input and output n-vectors during the simulation. Since T is colorless, obstruction-free solvable, and in an asynchronous system we cannot distinguish a non-participating process from an initially crash one, vector \(I'\) belongs to the domain of \(\varDelta \). Then, we observe that in \(\rho \) the identifiers of any two simulated processes are different. This ensures that the simulated system is non-anonymous. Consequently, A solves T in \(\rho \) and \(O' \in \varDelta (I')\) holds. Let O be the n-vector output in \(\rho \). By construction, we know that \({ val }(O) \subseteq { val }(O')\) holds. As T is colorless, we deduce that O belongs to \(\varDelta (I')\). As a consequence, since \({ val }(I') \subseteq { val }(I')\), T is colorless and \(O \in \varDelta (I')\), we conclude that \(O \in \varDelta (I)\).

To complete the proof, let us observe that all the steps in the above construction are obstruction-free, and that (as pointed out) the n-vector input in the simulation belongs to the domain of \(\varDelta \). As a consequence, if T is obstruction-free solvable in a non-anonymous system, it remains obstruction-free solvable in an anonymous system. \(\square \)

9 Conclusion

This paper first presents an obstruction-free (nk)-set agreement algorithm for a system made up of n asynchronous anonymous processes that communicate with the help of atomic read/write registers. This algorithm uses only \((n-k+1)\) registers. In terms of the number of registers, it is the best algorithm known so far, and, in the case of consensus, it is up to an additive factor of 1 close to the best known lower bound [41]. This algorithm answers the challenge posed in [13], and establishes a novel upper bound of \((n-k+1)\) on the number of registers to solve one-shot obstruction-free (nk)-set agreement. This upper bound improves the ones stated in [15] for both anonymous and non-anonymous systems.

Further, the paper introduces a simple extension of the base algorithm, that solves repeated (nk)-set agreement. The lower bound of \((n-k+1)\) atomic registers was established in [15] for this problem. Hence, the proposed algorithm proves that this bound is tight. A one-shot algorithm solving anonymous (nk)-set agreement problem in the context of x-obstruction-freedom is also described. This algorithm makes use of \((n-k+x)\) atomic read/write registers.

All the proposed algorithms rely on the same round-based data structure. The base one-shot algorithm does not require persistent local variables, and in addition to a proposed value, an atomic register solely contains two bits and a round number. The algorithm solving repeated (nk)-set agreement requires that each atomic register includes two more fields.

This paper also establishes two reduction results. The first one shows that any distributed task that is obstruction-free solvable in an anonymous system with any number of registers is also obstruction-free solvable with solely n registers. The second reduction shows that this amount of registers is also enough for every colorless task that is obstruction-free solvable in a non-anonymous system.

Let the MWMR-number of a concurrent object O be the minimal number of MWMR atomic registers needed to implement O in an n-process asynchronous anonymous system in which any number of processes may crash. Using this terminology, it is shown in [15] that the MWMR-number of the repeated obstruction-free (nk)-set agreement object is at least \((n-k+1)\). Showing that this number is actually \((n-k+1)\), this paper closes the corresponding lower bound problem. Furthermore, Theorem 5 shows that no object (defined by a sequential specification) has an MWMR-number greater than n. Finally, we conjecture that \((n-k+1)\) is the MWMR-number of the one-shot obstruction-free (nk)-set agreement object, and more generally that \((n-k+x)\) is the MWMR-number of one-shot x-obstruction-free (nk)-set agreement objects, when \(1\le x\le k<n\).