View Item 
      •   Home
      • 1. Schools
      • College of Engineering
      • School of Computer Science and Engineering (SCSE)
      • SCSE Journal Articles
      • View Item
      •   Home
      • 1. Schools
      • College of Engineering
      • School of Computer Science and Engineering (SCSE)
      • SCSE Journal Articles
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.
      Subject Lookup

      Browse

      All of DR-NTUCommunities & CollectionsTitlesAuthorsBy DateSubjectsThis CollectionTitlesAuthorsBy DateSubjects

      My Account

      Login

      Statistics

      Most Popular ItemsStatistics by CountryMost Popular Authors

      About DR-NTU

      Verifying linearizability via optimized refinement checking

      Thumbnail
      Author
      Liu, Yang
      Chen, Wei
      Liu, Yanhong A.
      Sun, Jun
      Zhang, Shao Jie
      Dong, Jin Song
      Date of Issue
      2013
      School
      School of Computer Engineering
      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.
      Subject
      DRNTU::Engineering::Computer science and engineering::Software
      Type
      Journal Article
      Series/Journal Title
      IEEE transactions on software engineering
      Collections
      • SCSE Journal Articles
      http://dx.doi.org/10.1109/TSE.2012.82
      Get published version (via Digital Object Identifier)

      Show full item record


      NTU Library, Nanyang Avenue, Singapore 639798 © 2011 Nanyang Technological University. All rights reserved.
      DSpace software copyright © 2002-2015  DuraSpace
      Contact Us | Send Feedback
      Share |    
      Theme by 
      Atmire NV
       

       


      NTU Library, Nanyang Avenue, Singapore 639798 © 2011 Nanyang Technological University. All rights reserved.
      DSpace software copyright © 2002-2015  DuraSpace
      Contact Us | Send Feedback
      Share |    
      Theme by 
      Atmire NV
       

       

      DCSIMG