Linearizability By Construction

This paper presents a methodology for building a class of highly concurrent linked objects that are linearizable by construction, and a corresponding verification technique. The main feature these objects have in common is that they allow correct sequential search operations. We derive our design from invariants and lemmas needed to guarantee the correctness of the search operation, which can then be translated to a purely thread modular proof. We design and verify an internal-external binary search tree following this methodology as an example. Together with generalizing the Hindsight lemma, we also prove a novel Data-Extension lemma that is particularly useful for trees. We show that some advanced highly concurrent data structures such as trees can be designed from some surprisingly simple invariants.