PROOF. Suppose we fix trace $\mathcal{T}_{t_k}$. We prove by induction on $t \ge t_k$ that if $\tau \in Q_{k-2} \setminus D'_{t-1}$ then

$$ \mathrm{Pr}[\tau_k = \tau | \mathcal{T}_t, \tau_k \in Q_{k-2} \setminus (D'_{t-1} \cup S_t)] = \pi(\tau)/\pi(Q_k \setminus D'_{t-1}), \quad (16) $$

where

$$ D'_{t} = \begin{cases} D_t & \text{if } t \ge t_k \\ \emptyset & \text{if } t < t_k. \end{cases} $$

For the base case $t = t_k$, we have that event $\tau_k \in Q_{k-2} \setminus (D'_{t-1} \cup S_t)$ is the same as $\tau_k \in Q_{k-2}$, because $D'_{t_k-1} = \emptyset$ and from Definition 3.27 and Lemma 3.50 it follows $\tau_k \notin S_{t_k}$. Thus, for $t = t_k$, the left side of (16) equals

$$ \mathrm{Pr}[\tau_k = \tau | \mathcal{T}_{\tau_k}, \tau_k \in Q_{k-2}]. $$

And if $\tau \in Q_{k-2}$, the above probability equals $\pi(\tau)/\pi(Q_k) = \pi(\tau)/\pi(Q_k \setminus D'_{t_k-1})$. This proves the base case of the induction.

For the induction step, we fix $t \ge t_k$, and we show that if $\tau \in Q_{k-2} \setminus D_t$ then

$$ \mathrm{Pr}[\tau_k = \tau | \mathcal{T}_{t+1}, \tau_k \in Q_{k-2} \setminus (D_t \cup S_{t+1})] = \pi(\tau)/\pi(Q_k \setminus D_t). $$

If if $\tau \in Q_{k-2} \setminus D_t$ then

$$ \begin{align*} \mathrm{Pr}[\tau_k = \tau | \mathcal{T}_t, \tau_k \in Q_{k-2} \setminus (D_t \cup S_t)] &= \frac{\mathrm{Pr}[\tau_k = \tau | \mathcal{T}_t, \tau_k \in Q_{k-2} \setminus (D'_{t-1} \cup S_t)]}{\mathrm{Pr}[\tau_k \in Q_{k-2} \setminus D_t | \mathcal{T}_t, \tau_k \in Q_{k-2} \setminus (D'_{t-1} \cup S_t)]} \\ &= \frac{\frac{\pi(\tau)}{\pi(Q_k \setminus D'_{t-1})}}{\frac{\pi(\tau_k \in Q_{k-2} \setminus D_t)}{\pi(Q_k \setminus D'_{t-1})}} \\ &= \frac{\pi(\tau)}{\pi(\tau_k \in Q_{k-2} \setminus D_t)}, \end{align*} $$

where in the second line we applied induction hypothesis (16). We show next that if $\tau \in Q_{k-2} \setminus D_t$,

$$ \mathrm{Pr}[\tau_k = \tau | \mathcal{T}_{t+1}, \tau_k \in Q_{k-2} \setminus (D_t \cup S_{t+1})] = \mathrm{Pr}[\tau_k = \tau | \mathcal{T}_t, \tau_k \in Q_{k-2} \setminus (D_t \cup S_t)]. \quad (17) $$

Combining that with the previous equation completes the proof of induction step. Thus, it remains to show (17).

To prove (17) we must argue that the additional information about step $t+1$ contained in $\mathcal{T}_{t+1}$, when $\tau_k \notin S_{t+1}$, does not change the distribution of $\tau_k$. Let $p$ denote the process that executes step $t+1$. If $p$ did not have a pending next operation before step $t+1$, let $mc$ denote the method call of $B$ that $p$ invokes in step $t+1$ (BDCAS() or read()) along with its arguments ($mc = \perp$ otherwise). Let $\mathcal{T}_t^+ = \mathcal{T}_t \cup \{(p, mc)\}$. We can replace $\mathcal{T}_t$ on the right side on (17) by $\mathcal{T}_t^+$, because revealing $p, mc$ does not reveal any new information about $\tau_k$, since $\mathcal{T}_t$ already contains all information that the adversary knows of at the end of step $t$.

Suppose that we fix $\mathcal{T}_t^+$, and that $\tau_k \in Q_{k-2} \setminus (D_t \cup S_t)$. Next we consider all possibilities for step $t+1$.

**Case 1: Step $t+1$ is a step of call read(a).** From $\mathcal{T}_t^+$, we can infer if step $t+1$ is the first step of call read(a): Process $p$ executes the first step of read(a) if indicated in $mc \neq \perp$, or if in its last step before step $t+1$, $p$ just finished the call in line 48 or finished the first read() call in line 49 (and the BDCAS() call did not return at that step).

If $a \neq x$ then we can infer from $\mathcal{T}_t^+$ exactly which operation process $p$ executes at step $t+1$ (including its outcome), as well as the return value of the call if a return command is executed. This is also true if $a = x$, even though $\mathcal{T}_t^+$ does not indicate the value of $A[x]$: It suffices that $\mathcal{T}_t^+$ contains the points at which the value of $A[x]$ changes, to infer the value of $A[x].stat$ and the value of $A[x].old_0$, and also to infer the value of $A[x].new_0$ when $A[x].stat = \text{True}$.

Therefore, $\mathcal{T}_{t+1}$ does not contain any information that cannot be inferred from $\mathcal{T}_t^+$.
**Case 2:** *Step t+1 is a step of call finish(a).* From $\mathcal{T}_t^+$, we can infer if step $t+1$ is the first step of call finish(a). There are several possibilities for the previous step for $p$, but only two involve if statements. First, $p$ invokes finish(a) call in line 48 if in its previous step $p$ executed line 54 and the if-condition was false. However, the value of the if-condition can be inferred from $\mathcal{T}_t$ (this is true also when $a_0 = x$, since $\mathcal{T}_t$ contains the points at which the value of $A[x]$ changes). Second, $p$ invokes finish(a) call in line 57 if in its previous step $p$ evaluated to false one of the two if-conditions in line 55. However, we will argue in Case 3 that when $\tau_k \in Q_{k-2} \setminus (D_t \cup S_t)$, trace $\mathcal{T}_t$ contains the value of $\gamma'$ if $\gamma' \neq \tau_k$, and if $\gamma' = \tau_k$ then we can infer from $\mathcal{T}_t$ the value of $\gamma'.old_0$.

We can assume that $a \neq x$, since otherwise we can infer from $\mathcal{T}_t^+$ exactly which operation process $p$ executes at step $t+1$ (including its outcome). Suppose also that $p$ does not executes an operation from lines 59–61 at step $t+1$, since they are just read operations.

First, suppose that the task that $p$ reads on $A[x]$ in line 59 of the call is $\tau \neq \tau_k$. Then $A[x] = \tau$ at some point before $t$ (precisely, at the point when $p$ reads $A[x]$). Also $L_t[x].val = \tau_k$, otherwise Lemmas 3.42 and 3.51 would contradict that $\tau_k \in Q_{k-2} \setminus (D_t \cup S_t)$. It follows that a successful unlock($\tau$) call was invoked before $t_k$, and thus the value of $\tau$ can be inferred from $\mathcal{T}_t$. Therefore, as in case $a \neq x$, we can infer from $\mathcal{T}_t^+$ exactly which operation process $p$ executes at step $t+1$.

Next we assume that $p$ reads task $\tau_k$ on $A[x]$ in line 59. From Lemma 3.44 and assumption $\tau_k \in Q_{k-2} \setminus (D_t \cup S_t)$, it follows that

(i) if $p$ executes line 62 at step $t+1$, the CAS() operation fails,

(ii) if $p$ executes line 64 at $t+1$, the CAS() operation is successful, and

(iii) $p$ does not execute the CAS() operation in line 67 at $t+1$.

From (i), if $p$ executes line 62, then nothing happens. (Note that if the CAS() were successful, it would reveal $\tau_k.add_1$!) From (ii), if $p$ executes line 64 at $t+1$, then $\tau_k \in S_{t+1}$. Hence, this case is not relevant to the proof of (17), because the probability on the left side is conditional on $\tau_k \notin S_{t+1}$. Moreover, $p$ does not execute lines 65 and 66 at $t+1$, because $p$ must have previously executed line 64. Finally, if $p$ executes an operation in line 63, then nothing happens.

Therefore, $\mathcal{T}_{t+1}$ does not contain any information that cannot be inferred from $\mathcal{T}_t^+$.

**Case 3:** *Step t + 1 is a step of call BDCAS().* We have already considered the case where step $t+1$ is a step of a method finish() or read() invoked in one of lines 48, 49 and 57. Also, if $p$ creates a new task at step $t+1$, in line 50, then this information can be inferred from $\mathcal{T}_t^+$. So, we assume that $p$ executes an operation in one of the remaining lines, lines 51–56 and 58, at step $t+1$.

Suppose first that the DCAS() operation is not applied to address $x$. Then the exact operation that $p$ executes at step $t+1$ (and its outcome) can be inferred from $\mathcal{T}_t^+$, in all cases except for two which involve a randomized decision: when $p$ executes line 2 of the propose() call invoked in line 51; and when $p$ executes line 34 during an unlock() call invoked in line 58. In both cases, however, knowing the random values involved in the operations does not provide any additional information about $\tau_k$.

For the remainder of the proof, we assume that the DCAS() operation is applied to address $x$. If $p$ executes the propose() operation in line 51 at step $t+1$, then, as before, knowing the randomness involved in the operations does not reveal any information about $\tau_k$ (recall that $\mathcal{T}_{t+1}$ contains random value $\alpha$). If $p$ executes a step of choose&lock() in line 52, then $\mathcal{T}_{t+1}$ provides no new information as $B$ does not change, because from Lemma 3.51 and assumption $\tau_k \in Q_{k-2} \setminus (D_t \cup S_t)$, it follows that $L_{t+1}[x].val = L_t[x].val = \tau_k$. Moreover, we can infer from $\mathcal{T}_t^+$ whether $t+1$ is the last step of call choose&lock(). If $p$ executes the RC read() operation in line 53 at step $t+1$, then no new information is revealed. The same is true if $p$ executes the if operation in line 54, and moreover the value of the if-condition can be inferred from $H_t^+$. It remains to consider the case where $p$ executes an operation in one of lines 55, 56 and 58 in step $t+1$.
First we assume that the value that *p* read in *line 53* during the same while-loop iteration is $\tau \neq \tau_k$. As noted above, from **Lemma 3.51** and assumption $\tau_k \in Q_{k-2} \setminus (D_t \cup S_t)$, it follows that $L_{t+1}[x].val = L_t[x].val = \tau_k$. Thus, $L_y[x].val = \tau$ for some $y < t$, which implies that a successful $L[x].Unlock(\tau)$ call was invoked before $t$. And since $\mathcal{T}_t$ contains the arguments of all method calls invoked, we conclude that $\mathcal{T}_t$ contains the value of $\tau$.

Suppose that *p* executes the operation in *line 55* at step $t+1$ (only the second of the two if-conditions involves a shared memory operation). This happens if $\tau \neq \perp$, and in its previous step *p* evaluated to true the if-condition in *line 54*. These can be inferred from $\mathcal{T}_t^+$, as well as the value of the second condition in *line 55*, evaluated at step $t+1$. Hence, $\mathcal{T}_{t+1}$ does not contain any additional information.

Next suppose that *p* executes the CAS() operation in *line 56* at step $t+1$. This happens if in its previous step, *p* evaluated to true the if-conditions in *line 54* (which can be inferred from $\mathcal{T}_t^+$). The outcome of the operation can also be inferred from $\mathcal{T}_t^+$.

Last suppose that *p* executes a step of operation unlock($\tau$) in *line 58* at step $t+1$. Recall that the value of $\tau$ is contained in $\mathcal{T}_t$, and $L_{t+1}[x].val = \tau_k \neq \tau$. It follows from **Claim 2.19** that step $t+1$ does not change the values of any of $L[x].S$, $L[x].P$, or $L[x].T$ [1]. Hence, $\mathcal{T}_{t+1}$ does not contain more information than $\mathcal{T}_t^+$.

Finally, we need to consider the case where *p* executes an operation in one of *lines 55, 56* and *58* in step $t+1$, and *p* previously read value $\tau_k$ in *line 53* in the same while-loop iteration. From assumption $\tau_k \in Q_{k-2} \setminus (D_t \cup S_t)$ it follows that $\tau_k \neq \perp$ and $\tau_k.old_0 = B_t[x].val'$, where $B_t[x].val'$ can be inferred from $\mathcal{T}_t$. If *p* executes *line 55* at step $t+1$ (which is possible since $\tau_k \neq \perp$), we can then infer from $H_t^+$ the value of the second if-condition. If *p* executes the CAS() operation in *line 56* at step $t+1$, then the outcome, success or failure, of the CAS operation can also be inferred from $\mathcal{T}_t^+$. Finally, it is not possible that *p* executes a step of call unlock($\tau_k$) in *line 58*, because otherwise **Lemma 3.60** would contradict that $\tau_k \notin D_t \cup S_t$.

This concludes the proof of (17), and the proof of **Lemma 3.32**.

□

## 3.7 k-Fated Tasks

We lower bound the expected number of tasks $\tau \in Q_{k-2}$ that are doomed or successful by the time that task $\tau_k$ itself is also doomed or successful. We call those tasks k-fated, and give their formal definition below.

**Definition 3.33 (k-Fated Tasks).** For $k \ge 2$, let $\rho_k$ be the following point

$$ \rho_k = \begin{cases} \min\{t: \tau_k \in D_t \cup S_t, t \ge t_k\}, & \text{if } \tau_k \in Q_{k-2} \\ t_k, & \text{otherwise.} \end{cases} $$

We define the set $F_k$ of k-fated tasks as

$$ F_k = Q_{k-2} \cap (D_{\rho_k} \cup S_{\rho_k}), $$

and let $f_k = |F_k|$.

From **Lemma 3.45**, it follows that point $\rho_k$, $k \ge 2$, always exists. Also, from **Lemma 3.51**, it follows that for all $k \ge 2$,

$$ t_k \le \rho_k < t_{k+1}. \qquad (18) $$

To show the main result we will need the next two lemmas. The first one is based on **Lemma 3.32**.

**LEMMA 3.34.** Let $k \ge 2$, and for any $t \ge 0$ let

$$ Z_t = Q_{k-2} \cap (D_t \cup S_t). $$

If $\tau \in Q_{k-2}$ and $t \ge t_k$ then

$$ \Pr[\tau_k = \tau | \mathcal{T}_{t_k}, \tau_k \in Q_{k-2}, t \le \rho_k, Z_{t_k} \dots Z_t] = \Pr[\tau_k = \tau | \mathcal{T}_{t_k}, \tau_k \in Q_{k-2}, t \le \rho_k, Z_{t_k} \dots Z_{t-1}]. $$
PROOF. Suppose that we fix trace $\mathcal{T}_{t_k}$. First we argue that no task in $Q_{k-2}$ is successful at point $\rho_k$ except possibly for $\tau_{k-1}$ and $\tau_k$, i.e.,

$$ (Q_{k-2} \setminus \{\tau_{k-1}, \tau_k\}) \cap S_{\rho_k} = \emptyset. $$

Suppose that $\tau \in Q_{k-2} \cap S_{\rho_k}$. Then Lemma 3.50 implies $L_y[x].val = \tau$ at some point $y \le \rho_k$. From Lemma 3.51 and the definition of $\rho_k$, it follows that $L_t[x].val$ remains the same for all $t_k \le t \le \rho_k$. Thus, $y \le t_k$. Moreover, $y \ge t_{k-1}$ because $r_\tau > t_{k-2}$, hence the earliest point that $\tau$ can be written to $L[x].val$ is $t_{k-1}$. Since $\tau_{k-1}$ and $\tau_k$ are the only values of $L_y[x].val$ for $t_{k-1} \le y \le t_k$, it follows that $\tau \in \{\tau_{k-1}, \tau_k\}$.

Next we argue that

$$ \tau_k \in S_{\rho_k} \implies Q_{k-2} \setminus \{\tau_{k-1}, \tau_k\} \subseteq D_{\rho_k}. $$

Suppose that $\tau_k \in S_{\rho_k}$. Then Lemma 3.50 implies $\rho_k > t_k$. At point $\rho_k$, a process $p$ changes the value of $A[\tau_k.add_1]$ to $\tau_k$, by executing a successful CAS() operation in line 64. This operation changes also the imminent interpreted value $B[x].val'$. As we saw above, no task $\tau \in Q_{k-2} \setminus \{\tau_{k-1}, \tau_{k-2}\}$ gets written to $L[x].val$ before $\rho_k$, and thus neither does it get written to array $A$ before $\rho_k$. Hence, the change in the imminent interpreted value $B[x].val'$ at point $\rho_k$ implies $\tau \in D_{\rho_k}$, for all $\tau \in Q_{k-2} \setminus \{\tau_{k-1}, \tau_{k-2}\}$.

Let

$$ A = \{\tau_{k-1}\} \cap Q_{k-2} \cap S_{t_k}, $$

i.e., $A = \{\tau_{k-1}\}$ if $\tau \in Q_{k-2} \cap S_{t_k}$, and $A = \emptyset$ otherwise. The value of $\tau_{k-1}$ can be inferred from $\mathcal{T}_{t_k}$, because between points $t_{k-1}$ and $t_k$ a successful unlock($\tau_{k-t}$) call is invoked, and $\mathcal{T}_{t_k}$ contains the arguments of all invoked method calls. Moreover, we have

$$ \tau_{k-1} \in Q_{k-2} \implies \tau_{k-1} \in D_{t_k} \cap S_{t_k}, $$

because if $\tau_{k-1} \in Q_{k-2}$ then $\tau_{k-1} \in D_{\rho_{k-1}} \cap S_{\rho_{k-1}}$, and $\rho_{k-1} < t_k$ by (18). Thus set $A$ can be inferred from $\mathcal{T}_{t_k}$.

Combining the above, and the definition of $Z_t = Q_{k-2} \cap (D_t \cup S_t)$, we obtain that

$$ Z_t = \begin{cases} (Q_{k-2} \cap D_t) \cup A, & \text{if } t_k \le t < \rho_k, \text{ or if } t = \rho_k \text{ and } \tau_k \notin S_{\rho_k} \\ Q_{k-2}, & \text{if } t = \rho_k \text{ and } \tau_k \in S_{\rho_k}. \end{cases} $$

Let $t \ge t_k$, and suppose that $t \le \rho_k$. Let $p$ be the process that executes step $t$. We distinguish three cases, depending on the following event:

$\mathcal{E}$ is the event that process $p$ just finished line 63 of call finish($x$) in its last step before step $t$, and moreover $p$ read $A[x] = \tau_k$ in line 59 of the same call.

Case 1: event $\mathcal{E}$ holds. In this case, $t = \rho_k > t_k$ and $\tau_k \in S_t$. The reason is that in step $t$ process $p$ executes either line 64 or line 67, since it just completed line 63 in its previous step. But, from Lemma 3.44, if $p$ executed a failed CAS() in line 64, or executed line 67, it would imply $\rho_k < t$. Thus, the only possibility left is that $p$ executes a successful CAS() in line 64, and thus $t = \rho_k$ and $\tau_k \in S_t$.

Then $Z_t = Q_{k-2}$, as we saw above. Therefore, the value of $Z_t$ is completely determined in this case (as $Q_{k-2}$ can be inferred from $\mathcal{T}_{t_k}$). It follows that for any $\tau \in Q_{k-2}$,

$$ \Pr[\tau_k = \tau | \tau_k \in Q_{k-2}, t \le \rho_k, \mathcal{E}, Z_{t_k}, \dots, Z_t] = \Pr[\tau_k = \tau | \tau_k \in Q_{k-2}, t \le \rho_k, \mathcal{E}, Z_{t_k}, \dots, Z_{t-1}]. $$

Case 2: event $\tilde{\mathcal{E}}$ holds and $t > t_k$. In this case we have that $\tau_k \notin S_t$. Then, from Lemma 3.32, if $\tau \in Q_{k-2} \setminus D_{t-1}$,

$$ \Pr[\tau_k = \tau | \mathcal{T}_t, \tau_k \in Q_{k-2} \setminus (D_{t-1} \cup S_t)] = \pi(\tau)/\pi(Q_{k-2} \setminus D_{t-1}). $$

For the left side we have that event $\tau_k \in Q_{k-2} \land t \le \rho_k \land \tilde{\mathcal{E}}$ implies $\tau_k \in Q_{k-2} \setminus (D_{t-1} \cup S_t)$, and moreover $D_{t_k}, \dots, D_t$ and thus $Z_{t_k}, \dots, Z_t$ can be inferred from $\mathcal{T}_t$. For the right side we have that $\pi(Q_{k-2} \setminus D_{t-1}) = \pi(Q_{k-2} \setminus Z_{t-1})$. Therefore, the above equation implies that if $\tau \in Q_{k-2} \setminus Z_{t-1}$,

$$ \Pr[\tau_k = \tau | \tau_k \in Q_{k-2}, t \le \rho_k, \tilde{\mathcal{E}}, Z_{t_k} \dots Z_t] = \pi(\tau)/\pi(Q_{k-2} \setminus Z_{t-1}). $$
(Thus, the probability is zero if $\tau \notin Q_{k-2} \setminus Z_{t-1}$.) Since the right side is independent of $Z_t$, it follows

$$ \Pr[\tau_k = \tau | \tau_k \in Q_{k-2}, t \le \rho_k, \tilde{\mathcal{E}}, Z_{t_k} \dots Z_t] = \Pr[\tau_k = \tau | \tau_k \in Q_{k-2}, t \le \rho_k, \tilde{\mathcal{E}}, Z_{t_k} \dots Z_{t-1}]. $$

Combining Cases 2 and 3 proves the lemma for the case where $t > t_k$.

Case 3: $t = t_k$. For every $\tau \in Q_{k-2}$, we have

$$ \Pr[\tau_k = \tau | \tau \in Q_{k-2}] = \pi(\tau)/\pi(Q_{k-2}). $$

As in Case 2, $D_{t_k}$ and thus $Z_{t_k}$ can be inferred from $\mathcal{T}_{t_k}$, and the right side does not depend on $Z_{t_k}$. Therefore, the lemma holds in this case, as well. $\square$

The next lemma analyzes a very simple game.

**LEMMA 3.35 (GUESSING GAME).** Consider the following game. An element $g^*$ of a finite set $G$ is sampled at random according to a distribution $\lambda$, such that $\max_{g \in G} \lambda(g) \le \epsilon < 1$. The player, who knows $G$ and $\lambda$, tries to guess $g^*$ in a sequence of attempts. In each attempt $i$, the player proposes a set $G_i \subseteq G$. If $g^* \in G_i$ the game ends and the player's score is $\sum_{j \le i} |G_j|$. Then, for any player strategy, the expected score is at least $(2\epsilon)^{-1}$.

**PROOF.** Clearly, proposing more than one elements in an attempt, or proposing an element twice can only increase the player's score. Hence, we can assume that the player just decides an order $g_1, g_2, \dots, g_{|G|}$ in which the elements are proposed, one element per attempt. The expected score is then

$$ \sum_{1 \le i \le |G|} i \cdot \lambda(g_i) \ge \sum_{1 \le i \le \lfloor 1/\epsilon \rfloor} i \cdot 1/\lfloor 1/\epsilon \rfloor, $$

where the inequality holds because $\lambda(g_i) \le \epsilon \le 1/\lfloor 1/\epsilon \rfloor$, and thus we can obtain a lower bound of the sum by assigning to each of the first $\lfloor 1/\epsilon \rfloor$ elements probability $1/\lfloor 1/\epsilon \rfloor$, and to the remaining ones probability zero. The desired lower bound then follows from

$$ \sum_{1 \le i \le \lfloor 1/\epsilon \rfloor} i \cdot 1/\lfloor 1/\epsilon \rfloor = \frac{\lfloor 1/\epsilon \rfloor \cdot (1 + \lfloor 1/\epsilon \rfloor)}{2} \cdot 1/\lfloor 1/\epsilon \rfloor \ge \frac{1/\epsilon}{2}. \quad \square $$

We are now ready to prove the main lemma of this section, which provides a lower bound on the expected value of $f_k$ given $\mathcal{T}_{t_k}$.

**LEMMA 3.36.** For $k \ge 2$ and $n \ge 157$,

$$ \mathbb{E}[f_k | \mathcal{T}_{t_k}] \ge \frac{1}{40} \cdot (1 - 4 \Pr[\mathcal{B}_{k-2} | \mathcal{T}_{t_k}]) \cdot g_{k-2}. $$

**PROOF.** Suppose that we fix $\mathcal{T}_{t_k}$ and that $g_{k-2} > 0$, otherwise the lemma holds trivially. As in Lemma 3.32, we denote by $\pi(\cdot)$ the probability distribution of $\tau_k$. We have

$$ \mathbb{E}[f_k] \ge \mathbb{E}[f_k | \tau_k \in Q_{k-2}] \cdot \Pr[\tau_k \in Q_{k-2}] \ge \mathbb{E}[f_k | \tau_k \in Q_{k-2}] \cdot \pi(Q_{k-2}). \quad (19) $$

Next we lower bound $\mathbb{E}[f_k | \tau_k \in Q_{k-2}]$, by expressing $f_k$ as the score of the game described in Lemma 3.35, using Lemma 3.34. Let $Z_t = Q_{k-2} \cap (D_t \cup S_t)$, for $t \ge 0$, as in Lemma 3.34. For each $t > t_k$, let

$$ G_t = Z_t \setminus Z_{t-1}, $$

and let $G_{t_k} = Z_{t_k}$. Then Lemma 3.34 gives that, for any $\tau \in Q_{k-2}$ and $t \ge t_k$,

$$ \Pr[\tau_k = \tau | \tau_k \in Q_{k-2}, t_k \le \rho_k, G_{t_k} \dots G_t] = \Pr[\tau_k = \tau | \tau_k \in Q_{k-2}, t_k \le \rho_k, G_{t_k} \dots G_{t-1}]. $$
Therefore, given $\tau_k \in Q_{k-2}$, $t \le \rho_k$, $G_{t_k} \dots G_{t-1}$, we have that $G_t$ is independent of $\tau_k$. It follows that the sequence $G_{t_k}$, $G_{t_k+1}$, \dots corresponds to a randomized player strategy for the guessing game of Lemma 3.35, where $G = Q_{k-2}$, $g^* = \tau_k$, and for each $\tau \in Q_{k-2}$,

$$ \lambda(\tau) = \Pr[\tau_k = \tau | \tau_k \in Q_{k-2}] = \pi(\tau)/\pi(Q_k). $$

Then Lemma 3.35 gives

$$ E \left[ \sum_{t_k \le t \le \rho_k} |G_t| \mid \tau_k \in Q_{k-2} \right] \ge \left( 2 \max_{\tau \in Q_{k-2}} \lambda(\tau) \right)^{-1} = \left( 2 \max_{\tau \in Q_{k-2}} \pi(\tau)/\pi(Q_k) \right)^{-1} \ge \pi(Q_k) \cdot g_{k-2}/20, $$

where for the last inequality we used Corollary 3.30 to obtain that $\pi(\tau) \le 20/g_{k-2}$ (recall we have assumed $g_{k-2} > 0$). And since $F_k = Q_{k-2} \cap (D_{\rho_k} \cup S_{\rho_k}) = Z_{\rho_k} = \bigcup_{t_k \le t \le \rho_k} G_t$, we have $f_k = |F_k| = \sum_{t_k \le t \le \rho_k} |G_t|$, and the inequality above yields

$$ E[f_k | \tau_k \in Q_{k-2}] \ge \pi(Q_{k-2}) \cdot g_{k-2}/20. $$

Substituting this to (19) gives

$$ E[f_k] \ge (\pi(Q_k))^2 \cdot g_{k-2}/20. $$

Finally,

$$ \begin{aligned} (\pi(Q_k))^2 &= (1 - \Pr[\tau_k \notin Q_k])^2 \ge 1 - 2 \Pr[\tau_k \notin Q_k] \\ &\ge 1 - 2(\Pr[\tau_k = \perp] + \Pr[(\tau_k \notin Q_{k-2} \cup \{\perp\}) \wedge \tilde{B}_k] + \Pr[\mathcal{B}_k]) \\ &\ge 1 - 2((1/\log n)^{g_{k-2}} + 6/\log^2 n + \Pr[\mathcal{B}_k]) \\ &\ge 1/2 - 2 \Pr[\mathcal{B}_k], \end{aligned} $$

where in the second-last line we used Corollaries 3.30 and 3.31, and the last line holds for $n \ge 157$. Substituting this to the previous inequality gives

$$ E[f_k] \ge (1/2 - 2 \Pr[\mathcal{B}_k]) \cdot g_{k-2}/20, $$

which concludes the proof of Lemma 3.36. $\square$

## 3.8 Lower Bounding the Sum of k-Fated Tasks

In this section and the next one, we establish respectively a lower bound and an upper bound on the sum of $f_k$ in execution $E'$. In particular, in this section we lower bound the expectation of that sum in terms of the expected number of propose() operations on object $L[x]$. We introduce some notation first.

**Definition 3.37 (C$_x$ and $\Pi_x$).** By $C_x$ we denote the number of successful $L[x].choose&lock()$ calls in $E'$,

$$ C_x = \max\{k: t_k \le |E'|\}. $$

By $\Pi_x$ we denote the number of $L[x].propose()$ operations in $E'$,

$$ \Pi_x = |\{\tau: \tau.add_0 = x, r_{\tau} \le |E'|\}|. $$

**LEMMA 3.38.** For all $n \ge 531$, $^3$

$$ E \left[ \sum_{2 \le k \le C_x + 2} f_k \right] \ge \frac{1}{160} \cdot E[\Pi_x]. $$

<footnote>$^3$We sum for $k$ up to $C_x + 2$ rather than up to $C_x$ for a technical reason, but we will see later that the difference is at most a constant.</footnote>
PROOF. We have

$$ \mathbf{E} \left[ \sum_{2 \le k \le C_x + 2} f_k \right] = \sum_{k \ge 2} \mathbf{E}[f_k \cdot \mathbf{1}_{k \le C_x + 2}]. $$

Recall that if $t \ge |E'|$ then $\mathcal{T}_t$ indicates which one was the last step of $E'$. Hence, we can infer from $\mathcal{T}_{t_k}$ if $t_k \le |E'|$, and thus if $k \le C_x$. In fact, we can infer from $\mathcal{T}_{t_k}$ if $k \le C_x + j$ for any given $j \ge 0$. We will use this observation several times below.

For $k \ge 2$,

$$ \begin{aligned} \mathbf{E}[f_k \cdot \mathbf{1}_{k \le C_x + 2} | \mathcal{T}_{t_k}] &= \mathbf{1}_{k \le C_x + 2} \cdot \mathbf{E}[f_k | \mathcal{T}_{t_k}] \\ &\ge \mathbf{1}_{k \le C_x + 2} \cdot \frac{1}{40} \cdot (1 - 4 \Pr[\mathcal{B}_{k-2} | \mathcal{T}_{t_k}]) \cdot g_{k-2} \tag{20} \\ &= \frac{1}{40} \cdot \mathbf{1}_{k \le C_x + 2} \cdot g_{k-2} - \frac{1}{10} \cdot \Pr[k \le C_x + 2 \wedge \mathcal{B}_{k-2} | \mathcal{T}_{t_k}] \cdot g_{k-2}, \end{aligned} $$

where the first equation holds because we can infer from $\mathcal{T}_{t_k}$ if $k \le C_x + 2$, and the second equation follows from Lemma 3.36.

For the first term in the last line of (20), we have

$$ \begin{aligned} \mathbf{E}[\mathbf{1}_{k \le C_x + 2} \cdot g_{k-2} | \mathcal{T}_{s_{k-2}}] &= \mathbf{1}_{k \le C_x + 2} \cdot \mathbf{E}[g_{k-2} | \mathcal{T}_{s_{k-2}}] \\ &= \mathbf{1}_{k \le C_x + 2} \cdot \mathbf{E}[p_{k-2} | \mathcal{T}_{s_{k-2}}]/2 \\ &= \mathbf{E}[\mathbf{1}_{k \le C_x + 2} \cdot p_{k-2} | \mathcal{T}_{s_{k-2}}]/2, \end{aligned} $$

where the first equation holds because we can infer if $k \le C_x + 2$ from $\mathcal{T}_{t_{k-2}}$ and thus also from $\mathcal{T}_{s_{k-2}}$,<fnref n="4" /> and the second equation holds because of equation (14) in Corollary 3.30. It follows

$$ \mathbf{E}[\mathbf{1}_{k \le C_x + 2} \cdot g_{k-2}] = \mathbf{E}[\mathbf{1}_{k \le C_x + 2} \cdot p_{k-2}]/2. \tag{21} $$

For the second term in the last line of (20), we have

$$ \Pr[k \le C_x + 2 \wedge \mathcal{B}_{k-2} | \mathcal{T}_{t_k}] \cdot g_{k-2} \le \Pr[k \le C_x + 2 + \lambda \wedge \mathcal{B}_{k-2} | \mathcal{T}_{t_k}] \cdot 3n, $$

because $g_{k-2} \le p_{k-2} \le 3n$, where the second inequality follows from Lemma 3.56. Let $j \ge 0$ be such that $0 \le j \cdot \lambda \le k - 2 < (j + 1)\lambda$. Then

$$ \Pr[k \le C_x + 2 + \lambda \wedge \mathcal{B}_{k-2} | \mathcal{T}_{s_{j\lambda}}] = \mathbf{1}_{k \le C_x + 2 + \lambda} \cdot \Pr[\mathcal{B}_{k-2} | \mathcal{T}_{s_{j\lambda}}] \le \mathbf{1}_{k \le C_x + 2 + \lambda} \cdot n^{-2}. $$

where the last inequality follows from equation (15) in Corollary 3.31. Combining the last two equations gives

$$ \mathbf{E}[\Pr[k \le C_x + 2 \wedge \mathcal{B}_{k-2} | \mathcal{T}_{t_k}] \cdot g_{k-2}] \le \frac{3}{n} \cdot \Pr[k \le C_x + 2 + \lambda]. \tag{22} $$

From (20)-(22), we obtain

$$ \begin{aligned} \mathbf{E}[f_k \cdot \mathbf{1}_{k \le C_x + 2}] &\ge \frac{1}{40} \cdot \mathbf{E}[\mathbf{1}_{k \le C_x + 2} \cdot g_{k-2}] - \frac{1}{10} \cdot \Pr[k \le C_x + 2 \wedge \mathcal{B}_{k-2}] \cdot g_{k-2} \\ &\ge \frac{1}{80} \cdot \mathbf{E}[\mathbf{1}_{k \le C_x + 2} \cdot p_{k-2}] - \frac{3}{10n} \cdot \Pr[k \le C_x + 2 + \lambda]. \end{aligned} $$

<footnote n="4">⁴However we may not be able to infer if $k \le C_x$, and this is the reason for choosing the sum range to be up to $C_x + 2$ rather than up to $C_x$.</footnote>
Substituting that to the very first equation of the proof, gives

$$
\begin{align*}
\mathbf{E} \left[ \sum_{2 \le k \le C_x + 2} f_k \right] &\ge \frac{1}{80} \cdot \sum_{k \ge 2} \mathbf{E} \left[ \mathbb{1}_{k \le C_x + 2} \cdot p_{k-2} \right] - \frac{3}{10n} \cdot \sum_{k \ge 2} \mathrm{Pr} \left[ k \le C_x + 2 + \lambda \right] \\
&= \frac{1}{80} \cdot \mathbf{E} \left[ \sum_{2 \le k \le C_x + 2} p_{k-2} \right] - \frac{3}{10n} \cdot \mathbf{E} \left[ C_x + \lambda + 1 \right] \\
&= \frac{1}{80} \cdot \mathbf{E} \left[ \sum_{0 \le k \le C_x} p_k \right] - \frac{3}{10n} \cdot (\mathbf{E} \left[ C_x \right] + \lambda + 1).
\end{align*}
$$

Finally, since

$$
\sum_{0 \le k \le C_x} p_k \ge \Pi_x,
$$

and

$C_x \le \Pi_x,$

we conclude that

$$
\mathbf{E} \left[ \sum_{2 \le k \le C_x + 2} f_k \right] \ge \frac{1}{80} \cdot \mathbf{E} \left[ \Pi_x \right] - \frac{3}{10n} \cdot \left( \mathbf{E} \left[ \Pi_x \right] + \lambda + 1 \right) \ge \frac{1}{80} \cdot \mathbf{E} \left[ \Pi_x \right] - \frac{3}{10n} \cdot \left( \mathbf{E} \left[ \Pi_x \right] + \log n + 1 \right) \ge \frac{1}{160} \left( \mathbf{E} \left[ \Pi_x \right] + \log n + 1 \right),
$$

for all $n \ge 531$.

□

3.9 Upper Bounding the Sum of k-Fated Tasks

We compute now an upper bound on the sum of $f_k$, in terms of the number $N_x$ of BDCAS() operations on address $x$ invoked in $E$. Note that $N_x$ is also the number of BDCAS() operations on address $x$ invoked in $E'$.

LEMMA 3.39. There is a constant $c'' > 0$ such that

$$
\sum_{2 \le k \le C_x + 2} f_k \le c'' \cdot N_x.
$$

PROOF. Suppose that process $p$ invokes a BDCAS() operation involving address $x$. Let $\Gamma$ be the set of tasks that $p$ creates during that operation, and for $k \ge 0$ let

$$
\Gamma_k = \Gamma \cap Q_k = \{\tau : \tau \in \Gamma, t_k < r_{\tau} < t_{k+2}\}.
$$

From Lemma 3.55, it follows that for all $k \ge 0$,

$|\Gamma_k| \le c_1,$

for some constant $c_1$. We also argue that the following holds for some constant $c_2$, for any $k \ge 0$,

$$
\Gamma \cap F_{k+2} \neq \emptyset \implies |\{\tau : \tau \in \Gamma, r_{\tau} \geq t_{k+3}\}| \leq c_2.
$$

Indeed if $\tau \in \Gamma \cap F_{k+2}$ then $\tau \in D_{\rho_{k+2}} \cap S_{\rho_{k+2}}$, and lemma Lemma 3.54 implies that $|\{\tau : \tau \in \Gamma, r_{\tau} \ge \rho_{k+2}\}| \le c_2$.
Moreover, from (18), $\rho_{k+2} < t_{k+3}$.

We will now use the above observations to bound $\sum_{0 \le k \le C_k} |\Gamma \cap F_{k+2}|$, which is precisely the contribution of the BDCAS() operation to the sum $\sum_{2 \le k \le C_x + 2} f_k$ we are interested in. Suppose that $\sum_{0 \le k \le C_k} |\Gamma \cap F_{k+2}| \ne 0$, and
let $k^* = \min\{k: F_{k+2} \cap \Gamma \neq \emptyset\}$. Then

$$ \sum_{0 \le k \le C_x} |\Gamma \cap F_{k+2}| \le \sum_{k \ge k^*} |\Gamma \cap F_{k+2}| \le \sum_{k \ge k^*} |\Gamma \cap Q_k| \\ = \sum_{k \ge k^*} |\Gamma_k| = \sum_{k^* \le k \le k^*+2} |\Gamma_k| + \sum_{k \ge k^*+3} |\Gamma_k| \le 3c_1 + 2c_2. $$

This is a bound on the contribution of a single BDCAS() operation. The total number of BDCAS() operation on x invoked before step $t_{C_x+2}$ is at most $N_x + 2$, because $N_x$ such operations are executed in $E'$, and at most two are invoked before $t_{C_x+2}$ by the process that runs solo in the extension $E''$ of $E'$. It follows

$$ \sum_{2 \le k \le C_x + 2} f_k \le (3c_1 + 2c_2) \cdot (N_x + 2). \quad \square $$

### 3.10 Completing the Proof of Theorem 3.25

Combining Lemmas 3.38 and 3.39, we obtain that the expected number of proposals on $L[x]$ in $E'$ is at most linear in the expected number of BDCAS() operations on address $x$,

$$ E[\Pi_x] \le (c''/c') \cdot E[N_x]. $$

The final step is to bound the number of steps in terms of $\Pi_x$. Let $T_x$ denote the number of steps of BDCAS() operations on address $x$ in $E'$. Then $T_x$ is an upper bound on the number of steps of BDCAS() operations on $x$ in $E$. Since all method calls are completed in $E'$, it is immediate from the algorithm that the number of steps of the BDCAS() operations on $x$ in $E'$, excluding the steps of methods of $L[x]$ invoked by BDCAS(), is at most $c_1 \cdot \Pi_x$, for a constant $c_1$. The number of $L[x].choose&lock()$ calls and the number of of $L[x].read()$ calls are exactly the same as the number $\Pi_x$ of $L[x].propose()$ calls, and each choose&lock() call involves at most $c_2 \log \log n$ steps, for some constant $c_2$, while each propose() and read() call consists of one step. Finally, the number of $L[x]. unlock()$ calls is at most $\Pi_x$, and Corollary 2.13 gives that the expected number of their steps is at most $c_3 \log \log n \cdot E[\Pi_t]$. It follows

$$ E[T_x] \le c_1 \cdot E[\Pi_x] + c_2 \log \log n \cdot E[\Pi_x] + 2 \cdot E[\Pi_x] + c_3 \log \log n \cdot E[\Pi_x] = c \log \log n \cdot E[\Pi_x], $$

for a constant $c$. Combining this with the previous inequality yields

$$ E[T_x] \le (c \cdot c''/c') \cdot \log \log n \cdot E[N_x], $$

and concludes the proof of Theorem 3.25.

### 3.11 Auxiliary Lemmas

We show that the imminent interpreted value of $B[a]$, if different from the interpreted value of $B[a]$, is the next interpreted value that $B[a]$ takes.

**CLAIM 3.40.** If $B_t[a].val \neq B_t[a].val'$, then for the earliest point $t' > t$ at which $B_{t'}[a].val \neq B_t[a].val$, $B_{t'}[a].val = B_t[a].val'$. Also, the task stored in $A[a]$ is not replaced in the interval $(t, t']$.

**PROOF.** If $B_t[a].val \neq B_t[a].val'$, then by Definition 3.26, $A_t[a].stat \neq \text{True}$, $A_t[A_t[a].add_1] = A_t[a]$, $B_t[a].val = A_t[a].old_i$, and $B_t[a].val' = A_t[a].new_i$, as this is the only configuration in which interpreted values and imminent interpreted values differ. From Lemma 3.11 and that $A_t[A_t[a].add_1] = A_t[a]$, it follows that $A_t[a].stat = \perp$. From Claim 3.6 and that each step consists of only one shared memory operation, $A_t[a].stat$ changes to True before $A[a]$ is replaced with a different task. By definition of interpreted value, the point when $A_t[a].stat$ changes to True is $t'$, and $B_{t'}[a].val = A_t[a].new_i = B_t[a].val'$.

**COROLLARY 3.41.** For any $t \ge 0$, either $B_t[a].val = B_t[a].val'$ or $B_t[a].val \prec_a B_t[a].val'$.
PROOF. Suppose that $B_t[a].val \neq B_t[a].val'$. As in Claim 3.40, we have that by Definition 3.26, $A_t[a].stat = \perp$, $A_t[A_t[a].add_1] = A_t[a]$, $B_t[a].val = A_t[a].old_i$, and $B_t[a].val' = A_t[a].new_i$. Since $A_t[a].old_i \neq A_t[a].new_i$, the task stored in $A_t[a]$ is not an initial task. Thus, $A_t[a].old_i$ and $A_t[a].new_i$ are the parameters $old_i$ and $new_i$ of some BDCAS() operation which created the task stored in $A_t[a]$ in line 50 before $t$. Since $old_i <_a new_i$ from the irreflexivity requirement, the corollary follows. $\square$

LEMMA 3.42. For any $t \ge 0$, $D_t \subseteq D_{t+1}$ and $S_t \subseteq S_{t+1}$.

PROOF. Suppose that $\tau \in D_t$, and we will show that $\tau \in D_{t+1}$. Since $\tau \in D_t$, from Definition 3.27, $A_{t'}[\tau.add_1] \neq \tau$ for all $t' \le t$, and, for some $i \in \{0, 1\}$, $B_t[\tau.add_i].val' \neq \tau.old_i$. It suffices to show that $A_{t+1}[\tau.add_1] \neq \tau$ and $B_{t+1}[\tau.add_i].val' \neq \tau.old_i$.

The process $p_\tau$ which creates $\tau$ does not return in line 49, and therefore there exists a point $t_i < t_\tau \le t$ in which $p_\tau$'s read($\tau.add_i$) method returns $\tau.old_i$. By Lemma 3.15, $B_{t_i}[\tau.add_i].val = \tau.old_i$.

Since $B_t[\tau.add_i].val' \neq \tau.old_i$, from Claim 3.40 if $B[\tau.add_i].val$ changes after $t$ then there exists a point $t'' \ge t$ such that $B_{t''}[\tau.add_i].val = B_t[\tau.add_i].val' \neq \tau.old_i$. From Claim 3.13 and Corollaries 3.19 and 3.41, $\tau.old_i = B_{t_i}[\tau.add_i].val <_{\tau.add_i} B_{t'}[\tau.add_i].val$ for all $t^* \ge t''$. Therefore, $B_{t+1}[\tau.add_i].val' \neq \tau.old_i$.

Now suppose for the purpose of proving a contradiction that $A_{t+1}[\tau.add_1] = \tau$. By Claim 3.3, there is a point no later than $t+1$ at which $A[\tau.add_0] = \tau$; let $t_0$ be the earliest such point. Since at most one shared memory operation takes place per point in time and $A[\tau.add_1] \neq A[\tau.add_0]$ changes at point $t+1$, $t_0 \le t$. From Lemma 3.11, $\tau.stat \neq$ False throughout the execution. From Claim 3.5 and Lemma 3.7 and that $\tau$ is not an initial task, $\tau.stat$ does not change to True until after point $t+1$, and hence $\tau_t.stat = \perp$. Using Claim 3.6, we also have that $A_t[\tau.add_0] = \tau$. Since $A_t[A_t[\tau.add_0].add_1] = A_t[\tau.add_1] \neq \tau$, from Definition 3.26 $B_t[\tau.add_0].val' = \tau.old_0$, so it follows that $i=1$ and $B_t[\tau.add_1].val' \neq \tau.old_1$; again from Definition 3.26, we have that $B_t[\tau.add_1].val' = A_t[\tau.add_1].new_1 \neq \tau.old_1$. This contradicts Claim 3.8.

Now suppose that $\tau \in S_t$: then, there exists some $t' \le t$ such that $A_{t'}[\tau.add_1] = \tau$. Since $t' \le t < t+1$, it also follows that $\tau \in S_{t+1}$. $\square$

CLAIM 3.43. Suppose process $p$ creates task $\tau$ (in line 50) at some point $t_\tau$. Let $t_{read} < t_\tau$ be the linearization point of $p$'s read($a_1$) operation in line 49 during the same iteration of the while-loop. Further, let $t > t_\tau$.

(a) If the value of $A[\tau.add_1]$ changes during $[t_{read}, t]$, then $\tau \in S_t \cup D_t$.

(b) If there is a task $\tau^*$ with $\tau^*.add_1 = \tau.add_1$, such that $\tau^*.stat$ changes from $\perp$ to True in $[t_{read}, t]$, then $\tau \in S_{t'} \cup D_{t'}$ for some $t' < t$.

PROOF. Let $a = \tau.add_1$. Consider the while-loop iteration in which $p$ creates task $\tau$ in line 50 (at point $t_\tau$). Then $p$'s read($a$) in line 49 of the same while-loop iteration returns $\tau.old_1$, as otherwise $p$ would complete its BDCAS() call in that line. Hence, by Lemma 3.15, $B_{t_{read}}[a].val = \tau.old_1$.

Let $\kappa$ be the task stored in $A[a]$ at point $t_{read}$. Then by the definition of the interpreted value of $B[a]$,

$$ \tau.old_1 = \begin{cases} \kappa.new_1 & \text{if } \kappa.stat = \text{True at point } t_{read}, \text{ and} \\ \kappa.old_1 & \text{otherwise.} \end{cases} \qquad (23) $$

To prove (a), we assume that

$$ A_z[a] \neq \tau \text{ for all } z \le t, \qquad (24) $$

because otherwise $\tau \in S_t$, and (a) follows immediately. Now, suppose that the value of $A[\tau.add_1]$ changes during $[t_{read}, t]$. Let $\tau' = A_t[a]$. By Claim 3.9 (b), $\kappa \neq \tau'$. Then by Claim 3.9 (a) $\kappa.new_1 <_a \tau'.new_1$. Since either $\kappa.old_1 <_a \kappa.new_1$ or $\kappa.old_1 = \kappa.new_1$ (the latter is the case if $\kappa = \lambda_a$), we obtain from (23) and transitivity of $<_a$ that $\tau.old_1 <_a \tau'.new_1$. Hence, by irreflexivity $\tau.old_1 \neq \tau'.new_1$. By (24) and since $A_t[a_1] = \tau'$, it follows that $\tau \in D_t$ since $B_t[a_1].val' = \tau'.new_1 \neq \tau.old_1$.
To prove (b), assume that there is a task $\tau^*$ with $\tau^* \cdot add_1 = \tau \cdot add_1$, such that $\tau^* \cdot stat$ changes from $\perp$ to True at point $t^* \in [t_{read}, t]$. By Lemma 3.7, $A_{t^*}[a] = \tau^*$. Since at most one shared memory operation takes place at point $t$, it follows that $A_{t^*-1}[a] = \tau^*$.

We assume that $\tau^* \neq \tau$, because otherwise $\tau \in S_{t^*-1}$, in which case (b) follows immediately. Also, if the value of $A[\tau.add_1]$ changes during $[t_{read}, t-1]$, then by (a) $\tau \in S_{t-1} \cup D_{t-1}$. So, suppose that the value of $A[\tau.add_1]$ does not change during $[t_{read}, t-1]$. Hence, $A[a] = \tau^* = \kappa$ throughout $[t_{read}, t-1]$.

Again using that at most one shared memory operation takes place at point $t$, it follows that $\kappa.stat$ changes to True after $t_{read}$. Then by Claim 3.5 $\kappa.stat \neq$ True at point $t_{read}$, so by (23), $\tau.old_1 = \kappa.old_1$. Moreover, then $\kappa$ is not an initial task, and so $\kappa.old_1 \neq \kappa.new_1$, and so $\tau.old_1 \neq \kappa.new_1$. Since $t_\tau \in [t_{read}, t-1]$, $A_{t_\tau}[a] = \kappa$, and it follows that $B_{t_\tau}[a].val' = \kappa.new_1 \neq old_1$. Hence, $\tau \in S_{t_\tau} \cup D_{t_\tau}$ which completes the proof of (b). $\square$

**LEMMA 3.44.** *Suppose that at point $t_{p@59}$, process $p$ reads $A[a] = \tau$ in line 59 of operation finish(a), and at some point $t > t_{p@59}$ during the same finish() call one of the following happens:*

(a) $p$ executes a successful CAS() operation in line 62,

(b) $p$ executes a failed CAS() operation in line 64, or

(c) $p$ executes line 67.

Then $\tau \in D_{t'} \cup S_{t'}$ for some $t' < t$.

*PROOF.* If $\tau = \lambda_a$, then $\tau \in S_{t'}$ for all $t' \ge 0$. Hence, assume that $\tau \neq \lambda_a$. By Claim 3.1 (b), task $\tau$ is created in line 50 at some point $t_\tau < t_{p@59}$.

First assume that (a) is true, i.e., at point $t$ process $p$ performs a successful $\tau_1.stat.CAS(\perp, \text{True})$ in line 62, where $\tau_1$ is the task that $p$ reads from $A[\tau.add_1]$ in line 61. Then $\tau_1.add_1 = \tau.add_1$, and so by Claim 3.43 (b) $\tau \in S_{t'} \cup D_{t'}$ for some $t' < t$.

Now assume that (b) is true. Then at point $t$ process $p$ executes a failed $A[\tau.a_1].CAS(\tau_1, \tau)$ in line 64, where $\tau_1$ is the task $p$ previously read from $A[\tau.a_1]$ in line 61 at some point $t_{61} < t$. Since the CAS fails, the value of $A[\tau.add_1]$ changes at some point $t' \in [t_{61}, t)$ from $\tau_1$ to a different value. Thus, by Claim 3.43 (a) $\tau \in S_{t'} \cup D_{t'}$.

Finally, assume that (c) is true. Then at point $t$ process $p$ executes a $\tau.stat.CAS(\perp, \text{False})$ in line 67. If prior to that $p$ executes a failed CAS in line 64 during the same finish() call, then the claim follows from part (b). If $p$ executes a successful CAS in line 64 at point $t_{p@64}$, then as a result of that $A_{t_{p@64}}[\tau.add_1] = \tau$, and so $\tau \in S_{t'}$ for $t' = t_{p@64} < t$.

Hence, assume that $p$ does not execute line 64. Then $p$ evaluates the if-condition in line 63 to False. Hence, $\tau_1.new_1 \neq \tau.old_1$, where $\tau_1$ is the task stored in $A[\tau.add_1]$ when $p$ reads that register in line 61 at point $t_{p@61}$. Thus, for $t' = t_{p@61} < t$, if $A[\tau.add_1] \neq \tau$ throughout $[0, t')$ then $\tau \in D_{t'}$ because $B_{t'}[\tau.add_1].val' = \tau_1.new_1 \neq \tau.old_1$, and otherwise $\tau \in S_{t'}$. $\square$

**LEMMA 3.45.** *If a process $p$ creates task $\tau$ during a BDCAS($\langle a_0, v_0, v'_0 \rangle$, $\langle a_1, v_1, v'_1 \rangle$) operation, and the operation returns before point $t$, then $\tau \in D_t \cup S_t$.*

*PROOF.* Since $p$'s BDCAS($\langle a_0, v_0, v'_0 \rangle$, $\langle a_1, v_1, v'_1 \rangle$) operation returns, there is an index $i$ such that $p$'s last read($a_i$) operation in line 49 returns a value different from $v_i$. Let $t^*$ be the linearization point of that read($a_i$) operation. Then by Lemma 3.15, $B_{t^*}[a_i].val \neq v_i$.

Now consider the iteration of the while-loop in which $p$ creates task $\tau$. Then $\tau.old_i = v_i$ and $\tau.add_i = a_i$ due to the arguments used in the newTask() call in line 50. Let $t_{read} < t^*$ be the point when $p$'s read($a_i$) in line 49 of that iteration linearizes. Since $p$'s BDCAS() call does not return in that while-loop iteration $B_{t_{read}}[a_i].val = v_i$. Hence,

$$ \tau.old_i = B_{t_{read}}[\tau.add_i].val \neq B_{t^*}[\tau.add_i].val. \quad (25) $$
First assume that $i = 1$. By (25) and Lemma 3.24 a successful BDCAS() operation op that uses an argument triple $\langle \tau.add_1, u_1, u'_1 \rangle$ for some values $u_1, u'_1$, linearizes at some point $lin(op) \in (t_{read}, t^*)$. By the definition of linearization points and by Claim 3.23, the process that executes op, creates a task $\kappa$ whose status changes to True at point $lin(op)$. Then $\kappa.add_1 = \tau.add_1$. Since $lin(op) \in (t_{read}, t^*) \subseteq (t_{read}, t]$ it follows from Claim 3.43 (b) that $\tau \in S_t \cup D_t$.

Now assume that $i = 0$. If $A_{t'}[\tau.add_0] \neq \tau$ for all $t' \le t^*$, then $\tau \in D_{t^*} \subseteq D_t$, since either $B_{t^*}[\tau.add_0].val' = B_{t^*}[\tau.add_0].val \neq \tau.old_0$, or $\tau.old_0 = B_{t_{read}}[\tau.add_i].val <_{\tau.add_0} B_{t^*}[\tau.add_0].val <_{\tau.add_0} B_{t^*}[\tau.add_0].val'$ by Corollaries 3.19 and 3.41, and by irreflexivity $\tau.old_0 \neq B_{t^*}[\tau.add_0].val'$. Hence, assume

$$ \exists t' \le t : A_{t'}[\tau.add_0] = \tau. \qquad (26) $$

First consider the case that $A_{t^*}[\tau.add_0] = \tau$. Then by the definition of interpreted value, $B_{t^*}[\tau.add_0].val \in \{\tau.old_0, \tau.new_0\}$. Thus, by (25), $B_{t^*}[\tau.add_0].val = \tau.new_0$. Then by the definition of interpreted value, $\tau.stat = \text{True}$ at point $t^*$. Since $\tau.stat = \text{False}$ when $\tau$ is being created, which is before $t^*$, it follows from Claim 3.43 (b) that $\tau \in S_{t^*} \cup D_{t^*} \subseteq S_t \cup D_t$.

Finally, consider the case that $A_{t^*}[\tau.add_0] \neq \tau$. By (26), before point $t^*$ the value of $A[\tau.add_0]$ changes from $\tau$ to a different value, say $\tau'$. This can only happen when some process executes a successful $A[\tau.add_0].CAS(\tau, \tau')$ in line 56. Then that process previously obtained $\tau$ from a finish() call in line 48, and hence, executed line 67 after reading $\tau$ from A in line 59. Then it follows from Lemma 3.44 (c) that $\tau \in S_t \cup D_t$. $\square$

**CLAIM 3.46.** Let $a \in M_0$, and $t$ a point in time such that $\tau = L_t[a_0]$ is a task. Then at all points $t' \ge t$, $B_{t'}[a_0].val = \tau.old_0$ or $\tau.old_0 <_a B_{t'}[a_0].val$.

**PROOF.** Since $\tau = L_t[a]$ is a task, some process $p$ calls propose($\tau$) on $L[a]$ in line 51 prior to $t$. (According to the RC specification, initially $L[a] = \perp$.) Due to the if-statement in line 49 and the arguments of $p$'s newTask() call in line 50, $p$'s preceding read($a$) in line 49 returns $\tau.old_0$. Hence, by Lemma 3.15, there is a point $t^* < t$ (namely the linearization point of $p$'s read($a$)), such that $B_{t^*}[a].val = \tau.old_0$. Thus, it follows immediately from Corollary 3.19 that $B_{t'}[a_0].val = \tau.old_0$ or $\tau.old_0 <_a B_{t'}[a_0].val$ for any $t' \in [t^*, \infty) \supseteq [t, \infty)$. $\square$

**CLAIM 3.47.** Let $\tau$ be a task, $a = \tau.add_0$, and $t$ a point in time such that $\tau.old_0 <_a B_t[a]$. Then either $A[a] = \tau$ at point $t$ or $A[a] \neq \tau$ throughout $[t, \infty)$.

**PROOF.** For the purpose of contradiction, assume that $A_t[a] \neq \tau$ but there is a point $t' > t$ at which the value of $A_t[a]$ changes to $\tau$. Then by Lemma 3.18 (b) $\tau.stat = \perp$ at point $t'$, and thus $B_{t'}[a].val = \tau.old_0$. Thus, we have $B_{t'}[a].val <_a B_t[a].val$, which contradicts Corollary 3.19, since $<_a$ is transitive and irreflexive. $\square$

**CLAIM 3.48.** Suppose process $p$ calls BDCAS($\langle a_0, v_0, v'_0 \rangle$, $\langle a_1, v_1, v'_1 \rangle$), and in one while-loop iteration $p$ first reads a task $\tau$ from $L[a_0]$ in line 53 at point $t$, and then it evaluates the if-condition in line 55 to False. Then $\tau.old_0 <_a B_t[a_0].val$.

**PROOF.** Let $\tau_0$ be the value that $p$'s finish($a_0$) call in line 48 returns at point $t_{p@48}$. Then by Claim 3.17

$$ \exists s \in \{\text{False, True}\} : \tau_0.stat = s \text{ throughout } [t_{p@48}, \infty). \qquad (27) $$

Since in line 54 process $p$ also reads $\tau_0$ from $A[a_0]$ at point $t_{p@54}$ (because it proceeds to line 55), it follows from Lemma 3.16 that

$$ A[a_0] = \tau_0 \text{ throughout } [t_{p@48}, t_{p@54}]. \qquad (28) $$

Thus, by (27) $p$'s read($a_0$) in line 49 returns $\tau_0.old_0$ if $s = \text{False}$ and $\tau_0.new_0$ if $s = \text{True}$. Since $p$'s BDCAS($\langle a_0, v_0, v'_0 \rangle$, $\langle a_1, v_1, v'_1 \rangle$) call does not return in line 49, the read($a_0$) operation returns $v_0$. Hence, by (27) and (28)

$$ B[a_0].val = v_0 \text{ throughout } [t_{p@48}, t_{p@54}]. \qquad (29) $$
Now consider the task $\tau$ that $p$ reads from $L[a_0]$ in line 53 at point $t_{p@53} \in [t_{p@48}, t_{p@54}]$. Since $p$ evaluates the if-condition in line 55 to False, $\tau.old_0 \neq v_0$. Thus, by (29) and Claim 3.46, $\tau.old_0 < a_0 B_t[a_0].val$. $\square$

CLAIM 3.49. Let $a \in M_0$.

(a) If at point $t$ the value of $A[a]$ changes from $\tau_0$ to $\tau \neq \tau_0$, then $L_t[a] = \tau$.

(b) Suppose at point $t$ some process executes a successful $L[a].unlock(\tau)$ operation. Then

(b1) either at point $t$ it holds $A[a] = \tau$ and $\tau.stat \neq \perp$, or $A[a] \neq \tau$ throughout the entire execution, and

(b2) if $\tau \neq \perp$ then $\tau \in S_{t'} \cup D_{t'}$ for some $t' < t$.

PROOF. Let $T_0 = 0$ be the beginning of the execution $E$ and for each integer $\ell \ge 1$ let $T_\ell$ be the point of the $\ell$-th shared memory operation in $E$. We will show by induction on $\ell$ that the claim is true provided $t \in [0, T_\ell)$. This is trivially true for $\ell = 0$.

Hence, assume we have proved that the claim is true for $t \in [0, T_\ell)$. Let $t \in [T_\ell, T_{\ell+1})$. If $t \in (T_\ell, T_{\ell+1})$, then no shared memory operation occurs at point $t$, and (a) and (b) are trivially true. Hence, assume $t = T_\ell$.

Part (a): Suppose at point $t = T_\ell$ the value of $A[a]$ changes from $\tau_0$ to $\tau \neq \tau_0$. Then some process $p$ executes a successful $A[a].CAS(\tau_0, \tau)$ operation in line 56 at point $t$. Prior to that, at point $t_{p@53} < t$ process $p$ reads $\tau$ from $L[a]$ in line 53. Thus, $L_{t_{p@53}}[a] = \tau$, so there must be a successful choose&lock() call that linearizes before $t_{p@53} < t$ and which decides $\tau$. (By the if-condition in line 55, $\tau \neq \perp$, so $\tau$ is not the initial value of $L[a]$, which is $\perp$ according to the RC specification.)

For the purpose of proving a contradiction assume $L_t[a] \neq \tau$. Then some successful unlock($\tau$) call linearizes at a point $t_u < t = T_\ell$. By the assumption that the claim is true for all $t < T_\ell$, we conclude from statement (b1) that either $A[a] = \tau$ at point $t_u$ or $A[a] \neq \tau$ throughout the entire execution. Since at point $t > t_u$ the value of $A[a]$ changes from $\tau_0$ to $\tau$, the latter cannot be the case, so $A_{t_u}[a] = \tau$. But then $A_{t_u}[a] = A_t[a] = \tau$, and so by Lemma 3.16 $A[a] = \tau$ throughout $[t_u, t)$. This contradicts that at point $t$ the value of $A[a]$ changes from $\tau_0 \neq \tau$ to $\tau$. Thus, (a) is true for $t = T_\ell$ and thus also for $t \in [0, T_{\ell+1})$.

Part (b): Suppose that at point $t = T_\ell$ some process $p$ executes a successful $L[a].unlock(\tau)$ operation. If $\tau = \perp$, then by Claim 3.1 $A[a] \neq \tau$ throughout the entire execution, so (b) is true. Hence, assume $\tau \neq \perp$. Let $t_{p@53}$ be the point when $p$ reads $L[a]$ in line 53 prior to its successful $L[a].unlock(\tau)$. Then $L[a] = \tau$ at that point. Since $p$'s unlock($\tau$) at point $t$ is successful, and (from the sequential specification of RC) $L[a]$ is ABA-free,

$$L[a] = \tau \text{ throughout } [t_{p@53}, t]. \qquad (30)$$

Now let $t_f$ be the point when $p$ reads $A[a]$ in line 59 during the finish() call $p$ executes in line 48, and let $t_{p@54}$ be the point when it reads $A[a]$ again in line 54. Since $p$ evaluates the if-statement in line 54 to True, it reads the same value $\tau_0$ from $A[a]$ at points $t_f$ and $t_{p@54}$. Then by Lemma 3.16, $A[a] = \tau_0$ throughout the entire interval $[t_f, t_{p@54}]$, and in particular

$$A_{t_{p@53}} = \tau_0. \qquad (31)$$

Since we assume that the claim is true for all $t < T_\ell$ and already proved that (a) is true for $t = T_\ell$, it follows from part (a) of the claim and (30) that if the value of $A[a]$ changes in the interval $[t_{p@53}, t]$, then it changes to $\tau$. Thus,

$$A[a] \in \{\tau_0, \tau\} \text{ throughout } [t_f, t]. \qquad (32)$$

First assume that $p$ evaluates the if-condition in line 55 to True. Then at some point $t_{p@56}$ process $p$ executes $A[a].CAS(\tau_0, \tau)$ in line 56. Hence, by (32) $A[a] = \tau$ throughout $[t_{p@56}, t]$. Moreover, during its finish($a$) call in line 57 process $p$ reads $\tau$ from $A_t[a]$ in line 59, and executes $\tau.stat.CAS(\perp, \text{False})$ in line 67. Hence, $\tau.stat \neq \perp$ at point $t$ by Claim 3.5, and since $A[a] = \tau$ at point $t$ (b1) is true. Moreover, (b2) follows from Lemma 3.44 (c).
Now assume that $p$ evaluates the if-condition in line 55 to False. Then by Claim 3.48, $\tau.old_0 <_a B_{t_p@53}[a].val$. Hence, by (31) and Claim 3.47, $A[a] \neq \tau$ throughout $[t_p@53, \infty)$. We will now show that

$$A[a] \neq \tau \text{ throughout } [0, t_p@53].$$

Then clearly (b1) is true. Moreover, $p \in D_{t_p@53}$ by Corollary 3.41, and so (b2) is true.

For the purpose of proving a contradiction, assume there is a point in $[0, t_p@53)$ at which $A[a] = \tau$. Since $L_{t_p@53}[a] = \tau$, some process proposes $\tau$ in line 51, so $\tau$ is not the initial task $\lambda_a$. Hence, at some point $t' < t_p@53 < t = T_\ell$ the value of $A[a]$ changes to $\tau$. Then by part (a) of the claim (which we proved true for all $t < T_\ell$), we have $L_{t'}[a] = \tau \neq \perp$. By (30) and since $L[a]$ is ABA-free,

$$L[a] = \tau \text{ throughout } [t', t]. \qquad (33)$$

Since $A_{t'}[a] = \tau$, it follows from (32) that at some point $t'' \in [t', t_f) \subseteq [t', t]$ the value of $A[a]$ changes to $\tau_0$ from a different value. By part (a) of the claim $L[a] = \tau_0 \neq \tau$ at point $t''$, which contradicts (33). $\square$

**LEMMA 3.50.** Let $a \in [m]$, $t$ a point in time, and $\tau \neq \lambda_a$ a task such that $A_t[a] = \tau$.

(a) If $a \in M_0$, then there is a point $t' < t$ such that $L_{t'}[a] = \tau$.

(b) If $a \in M_1$, then there is a point $t' < t$ such that $A_{t'}[\tau.add_0] = \tau$.

**PROOF.** Part (a) follows immediately from Claim 3.49 (a) and part (b) from Claim 3.3. $\square$

**LEMMA 3.51.** Let $a \in M_0$, let $\tau$ be a task, and let $t_1 < t_2$ be two points in time such that $L_{t_1}[a] = \tau \neq L_{t_2}[a]$. Then there exists a point $t < t_2$ such that $\tau \in D_t \cup S_t$.

**PROOF.** Since $\tau$ is a task, $\tau \neq \perp$. As $L_{t_1}[a] = \tau \neq L_{t_2}[a]$, at some point $t_p@58 \in [t_1, t_2]$ some process $p$ executes a successful $L[a].unlock(\tau)$ operation in line 58. Hence, by Claim 3.49 (b) there exists $t < t_p@58 \le t_2$ such that $\tau \in D_t \cup S_t$. $\square$

**CLAIM 3.52.** Let $\tau$ be a task that is created at $t_\tau$, and suppose that, for some point $t \ge t_\tau$, there is an index $i \in \{0, 1\}$ such that $B_t[\tau.add_i] \neq \tau.old_i$. Then $B_{t'}[\tau.add_i].val \neq \tau.old_i$ for all $t' \ge t$.

**PROOF.** Let $p$ be the process creating $\tau$ at point $t_\tau$, i.e., $p$'s newTask() in line 50 returns $\tau$ at that point. Then before that, in line 49 process $p$ executes a read($\tau.add_i$) operation for each $i \in \{0, 1\}$. Since $p$ does not complete its BDCAS() call in this line, that read($\tau.add_i$) operation returns $\tau.old_i$. Hence, by Lemma 3.15, the interpreted value of $B[\tau.add_i]$ is $\tau.old_i$ at the linearization point of that read($\tau.add_i$), and thus at some point before $t_\tau$.

Assume that $B_t[\tau.add_i].val \neq \tau.old_i$ for some $i \in \{0, 1\}$. Let $a = \tau.add_i$. By Claim 3.13 and Corollary 3.19, $\tau.old_i <_a B_t[\tau.add_i].val$. Now the claim follows by irreflexivity and transitivity of $<_a$. $\square$

**CLAIM 3.53.** Let $t_1 < t_2$. Suppose that process $p$ calls BDCAS($\langle a_0, v_0, v'_0 \rangle$, $\langle a_1, v_1, v'_1 \rangle$), and during that call it creates a task $\tau$, such that $\tau \in D_{t_1} \cup S_{t_1}$, and during $[t_1, t_2]$ process $p$ completes a finish($a_0$) call in line 48. Then there is an index $i \in \{0, 1\}$ such if $p$ calls read($a_i$) in line 49 after point $t_2$, then that read() operation returns a value different from $v_i$.

**PROOF.** Since $\tau$ is not an initial task, process $p$ creates $\tau$ at some point $t_\tau \le t_1$, and for each $i \in \{0, 1\}$

$$\tau.old_1 = v_1 \neq v'_1 = \tau.new_1. \qquad (34)$$

Moreover, since $p$'s BDCAS() does not complete in its execution of line 49, it follows that for each $i \in \{0, 1\}$, there is a point $t_p@49, i < t_\tau$ in which $B[a_i].val = v_i$.

First assume that either $\tau \in S_{t_1}$, or $\tau \in D_{t_1}$ because there is a task $\tau'$ (in case $\tau \in S_{t_1}$ we have $\tau = \tau'$) such that $A_{t_1}[a_1] = \tau'$, and $B[a_1].val' = \tau'.new_1 \neq \tau.old_1 = v_1$. Consider the first process $p'$ to execute line 62, 66,
or 71 after $\tau'$ is first placed into $A[a_1]$, and call this point $t^*$. From Lemma 3.7 and that $\tau'$.stat is initialized to $\perp$, $B[a_1]$ changes from $\tau'$.old$_1$ to $\tau'$.new$_1$ at point $t^*$, so $t^* > t_{p@49,i}$. Consider $p$'s read($a_1$) call after point $t_2$. At some point $t_{p@70}$ process $p$ reads some task $\tau''$ from $A[a_1]$ in line 70, and then at point $t_{p@71}$ it performs $\tau''$.stat.CAS($\perp$, True) in line 71. Thus, $t_{p@71} \ge t^*$. Since $B[a_1]$.val was $v_1$ at point $t_{p@49,i}$ and $\tau'$.new$_1$ at point $t^* \le t_{p@71}$, the claim follows from Claim 3.13.

Now assume that $\tau \in D_{t_1}$ because $B_{t_1}[a_0]$.val' $\neq$ $\tau$.old$_0$ = $v_0$.

Consider the case where $B_{t_1}[a_0]$.val' = $B_{t_1}[a_0]$.val $\neq$ $\tau$.old$_0$; since $t_\tau \le t_1$, it follows from Claim 3.52 that $B_{t'}[a_0]$.val $\neq$ $\tau$.old$_0$ for all $t' > t_1$, and from Claim 3.40 that $B_{t'}[a_0]$.val' $\neq$ $\tau$.old$_0$ for all $t' > t_1$. (Note that Definition 3.26 and Corollary 3.19 implies that if $B_{t'}[a_0]$.val $\neq$ $B_{t'}[a_0]$.val'$$, then $B_{t'}[a_0]$.val $<$ $B_{t'}[a_0]$.val'.). Hence, by Lemma 3.15, the read($a_0$) that $p$ calls at point $t_2$ returns a value different from $\tau$.old$_0$ = $v_0$.

The remaining case is when $B_{t_1}[a_0]$.val' $\neq$ $\tau$.old$_0$ and $B_{t_1}[a_0]$.val' $\neq$ $B_{t_1}[a_0]$.val. In this case, there is a non-initial task $\tau'$ such that $A_{t_1}[\tau'$.add$_1$] = $\tau'$, $\tau'$.add$_0$ = $\tau$.add$_0$ = $a_0$, and $\tau'$.old$_0$ = $\tau$.old$_0$ = $v_0$. By Claim 3.3,

$$ \text{there is a point } t_0 \le t_1 \text{ at which } A[\tau'.add_1] = A[a_0] = \tau'. \qquad (35) $$

By the claim's assumptions, $p$ completes a finish($a_0$) call in $[t_1, t_2]$. Let $t_f \ge t_1$ be the point when the finish($a_0$) call returns. If the finish() call returns $\tau'' \neq \tau'$, then $p$ reads $\tau''$ from $A[a_0]$ in line 59 of that finish() call. Hence, by Lemma 3.18 (b) and Claim 3.5 $\tau'$.stat $\neq$ $\perp$ at point $t_f$. If, on the other hand, the finish() call returns $\tau'$, then by Claim 3.17 $\tau'$.stat $\neq$ $\perp$ at point $t_f$. In either case, by Lemma 3.11 $\tau'$.stat = True when $p$'s finish() call terminates at point $t_f$. Since by Claim 3.5 $\tau'$.stat does not change once it is True, and by Lemma 3.7 it changes to True while $A[a_0] = \tau'$, by (35) there is a point $t^* \in [t_0, t_f]$ at which $A[a_0] = \tau'$ and $\tau'$.stat = True. Hence, $v_0 = \tau'$.old$_0 < a_0$, $\tau'$.new$_0$ = $B_{t^*}[a_0]$.val (because $\tau'$ is a non-initial task). Thus, by Claim 3.13 and transitivity and irreflexivity of $<_a$, $B_{t'}[a_0]$.val $\neq$ $v_0$ for all $t' > t^*$. Hence, by Lemma 3.15, the read($a_0$) that $p$ calls at point $t_2$ returns a value different from $v_0$. $\square$

**LEMMA 3.54.** *If process $p$ proposes task $\tau$ during a BDCAS() operation and $\tau \in D_t \cup S_t$, then $p$ executes line 51 at most once after $t$ and before the BDCAS() returns.*

**PROOF.** Suppose for the purpose of proving a contradiction that $p$ executes line 51 twice after $t$ and before its BDCAS() call returns, at points $t_1$ and $t_2$. From the while-loop of BDCAS(), it follows that $p$ executes lines 48 and 49 in $(t_1, t_2)$. Since $\tau \in D_t \cup S_t \subseteq D_{t_1} \cup S_{t_1}$ (by Lemma 3.42), using Claim 3.53 it follows that for some $i \in \{0, 1\}$, $p$'s read($a_i$) operation in line 49 returns a value different from its argument old$_i$. Thus, $p$ returns in line 49, contradicting that it executes line 51 at point $t_2$ before its BDCAS() call returns. $\square$

**LEMMA 3.55.** *Let $a \in M_0$ and let $t_0 < t_1 < t_2 < t_3$ be four points in time, such that at each point $t_i$, $i \in \{0, \dots, 3\}$, process $p$ executes an $L[a]$.choose&lock() call in line 52. Then some successful $L[a]$.unlock() call and some successful $L[a]$.choose&lock() call linearize in $(t_0, t_3]$.*

**PROOF.** Suppose the claim is not true, i.e., either no successful $L[a]$.choose&lock() linearizes in $(t_0, t_3]$ or no successful $L[a]$.unlock() call linearizes in $(t_0, t_3)$. Since $p$ calls choose&lock() at point $t_0$, $L[a]$ is locked at $t_0$. If any successful $L[a]$.unlock() call linearizes in $(t_0, t_3)$, then a successful $L[a]$.choose&lock() linearizes no later than $p$'s next choose&lock() call in the interval, contradicting both cases. Therefore, no successful $L[a]$.unlock() call linearizes in $(t_0, t_3)$, and $L[a]$ is locked throughout $(t_0, t_3]$, so there is a value $\tau$ such that $L[a] = \tau$ throughout $(t_0, t_3]$. By Claim 3.49, if the value of $A[a]$ changes in the interval $(t_1, t_3]$, then it changes from $\tau' \neq \tau$ to $\tau$. In particular, the value of $A[a]$ changes at most once in the interval $(t_0, t_3]$. Process $p$ executes at least two complete iterations of the while-loop in the interval $(t_0, t_3]$, and thus throughout at least one complete iteration $A[a]$ remains unchanged. Hence, let $\tau_0$ be a task such that $A[a] = \tau_0$ throughout one of the two iterations. Then $p$'s finish() call in line 48 returns $\tau_0$ because $p$ reads that value from $A[a]$ in line 59. Moreover, $p$ reads $\tau_0$
from $A[a]$ in line 54, and so the if-statement in that line evaluates to True. In line 53 process $p$ reads $\tau$ from $L[a]$, and so in line 58 $p$ calls $L[a].unlock(\tau)$. Clearly, this unlock() call is successful, which is a contradiction. □

**LEMMA 3.56.** Let $a \in M_0$ and let $s_1 < s_2$ be two points in which some successful $L[a].unlock()$ calls linearize. Then the number of method calls to $L[a]$ in the interval $(s_1, s_2)$ is no more than $3n$ for each of $L[a].propose()$, $L[a].choose&lock()$, $L[a].unlock()$, and no more than $4n$ for $L[a].read()$.

**PROOF.** It suffices to show that if any process executes four invocations of $L[a].propose()$, $L[a].choose&lock()$, or $L[a].unlock()$ in a given interval (or five invocations of $L[a].read()$), then some successful $L[a].unlock()$ operation linearizes in that interval.

The case of $L[a].choose&lock()$ follows immediately from Lemma 3.55. Let $o$ be one of operations $L[a].propose()$ or $L[a].unlock()$, and suppose for the purpose of proving a contradiction that a process $p$ executes $o$ at points $o_0, o_1, o_2, o_3$ but no successful $L[a].unlock$ operation linearizes in the interval $(o_0, o_3]$. Because $p$ can only execute $o$ at points lines 51 and 58, respectively, it follows that $p$ executes line 52 at points $t_0, t_1, t_2$ such that $o_0 < t_0 < o_1 < t_1 < o_2 < t_2 < o_3$. Using similar arguments to Lemma 3.55, $L[a]$ is locked throughout $[t_0, o_3]$, and $p$ executes at least two complete iterations of the while-loop in the interval $[t_0, o_3]$. Following the proof of Lemma 3.55, $p$ executes a successful $L[a].unlock()$ operation by the end of the two complete while-loop iterations, which is a contradiction. The case of $L[a].read()$ is nearly identical, except that we need five $L[a].read()$ operations to guarantee that $p$ executes at least two complete while-loop iterations while $L[a]$ is locked. This is because $t_0$ is in a different while-loop iteration than $o_0$ for this case. □

**CLAIM 3.57.** Let $[t_1, t_2]$ be a time interval during which only process $p$ takes steps, and only executes a single BDCAS $((a_0, v_0, v'_0), (a_1, v_1, v'_1))$ call. If $p$ completes $k$ full iterations of the while-loop during $[t_1, t_2]$, then in each complete iteration it executes line 58, and the $L[a_0].unlock()$ call in that line is successful. Moreover, $p$'s choose&lock() calls in line 52 during iterations 2, ..., $k$ are successful.

**PROOF.** Consider any complete iteration of the while-loop during interval $[t_1, t_2]$. Let $\tau$ be the task that $p$'s finish() call in line 48 returns. Then $p$ reads $\tau$ from $A[a_0]$ in line 59 during the corresponding finish() call. Since $A[a_0]$ does not change until $p$ reads $A[a]$ again in line 54, the if-condition in that line evaluates to True. Hence, in each of the $k$ iterations of the while-loop, process $p$ executes lines 55–58. In particular, when $p$ calls $L[a_0].unlock(\tau')$ in line 58, it uses the argument $\tau'$ that it read from $L[a_0]$ in line 53. Hence, each such unlock() call succeeds.

Thus, whenever $p$ calls choose&lock() in line 52 during one of iterations 2, ..., $k$, $L[a_0]$ is unlocked. Hence, each such choose&lock() call is successful. □

**CLAIM 3.58.** Suppose that after point $t$ only process $p$ takes steps, and only executes a single BDCAS $((a_0, v_0, v'_0), (a_1, v_1, v'_1))$ call, until the first point $t^* > t$ such that $L_{t^*}^*[v_0].val = \tau$, where $\tau$ is one of the tasks $p$ proposes in line 51. The expected number of shared memory steps in $[t, t^*]$ is at most $O(\log^2 n \log \log n)$.

**PROOF.** For $i \ge 1$, let $t_i$ be the point when $p$ starts its $i$-th complete while-loop iteration.

By Claim 3.57, during each of the iterations process $p$ executes a successful $L[a_0].unlock()$ call in line 58. Then the RC methods invoked by $p$ in each while-loop iteration correspond to the algorithm in Figure 6, where $R = L[a_0]$. Precisely, lines 42–46 correspond to lines 50–53 and 58, respectively, and the while-loop condition in line 41 is false until just after $t^*$. The claim follows by applying Lemma 2.54. □

**LEMMA 3.59 (PROBABILISTIC OBSTRUCTION FREEDOM).** If process $p$ invokes some method call BDCAS $((a_0, v_0, v'_0), (a_1, v_1, v'_1))$, and at some point during the operation, $p$ starts to run solo, then the operation returns after at most $O(\log^2 n \log \log n)$ shared memory steps in expectation.

**PROOF.** By applying Claim 3.58 twice, there is a point $t$ and a point $t' > t$ such that
• $t'$ is at most $O(\log^2 n \log \log n)$ expected steps after $p$ starts running solo, and

• $L_t[add_0] = \tau$ and $L_{t'}[a_0] = \tau'$ for two distinct tasks $\tau$ and $\tau'$ proposed by $p$.

Thus, by Lemma 3.51 $\tau \in D_{t'} \cup S_{t'}$. Hence, after point $t$ process $p$ completes at most two more iterations of the while-loop according to Lemma 3.54, which by Lemma 2.47 adds at most $O(\log n \log \log n)$ steps in expectation. $\square$

LEMMA 3.60. Let $a \in M_0$, let $\tau$ be a task, and suppose at point $t$ some process is poised to call $L[a].unlock(\tau)$ in line 58. Then $\tau \in D_{t'} \cup S_{t'}$ for some $t' < t$.

PROOF. Consider the execution prefix that ends at point $t$. If $L_t[a] = \tau$ and $L[a]$ is locked at point $t$, then we can let $p$ run solo until its $L[a].unlock(a)$ completes. Hence, by Claim 3.49 (b2) $\tau \in D_{t'} \cup S_{t'}$. Then this is obviously also true for any other execution that has the same prefix up to point $t$.

Now suppose that either $L_t[a] \neq \tau$ or $L[a]$ is unlocked. Since $p$ reads $\tau$ from $L[a]$ in line 53 prior to $t$, there is a point $t^* < t$ at which a successful $L[a].unlock(\tau)$ call linearizes. For that case we have already proved that there exists $t' < t^* < t$ such that $\tau \in D_{t'} \cup S_{t'}$. $\square$

# 4 CONCLUSION

We presented a new and more efficient implementation of the repeated choice object, originally introduced by Giakkoupis, Giv, and Woelfel [9]. Using this improved building block in the DCAS algorithm of the same paper improves the algorithm’s expected amortized step complexity from $O(\log n)$ to $O(\log \log n)$. The improved complexity of the RC object is obtained by adding a binary search before the linear search, and distributing the work for clearing parts of an array over multiple processes when needed, and otherwise only partially clearing the array. While this sounds simple, it turned out to be quite challenging. Both the new RC algorithm and its analysis are highly involved. As the randomized properties of the new RC object are different from the previous one, we also provided a new analysis of the BDCAS building block used in the DCAS algorithm.

We believe that the RC object may have other applications. A natural open question is whether a similar primitive with constant step complexity exists.

# ACKNOWLEDGMENTS

We thank the anonymous reviewers for their insightful comments. Support is gratefully acknowledged from the Agence Nationale de la Recherche (ANR) under project ByBloS (ANR-20-CE25-0002), the Natural Sciences and Engineering Research Council of Canada (NSERC) under Discovery Grant RGPIN/2019-04852, the Canada Graduate Scholarships-Doctoral program (CGSD-578918-2023/198), and the Canada Research Chairs program, as well as the University of Calgary’s Eyes High Doctoral Recruitment Scholarship program.

# REFERENCES

[1] Yehuda Afek, Michael Merritt, Gadi Taubenfeld, and Dan Touitou. 1997. Disentangling multi-object operations. In *Proceedings of the 16th SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC)*. 111–120. https://doi.org/10.1145/259380.259431

[2] Ole Agesen, David Detlefs, Christine Flood, Alexander Garthwaite, Paul Martin, Mark Moir, Nir Shavit, and Guy Steele. 2002. DCAS-based concurrent deques. *Theory of Computing Systems* 35 (June 2002), 349–386. https://doi.org/10.1007/s00224-002-1058-2

[3] Zahra Aghazadeh and Philipp Woelfel. 2016. Upper bounds for boundless tagging with bounded objects. In *Proceedings of the 30th International Symposium on Distributed Computing (DISC)*. 442–457. https://doi.org/10.1007/978-3-662-53426-7_32

[4] James H. Anderson and Mark Moir. 1995. Universal constructions for multi-object operations. In *Proceedings of the 14th SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC)*. 184–193. https://doi.org/10.1145/224964.224985

[5] Hagit Attiya and Eyal Dagan. 2001. Improved implementations of binary universal operations. *Journal of the ACM* 48, 5 (Sept. 2001), 1013–1037. https://doi.org/10.1145/502102.502105

[6] Hagit Attiya and Eshcar Hillel. 2011. Highly concurrent multi-word synchronization. *Theoretical Computer Science* 412, 12-14 (2011), 1243–1262. https://doi.org/10.1016/j.tcs.2010.12.049

[7] Oksana Denysyuk and Philipp Woelfel. 2016. Are Shared Objects Composable under an Oblivious Adversary?. In *Proceedings of the 35th SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC)*. 335–344. https://doi.org/10.1145/2933057.2933115
[8] Steven Feldman, Pierre LaBorde, and Damian Dechev. 2015. A wait-free multi-word compare-and-swap operation. *International Journal of Parallel Programming* 43, 4 (2015), 572–596. https://doi.org/10.1007/s10766-014-0308-7

