On Liveness of Dynamic Storage

Abstract

Dynamic distributed storage algorithms such as DynaStore, Reconfigurable Paxos, RAMBO, and RDS, do not ensure liveness (wait-freedom) in asynchronous runs with infinitely many reconfigurations. We prove that this is inherent for asynchronous dynamic storage algorithms. Our result holds even if only one process may fail, provided that machines that were successfully removed from the system’s configuration can be switched off by a system administrator. To circumvent this result, we define a dynamic eventually perfect failure detector, and present an algorithm that uses it to emulate wait-free dynamic atomic storage. Though some of the previous algorithms have been designed for eventually synchronous models, to the best of our knowledge, our algorithm is the first to ensure liveness for all operations without restricting the reconfiguration rate.

A. Spiegelman is grateful to the Azrieli Foundation or the award of an Azrieli Fellowship.

A Correctness Proof

In Sect. A.1 we prove that our algorithm satisfies atomicity, and in Sect. A.2 wait-freedom.

1.1 A.1 Atomicity

Every operation is uniquely defined by the process that invoked it and its local number. During the proof we refer to operation op invoked by process $p_i$ with local number $opNum_i = n$ as the tuple $\langle p_i, op, n\rangle$. We begin the proof with three lemmas that link completed operations to sm states.

Lemma 3

Consider operation op invoked by some process $p_i$ in r with local number $opNum_i = n$. If op returns in r at time t, then there is at least one request Req that contains $\langle p_i,op,n\rangle$ and has been chosen in a consensus in r before time t.

Proof

When operation op return, $sm_i.lastOps[i].num=n$ (line 17 or 18 in Algorithm 2). Processes update sm during a decide handler, or when a newer sm is received, and the first update occurs when some process $p_j$ writes n to $sm_j.lastOps[i].num$ during a decide handler. In the decide handler, n is written to sm.lastOps[i].num when the chosen request in the corresponding consensus contains $\langle p_i,op,n\rangle$.

Lemma 4

For two processes $p_i,p_j$, let t be a time in a run r in which neither $p_i$ or $p_j$ is executing a decide handler. Then at time t, if $sm_i.ts=sm_j.ts$, then $sm_i=sm_j$.

Proof

We prove by induction on timestamps. Initially, all correct processes have the same sm with timestamp 0. Now consider timestamp TS, and assume that for every two processes $p_i,p_j$ at any time not during the execution of decide handlers, if $sm_i.ts=sm_j.ts=TS$, then $sm_i=sm_j$. Processes increase their sm.ts to $TS+1$ either at the end of a decide handler associated with TS or when they receive a message with sm s.t. $sm.ts=TS+1$. By the agreement property of consensus and by the determinism of the algorithm, all the processes that perform the decide handler associated with TS perform the same operations, and therefore move sm (at the end of the handler) to the same state. It is easy to show by induction that all the processes that receive a message with sm s.t. $sm.ts=TS+1$ receive the same sm. The lemma follows.

Observation 1

For two process $p_i,p_j$, let $sm_1$ and $sm_2$ be the values of $sm_j$ at two different times in a run r. If $sm_1.ts \ge sm_2.ts$, then $sm_1.lastOps[i].num \ge sm_2.lastOps[i].num$.

Lemma 5

Consider operation $\langle p_i, op, opNum_i \rangle$ invoked in r with $opNum_i = n$. Then $\langle p_i, op, n \rangle$ is part of at most one request that is chosen in a consensus in r.

Proof

Assume by way of contradiction that $\langle p_i, op, n \rangle$ is part of more than one request that is chosen in a consensus in r. Now consider the earliest one, Req, and assume that it is chosen in a consensus associated with timestamp TS. At the end of the decide handler associated with timestamp TS, $sm.lastOps[i].num=n$ and the timestamp is increased to $TS+1$. Thus, by Lemma 4 $sm.lastOps[i].num=n$ holds for every sm s.t. $sm.ts=TS+1$. Consider now the next request, $Req_1$, that contains $\langle p_i, op, n \rangle$, and is chosen in a consensus. Assume that this consensus associated with timestamp $TS'$, and notice that $TS' > TS$. By the validity of consensus, this request is proposed by some process $p_j$, when $sm_j.ts$ is equal to $TS'$. By Observation 1, at this point $sm_j.lastOps[i].num \ge n$, and therefore $p_j$ does not include $\langle p_i, op, n \rangle$ in $Req_1$ (line 27 in Algorithm 2). A contradiction.

