Lock-free concurrent binomial heaps

Journal article

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.

Authors: Lowe, G

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Elsevier
• Journal: Journal of Logical and Algebraic Methods in Programming
• Volume: 101
• Pages: 44-87
• Publication date: 2018-08-24
• Acceptance date: 2018-08-10
• DOI: 10.1016/j.jlamp.2018.08.001
• ISSN: 2352-2208
• Keywords: lock-freedom; binomial heaps; concurrent datatypes; Linearizability