Model Checking Linearizability via Refinement

Linearizability is an important correctness criteria for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires that 1) all executions of concurrent operations be serializable, and 2) the serialized executions be correct with respect to the sequential semantics. This paper describes a new method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. Our method avoids the often difficult task of identifying linearization points in implementations, but can also take advantage of linearization points if they are given. The method exploits modeling checking of finite state systems specified as concurrent processes with shared variables. Partial order reduction is exploited to effectively reduce the search space. The approach is built into a toolset that supports a rich set of concurrent operators. The tool has been used to automatically check a variety of implementations of concurrent objects, including the first algorithms for the mailbox problem and scalable NonZero indicators. Our system was able to find all known and injected bugs in these implementations.