Please use this identifier to cite or link to this item:
Title: Verifying linearizability via optimized refinement checking
Authors: Liu, Y.
Chen, W.
Liu, Y.A.
Sun, J.
Zhang, S.J.
Dong, J.S. 
Keywords: Linearizability
model checking
Issue Date: 2013
Citation: Liu, Y., Chen, W., Liu, Y.A., Sun, J., Zhang, S.J., Dong, J.S. (2013). Verifying linearizability via optimized refinement checking. IEEE Transactions on Software Engineering 39 (7) : 1018-1039. ScholarBank@NUS Repository.
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 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. © 1976-2012 IEEE.
Source Title: IEEE Transactions on Software Engineering
ISSN: 00985589
DOI: 10.1109/TSE.2012.82
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.


checked on Jul 10, 2020


checked on Jul 10, 2020

Page view(s)

checked on Jun 28, 2020

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.