Decidability of linearizabilities for relaxed data structures  

作　　者：Chao WANG Yi LV Peng WU 

机构地区：[1]State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China [2]University of Chinese Academy of Sciences, Beijing 100049, China

出　　处：《Science China(Information Sciences)》2018年第1期109-118,共10页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China (Grants Nos. 61672504, 60721061, 60833001, 61572478, 61672503, 61100069, 61161130530);National Basic Research Program of China (973 Program) (Grant No. 2014CB340700)

摘　　要：Many recent implementations of concurrent data structures relaxed their linearizability requirements for better performance and scalability. Quasi-linearizability, k-linearizability and regular-relaxed linearizability are three quantitative relaxation variants of linearizability that have been proposed as correctness conditions of relaxed data structures, yet preserving the intuition of linearizability. Quasi-linearizability has been proved undecidable. In this paper, we first show that k-linearizability is undecidable for a bounded number of processes, by reducing quasi-linearizability into it. We then show that regular-relaxed linearizability is decidable for a bounded number of processes. We also find that the number of the states of a relaxed specification is exponential to the number of the states of the underlying specification automaton（representing its relaxation strategy）, and polynomial to the number of the states of the underlying quantitative sequential specification and the number of operations.Many recent implementations of concurrent data structures relaxed their linearizability requirements for better performance and scalability. Quasi-linearizability, k-linearizability and regular-relaxed linearizability are three quantitative relaxation variants of linearizability that have been proposed as correctness conditions of relaxed data structures, yet preserving the intuition of linearizability. Quasi-linearizability has been proved undecidable. In this paper, we first show that k-linearizability is undecidable for a bounded number of processes, by reducing quasi-linearizability into it. We then show that regular-relaxed linearizability is decidable for a bounded number of processes. We also find that the number of the states of a relaxed specification is exponential to the number of the states of the underlying specification automaton（representing its relaxation strategy）, and polynomial to the number of the states of the underlying quantitative sequential specification and the number of operations.

关 键 词：concurrent data structures quantitative relaxation LINEARIZABILITY DECIDABILITY finite automata 

分 类 号：TP4[自动化与计算机技术]