[9] George Giakkoupis, Mehrdad Jafari Giv, and Philipp Woelfel. 2021. Efficient Randomized DCAS. In *Proceedings of the 53rd Annual ACM Symposium on Theory of Computing (STOC)*. 1–64. https://doi.org/10.1145/3406325.3451133

[10] George Giakkoupis, Mehrdad Jafari Giv, and Philipp Woelfel. 2021. *Efficient randomized DCAS*. Research Report. Inria. https://hal.inria.fr/hal-03195692

[11] Wojciech Golab, Lisa Higham, and Philipp Woelfel. 2011. Linearizable implementations do not suffice for randomized distributed computation. In *Proceedings of the 43rd Annual ACM Symposium on Theory of Computing (STOC)*. 373–382. https://doi.org/10.1145/1993636.1993687

[12] Michael Greenwald. 2002. Two-handed emulation: How to build non-blocking implementation of complex data-structures using DCAS. In *Proceedings of the 21st SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC)*. 260–269. https://doi.org/10.1145/571825.571874

[13] Michael Greenwald and David R. Cheriton. 1996. The synergy between non-blocking synchronization and operating system structure. In *Proceedings of 2nd USENIX Symposium on Operating Systems Design and Implementation (OSDI)*. 123–136. https://doi.org/10.1145/238721.238767