Based on the above lemmas, we can define, for each run r, a linearization $\sigma _r$, where operations are ordered as they are chosen for execution on sm’s in r.

Definition 3

For a run r, we define the sequential run $\sigma _r$ to be the sequence of operations decided in consensus instances in r, ordered by the order of the chosen requests they are part of in r. The order among operations that are part of the same chosen request is the following: first all writes, then all reads, and finally, all reconfig operations. Among each type, operations are ordered by the process ids of the processes that invoked them, from the highest to the lowest.

Note that for every run r, the sequential run $\sigma _r$ is well defined. Moreover, $\sigma _r$ contains every completed operation in r exactly once, and every invoked operation at most once.

In order to prove atomicity we show that (1) $\sigma _r$ preserves r’s real time order (Lemma 6); and (2) every read operation rd in r returns the value that was written by the last write operation that precedes rd in $\sigma _r$, or $\perp$ if there is no such operation (Lemma 7).

Lemma 6

If operation $op_1$ returns before operation $op_2$ is invoked in r, then $op_1$ appears before $op_2$ in $\sigma _r$.

Proof

By Lemma 3, $op_1$ is part of a request $Req_1$ that is chosen in a consensus before $op_2$ is invoked, and thus $op_2$ cannot be part of $Req_1$ or any other request that is chosen before $Req_1$. Hence $op_1$ appears before $op_2$ in $\sigma _r$.

Lemma 7

Consider read operation $rd = \langle p_i, RD, n \rangle$ in r, which returns a value v. Then v is written by the last write operation that precedes rd in $\sigma _r$, or $v=\perp$ if there is no such operation.

Proof

By Lemmas 3 and 5, rd is part of exactly one request $Req_1$ that is chosen in a consensus, associated with some timestamp TS. Thus sm.lastOps[i] is set to $\langle n, val \rangle$ in the decide handler associated with TS. By Lemma 4, $sm.lastOps[i]=\langle n, val \rangle$ for all sm s.t. $sm.ts=TS+1$. By Lemma 5 and since we consider only well-formed runs, $sm_i.lastOps[i]=\langle n, val \rangle$ when rd returns, and therefore rd returns val. Now consider three cases:

• There is no write operation in $Req_1$ or in any request that was chosen before $Req_1$ in r. In this case, there is no write operation before rd in $\sigma _r$, and no process writes to sm.value before sm.lastOps[i] is set to $\langle n, val\rangle$, and therefore, rd returns $\perp$ as expected.

• There is a write operation in $Req_1$ in r. Consider the write operation w in $Req_1$ that is invoked by the process with the lowest id, and assume its argument is $v'$. Notice that w is the last write that precedes rd in $\sigma _r$. By the code of the decide handler, sm.value equals $v'$ at the time when sm.lastOps[i] is set to $\langle n, val\rangle$. Therefore, $val = v'$, rd returns the value that is written by the last write operation that precedes it in $\sigma _r$.

