Verifying a quantitative relaxation of linearizability via refinement

作     者：Adhikari, Kiran Street, James Wang, Chao Liu, Yang Zhang, Shaojie 

作者机构：Virginia Tech Blacksburg VA 24061 USA Nanyang Technol Univ Singapore Singapore Singapore Univ Technol & Design Singapore Singapore 

出 版 物：《INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER》 (国际技术传输软件工具杂志)

年 卷 期：2016年第18卷第4期

页      面：393-407页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：National Science Foundation  NSF  (CCF-1149454  CCF-1149454) 

主　　题：Linearizability Model checking Concurrent data structure Refinement Quantitative relaxation 

摘      要：The recent years have seen increasingly widespread use of highly concurrent data structures in both multi-core and distributed computing environments, thereby escalating the priority for verifying their correctness. Quasi linearizability is a quantitative variation of the standard linearizability correctness condition to allow more implementation freedom for performance optimization. However, ensuring that the implementation satisfies the quantitative aspect of this new correctness condition is often an arduous task. In this paper, we propose the first automated method for formally verifying quasi linearizability of the implementation model of a concurrent data structure with respect to its sequential specification. The method is based on checking a relaxed version of the refinement relation between the implementation model and the specification model through explicit state model checking. Our method can directly handle concurrent systems where each thread or process makes infinitely many method calls. Furthermore, unlike many existing verification methods, it does not require the user to supply annotations of the linearization points. We have implemented the new method in the PAT verification framework. Our experimental evaluation shows that the method is effective in verifying the new quasi linearizability requirement and detecting violations.