Proofs: Combining tree

The combining tree is a linearizable, deadlock-free counter full

This proof shows: correctness, linearizability, progress.

We use the pseudocode of the page. Each node procedure runs under the monitor of its node, so it is atomic, except that "wait until" releases the monitor while the condition is false and holds it from the moment the condition is true until the procedure ends. Concurrent callers have distinct ids, so at most two threads start at each leaf at any time. Depth is measured from the root, which has depth 0.

Rounds at a node. Fix a non-root node $n$. A round at $n$ starts when a thread $A$ sets $n.status$ from IDLE to FIRST at line L10 and ends when $n.status$ is IDLE again. We call $A$ the active thread of the round. If some thread $B$ sets FIRST to SECOND at line L11 during the round, $B$ is its passive thread.

Lemma 1 (one pair per round). In each round at $n$ there is one active thread and at most one passive thread, and the passive thread, if any, arrives before the active thread combines at $n$. The round ends at line L20 if there is no passive thread, and at line L19 otherwise. During a round no other thread passes line L9 or line L13 at $n$ except as stated.

Proof. Line L10 needs status IDLE, so only one thread starts the round, and line L11 needs status FIRST, so at most one passive thread comes. The flag $n.locked$ is true from line L11 of the passive thread until its line L17, and again from line L14 of the active thread until the end of the round (line L20, or line L19 of the passive thread). The active thread passes line L13 only when the flag is false: either before any passive thread came, and then line L14 sets the flag with status FIRST, so no passive thread can come until line L20 ends the round; or after line L17 of the passive thread.

It remains to show that no third thread $T$ runs line L10 to L12 at $n$ during the round, which we prove by induction on the height of $n$. A thread reaches $n$ either at the start of a call, if $n$ is its leaf, or after it was active at a child of $n$. If $n$ is a leaf, the only threads that start there are the two with ids $2i$ and $2i + 1$, so $T$ is $A$ or $B$ in a later call. $B$ returns only at line L19, which ends the round. $A$ returns after line L20, which ends the round, or after line L21, which leaves status RESULT and the flag set, so a new call of $A$ waits at line L9. If $n$ is not a leaf, $A$ and $B$ came from children $c_A e c_B$ of $n$, where their own rounds are in progress: the round of $B$ at $c_B$ lasts until $B$ distributes there, after line L19 at $n$, and the round of $A$ at $c_A$ lasts until $A$ distributes there, after it has distributed at $n$. By the induction hypothesis no third thread becomes active at $c_A$ or $c_B$ during these rounds, so $T$ cannot come from there before $A$ has distributed at $n$, and after that the flag is set until the round ends. $\square$

Lemma 2 (what a thread carries). Say that a thread $T$ covers itself and, for each node $n$ at which $T$ combined as the active thread with status SECOND, all threads covered by the passive thread of $n$ in its call. Then the value combined that $T$ passes to line L6 is the number of threads it covers, the sets covered at different nodes are disjoint, and a thread is covered only by threads of the same batch, defined below.

Proof. By induction on the climb of $T$. At the start combined $= 1$, for $T$ itself. At line L15 at node $n$, $T$ adds $n.second$, which the passive thread $B$ of the round wrote at line L17 as its own combined value, so by induction on $B$ (whose climb ended at $n$, below $T$'s stop node, and happened earlier) it is the number of threads that $B$ covers. Line L14 records the old value of combined in $n.first$. The sets are disjoint because they come from different subtrees: $B$ climbed only in the subtree of the child of $n$ from which it came, and each thread is counted by the one active thread that combined with it. $\square$

Batches. A call that runs line L16 at the root is the head of a batch; the batch is the set of threads that the head covers, of size $c$. The head's root step adds $c$ to the counter and gets prior.

Lemma 3 (distribution). The threads of a batch return the values prior, prior $+ 1$, $\ldots$, prior $+ c - 1$, each value once.

Proof. We show more: if a thread $T$ gets value $q$ at line L6 and covers $k$ threads, then the threads it covers return $q, \ldots, q + k - 1$, with $T$ itself returning $q$. $T$ returns $q$ at line L8. $T$ combined at its nodes from the leaf up, and at the node $n$ of its $j$-th combine it had already covered $n.first$ threads, those of the nodes below $n$ and itself. The passive thread $B$ of $n$ covers $n.second$ threads. Line L21 gives $B$ the value $q + n.first$, and $B$ returns it from line L19, since the passive thread reads $n.result$ in the same atomic block that ends its wait. By induction on $B$, the threads $B$ covers get $q + n.first, \ldots, q + n.first + n.second - 1$. The nodes of $T$ in order from the leaf give consecutive blocks that start right after the block of the nodes below, so the blocks of $T$, from the leaf up, are $\{q\}$ and then consecutive ranges that fill $q + 1, \ldots, q + k - 1$. $\square$

Theorem (linearizability). Each history of the combining tree is linearizable with respect to the sequential counter.

Proof. The root steps of different batches are atomic steps at the root monitor and are totally ordered. Each one adds the size of its batch to the root result, so by Lemma 3 the batches get disjoint ranges of values, in the order of their root steps, and all values from the initial count up are used. Linearize every call of a batch at the root step of the batch, ordered by value within the batch. Take any call $X$ of the batch. $X$ is pending at this step: it started before, since it has precombined and deposited its increment (or is the head), and it has not returned, since it returns only after the head has distributed, which is after the root step. So each linearization point is inside its call's interval, and the order of points respects real time. In this order, the $k$-th call gets the initial count plus $k - 1$, which is the sequential specification. A pending call that has not reached the root step of its batch is removed from the completion; a call whose batch has done its root step is completed with the value given by Lemma 3. $\square$

Theorem (deadlock-freedom). If threads keep taking steps and some call is pending, some call returns.

Proof. Classify the waits. (a) An active thread at line L13 of node $n$ waits for the passive thread $B$ of $n$ to run line L17 (Lemma 1). (b) A passive thread at line L18 of $n$ waits for the active thread of $n$ to run line L21. (c) A thread at line L9 of $n$ waits for the end of the current round at $n$.

Claim 1. Each thread that has finished precombining reaches line L6. Its combines are at nodes on its path below its stop node. A wait (a) at depth $d$ is for a thread $B$ whose remaining combines are at depths greater than $d$, after which $B$ runs line L17 with no further wait. By induction on depth, from the deepest nodes up, each such wait ends.

Claim 2. Each thread that has reached line L6 returns. At the root, line L16 has no wait, and line L20 and line L21 have none. A passive thread at stop node $n$ of depth $d \ge 1$ waits (b) for the active thread $A$ of $n$. By Claim 1, $A$ reaches line L6 at its stop node, of depth less than $d$. By induction on the depth of the stop node, from the root down, $A$ returns, and it runs line L21 at $n$ on its way, which ends the wait of the passive thread, which then returns.

Claim 3. Suppose no call returns from some moment on. By Claims 1 and 2, each thread that has finished precombining returns, so from that moment on no thread has finished precombining: every pending thread is in its precombining phase. A flag is set only by a thread that has finished precombining (lines L11 and L14) and cleared by such threads before they return, so then every flag is false, no thread waits at line L9, and each pending thread finishes precombining within $O(\log w)$ of its own steps. This contradicts the assumption. $\blacksquare$