Lock-free concurrent binomial heaps

We present a linearizable, lock-free concurrent binomial heap. In our experience, a binomial heap is considerably more complex than previously considered concurrent datatypes. The implementation presents a number of challenges. We need to deal with interference when a thread is traversing the heap, searching for the smallest key: our solution is to detect such interference, and restart the traversal. We must avoid interference between updating operations: we add labels to nodes to prevent interfering updates to those nodes; and we add labels to heaps to prevent union operations interfering with other operations on the same heap. This labelling blocks other operations: to achieve lock-freedom, those threads help with the blocking operation; this requires care to ensure correctness, and to avoid cycles of helping that would lead to deadlock. We use a number of techniques to ensure decent efficiency. The complexity of the implementation adds to the difficulty of the proofs of linearizability and lock-freedom: we present each proof in a modular way, proving results about each operation individually, and then combining them to give the desired results. We hope some of these techniques can be applied elsewhere. (C) 2018 Elsevier Inc. All rights reserved.