logo

SCIENCE CHINA Information Sciences, Volume 61, Issue 1: 012103(2018) https://doi.org/10.1007/s11432-016-9062-x

Decidability of linearizabilities for relaxed data structures

Chao WANG1,2,*, Yi LV1,2, Peng WU1,2
More info
  • ReceivedNov 21, 2016
  • AcceptedMar 31, 2017
  • PublishedSep 1, 2017

Abstract

Many recent implementations of concurrent data structures relaxed theirlinearizability 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.


Acknowledgment

This work was partially supported by National Natural Science Foundation of China (Grants Nos. 61672504, 60721061, 60833001, 61572478, 61672503, 61100069, 61161130530) and National Basic Research Program of China (973 Program) (Grant No. 2014CB340700).


References

[1] Haas A, Lippautz M, Henzinger T A, et al. Distributed queues in shared memory: multicore performance and scalability through quantitative relaxation. In: Proceedings of Computing Frontiers Conference, Ischia, 2013. 1--9. Google Scholar

[2] Kirsch C M, Lippautz M, Payer H. Fast and scalable, lock-free k-fifo queues. In: Proceedings of the 12th International Conference on Parallel Computing Technologies, St. Petersburg, 2013. 208--223. Google Scholar

[3] Kirsch C M, Payer H, Rock H, et al. Performance, scalability, and semantics of concurrent FIFO queues. In: Proceedings of the 12th International Conference on Algorithms and Architectures for Parallel Processing, Fukuoka, 2012. 273--287. Google Scholar

[4] Wimmer M, Versaci F, Traff J L, et al. Data structures for task-based priority scheduling. In: Proceedings of ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Orlando, 2014. 379--380. Google Scholar

[5] Herlihy M P, Wing J M. Linearizability: a correctness condition for concurrent objects. ACM Trans Program Lang Syst, 1990, 12: 463--492. Google Scholar

[6] Afek Y, Korland G, Yanovsky E. Quasi-linearizability: relaxed consistency for improved concurrency. In: Proceedings of the 14th International Conference on Principles of Distributed Systems, Tozeur, 2010. 395--410. Google Scholar

[7] Henzinger T A, Kirsch C M, Payer H, et al. Quantitative relaxation of concurrent data structures. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Rome, 2013. 317--328. Google Scholar

[8] Wang C, Lv Y, Wu P. Decomposable relaxation for concurrent data structures. In: Proceedings of the 43th International Conference on Current Trends in Theory and Practice of Computer Science. Berlin: Springer-Verlag, 2017. 188--202. Google Scholar

[9] Alur R, McMillan K, Peled D. Model-checking of correctness conditions for concurrent objects. Inf Comput, 2000, 160: 167--188. Google Scholar

[10] Bouajjani A, Emmi M, Enea C, et al. Verifying concurrent programs against sequential specifications. In: Proceedings of the 22nd European Conference on Programming Languages and Systems. Berlin: Springer, 2013. 290--309. Google Scholar

[11] Wang C, Lv Y, Liu G, et al. Quasi-linearizability is undecidable. In: Proceedings of the 13th Asian Symposium on Programming Languages and Systems. Berlin: Springer, 2015. 369--386. Google Scholar

[12] Adhikari K, Street J, Wang C, et al. Verifying a quantitative relaxation of linearizability via refinement. In: Proceedings of the 20th International Symposium on Model Checking Software, New York, 2013. 24--42. Google Scholar

[13] Zhang L, Chattopadhyay A, Wang C. Round-up: runtime checking quasi linearizability of concurrent data structures. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering, Silicon Valley, 2013. 4--14. Google Scholar

[14] Bouajjani A, Emmi M, Enea C, et al. Tractable refinement checking for concurrent objects. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, 2015. 651--662. Google Scholar

[15] Cerny P, Radhakrishna A, Zufferey D, et al. Model checking of linearizability of concurrent list implementations. In: Proceedings of the 22nd International Conference on Computer Aided Verification. Berlin: Springer, 2010. 465--479. Google Scholar

[16] Wang C, Lv Y, Wu P. Bounded TSO-to-SC linearizability is decidable. In: Proceedings of the 42th International Conference on Current Trends in Theory and Practice of Computer Science. Berlin: Springer-Verlag, 2016. 404--417. Google Scholar

[17] Hamza J. On the complexity of linearizability. In: Proceedings of the International Conference on NETworkedked sYStems, Agadir, 2015. 308--321. Google Scholar

[18] Burckhardt S, Dern C, Musuvathi M, et al. Line-up: a complete and automatic linearizability checker. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, Toronto, 2010. 330--340. Google Scholar

[19] Liu Y, Chen W, Liu Y A, et al. Verifying linearizability via optimized refinement checking. IEEE Trans Softw Eng, 2013, 39: 1018--1039. Google Scholar

[20] Amit D, Rinetzky N, Reps T, et al. Comparison under abstraction for verifying linearizability. In: Proceedings of the 19th International Conference on Computer Aided Verification, Berlin, 2007. 477--490. Google Scholar

[21] Berdine J, Lev-Ami T, Manevich R, et al. Thread quantification for concurrent shape analysis. In: Proceedings of the 20th International Conference on Computer Aided Verification, Princeton, 2008. 399--413. Google Scholar

[22] Vafeiadis V. Automatically proving linearizability. In: Proceedings of the 22nd International Conference on Computer Aided Verification. Berlin: Springer, 2010. 450--464. Google Scholar

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有

京ICP备18024590号-1