July 1990 | MAURICE P. HERLIHY and JEANNETTE M. WING
The paper introduces the concept of linearizability as a correctness condition for concurrent objects, which allows for high concurrency while enabling programmers to specify and reason about these objects using sequential techniques. Linearizability ensures that each operation appears to take effect instantaneously, and the order of nonconcurrent operations is preserved. The authors define linearizability formally and demonstrate its locality and nonblocking properties, contrasting it with other correctness conditions like sequential consistency and serializability. They present a method for proving the correctness of implementations of linearizable objects and illustrate it with examples of concurrent queues and registers. The paper also discusses the practical implications of linearizability, emphasizing its suitability for systems requiring real-time response and concurrency.The paper introduces the concept of linearizability as a correctness condition for concurrent objects, which allows for high concurrency while enabling programmers to specify and reason about these objects using sequential techniques. Linearizability ensures that each operation appears to take effect instantaneously, and the order of nonconcurrent operations is preserved. The authors define linearizability formally and demonstrate its locality and nonblocking properties, contrasting it with other correctness conditions like sequential consistency and serializability. They present a method for proving the correctness of implementations of linearizable objects and illustrate it with examples of concurrent queues and registers. The paper also discusses the practical implications of linearizability, emphasizing its suitability for systems requiring real-time response and concurrency.