Proofs: Fine-grained concurrent heap

The fine-grained heap conserves items, is a heap when quiescent, is exact for isolated calls, and is deadlock-free full

This proof shows: correctness, linearizability, progress.

We use the pseudocode of the page, with capacity $N$ and $rev$ the bit-reversed order. LOCK and UNLOCK are those of a mutex. Each insert runs with an id $me \ge 1$ that no other running insert uses. The specification is the exact priority queue on a multiset $Q$. We prove four safety properties and deadlock-freedom, and we show that linearizability, the property named in the front matter, does not hold.

Lemma 1 (exclusion). Every read and write of a slot is done by the holder of its lock, and every read and write of $size$ by the holder of the size lock.

Proof. By inspection of lines L1 to L21: each access sits between a LOCK and the matching UNLOCK of the same lock. $\square$

Call the slots $rev(1), \ldots, rev(size)$ in range. Call a slot pending for an insert between lines L1 and L3 if it is the slot $rev(size)$ that the insert chose, and for a delete-min between lines L14 and L15 if it is its bottom slot $b$. Since $rev$ is a bijection between $1..2^k - 1$ and the slots of the first $k$ levels, and the parent of $rev(n)$ is $rev(m)$ for some $m < n$, the in-range slots are closed under taking parents.

Lemma 2 (shape). At every moment: (a) a slot that is not pending is not EMPTY exactly when it is in range; (b) each slot is pending for at most one call; (c) an insert pending at slot $rev(size)$ either holds the size lock or holds the slot lock, and a delete-min pending at $b$ holds the lock of $b$, with $b$ out of range.

Proof. By induction on the steps. At the start all slots are EMPTY and $size = 0$. Only lines L1, L3, L14, L15 change $size$ or the set of pending slots, and only lines L3, L15 and the swaps change whether a slot is EMPTY. Line L1 adds $rev(size + 1)$ to the range and makes it pending, under the size lock. Line L2 takes the slot lock before it releases the size lock, so (c) holds for the insert. Line L3 writes an item and ends the pending state. Line L14 removes $b = rev(size)$ from the range and makes it pending, under its lock; no insert is pending at $b$, since that insert would hold the size lock or the lock of $b$ (by (c)), and so $b$ was not EMPTY. Line L15 makes $b$ EMPTY and ends the pending state. A swap at line L7 or L20 exchanges two slots that are both not EMPTY (line L6 requires the parent AVAILABLE and the child tagged $me$; line L19 picks a child that is not EMPTY, and slot $i$ holds the moving item). Line L17 writes the root only when it is not EMPTY. So each step keeps (a), (b) and (c). $\square$

Lemma 3 (conservation). Each item that was inserted and not yet returned is, at every moment, either in exactly one slot that is not EMPTY, or held by exactly one call: by its insert before line L3, or by a delete-min between lines L15 and L17. Each item returned by a delete-min was inserted, and is returned once.

Proof. Line L3 moves the item of the insert into its slot. That slot is EMPTY at this moment: it was out of range before line L1, so by Lemma 2(a) EMPTY or pending for a delete-min, and the delete-min empties it at line L15 before it unlocks it, while the insert waits for the lock at line L2. Line L15 moves the bottom item from its slot into the hands of the delete-min. Line L17 exchanges the held item with the root item, so the held item is now in a slot and the root item is held. If the root is EMPTY at line L16, nothing moves. The swaps exchange two items between slots. A delete-min returns the item it holds and then holds nothing more. No other step moves an item. $\square$

Lemma 4 (tags). At every moment, at most one slot holds the tag $me$ of a running insert $I$. While $I$ is in the loop of lines L4 to L11 at index $i$, that slot, if it exists, is $i$ or an ancestor of $i$. After $I$ returns, no slot holds the tag $me$.

Proof. The tag $me$ is written once, at line L3, into slot $i$. Swaps move a tag with its item; line L8, line L12 and line L17 overwrite tags with AVAILABLE; line L15 overwrites with EMPTY. So the tag is on at most one slot. A swap at line L7 by $I$ moves the tag from $i$ to $p$, and $I$ sets $i \leftarrow p$. A swap at line L7 by another insert $J$ needs its parent AVAILABLE, so it never moves $me$ down; it moves $J$'s own tag up. A swap at line L20 moves the item of the child up and the item of the delete-min, which is AVAILABLE, down. So the tag $me$ only moves up the tree, or disappears. At line L9, the child is not tagged $me$, so by the claim the tag is above $i$, at $p$ or higher, and $I$ sets $i \leftarrow p$. So the claim holds through the loop.

The loop ends either at line L8, which overwrites the tag $me$ at slot $i$, or with $i = 1$. In the second case, by the claim, the tag is at the root or gone, and line L12 overwrites it. $\square$

Lemma 5 (no stuck owner). When an insert $I$ holds the locks of $p$ and $i$ in its loop and slot $i$ is tagged $me$, the parent $p$ is not EMPTY.

Proof. Slot $i$ is not EMPTY and not pending: $I$'s own pending state ended at line L3, and a delete-min pending at $i$ would hold its lock. By Lemma 2(a) $i$ is in range, so $p$ is in range. $p$ is not pending for an insert, since that insert's slot is $rev(size)$, the in-range slot with the largest index in the order, and the index of $p$ is smaller than that of $i$. It is not pending for a delete-min, since such a slot is out of range. So by Lemma 2(a) $p$ is not EMPTY. $\square$

So when $I$ owns the child, the parent is AVAILABLE, and $I$ moves at line L7 or stops at line L8, or the parent is tagged by another insert, and $I$ waits at line L11.

