{"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":1771046019905,"version":"3.50.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031212123","type":"print"},{"value":"9783031212130","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-21213-0_10","type":"book-chapter","created":{"date-parts":[[2022,12,10]],"date-time":"2022-12-10T06:08:19Z","timestamp":1670652499000},"page":"149-165","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Decidability of\u00a0Liveness for\u00a0Concurrent Objects on\u00a0the\u00a0TSO Memory Model"],"prefix":"10.1007","author":[{"given":"Chao","family":"Wang","sequence":"first","affiliation":[]},{"given":"Gustavo","family":"Petri","sequence":"additional","affiliation":[]},{"given":"Yi","family":"Lv","sequence":"additional","affiliation":[]},{"given":"Teng","family":"Long","sequence":"additional","affiliation":[]},{"given":"Zhiming","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,11]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-030-67087-0_4","volume-title":"Networked Systems","author":"PA Abdulla","year":"2021","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Derevenetc, E., Leonardsson, C., Meyer, R.: On the state reachability problem for concurrent programs under power. In: Georgiou, C., Majumdar, R. (eds.) NETYS 2020. LNCS, vol. 12129, pp. 47\u201359. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67087-0_4"},{"issue":"1","key":"10_CR2","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1006\/inco.1996.0083","volume":"130","author":"PA Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Inf. Comput. 130(1), 71\u201390 (1996)","journal-title":"Inf. Comput."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Manuel, V., Hermenegildo., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17\u201323 January 2010, pp. 7\u201318. ACM (2010)","DOI":"10.1145\/1706299.1706303"},{"key":"10_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.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26\u201328 January 2011, pp. 55\u201366. ACM (2011)","DOI":"10.1145\/1925844.1926394"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-642-37036-6_29","volume-title":"Programming Languages and Systems","author":"A Bouajjani","year":"2013","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533\u2013553. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29"},{"key":"10_CR6","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.) ESOP 2012. LNCS, vol. 7211, pp. 87\u2013107. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_5"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"10_CR8","unstructured":"Intel Corporation. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual (2021)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-319-10181-1_21","volume-title":"Integrated Formal Methods","author":"J Derrick","year":"2014","unstructured":"Derrick, J., Smith, G., Dongol, B.: Verifying linearizability on TSO architectures. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 341\u2013356. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_21"},{"key":"10_CR10","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). https:\/\/doi.org\/10.1007\/978-3-642-33651-5_3"},{"key":"10_CR11","unstructured":"Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann (2008)"},{"key":"10_CR12","unstructured":"Lahav, O., Namakonov, E., Oberhauser, J., Podkopaev, A., Viktor, V.: Making weak memory models fair. CoRR, arXiv preprint arXiv2012.01067 (2020)"},{"issue":"9","key":"10_CR13","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 programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Leijen, D., Schulte, W., Sebastian, B.: The design of a task parallel library. In: Arora, Shail., Leavens, G.T. (eds.) Proceedings of the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009, 25\u201329 October 2009, Orlando, Florida, USA, pp. 227\u2013242. ACM (2009)","DOI":"10.1145\/1640089.1640106"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-40184-8_17","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"H Liang","year":"2013","unstructured":"Liang, H., Hoffmann, J., Feng, X., Shao, Z.: Characterizing progress properties of concurrent objects via contextual refinements. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 227\u2013241. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_17"},{"key":"10_CR16","unstructured":"ARM Limited. ARM Architecture Reference Manual ARMv8 (2013)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.V.: The java memory model. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, 12\u201314 January 2005, pp. 378\u2013391. ACM (2005)","DOI":"10.1145\/1047659.1040336"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Vechev, M.T., Saraswat, V.A.: Idempotent work stealing. In: Reed, D.A., Sarkar, V. (eds.) Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2009, Raleigh, NC, USA, 14\u201318 February 2009, pp. 45\u201354. ACM (2009)","DOI":"10.1145\/1594835.1504186"},{"key":"10_CR19","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). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Petrank, E., Musuvathi, M., Steensgaard, B.: Progress guarantee for parallel programs via bounded lock-freedom. In: Hind, M., Diwan, A. (eds.) Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, 15\u201321 June 2009, pp. 144\u2013154. ACM (2009)","DOI":"10.1145\/1543135.1542493"},{"issue":"1946","key":"10_CR21","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"EL Post","year":"1946","unstructured":"Post, E.L.: A variant of a recursively unsolvable problem. Bull. Am. Math. Soc. 52(1946), 264\u2013268 (1946)","journal-title":"Bull. Am. Math. Soc."},{"key":"10_CR22","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/BF00290732","volume":"19","author":"K Ruohonen","year":"1983","unstructured":"Ruohonen, K.: On some variants of post\u2019s correspondence problem. Acta Inf. 19, 357\u2013367 (1983)","journal-title":"Acta Inf."},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-319-24953-7_24","volume-title":"Automated Technology for Verification and Analysis","author":"C Wang","year":"2015","unstructured":"Wang, C., Lv, Y., Wu, P.: TSO-to-TSO linearizability is undecidable. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 309\u2013325. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_24"},{"key":"10_CR24","unstructured":"Wang, C., Lv, Y., Wu, P., Jia., Q.: Decidability of bounded linearizability on TSO memory model. Technical Report ISCAS-SKLCS-21-01, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (2021). http:\/\/lcs.ios.ac.cn\/~lvyi\/files\/ISCAS-SKLCS-21-01.pdf"},{"key":"10_CR25","unstructured":"Wang, C., Petri, G., Lv, Y., Long, T., Liu., Z.: Decidability of liveness for concurrent objects on the TSO memory model. Technical Report ISCAS-SKLCS-22-02, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (2021). http:\/\/lcs.ios.ac.cn\/~lvyi\/files\/ISCAS-SKLCS-22-02.pdf"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-21213-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,10]],"date-time":"2022-12-10T06:14:46Z","timestamp":1670652886000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-21213-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031212123","9783031212130"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-21213-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"11 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}