{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:26:21Z","timestamp":1740108381448,"version":"3.37.3"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2017,10,23]],"date-time":"2017-10-23T00:00:00Z","timestamp":1508716800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["No.60721061","No.60833001"],"award-info":[{"award-number":["No.60721061","No.60833001"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["No.61672504","No.61572478"],"award-info":[{"award-number":["No.61672504","No.61572478"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["No.61672503","No.61100069"],"award-info":[{"award-number":["No.61672503","No.61100069"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["No.61161130530"],"award-info":[{"award-number":["No.61161130530"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Key Basic Research Program of China","award":["No.2014CB340701"],"award-info":[{"award-number":["No.2014CB340701"]}]},{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"crossref","award":["No.2017YFB0801900"],"award-info":[{"award-number":["No.2017YFB0801900"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s00236-017-0305-6","type":"journal-article","created":{"date-parts":[[2017,10,23]],"date-time":"2017-10-23T22:36:02Z","timestamp":1508798162000},"page":"649-668","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["TSO-to-TSO linearizability is undecidable"],"prefix":"10.1007","volume":"55","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0691-990X","authenticated-orcid":false,"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,10,23]]},"reference":[{"key":"305_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. In: LICS 1996, pp. 219\u2013228. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561322"},{"key":"305_CR2","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Hermenegildo, M.V., Palsberg, J. (eds.) POPL 2010, pp. 7\u201318. ACM (2010)","DOI":"10.1145\/1706299.1706303"},{"key":"305_CR3","doi-asserted-by":"crossref","unstructured":"Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C\/C++ concurrency. In: Giacobazzi, R., Cousot, R. (eds.) POPL 2013, pp. 235\u2013248. ACM (2013)","DOI":"10.1145\/2429069.2429099"},{"key":"305_CR4","volume-title":"Understanding the Linux Kernel","author":"D Bovet","year":"2005","unstructured":"Bovet, D., Cesati, M.: Understanding the Linux Kernel, 3rd edn. O\u2019Reilly, Sebastopol (2005)","edition":"3"},{"key":"305_CR5","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Ball, T., Sagiv, M. (eds.) POPL 2011, pp. 55\u201366. ACM (2011)","DOI":"10.1145\/1926385.1926394"},{"key":"305_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013, pp. 290\u2013309. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_17"},{"key":"305_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: Rajamani, S.K., Walker, D. (eds.) POPL 2015, pp. 651\u2013662. ACM (2015)","DOI":"10.1145\/2676726.2677002"},{"key":"305_CR8","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (eds.) ESOP 2012, pp. 87\u2013107. Springer (2012)","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"305_CR9","doi-asserted-by":"crossref","unstructured":"Derrick, J., Smith, G., Groves, L., Dongol, B.: Using coarse-grained abstractions to verify linearizability on TSO. In: Yahav, E. (eds.) HVC 2014, pp. 1\u201316. Springer (2014)","DOI":"10.1007\/978-3-319-13338-6_1"},{"key":"305_CR10","doi-asserted-by":"crossref","unstructured":"Derrick, J., Smith, G., Dongol, B.: Verifying linearizability on TSO architectures. In: Albert, E., Sekerinski, E. (eds.) IFM 2014, pp. 341\u2013356. Springer (2014)","DOI":"10.1007\/978-3-319-10181-1_21"},{"key":"305_CR11","doi-asserted-by":"crossref","unstructured":"Filipovic, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. In: Castagna, G. (eds.) ESOP 2009, pp. 252\u2013266. Springer (2009)","DOI":"10.1007\/978-3-642-00590-9_19"},{"key":"305_CR12","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (eds.) DISC 2012, pp. 31\u201345. Springer (2012)","DOI":"10.1007\/978-3-642-33651-5_3"},{"issue":"3","key":"305_CR13","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"9","key":"305_CR14","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess program. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"issue":"7","key":"305_CR15","doi-asserted-by":"crossref","first-page":"1018","DOI":"10.1109\/TSE.2012.82","volume":"39","author":"Y Liu","year":"2013","unstructured":"Liu, Y., Chen, W., Liu, Y.A., Sun, J., Zhang, S.J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE Trans. Softw. Eng. 39(7), 1018\u20131039 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"305_CR16","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Palsberg, J., Abadi, M. (eds.) POPL 2005, pp. 378\u2013391. ACM (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"305_CR17","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009, pp. 391\u2013407. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"305_CR18","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Hall, M. W., Padua, D.A. (eds.) PLDI 2011, pp. 175\u2013186. ACM (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"305_CR19","doi-asserted-by":"crossref","unstructured":"Schnoebelen, P.: Bisimulation and other undecidable equivalences for lossy channel systems. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001, pp. 385\u2013399. Springer (2001)","DOI":"10.1007\/3-540-45500-0_19"},{"key":"305_CR20","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: Pasareanu, C.S. (ed.) SPIN 2009, pp. 261\u2013278. Springer (2009)","DOI":"10.1007\/978-3-642-02652-2_21"},{"key":"305_CR21","doi-asserted-by":"crossref","unstructured":"Wang, C., Lv, Y., Wu, P.: Bounded TSO-to-SC linearizability is decidable. In: Freivalds, M.R., Engels, G., Catania, B. (eds.) SOFSEM 2016, pp. 404\u2013417. Springer (2016)","DOI":"10.1007\/978-3-662-49192-8_33"},{"key":"305_CR22","doi-asserted-by":"crossref","unstructured":"Wang, C., Lv, Y., Wu, P.: TSO-to-TSO linearizability is undecidable. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015, pp. 309\u2013325. Springer (2015)","DOI":"10.1007\/978-3-319-24953-7_24"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-017-0305-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0305-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0305-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,18]],"date-time":"2020-05-18T11:27:44Z","timestamp":1589801264000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-017-0305-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,23]]},"references-count":22,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["305"],"URL":"https:\/\/doi.org\/10.1007\/s00236-017-0305-6","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2017,10,23]]}}}