• There is no write operation in $Req_1$, but there is a request that contains a write operation and is chosen before $Req_1$ in r. Consider the last such request $Req_2$, and consider the write operation w invoked by the process with the lowest id in $Req_2$. Assume that w’s argument is $v'$, and $Req_2$ was chosen in a consensus associated with timestamp $TS'$ (notice that $TS'<TS$). By the code of the decide handler and Lemma 4, in all the sm’s s.t. $sm.ts=TS'+1$, the value of sm.value is $v'$. Now, since there is no write operation in any chosen request between $Req_2$ and $Req_1$ in r, no process writes to sm.value when $TS'< sm.ts < TS$. Hence, when sm.lastOps[i] is set to $\langle n, val\rangle$, sm.value equals $v'$, and thus $val = v'$. Therefore, rd returns the value that is written by the last write operation that precedes rd in $\sigma _r$.

Corollary 1

Algorithms 1–3 implement an atomic storage service.

1.2 A.2 Liveness

Consider operation $op_i$ invoked at time t by a correct process $p_i$ in run r. Notice that r is a run with either infinitely or finitely many invocations. We show that, in both cases, if $p_i$ is active in r, then $op_i$ returns in r.

We associate the addition or removal of process $p_j$ by a process $p_i$ with the timestamp that equals $sm_i.ts$ at the time when the operation returns. The addition of all processes in $P_0$ is associated with timestamp 0.

First, we consider runs with infinitely many invocations. In Lemma 8, we show that for every process p, every sm associated with a larger timestamp than p’s addition contains p in sm.cng.mem. In Observation 2, we show that in a run with infinitely many invocations, for every timestamp ts, there is a completed operation that has a bigger timestamp than ts at the time of the invocation. Moreover, after the stabilization time of the FD, operations must help all the slow active processes in order to complete. In Lemma 9, we use the observation to show that any operation invoked in a run with infinitely many invocations returns.

Next, we consider runs with finitely many invocations. We show Lemma 10 that eventually all the active members of the last sm adopt it. Then, in Lemma 11, we show that every operation invoked by an active process completes. Finally, Theorem 2, stipulates that the algorithm satisfies wait-freedom.

Lemma 8

Assume the addition of $p_i$ is associated with timestamp TS in run r. If $p_i$ is active, then $p_i \in sm.cng.mem$ for every sm s.t. $sm.ts \ge TS$.

Proof

The proof is by induction on sm.ts. Base: If $p_i \in P_0$, then $p_i \in sm.cng.mem$ for all sm s.t. $sm.ts=0$. Otherwise, $\langle add,p_i \rangle$ is part of a request that is chosen in a consensus associated with timestamp $TS'=TS-1$, and thus, by Lemma 4, $p_i \in sm.cng.mem$ for all sm s.t. $sm.ts=TS'+1 = TS$. Induction: Process $p_i$ is active, so no process invokes $\langle remove,p_i \rangle$, and therefore, together with the validity of consensus, no chosen request contains $\langle remove,p_i \rangle$. Hence, if $p_i \in sm.cng.mem$ for sm with $sm.ts=k$, then $p_i \in sm.cng.mem$ for every sm s.t. $sm.ts = k+1$.

Claim

Consider a run r of the algorithm with infinitely many invocations. Then for every time t and timestamp TS, there is a completed operation that is invoked after time t by a process with $sm.ts > TS$ at the time of the invocation.

Proof

Recall that r is well-formed and only processes in V(t).join can invoke operations at time t. Therefore, there are infinitely many completed operations in r. Since a finite number of operations are completed with each timestamp, the claim follows.

Lemma 9

Consider an operation $op_i$ invoked at time t by an active process $p_i$ in a run r with infinitely many invocations. Then $op_i$ completes in r.

Proof

Assume by way of contradiction that $p_i$ is active and $op_i$ does not complete in r. Assume w.l.o.g. that $p_i$’s addition is associated with timestamps TS and $op_i$ is invoked with $opNum_i=n$. Consider a time $t'>t$ after $p_i$ invokes $op_i$ and the FD has stabilized. By Claim A.2, there is a completed operation $op_j$ in r, invoked by some process $p_j$ at a time $t'' > t'$ when $sm_j.ts > TS$, whose completion is associated with timestamp $TS'$. By Lemma 8, $p_i \in sm_j.cng.mem$, at time $t''$. Now by the algorithm and by the eventual strong accuracy property of the FD, $p_j$ proposes $op_j$ and $op_i$ in the same request, and continues to propose both of them until one is selected. Note that it is impossible for $op_j$ to be selected without $op_i$ since any process that helps $p_j$ after stabilization also helps $p_i$. Hence, since $op_j$ completes, they are both performed in the same decide handler. The run is well-formed, so $p_i$ does not invoke operations that are associated with $opNum_i > n$. Hence, following the time when $op_i$ is selected, for all sm s.t. $sm.ts > TS'$, $sm.lastOps[i].num = n$. Now, again by Claim A.2, consider a completed operation $op_k$ in r, that is invoked by some process $p_k$ at time $t'''$ after the stabilization time of the FD s.t. $sm_k.ts > TS'$ at time $t'''$. Operation $op_k$ cannot complete until $p_i$ receives $p_k$’s sm. Therefore, $p_i$ receives sm s.t. $sm.ts \ge TS'$, and thus $sm.lastOps[i].num = n$. Therefore, $p_i$ learns that $op_i$ was performed, and $op_i$ completes. A contradiction.

We now proceed to prove liveness in runs with finitely many invocations.

Definition 4

For every run r of the algorithm, and for any point t in r, let $TS_t$ be the timestamp associated with the last consensus that made a decision in r before time t. Define $sm^t$, at any point t in r, to be the sm’s state after the completion of the decide handler associated with timestamp $TS_t$ at any process. By Lemma 4, $sm^t$ is unique. Recall that $sm^0$ is the initial state.

Claim

For every run r of the algorithm, and for any point t in r, there is a majority of $sm^t.cng.mem$ M s.t. $M \subseteq (V(t).membership \cup P(t).join) \setminus F(t)$.

Proof

By the code of the algorithm, for every run r and for any point t in r, $V(t).membership\subseteq sm^t.cng.mem$ and $sm^t.cng.mem \cap V(t).remove=\{\}$. The claim follows from failure condition.

Observation 2

Consider a run r of the algorithm with finitely many invocations. Then there is a point t in r s.t. for every $t'>t$, $sm^t=sm^{t'}$. Denote this sm to be $\hat{sm}$.

