Linearizability Analysis of the Contention-Friendly Binary Search Tree

Uri Abraham, Avi Hayoun

We present a formal framework for proving the correctness of set implementations backed by binary-search-tree (BST) and linked lists, which are often difficult to prove correct usi…