{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T12:23:04Z","timestamp":1771244584684,"version":"3.50.1"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62002298, 62372439, 62032019, 62002332, 62372386"],"award-info":[{"award-number":["62002298, 62372439, 62032019, 62002332, 62372386"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Beijing Natural Science Foundation","award":["F251021 and 4232038"],"award-info":[{"award-number":["F251021 and 4232038"]}]},{"DOI":"10.13039\/501100012226","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"crossref","award":["SWU019036"],"award-info":[{"award-number":["SWU019036"]}],"id":[{"id":"10.13039\/501100012226","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Capacity Development Grant of Southwest University","award":["SWU116007"],"award-info":[{"award-number":["SWU116007"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2026,3,31]]},"abstract":"<jats:p>\n                    In this article, we consider a special class of liveness properties for systems consisting of concurrent objects. These properties ensure the termination of methods calls under certain fairness assumptions and thus the progress of the execution. Liveness properties are defined for concurrent objects and they typically include\n                    <jats:italic toggle=\"yes\">lock-freedom<\/jats:italic>\n                    ,\n                    <jats:italic toggle=\"yes\">wait-freedom<\/jats:italic>\n                    ,\n                    <jats:italic toggle=\"yes\">deadlock-freedom<\/jats:italic>\n                    ,\n                    <jats:italic toggle=\"yes\">starvation-freedom,<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">obstruction-freedom<\/jats:italic>\n                    .\n                  <\/jats:p>\n                  <jats:p>\n                    It is known that these five liveness properties are decidable for\n                    <jats:italic toggle=\"yes\">sequential consistency<\/jats:italic>\n                    (SC) memory model of finite-state programs with a bounded number of processes. However, the problem of decidability of liveness for finite state concurrent programs running on relaxed memory models remains open. In this article, we address the decidability problem of liveness properties of concurrent objects for the\n                    <jats:italic toggle=\"yes\">total store order (TSO) memory<\/jats:italic>\n                    model which is used in the x86 architecture. In particular, we prove that for a bounded number of processes, lock-freedom, wait-freedom, deadlock-freedom and starvation-freedom are undecidable, and that obstruction-freedom is decidable on TSO for a bounded number of processes.\n                  <\/jats:p>\n                  <jats:p>\n                    Further on, we investigate the verification problem of\n                    <jats:italic toggle=\"yes\">\n                      <jats:italic toggle=\"yes\">k<\/jats:italic>\n                      -bounded wait-freedom\n                    <\/jats:italic>\n                    , a bounded version of wait-freedom, and show that for each bound\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    , the problem of checking\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    -bounded wait-freedom is decidable on TSO for a bounded number of processes. We show that the complexity for checking obstruction-freedom and checking\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    -bounded wait-freedom are both non-primitive recursive. We also discover an interesting difference between liveness on TSO and that on SC. Our finding is that wait-freedom implies\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    -bounded wait-freedom for some\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    on SC memory model, but this implication does not hold on the TSO model. We prove this by generating a concrete object on TSO that is wait-free but not\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    -bounded wait-free for any\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3766061","type":"journal-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T11:36:14Z","timestamp":1763811374000},"page":"1-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Decidability of Liveness on the TSO Memory Model"],"prefix":"10.1145","volume":"38","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3524-7583","authenticated-orcid":false,"given":"Chao","family":"Wang","sequence":"first","affiliation":[{"name":"Southwest University","place":["Chongqing, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3289-4574","authenticated-orcid":false,"given":"Gustavo","family":"Petri","sequence":"additional","affiliation":[{"name":"ARM research","place":["Cambridge, United Kingdom of Great Britain and Northern Ireland"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0691-990X","authenticated-orcid":false,"given":"Yi","family":"Lv","sequence":"additional","affiliation":[{"name":"Institute of Software Chinese Academy of Sciences","place":["Beijing, China"]},{"name":"University of Chinese Academy of Sciences","place":["Beijing, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9773-418X","authenticated-orcid":false,"given":"Teng","family":"Long","sequence":"additional","affiliation":[{"name":"China University of Geosciences Beijing","place":["Beijing, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-7127-7362","authenticated-orcid":false,"given":"Xinhang","family":"Song","sequence":"additional","affiliation":[{"name":"Southwest University","place":["Chongqing, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9771-3071","authenticated-orcid":false,"given":"Zhiming","family":"Liu","sequence":"additional","affiliation":[{"name":"Southwest University","place":["Chongqing, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,2,13]]},"reference":[{"key":"e_1_3_1_2_2","volume-title":"SPARC Architecture Manual - Version 8","year":"1992","unstructured":"1992. SPARC Architecture Manual - Version 8. Prentice Hall."},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67087-0_4"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8_10"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0083"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_3_1_7_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"e_1_3_1_11_2","unstructured":"Tom Shanley. 2010. \\(\\times 86\\) Instruction Set Architecture. Mindshare Press."},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10181-1_21"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33651-5_3"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45414-4_21"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102808"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/872035.872048"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/1734069"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Ori Lahav Egor Namakonov Jonas Oberhauser Anton Podkopaev and Viktor Vafeiadis. 2021. Making weak memory models fair. Proc. ACM Program. Lang. 5 OOPSLA (2021) 1\u201327. DOI:10.1145\/3485475","DOI":"10.1145\/3485475"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/361082.361093"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640106"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_17"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","unstructured":"K. C. Wang. 2017. ARM architecture and programming. In Embedded and Real-Time Operating Systems. Springer International Publishing Cham 7\u201346. DOI:10.1007\/978-3-319-51517-5_2","DOI":"10.1007\/978-3-319-51517-5_2"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1504176.1504186"},{"key":"e_1_3_1_27_2","volume-title":"Communication and Concurrency","author":"Milner Robin","year":"1989","unstructured":"Robin Milner. 1989. Communication and Concurrency. Prentice Hall."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542493"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1946-08555-9"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00290732"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(01)00337-4"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_24"},{"key":"e_1_3_1_35_2","volume-title":"Decidability of Bounded Linearizability on TSO Memory Model","author":"Wang Chao","year":"2021","unstructured":"Chao Wang, Yi Lv, Peng Wu, and Qiaowen Jia. 2021. 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. Retrieved from http:\/\/lcs.ios.ac.cn\/lvyi\/files\/ISCAS-SKLCS-21-01.pdf"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21213-0_10"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3766061","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T11:48:51Z","timestamp":1771242531000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3766061"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,13]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,3,31]]}},"alternative-id":["10.1145\/3766061"],"URL":"https:\/\/doi.org\/10.1145\/3766061","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,13]]},"assertion":[{"value":"2024-03-02","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}