Model Checking Linearizability via Refinement

Abstract. Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking 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 determining linearization points in implementations, but can also take advantage of linearization points if they are given. The method exploits model checking of finite state systems specified as concurrent processes with shared variables. Partial order reduction is used 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 variet...

• Type: Conference
• Year: 2009
• Where: FM
• Authors: Yang Liu 0003, Wei Chen, Yanhong A. Liu, Jun Sun 0001
• Keywords: Concurrent Objects, Concurrent Operations, FM 2009, Formal Methods, Linearization Points