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.

翻译：现代高并发搜索数据结构（如搜索树）通过使操作在无任何同步的情况下遍历数据结构，实现了多核可扩展性与高性能。然而，这些算法因难以证明其线性化特性而著称——这需要识别遍历结果正确的时间点。问题在于，当数据结构在遍历过程中发生修改时，会导致复杂的行为，需要精细推理所有遍历读取操作与修改数据结构的写入操作之间的交错。本文提出一种通用证明技术，以显著简化的方式证明非同步遍历的正确性，相较于典型的并发推理和先前的证明技术更为简洁。我们的框架仅依赖于遍历的序属性，以及关于算法写入操作修改数据结构的、概念简单且广泛适用的条件。证明目标数据结构满足该条件仅需简单的并发推理，无需考虑写入与读取操作的交互。该推理过程可进一步借助我们的框架简化。为展示该技术，我们将其应用于证明多种有趣且具有挑战性的并发二叉搜索树：逻辑排序AVL树、Citrus树以及完全友好竞争树。其中逻辑排序树和完全友好竞争树均超出了以往旨在简化线性化性证明的方法所能处理的范畴。