混沌中的有序：使用局部视图证明线性化
Order out of Chaos: Proving Linearizability Using Local Views
摘要：
证明高度并发数据结构（例如使用乐观并发控制的数据结构）的线性化是一项具有挑战性的任务。主要的困难在于推理线程获得的内存视图，因为当它们执行时，线程从不同的时间点观察不同的内存片段。直到今天，每一个线性化证明都是从零开始解决这个挑战的。我们提出了一个统一的证明参数的正确性的非同步遍历，并将其应用于证明线性化的几个高度并发的搜索数据结构，包括乐观的自平衡二叉搜索树，懒惰列表和无锁跳表。我们的框架利用{ \em顺序推理}关于线程的视图，考虑线程，如果它遍历数据结构没有其他操作的干扰。我们的主要贡献是显示沿搜索路径的可达性的属性可以推导出并发遍历从这样的无干扰遍历，当某些直观的条件得到满足。基于这种\emph{local view arguments}的遍历的正确性大大简化了线性化证明。为了应用我们的框架，用户证明数据结构满足两个条件：（1）存储器上的顺序的非循环性，即使在跨中间存储器状态考虑时也是如此，以及（2）保留搜索路径到被干扰写入修改的位置。建立的条件，以及充分的线性化证明，利用我们的证明论点，减少到简单的并发推理。其结果是一个清晰和可理解的正确性证明，并阐明了几个现有的数据结构的基础上的共同模式。
英文摘要：
Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is a challenging task. The main difficulty is in reasoning about the view of the memory obtained by the threads, because as they execute, threads observe different fragments of memory from different points in time. Until today, every linearizability proof has tackled this challenge from scratch. We present a unifying proof argument for the correctness of unsynchronized traversals, and apply it to prove the linearizability of several highly concurrent search data structures, including an optimistic self-balancing binary search tree, the Lazy List and a lock-free skip list. Our framework harnesses {\em sequential reasoning} about the view of a thread, considering the thread as if it traverses the data structure without interference from other operations. Our key contribution is showing that properties of reachability along search paths can be deduced for concurrent traversals from such interference-free traversals, when certain intuitive conditions are met. Basing the correctness of traversals on such \emph{local view arguments} greatly simplifies linearizability proofs. To apply our framework, the user proves that the data structure satisfies two conditions: (1) acyclicity of the order on memory, even when it is considered across intermediate memory states, and (2) preservation of search paths to locations modified by interfering writes. Establishing the conditions, as well as the full linearizability proof utilizing our proof argument, reduces to simple concurrent reasoning. The result is a clear and comprehensible correctness proof, and elucidates common patterns underlying several existing data structures.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
