Proving Highly-Concurrent Traversals Correct

Modern highly-concurrent search data structures, such as search trees, obtainmulti-core scalability and performance by having operations traverse the datastructure without any synchronization. As a result, however, these algorithmsare notoriously difficult to prove linearizable, which requires identifying apoint in time in which the traversal's result is correct. The problem is thattraversing the data structure as it undergoes modifications leads to complexbehaviors, necessitating intricate reasoning about all interleavings of readsby traversals and writes mutating the data structure. In this paper, we present a general proof technique for provingunsynchronized traversals correct in a significantly simpler manner, comparedto typical concurrent reasoning and prior proof techniques. Our frameworkrelies only on sequential properties} of traversals and on a conceptuallysimple and widely-applicable condition about the ways an algorithm's writesmutate the data structure. Establishing that a target data structure satisfiesour condition requires only simple concurrent reasoning, without consideringinteractions of writes and reads. This reasoning can be further simplified byusing our framework. To demonstrate our technique, we apply it to prove several interesting andchallenging concurrent binary search trees: the logical-ordering AVL tree, theCitrus tree, and the full contention-friendly tree. Both the logical-orderingtree and the full contention-friendly tree are beyond the reach of previousapproaches targeted at simplifying linearizability proofs.