[14] Rachid Guerraoui, Alex Kogan, Virendra J. Marathe, and Igor Zablotchi. 2020. Efficient multi-word compare and swap. In *Proceedings of the 34th International Symposium on Distributed Computing (DISC)*. 4:1–4:19. https://doi.org/10.4230/LIPIcs.DISC.2020.4

[15] Phuong Hoai Ha and Philippas Tsigas. 2004. Reactive multi-word synchronization for multiprocessors. *The Journal of Instruction-Level Parallelism* 6 (2004), 25 pages. http://www.jilp.org/vol6/v6paper3.pdf

[16] Timothy L. Harris, Keir Fraser, and Ian A. Pratt. 2002. A practical multi-word compare-and-swap operation. In *Proceedings of the 16th International Symposium on Distributed Computing (DISC)*. 265–279. https://doi.org/10.1007/3-540-36108-1_18

[17] Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A correctness condition for concurrent objects. *ACM Transactions on Programming Languages and Systems* 12, 3 (1990), 463–492.

[18] Amos Israeli and Lihu Rappoport. 1994. Disjoint-access-parallel implementations of strong shared memory primitives. In *Proceedings of the 13th SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC)*. 151–160. https://doi.org/10.1145/197917.198079

[19] Yujie Liu and Michael F. Spear. 2012. A lock-free, array-based priority queue. In *Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPOPP)*. 323–324. https://doi.org/10.1145/2145816.2145876

