{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T05:13:39Z","timestamp":1771046019980,"version":"3.50.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319249520","type":"print"},{"value":"9783319249537","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24953-7_24","type":"book-chapter","created":{"date-parts":[[2015,10,7]],"date-time":"2015-10-07T15:00:11Z","timestamp":1444230011000},"page":"309-325","source":"Crossref","is-referenced-by-count":4,"title":["TSO-to-TSO Linearizability Is Undecidable"],"prefix":"10.1007","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":[[2015,11,22]]},"reference":[{"key":"24_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":"24_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\/1707801.1706303"},{"key":"24_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\/2480359.2429099"},{"key":"24_CR4","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\/1925844.1926394"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-37036-6_17","volume-title":"Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 290\u2013309. Springer, Heidelberg (2013)"},{"key":"24_CR6","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\/2775051.2677002"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-28869-2_5","volume-title":"Programming Languages and Systems","author":"S Burckhardt","year":"2012","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 87\u2013107. Springer, Heidelberg (2012)"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-00590-9_19","volume-title":"Programming Languages and Systems","author":"I Filipovi\u0107","year":"2009","unstructured":"Filipovi\u0107, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 252\u2013266. Springer, Heidelberg (2009)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-33651-5_3","volume-title":"Distributed Computing","author":"A Gotsman","year":"2012","unstructured":"Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31\u201345. Springer, Heidelberg (2012)"},{"issue":"3","key":"24_CR10","doi-asserted-by":"publisher","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":"24_CR11","doi-asserted-by":"publisher","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":"24_CR12","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., Sun, J., Zhang, S.J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE Trans. Software Eng. 39(7), 1018\u20131039 (2013)","journal-title":"IEEE Trans. Software Eng."},{"key":"24_CR13","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\/1047659.1040336"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-642-03359-9_27","volume-title":"Theorem Proving in Higher Order Logics","author":"S Owens","year":"2009","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. LNCS, vol. 5674, pp. 391\u2013407. Springer, Heidelberg (2009)"},{"key":"24_CR15","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\/1993316.1993520"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/3-540-45500-0_19","volume-title":"Theoretical Aspects of Computer Software","author":"P Schnoebelen","year":"2001","unstructured":"Schnoebelen, P.: Bisimulation and other undecidable equivalences for lossy channel systems. In: Kobayashi, N., Babu, C.S. (eds.) TACS 2001. LNCS, vol. 2215, pp. 385\u2013399. Springer, Heidelberg (2001)"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-02652-2_21","volume-title":"Model Checking Software","author":"M Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: P\u0103s\u0103reanu, C.S. (ed.) Model Checking Software. LNCS, vol. 5578, pp. 261\u2013278. Springer, Heidelberg (2009)"},{"key":"24_CR18","unstructured":"Wang, C., Lv, Y., Wu, P.: TSO-to-TSO Linearizability is Undecidable. Technical report ISCAS-SKLCS-15-03, State Key Laboratory of Computer Science, ISCAS, CAS (2015). http:\/\/lcs.ios.ac.cn\/~lvyi\/files\/ISCAS-SKLCS-15-03.pdf"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24953-7_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T23:03:07Z","timestamp":1748646187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24953-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319249520","9783319249537"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24953-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}