Proving Highly-Concurrent Traversals Correct
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham
TL;DR
This paper addresses the difficulty of proving linearizability for highly-concurrent traversals by introducing a general proof technique that relies on sequential properties of traversals and a forepassed condition on interfering writes. The core ideas are single-step compatibility between the traversal and reachability predicates, and a forepassed interference constraint that eliminates the need to reason about complex read-write interleavings. A main theorem shows that if these conditions hold, traversal correctness—and thus linearizability—follows, with extensions to contentions on additional fields. The framework is validated on challenging BSTs such as the Logical Ordering tree, the Citrus tree, and the full Contention-Friendly tree, including cases where prior approaches fail. The work simplifies and unifies traversal proofs, with potential for mechanization and broader impact on designing and verifying optimistic traversals in concurrent data structures.
Abstract
Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any synchronization. As a result, however, these algorithms are notoriously difficult to prove linearizable, which requires identifying a point in time in which the traversal's result is correct. The problem is that traversing the data structure as it undergoes modifications leads to complex behaviors, necessitating intricate reasoning about all interleavings of reads by traversals and writes mutating the data structure. In this paper, we present a general proof technique for proving unsynchronized traversals correct in a significantly simpler manner, compared to typical concurrent reasoning and prior proof techniques. Our framework relies only on sequential properties} of traversals and on a conceptually simple and widely-applicable condition about the ways an algorithm's writes mutate the data structure. Establishing that a target data structure satisfies our condition requires only simple concurrent reasoning, without considering interactions of writes and reads. This reasoning can be further simplified by using our framework. To demonstrate our technique, we apply it to prove several interesting and challenging concurrent binary search trees: the logical-ordering AVL tree, the Citrus tree, and the full contention-friendly tree. Both the logical-ordering tree and the full contention-friendly tree are beyond the reach of previous approaches targeted at simplifying linearizability proofs.