Theorem 1 (quiescent heap). At every moment at which no call is running, the slots that are not EMPTY are exactly $rev(1), \ldots, rev(size)$, all of them are AVAILABLE, and each is at least its parent. They hold exactly the inserted items that have not been returned.

Proof. With no call running, no slot is pending, so the first claim is Lemma 2(a), and no tag of an insert remains by Lemma 4. The last claim is Lemma 3. For the heap order, call a pair (parent $p$, child $c$) of AVAILABLE slots broken if $c < p$. We show that each broken pair is covered by a running call: either the child is the slot $i$ of an insert whose tag is on $c$, or one of the slots is the slot $i$ of a delete-min after line L17. Then, with no call running, no pair is broken.

Initially no pair is broken. A pair can become broken only when the value or tag of one of its slots changes. Line L3 writes a tagged item, which is not AVAILABLE. Line L7 swaps the child and parent of $I$ when the child is smaller: afterwards the item of $I$, still tagged, is at $p$, and its pair with the parent of $p$ is not of two AVAILABLE slots; the old parent value is now at $c$ and is at most the values below $c$, since it was at most the old value of $c$, and the pairs below $c$ with AVAILABLE children were not broken or were covered by the same calls as before. Line L8 makes the child AVAILABLE only when it is at least its parent; its own children are at least the old value only if they were not broken, and a child of an item that was tagged is not compared in any AVAILABLE pair, so the children of $c$ are covered or correct as before. Lines L12 and L17 make the root AVAILABLE: L12 after the item of $I$ has reached the root, where it has no parent; its pairs with children are covered as before; L17 puts the item of the delete-min at the root and covers its pairs, since $i = 1$. Each swap at line L20 moves the item of the delete-min down one level, past the smaller child: the new parent is the smaller of the two children, so it is at most its other child and at least its own parent, and the delete-min, now at $i = c$, covers the pairs of $c$. Line L19 and the else branch of line L20 end the walk only when slot $i$ has no child or its item is at most its smallest child, so no pair is left broken. Line L15 empties a slot and does not break a pair. Line L9 changes no slot. So each broken pair stays covered until it is repaired, and the theorem follows. $\square$

Theorem 2 (isolated calls). A call that overlaps no other call returns what the sequential heap returns: insert adds its item, and delete-min returns the minimum of $Q$, or EMPTY if $Q$ is empty.

Proof. The call starts at a quiescent moment, so by Theorem 1 the array is a valid heap of $Q$ with $size = |Q|$. No other call runs, so every lock is free and no tag of another insert exists. The insert then runs the sequential sift-up: line L6 holds at every step, line L7 swaps while the item is smaller than its parent, and line L8 or line L12 marks it. The delete-min runs the sequential delete-min: it moves the last item to the root and sifts it down, and it returns the old root, which is the minimum of a valid heap, or EMPTY when $size = 0$, which means $Q$ is empty. $\square$

Theorem 3 (not linearizable). The heap is neither linearizable nor quiescently consistent with respect to the exact priority queue.

Proof. Two schedules of the page. First, let slots 1, 2, 3 hold 0, 1, 13. Delete-min $A$ takes 13 from slot 3, locks the root and swaps 13 into it, keeping 0. Delete-min $B$ takes 1 from slot 2 and waits for the root. $A$ finds its left child EMPTY at line L19 and returns 0. $B$ swaps 1 into the root and returns 13. The two calls overlap, so either order is allowed, but on $\{0, 1, 13\}$ the second of two exact delete-mins returns 1, never 13. So the history is not linearizable.

Second, let slots 1 and 2 hold 2 and 5. Delete-min $D_1$ takes 5 from slot 2. $D_2$ takes 2 from the root and returns 2. $D_3$ sees $size = 0$ and returns EMPTY. An insert of 9 puts 9 at the root. $D_1$ swaps 5 into the root and returns 9. The history starts and ends in quiescent states, and all four calls overlap $D_1$, so quiescent consistency would let us order them in any way. In every order, 5 is in $Q$ from the start to the end, since no call returns 5, so no exact delete-min can return EMPTY. So the history is not quiescently consistent, and so not linearizable. $\square$

Theorem 4 (deadlock-freedom). If threads keep taking steps and some call is running, some call finishes.

Proof. Order the locks as: the size lock first, then the slots by index. A call waits for a lock only while it holds locks that come earlier in this order: insert waits for the size lock holding nothing, for its slot at line L2 holding the size lock, and for a parent and then its child at line L5, holding nothing and then the parent; delete-min waits for its bottom slot holding the size lock, for the root at line L16 holding nothing, and for two children while it holds their parent. So no cycle of threads waiting for locks exists, and every lock that is held is released after a bounded number of steps of its holder, unless the holder waits for a later lock; by induction from the latest lock in the order, every lock wait ends.

The remaining wait is the retry of line L11. By Lemma 5 and the cases of lines L6 to L9, an insert $I$ retries without moving only when it owns the child $i$ and the parent $p$ is tagged by another insert $J$. Suppose that from some moment no call finishes. Delete-mins never retry, so each one finishes after its lock waits end; so from some moment only inserts run, and only inserts that retry. Take a retrying insert $J$ whose item is at the slot nearest the root among all tagged slots. By Lemma 4, $J$ is at its item's slot or below it. If $J$ is below its item, its child is not tagged by $J$, so line L9 moves $J$ up. If $J$ is at its item's slot, its parent is not tagged by another insert, by the choice of $J$, and it is not EMPTY by Lemma 5, so it is AVAILABLE, and $J$ moves its item up at line L7 or stops at line L8. Each of these moves reduces the depth of $J$ or of its item, or ends $J$'s loop, and $J$ then finishes after line L12. So some insert finishes, which is the contradiction. $\blacksquare$