Proofs: Diffracting tree

The diffracting tree is a quiescently consistent, lock-free counter full

This proof shows: correctness, quiescent-consistency, progress.

We use the pseudocode of the page, with width $w = 2^k$ and $w - 1$ balancers. Every read, write, compare-and-swap (CAS) and fetch-and-add on one word is atomic. Concurrent callers have distinct ids, and each thread runs at most one call at a time. A token is one call of GET-AND-INCREMENT.

Lemma 1 (the exchanger pairs symmetrically). If an exchange by token $x$ on slot $s$ returns $y \ne$ TIMEOUT, then $y$ is a token whose concurrent exchange on $s$ returned $x$. An exchange that returns TIMEOUT is not returned by any other exchange.

Proof. Look at the writes to $s$. From EMPTY, only a CAS at line L14 by some $x$ changes it, to $(x, \text{WAITING})$. From $(x, \text{WAITING})$, only two CASes can succeed: $x$'s own CAS at line L16, which expects its own id and sets EMPTY, or a CAS at line L18 by some $y$, which sets $(y, \text{BUSY})$, and then $y$ returns $x$. From $(y, \text{BUSY})$, no CAS of the code succeeds, since each expects EMPTY or WAITING, and the only plain writes are those of $x$ at lines L15 and L17. While $x$ waits after its successful line L14, it is the only thread that writes $s$ other than through line L18. So if $y$'s CAS succeeds, $x$'s CAS at line L16 fails, $x$ reads $(y, \text{BUSY})$ at line L15 or line L17, returns $y$, and sets $s$ to EMPTY. If no such CAS by $y$ succeeds, $x$'s CAS at line L16 succeeds and $x$ returns TIMEOUT, and nobody returned $x$. A token that returns at line L18 was paired with the waiting $x$ in the same way, so the pairing is a matching on tokens. $\square$

Lemma 2 (one balancer). For a balancer $b$, let $o_0$ and $o_1$ be the numbers of tokens that have returned side 0 and side 1 from BALANCE on $b$. At any moment when no token is inside BALANCE on $b$, $o_0 - o_1 \in \{0, 1\}$. If $n$ tokens have entered and left, $o_0 = \lceil n/2 \rceil$ and $o_1 = \lfloor n/2 \rfloor$.

Proof. A token leaves either at line L9 or at line L11. By Lemma 1, the tokens that leave at line L9 come in pairs that met in a slot of $b$. When no token is inside BALANCE on $b$, both members of each pair have left, and since the ids differ, one of them took side 0 and the other side 1. So diffracted tokens add the same amount to $o_0$ and $o_1$. A token leaves at line L11 with the value $t$ that its successful CAS changed to $1 - t$. Successful CASes on $b.toggle$ are totally ordered, each flips the bit, and the bit starts at 0, so the values returned are $0, 1, 0, 1, \ldots$ in this order. After $m$ successful CASes, side 0 got $\lceil m/2 \rceil$ of them and side 1 got $\lfloor m/2 \rfloor$. Adding the pairs gives $o_0 - o_1 = \lceil m/2 \rceil - \lfloor m/2 \rfloor \in \{0, 1\}$, and with $o_0 + o_1 = n$ the two counts are $\lceil n/2 \rceil$ and $\lfloor n/2 \rfloor$. $\square$

Lemma 3 (the step property of the tree). In a quiescent state in which $n$ tokens have entered the tree, wire $i$ has received $c_i = \lceil (n - i)/w \rceil$ tokens, for $0 \le i < w$.

Proof. In a quiescent state every token that entered a balancer has left it, so the tokens that enter a child are exactly the tokens that left its parent on that side. Induction on $k$. For $k = 1$ the tree is one balancer, and Lemma 2 gives $c_0 = \lceil n/2 \rceil$ and $c_1 = \lfloor n/2 \rfloor = \lceil (n - 1)/2 \rceil$. For $k > 1$, the root sends $a = \lceil n/2 \rceil$ tokens to the subtree of side 0 and $b = \lfloor n/2 \rfloor$ to the subtree of side 1. Both subtrees are diffracting trees of width $w/2$, and the root has fixed bit 0 of the wire: wire $j$ of subtree $d$ is wire $2j + d$ of the tree. By induction, wire $2j$ gets $\lceil (a - j)/(w/2) \rceil$ tokens. Since $a - j = \lceil (n - 2j)/2 \rceil$ and $\lceil \lceil x/2 \rceil / (w/2) \rceil = \lceil x/w \rceil$ for each integer $x$, this is $\lceil (n - 2j)/w \rceil$. In the same way $b - j = \lceil (n - 1 - 2j)/2 \rceil$, and wire $2j + 1$ gets $\lceil (n - (2j + 1))/w \rceil$. $\square$

Lemma 4 (values in a quiescent state). In a quiescent state in which $n$ tokens have entered, the tokens have returned exactly the values $0, 1, \ldots, n - 1$, each once.

Proof. Wire $i$'s counter was incremented by each of its $c_i$ tokens, by fetch-and-add, so they got $k = 0, \ldots, c_i - 1$ and returned $i + wk$. A number $v \ge 0$ is $i + wk$ for exactly one pair, $i = v \bmod w$ and $k = \lfloor v/w \rfloor$, and $k < \lceil (n - i)/w \rceil$ holds exactly when $i + wk < n$. So the values returned are $\{0, \ldots, n - 1\}$, each once. $\square$

Theorem (quiescent consistency). Each history $H$ of the diffracting tree is quiescently consistent with respect to the sequential counter.

Proof. First complete $H$. Extend the execution by letting only the pending calls take steps, in any fair order, and start no new call. By the theorem on progress below, and since only finitely many calls are left, they all return, and the extended history $H'$ is $H$ with responses appended for its pending calls, a completion of $H$ that ends in a quiescent state. Let $q_1 < q_2 < \cdots < q_r$ be the quiescent points of $H'$, with $q_r$ at the end, and let $n_j$ be the number of calls that returned before $q_j$. By Lemma 4 the calls that returned before $q_j$ got exactly the values $0, \ldots, n_j - 1$, so the calls between $q_{j-1}$ and $q_j$ got exactly $n_{j-1}, \ldots, n_j - 1$. Let $S$ list the calls of each segment in the order of their values, and the segments in order. $S$ is a legal sequential counter history with the same results as $H'$, and if a quiescent point separates calls $a$ and $b$, $a$ is in an earlier segment and precedes $b$ in $S$. $\square$

Theorem (lock-freedom). In every infinite execution in which some call is pending, infinitely many calls return.

Proof. Suppose that from some moment on no call returns. Each call passes $k$ balancers. In a balancer, the prism part (lines L7 to L9, with lines L12 to L19) ends within $O(\text{patience}^2)$ own steps, and the fetch-and-add at line L5 is one step. So some thread must run the loop of line L10 for ever. Each turn of that loop that fails means that the toggle changed between its read and its CAS, which needs a successful CAS by another token, and each successful CAS ends that token's BALANCE on that balancer. No thread starts a new call before its current call returns, so at most $p$ calls are active, each with at most $k$ successful CASes. So after some moment no CAS at line L10 succeeds. Then no toggle changes, and the next CAS of a thread in the loop of line L10 succeeds. This contradicts the assumption. $\blacksquare$