Proofs: Buffer tree

The buffer tree answers every query as of its time and keeps its invariants full

This proof shows: correctness, termination.

We use the pseudocode of the page, with $m \ge 4$ , $B \ge 1$ and $M = mB$ . The operations carry distinct time stamps $1, 2, \ldots$ in the order of the input. For a time $t$ , let $D_t$ be the set of the abstract dictionary after the operations with stamps at most $t$ . A query with stamp $t$ and key $k$ is correct if its answer is $k \in D_{t-1}$ . The range of the root is all keys; the range of the child $c_i$ of $x$ is the part of the range of $x$ between the routing keys $r_{i-1}$ and $r_i$ (with $r_0 = -\infty$ and the last one $+\infty$ ). For a node $x$ , let $L(x)$ be the set of keys in the leaves below $x$ , and let $P(x)$ be the sequence of operations in the buffers of $x$ and of all its descendants.

Claim. After each step of the algorithm, outside of a running call of EMPTY, these hold:

(T1) the routing keys of each node are increasing, the keys of each leaf are in its range, and all leaves are at one depth;
(T2) each operation in the buffer of $x$ has its key in the range of $x$ ;
(T3) each buffer is in time order, and every operation in a buffer of $y$ is older than every operation in a buffer of a proper ancestor of $y$ ;
(D) for every key $k$ , let $t$ be the stamp of the oldest operation on $k$ still in a buffer (or the current time plus one if there is none). Then $k \in L(\text{root})$ if and only if $k \in D_{t-1}$ ;
(Q) every answered query is correct.

Base. The empty tree has one bottom root with an empty leaf and an empty buffer. All five properties hold.

Lines L1 and L2. Line L1 appends a new operation, the youngest of all, to the root buffer. The root has no ancestor, the operation is younger than every buffered one, and the range of the root is all keys, so (T2) and (T3) hold. No leaf changes. For (D): if the new operation is on $k$ and no other operation on $k$ is buffered, then $t$ becomes the new stamp, and $D_{t-1}$ is the old current set, which holds $k$ exactly when $L$ does by (D) before the step. Otherwise $t$ does not change. Line L2 calls EMPTY, treated next.

EMPTY(x). We show by induction on the calls: if, when EMPTY $(x)$ starts, the buffers of all proper ancestors of $x$ are empty and (T1) to (T3), (D) and (Q) hold, then they hold when it returns.

Line L3 takes the buffer of $x$ , in time order by (T3). Consider an operation $o$ in it, with key $k$ .

Lines L5 and L6 (x not bottom). Line L5 routes $o$ to the unique child $c$ whose range holds $k$ , which exists by (T1) and (T2), so (T2) holds for $c$ . The operations are appended in time order, and each one is younger than every operation already in the buffer of $c$ or below it, by (T3) for $x$ before the step. The ancestors of $c$ other than $x$ have empty buffers, and $x$ is now empty, so (T3) holds. No leaf changes, and the set of buffered operations does not change, so (D) holds. Line L6 calls EMPTY on children of $x$ ; the buffers of their ancestors, $x$ and above, are empty, so the induction hypothesis applies to each call, in turn. The calls of L6 on different children touch disjoint subtrees, except for splits, which we treat below.

Lines L7 to L10 (x bottom). Let $k$ be a key in the range of $x$ . By (T2) and (T3), every buffered operation on $k$ is in the buffer of $x$ or above, and the buffers above are empty, so all of them are in ops, and they are the youngest operations on $k$ there have been: every older one has already been applied. By (D), before line L8, $k \in S$ exactly when $k \in D_{t-1}$ , where $t$ is the stamp of the first operation on $k$ in ops. Line L8 goes through ops in time order, and line L9 changes the membership of $k$ in $S$ exactly as the dictionary does: an insert adds $k$ , a delete removes it, and a query does not change it. So, by induction along the loop, when line L9 meets an operation with stamp $s$ on $k$ , $k \in S$ exactly when $k \in D_{s-1}$ , because the operations with stamps between $t$ and $s$ that act on $k$ are exactly the earlier ones on $k$ in ops. So each query is answered correctly, which keeps (Q). After the loop, no operation on $k$ is buffered, and $k \in S$ exactly when $k \in D_{\text{now}}$ , which is (D). Line L10 writes $S$ in increasing order into leaves of at most $B$ keys and sets the routing keys to the first keys of the leaves after the first, so the routing keys are increasing and the keys of each leaf are in its range. The leaves are still one level below $x$ , so all leaves keep one depth: (T1) holds. Keys of other bottom nodes do not change.

SPLIT(x). Line L11 calls SPLIT only from a bottom node $x$ inside EMPTY $(x)$ , after line L3, so the buffer of $x$ and of all its ancestors are empty. SPLIT goes up only to the parent, which is an ancestor of the first $x$ , so the same holds at every call. Line L12 cuts the $c > m$ children of $x$ into $g = \lceil c/m \rceil$ groups of sizes $\lfloor c/g \rfloor$ or $\lceil c/g \rceil$ , each at most $m$ and at least $\lfloor c/g \rfloor \ge 1$ . Line L13 gives each group its own node with the routing keys inside the group, and puts the routing keys between the groups into the parent, after the key that led to $x$ . So the routing keys of the parent stay increasing, and the range of each new node is the union of the ranges of its children, which keeps (T1). The new nodes are at the depth of $x$ , so the leaf depths do not change. Line L14 adds a new root above the old root and the new nodes when $x$ was the root; this adds one to the depth of all leaves at once, which keeps them equal. All moved nodes have empty buffers, and no operation moves, so (T2), (T3), (D) and (Q) hold. Line L15 repeats the step at the parent, which can now have more than $m$ children, and stops at a node with at most $m$ children, so after SPLIT every node has at most $m$ children.

A split can move a sibling $c'$ of the current path, whose buffer is not empty, to a new node. This is harmless: $c'$ keeps its subtree and its range, and its new parent has an empty buffer, so (T2) and (T3) hold for its operations. When the loop of line L6 then calls EMPTY on $c'$ , its ancestors are still empty, since only the path of the current call can have held operations and all of it was emptied.

Buffer sizes. After an operation, no buffer is full: line L2 empties the root when it overflows, and line L6 empties each child that overflows after line L5. A child that is not full when line L6 runs is not touched again in that call, so at the end every buffer holds at most $M$ operations.

Flush. The flush calls EMPTY top-down on every node with a nonempty buffer, starting at the root. In each call the buffers of the ancestors are empty, since the parent was emptied first in the same pass, so the arguments above apply. The pass repeats while a buffer is nonempty. When it ends, no operation is buffered, so by (Q) every query has been answered, and by (D) the leaves hold exactly the current set $D_{\text{now}}$ . The global rebuild flushes first and then builds a tree with empty buffers from the sorted keys, with groups of at most $m$ children and all leaves at one depth, so it keeps all five properties.

Termination. Each call of EMPTY at a non-bottom node moves every operation in its buffer one level down, and EMPTY-BOTTOM removes the operations it gets. An operation is in exactly one buffer, and the tree has finite height, so the number of moves of each operation is bounded by the height plus one, and the recursion of EMPTY ends. SPLIT goes up one level per call and stops at the root. Each pass of the flush either empties all buffers or moves some operation down, because it calls EMPTY on the root and on every nonempty buffer it reaches; operations only move down and new operations do not arrive during a flush, so the flush ends after finitely many passes.

So every query gets its correct answer by the end of the flush at the latest, and the leaves always hold the current set once all buffers are empty. $\blacksquare$