{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T21:51:55Z","timestamp":1648590715440},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2018,1]]},"DOI":"10.1007\/s11432-016-9062-x","type":"journal-article","created":{"date-parts":[[2017,9,6]],"date-time":"2017-09-06T13:28:59Z","timestamp":1504704539000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Decidability of linearizabilities for relaxed data structures"],"prefix":"10.1007","volume":"61","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Lv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peng","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,1]]},"reference":[{"key":"9062_CR1","first-page":"1","volume-title":"Distributed queues in shared memory: multicore performance and scalability through quantitative relaxation","author":"A Haas","year":"2013","unstructured":"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\u20139"},{"key":"9062_CR2","first-page":"208","volume-title":"Fast and scalable, lock-free k-fifo queues","author":"C M Kirsch","year":"2013","unstructured":"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\u2013223"},{"key":"9062_CR3","first-page":"273","volume-title":"Performance, scalability, and semantics of concurrent FIFO queues","author":"C M Kirsch","year":"2012","unstructured":"Kirsch C M, Payer H, R\u00f6ck 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\u2013287"},{"key":"9062_CR4","first-page":"379","volume-title":"Data structures for task-based priority scheduling","author":"M Wimmer","year":"2014","unstructured":"Wimmer M, Versaci F, Tr\u00e4ff 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\u2013380"},{"key":"9062_CR5","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M P Herlihy","year":"1990","unstructured":"Herlihy M P, Wing J M. Linearizability: a correctness condition for concurrent objects. ACM Trans Program Lang Syst, 1990, 12: 463\u2013492","journal-title":"ACM Trans Program Lang Syst"},{"key":"9062_CR6","first-page":"395","volume-title":"Quasi-linearizability: relaxed consistency for improved concurrency","author":"Y Afek","year":"2010","unstructured":"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\u2013410"},{"key":"9062_CR7","first-page":"317","volume-title":"Quantitative relaxation of concurrent data structures","author":"T A Henzinger","year":"2013","unstructured":"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\u2013328"},{"key":"9062_CR8","first-page":"188","volume-title":"Proceedings of the 43th International Conference on Current Trends in Theory and Practice of Computer Science","author":"C Wang","year":"2017","unstructured":"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\u2013202"},{"key":"9062_CR9","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1999.2847","volume":"160","author":"R Alur","year":"2000","unstructured":"Alur R, McMillan K, Peled D. Model-checking of correctness conditions for concurrent objects. Inf Comput, 2000, 160: 167\u2013188","journal-title":"Inf Comput"},{"key":"9062_CR10","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-37036-6_17","volume-title":"Proceedings of the 22nd European Conference on Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"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\u2013309"},{"key":"9062_CR11","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-319-26529-2_20","volume-title":"Proceedings of the 13th Asian Symposium on Programming Languages and Systems","author":"C Wang","year":"2015","unstructured":"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\u2013386"},{"key":"9062_CR12","first-page":"24","volume-title":"Verifying a quantitative relaxation of linearizability via refinement","author":"K Adhikari","year":"2013","unstructured":"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\u201342"},{"key":"9062_CR13","first-page":"4","volume-title":"Round-up: runtime checking quasi linearizability of concurrent data structures","author":"L Zhang","year":"2013","unstructured":"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\u201314"},{"key":"9062_CR14","first-page":"651","volume-title":"Tractable refinement checking for concurrent objects","author":"A Bouajjani","year":"2015","unstructured":"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\u2013662"},{"key":"9062_CR15","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-642-14295-6_41","volume-title":"Proceedings of the 22nd International Conference on Computer Aided Verification","author":"P Cern\u00fd","year":"2010","unstructured":"Cern\u00fd 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\u2013479"},{"key":"9062_CR16","first-page":"404","volume-title":"Proceedings of the 42th International Conference on Current Trends in Theory and Practice of Computer Science","author":"C Wang","year":"2016","unstructured":"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\u2013417"},{"key":"9062_CR17","first-page":"308","volume-title":"On the complexity of linearizability","author":"J Hamza","year":"2015","unstructured":"Hamza J. On the complexity of linearizability. In: Proceedings of the International Conference on NETworkedked sYStems, Agadir, 2015. 308\u2013321"},{"key":"9062_CR18","first-page":"330","volume-title":"Line-up: a complete and automatic linearizability checker","author":"S Burckhardt","year":"2010","unstructured":"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\u2013340"},{"key":"9062_CR19","doi-asserted-by":"publisher","first-page":"1018","DOI":"10.1109\/TSE.2012.82","volume":"39","author":"Y Liu","year":"2013","unstructured":"Liu Y, Chen W, Liu Y A, et al. Verifying linearizability via optimized refinement checking. IEEE Trans Softw Eng, 2013, 39: 1018\u20131039","journal-title":"IEEE Trans Softw Eng"},{"key":"9062_CR20","first-page":"477","volume-title":"Comparison under abstraction for verifying linearizability","author":"D Amit","year":"2007","unstructured":"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\u2013490"},{"key":"9062_CR21","first-page":"399","volume-title":"Thread quantification for concurrent shape analysis","author":"J Berdine","year":"2008","unstructured":"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\u2013413"},{"key":"9062_CR22","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-642-14295-6_40","volume-title":"Proceedings of the 22nd International Conference on Computer Aided Verification","author":"V Vafeiadis","year":"2010","unstructured":"Vafeiadis V. Automatically proving linearizability. In: Proceedings of the 22nd International Conference on Computer Aided Verification. Berlin: Springer, 2010. 450\u2013464"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-016-9062-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-9062-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-9062-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T19:53:35Z","timestamp":1552679615000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-016-9062-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,1]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["9062"],"URL":"https:\/\/doi.org\/10.1007\/s11432-016-9062-x","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,1]]},"assertion":[{"value":"21 November 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 February 2017","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 March 2017","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 September 2017","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"012103"}}