On Correctness of Data Structures under Reads-Write Concurrency
On Correctness of Data Structures under Reads-Write Concurrency
复制标题
读写并发下数据结构的正确性探讨
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
I. Keidar
中科院分区：
文献类型：
--
作者：
Kfir Lev;G. Chockler;I. Keidar
研究了读写并发情况下共享数据结构的正确性。在存在并发更新的情况下，确保只读操作正确性的一种流行方法是读集验证，它检查所有读变量自首次读取以来是否未发生过更改。在实践中，这种方法通常过于保守，从而对性能产生不利影响。在本文中，我们引入了一个新的框架来推理读写并发下数据结构的正确性，它用更通用的标准取代了对整个读集的验证。也就是说，我们不是验证所有读共享变量是否仍然保存从它们读取的值，而是验证共享变量上的抽象条件，我们称之为基条件。我们表明，在每个时间点读取满足某些基本条件的值意味着只读操作与更新并行执行的正确性。令人惊讶的是，结果的正确性保证并不等同于线性化，而是通过两个新条件：有效性和规律性来获得。粗略地说，前者要求只读操作永远不会达到顺序执行中无法达到的状态；后者将Lamport的正则性概念推广到任意数据结构，并且比线性化弱。我们进一步扩展我们的框架来捕获线性化。我们将演示如何将我们的框架应用于各种数据结构（如链表）实现的正确性推理。
We study the correctness of shared data structures under reads-write concurrency. A popular approach to ensuring correctness of read-only operations in the presence of concurrent update, is read-set validation, which checks that all read variables have not changed since they were first read. In practice, this approach is often too conservative, which adversely affects performance. In this paper, we introduce a new framework for reasoning about correctness of data structures under reads-write concurrency, which replaces validation of the entire read-set with more general criteria. Namely, instead of verifying that all read shared variables still hold the values read from them, we verify abstract conditions over the shared variables, which we call base conditions. We show that reading values that satisfy some base condition at every point in time implies correctness of read-only operations executing in parallel with updates. Somewhat surprisingly, the resulting correctness guarantee is not equivalent to linearizability, and is instead captured through two new conditions: validity and regularity. Roughly speaking, the former requires that a read-only operation never reaches a state unreachable in a sequential execution; the latter generalizes Lamport’s notion of regularity for arbitrary data structures, and is weaker than linearizability. We further extend our framework to capture also linearizability. We illustrate how our framework can be applied for reasoning about correctness of a variety of implementations of data structures such as linked lists.