The following lemma follows from Lemma 4, Claim A.2, and the periodic update messages; for space limitations, we omit its proof.

Lemma 10

Consider a run r of the algorithm with finitely many invocations. Then eventually for every active process $p_i \in \hat{sm}.cng.mem$, $sm_i=\hat{sm}$.

Lemma 11

Consider an operation $op_i$ invoked at time t by an active process $p_i$ in a run r with finitely many invocations. Then $op_i$ completes in r.

Proof

By Lemma 8, $p_i \in \hat{sm}.cng.mem$, and by Lemma 10, there is a point $t'$ in r s.t. $sm_i=\hat{sm}$ for all $t \ge t'$. Assume by way of contradiction that $op_i$ does not complete in r. Therefore, $op_i$ is either stuck in one of its waits or continuously iterates in a while loop. In each case, we show a contradiction. Denote by con the consensus associated with timestamp $\hat{sm}.ts$. By definition of $\hat{sm}$, no decision is made in con in r.

• Operation $op_i$ waits in line 16 (Algorithm 2) forever. Notice that $\hat{sm}.cng.rem$ contains all the process that were removed in r, so, after time $t'$, $p_i$ does not wait for a reply from a removed process. By the strong completeness property of FD, $p_i$ does not wait for faulty processes forever. A contradiction.

• Operation $op_i$ waits in line 18 (Algorithm 2) forever. Notice that from time $t'$ till $p_i$ proposes in con, $pend_i$  = false. Therefore, $p_i$ proposes in con in line 22 (Algorithm 2), and waits in line 18 after the propose. By Observation 2, there is a majority M of $\hat{sm}.cng.em$ s.t. $M \subseteq V(t).membership \cup P(t).join \setminus F(t)$. Therefore, by the termination of consensus, eventually a decision is made in con. A contradiction to the definition of $\hat{sm}$.

• Operation $op_i$ remains in the while loop in line 17 (Algorithm 2) forever. Since it does not waits in line 18 (Algorithm 2) forever, $op_i$ proposes infinitely many times, and since each propose is made in a different consensus and $p_i$ can propose in a consensus beyond the first one only once a decision is made in the previous one, infinitely many decisions are made in r. A contradiction to the definition of $\hat{sm}$.

• Operation $op_i$ waits in line 27 (Algorithm 2) forever. Consider two cases. First, $sm_i \ne \hat{sm}$ when $p_i$ performs line 26 (Algorithm 2). In this case, $p_i$ continues at time $t'$, when it adopts $\hat{sm}$, because $sm_i.ts>ts$ hold at time $t'$. In the second case ($sm_i = \hat{sm}$ when $p_i$ performs line 26), $p_i$ sends update message to all processes in $\hat{sm}.cng.mem$, and waits for a majority to reply. By Observation 2, there is a correct majority in $\hat{sm}.cng.mem$, and thus $p_i$ eventually receives the replies and continues. In both cases we have contradiction.

Therefore, $p_i$ completes in r.

We conclude with the following theorem:

Theorem 2

Algorithms 1–3 implement wait-free atomic dynamic storage.