Linearizability is a correctness condition for concurrent objects that ensures that each operation appears to take effect instantaneously, providing a sequential-like behavior for concurrent systems. It allows high concurrency while enabling programmers to use sequential reasoning techniques. Linearizability is a local and nonblocking property, meaning that each object can be verified independently, and processes are not forced to wait. It generalizes and unifies various correctness conditions, including sequential consistency and serializability. The paper defines linearizability, compares it to other correctness conditions, and presents a method for proving the correctness of implementations. It also discusses how to reason about concurrent objects given they are linearizable. Linearizability is particularly useful for systems requiring real-time responses, as it ensures nonblocking behavior. The paper includes examples of linearizable queue and register implementations, and discusses the differences between linearizability and other correctness conditions like serializability. The paper also presents a verification method for linearizable implementations, including the use of representation invariants and abstraction functions. The method is illustrated with examples of queue implementations, including those with critical sections. The paper concludes that linearizability is a simple and effective correctness condition for concurrent systems.Linearizability is a correctness condition for concurrent objects that ensures that each operation appears to take effect instantaneously, providing a sequential-like behavior for concurrent systems. It allows high concurrency while enabling programmers to use sequential reasoning techniques. Linearizability is a local and nonblocking property, meaning that each object can be verified independently, and processes are not forced to wait. It generalizes and unifies various correctness conditions, including sequential consistency and serializability. The paper defines linearizability, compares it to other correctness conditions, and presents a method for proving the correctness of implementations. It also discusses how to reason about concurrent objects given they are linearizable. Linearizability is particularly useful for systems requiring real-time responses, as it ensures nonblocking behavior. The paper includes examples of linearizable queue and register implementations, and discusses the differences between linearizability and other correctness conditions like serializability. The paper also presents a verification method for linearizable implementations, including the use of representation invariants and abstraction functions. The method is illustrated with examples of queue implementations, including those with critical sections. The paper concludes that linearizability is a simple and effective correctness condition for concurrent systems.