[20] Michael Luby. 1988. *On the parallel complexity of symmetric connection networks*. Technical Report 214/88. Department of Computer Science, University of Toronto.

[21] Victor Luchangco, Mark Moir, and Nir Shavit. 2003. Nonblocking *k*-compare-single-swap. In *25th ACM Symposium on Parallel Algorithms and Architectures (SPAA)*. 314–323. https://doi.org/10.1145/777412.777468

[22] Charles Martel and Ramesh Subramonian. 1994. On the Complexity of Certified Write-All Algorithms. *Journal of Algorithms* 16, 3 (1994), 361–387. https://doi.org/10.1006/jagm.1994.1017

[23] Henry Massalin and Calton Pu. 1992. A lock-free multiprocessor OS kernel. *ACM SIGOPS Operating Systems Review* 26, 2 (1992), 108. https://doi.org/10.1145/142111.993246

[24] Mark Moir. 1997. Transparent support for wait-free transactions. In *Proceedings of the 11th International Workshop on Distributed Algorithms (WDAG)*. 305–319. https://doi.org/10.1007/BFb0030692

[25] Nir Shavit and Dan Touitou. 1995. Software Transactional Memory. In *Proceedings of the 14th SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC)*. 204–213. https://doi.org/10.1145/224964.224987

[26] Håkan Sundell. 2011. Wait-free multi-word compare-and-swap using greedy helping and grabbing. *International Journal of Parallel Programming* 39, 6 (2011), 694–716. https://doi.org/10.1007/s10766-011-0167-4