Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-05089-3_21
Title: Model checking linearizability via refinement
Authors: Liu, Y. 
Chen, W.
Liu, Y.A.
Sun, J. 
Issue Date: 2009
Source: Liu, Y.,Chen, W.,Liu, Y.A.,Sun, J. (2009). Model checking linearizability via refinement. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5850 LNCS : 321-337. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-05089-3_21
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 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. © 2009 Springer-Verlag Berlin Heidelberg.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/40684
ISBN: 3642050883
ISSN: 03029743
DOI: 10.1007/978-3-642-05089-3_21
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

34
checked on Dec 13, 2017

Page view(s)

48
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


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