LINEARIZABILITY - A CORRECTNESS CONDITION FOR CONCURRENT OBJECTS
LINEARIZABILITY - A CORRECTNESS CONDITION FOR CONCURRENT OBJECTS
复制标题
DOI：
10.1145/78969.78972
复制
发表时间：
1990-07-01
影响因子：
1.3
通讯作者：
WING, JM
中科院分区：
文献类型：
--
作者：
HERLIHY, MP;WING, JM
并发对象是由并发进程共享的数据对象。可线性化是利用抽象数据类型语义的并发对象的正确性条件。它允许高度并发，但允许程序员使用序列域中的已知技术指定并发对象并对其进行推理。Linearizable提供了一种错觉，即并发进程应用的每个操作在其调用和响应之间的某个点立即生效，这意味着并发对象的操作的含义可以由前置条件和后置条件赋予。本文定义了可线性化的概念，并将其与其他正确性条件进行了比较，提出并证明了一种证明实现正确性的方法，并展示了如何在并发对象可线性化的情况下对其进行推理。
A concurrent object is a data object shared by concurrent processes. Linearizability is a correctness condition for concurrent objects that exploits the semantics of abstract data types. It permits a high degree of concurrency, yet it permits programmers to specify and reason about concurrent objects using known techniques from the sequential domain. Linearizability provides the illusion that each operation applied by concurrent processes takes effect instantaneously at some point between its invocation and its response, implying that the meaning of a concurrent object's operations can be given by pre- and post-conditions. This paper defines linearizability, compares it to other correctness conditions, presents and demonstrates a method for proving the correctness of implementations, and shows how to reason about concurrent objects, given they are linearizable.