This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Verifying Linearizability via Optimized Refinement Checking
July 2013 (vol. 39 no. 7)
pp. 1018-1039
Yang Liu, Nanyang Technological University, Singapore
Wei Chen, Microsoft Research Asia, Beijing
Yanhong A. Liu, State University of New York at Stony Brook, Stony Brook
Jun Sun, Singapore University of Technology and Design, Singapore
Shao Jie Zhang, National University of Singapore, Singapore
Jin Song Dong, National University of Singapore, Singapore
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 are serializable, and 2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on refinement checking of finite-state systems specified as concurrent processes with shared variables. To tackle state space explosion, we develop and apply symmetry reduction, dynamic partial order reduction, and a combination of both for refinement checking. We have built the method into the PAT model checker, and used PAT to automatically check a variety of implementations of concurrent objects, including the first algorithm for scalable nonzero indicators. Our system is able to find all known and injected bugs in these implementations.
Index Terms:
History,Sun,Educational institutions,Optimization,Electronic mail,Semantics,PAT,Linearizability,refinement,model checking
Citation:
Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun, Shao Jie Zhang, Jin Song Dong, "Verifying Linearizability via Optimized Refinement Checking," IEEE Transactions on Software Engineering, vol. 39, no. 7, pp. 1018-1039, July 2013, doi:10.1109/TSE.2012.82
Usage of this product signifies your acceptance of the Terms of Use.