{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:03Z","timestamp":1751660523332,"version":"3.41.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["389792660 TRR 248--CPEC"],"award-info":[{"award-number":["389792660 TRR 248--CPEC"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["610150 ERC Synergy Grant ImPACT"],"award-info":[{"award-number":["610150 ERC Synergy Grant ImPACT"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads. Our main result shows that context-bounded fair termination is decidable for the model; context-bounded implies that each spawned thread can be context switched a fixed constant number of times. Our proof is technical, since fair termination requires reasoning about the composition of unboundedly many threads each with unboundedly large stacks. In fact, techniques for related problems, which depend crucially on replacing the pushdown threads with finite-state threads, are not applicable. Instead, we introduce an extension of vector addition systems with states (VASS), called VASS with balloons (VASSB), as an intermediate model; it is an infinite-state model of independent interest. A VASSB allows tokens that are themselves markings (balloons). We show that context bounded fair termination reduces to fair termination for VASSB. We show the latter problem is decidable by showing a series of reductions: from fair termination to configuration reachability for VASSB and thence to the reachability problem for VASS. For a lower bound, fair termination is known to be non-elementary already in the special case where threads run to completion (no context switches).<\/jats:p>\n          <jats:p>We also show that the simpler problem of context-bounded termination is 2EXPSPACE-complete, matching the complexity bound---and indeed the techniques---for safety verification. Additionally, we show the related problem of fair starvation, which checks if some thread can be starved along a fair run, is also decidable in the context-bounded case. The decidability employs an intricate reduction from fair starvation to fair termination. Like fair termination, this problem is also non-elementary.<\/jats:p>","DOI":"10.1145\/3434325","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Context-bounded verification of liveness properties for multithreaded shared-memory programs"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9371-0807","authenticated-orcid":false,"given":"Pascal","family":"Baumann","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9926-0931","authenticated-orcid":false,"given":"Ramanathan S.","family":"Thinniyam","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_2_1_2_1","volume-title":"Apt and Ernst-R\u00fcdiger Olderog","author":"Krzysztof","year":"1991","unstructured":"Krzysztof R. Apt and Ernst-R\u00fcdiger Olderog . 1991 . Verification of Sequential and Concurrent Programs. Springer-Verlag . Krzysztof R. Apt and Ernst-R\u00fcdiger Olderog. 1991. Verification of Sequential and Concurrent Programs. Springer-Verlag."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_19"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_13"},{"key":"e_1_2_1_5_1","first-page":"272","volume-title":"Parity Games on Bounded Phase Multi-pushdown Systems. In Networked Systems-5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings (Lecture Notes in Computer Science","volume":"10299","author":"Atig Mohamed Faouzi","year":"2017","unstructured":"Mohamed Faouzi Atig , Ahmed Bouajjani , K. Narayan Kumar , and Prakash Saivasan . 2017 . Parity Games on Bounded Phase Multi-pushdown Systems. In Networked Systems-5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings (Lecture Notes in Computer Science , Vol. 10299 ). Springer , 272 - 287 . Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. 2017. Parity Games on Bounded Phase Multi-pushdown Systems. In Networked Systems-5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings (Lecture Notes in Computer Science, Vol. 10299 ). Springer, 272-287."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_11"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(4:4)2011"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15579-1_37"},{"key":"e_1_2_1_9_1","volume-title":"47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbr\u00fccken, Germany (Virtual Conference) (LIPIcs","volume":"168","author":"Baumann Pascal","year":"2020","unstructured":"Pascal Baumann , Rupak Majumdar , Ramanathan S. Thinniyam , and Georg Zetzsche . 2020 a. The Complexity of Bounded Context Switching with Dynamic Thread Creation. In 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbr\u00fccken, Germany (Virtual Conference) (LIPIcs , Vol. 168 ). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, 111 : 1-111 : 16. Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. 2020a. The Complexity of Bounded Context Switching with Dynamic Thread Creation. In 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbr\u00fccken, Germany (Virtual Conference) (LIPIcs, Vol. 168 ). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, 111 : 1-111 : 16."},{"key":"e_1_2_1_10_1","volume-title":"Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs. arXiv","author":"Baumann Pascal","year":"2011","unstructured":"Pascal Baumann , Rupak Majumdar , Ramanathan S. Thinniyam , and Georg Zetzsche . 2020b. Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs. arXiv : 2011 .04581 Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. 2020b. Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs. arXiv: 2011.04581"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Julius Richard B\u00fcchi. 1964. Regular canonical systems. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 6 3-4 ( 1964 ) 91-111.  Julius Richard B\u00fcchi. 1964. Regular canonical systems. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 6 3-4 ( 1964 ) 91-111.","DOI":"10.1007\/BF01969548"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039622"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250771"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941487.1941509"},{"key":"e_1_2_1_15_1","unstructured":"Bruno Courcelle. 1991. On construction obstruction sets of words. EATCS 44 ( 1991 ) 178-185.  Bruno Courcelle. 1991. On construction obstruction sets of words. EATCS 44 ( 1991 ) 178-185."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3313276.3316369"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0258-3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.417"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935310"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_9"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0021-9800(69)80111-0"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"David Harel. 1986. Efective transformations on infinite trees with applications to high undecidability dominoes and fairness. J. ACM 33 ( 1986 ) 224-248.  David Harel. 1986. Efective transformations on infinite trees with applications to high undecidability dominoes and fairness. J. ACM 33 ( 1986 ) 224-248.","DOI":"10.1145\/4904.4993"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Rodney R Howell Louis E Rosier and Hsu-Chun Yen. 1991. A taxonomy of fairness and temporal logic problems for Petri nets. Theoretical Computer Science 82 2 ( 1991 ) 341-372.  Rodney R Howell Louis E Rosier and Hsu-Chun Yen. 1991. A taxonomy of fairness and temporal logic problems for Petri nets. Theoretical Computer Science 82 2 ( 1991 ) 341-372.","DOI":"10.1016\/0304-3975(91)90228-T"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Petr Jan\u010dar. 1990. Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science 74 1 ( 1990 ) 71-93.  Petr Jan\u010dar. 1990. Decidability of a temporal logic problem for Petri nets. Theoretical Computer Science 74 1 ( 1990 ) 71-93.","DOI":"10.1016\/0304-3975(90)90006-4"},{"key":"e_1_2_1_27_1","first-page":"181","article-title":"Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs","author":"Kahlon Vineet","year":"2008","unstructured":"Vineet Kahlon . 2008 . Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs . IEEE Computer Society , 181 - 192 . Vineet Kahlon. 2008. Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs. IEEE Computer Society, 181-192.","journal-title":"IEEE Computer Society"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802201"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385980"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_2_1_31_1","volume-title":"Reps","author":"Lal Akash","year":"2008","unstructured":"Akash Lal , Tayssir Touili , Nicholas Kidd , and Thomas W . Reps . 2008 . Interprocedural Analysis of Concurrent Programs Under a Context Bound. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science, Vol. 4963 ). Springer , 282-298. Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas W. Reps. 2008. Interprocedural Analysis of Concurrent Programs Under a Context Bound. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings (Lecture Notes in Computer Science, Vol. 4963 ). Springer, 282-298."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_26"},{"key":"e_1_2_1_33_1","volume-title":"Third International Andrei Ershov Memorial Conference, PSI'99","author":"Irina","year":"1999","unstructured":"Irina A. Lomazova and Philippe Schnoebelen. 1999. Some Decidability Results for Nested Petri Nets. In Perspectives of System Informatics , Third International Andrei Ershov Memorial Conference, PSI'99 , Akademgorodok, Novosibirsk, Russia , July 6-9, 1999 , Proceedings (Lecture Notes in Computer Science, Vol. 1755 ). Springer, 208-220. Irina A. Lomazova and Philippe Schnoebelen. 1999. Some Decidability Results for Nested Petri Nets. In Perspectives of System Informatics, Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6-9, 1999, Proceedings (Lecture Notes in Computer Science, Vol. 1755 ). Springer, 208-220."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/800076.802477"},{"key":"e_1_2_1_35_1","first-page":"424","volume-title":"VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings (Lecture Notes in Computer Science","volume":"10145","author":"Muscholl Anca","year":"2017","unstructured":"Anca Muscholl , Helmut Seidl , and Igor Walukiewicz . 2017 . Reachability for Dynamic Parametric Processes. In Verification, Model Checking, and Abstract Interpretation-18th International Conference , VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings (Lecture Notes in Computer Science , Vol. 10145 ). Springer , 424 - 441 . Anca Muscholl, Helmut Seidl, and Igor Walukiewicz. 2017. Reachability for Dynamic Parametric Processes. In Verification, Model Checking, and Abstract Interpretation-18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings (Lecture Notes in Computer Science, Vol. 10145 ). Springer, 424-441."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Charles Rackof. 1978. The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6 2 ( 1978 ) 223-231.  Charles Rackof. 1978. The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6 2 ( 1978 ) 223-231.","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Ganesan Ramalingam. 2000. Context-sensitive synchronization-sensitive analysis is undecidable. ACM TOPLAS 22(2) ( 2000 ) 416-430.  Ganesan Ramalingam. 2000. Context-sensitive synchronization-sensitive analysis is undecidable. ACM TOPLAS 22(2) ( 2000 ) 416-430.","DOI":"10.1145\/349214.349241"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054116400074"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Moshe Y. Vardi. 1991. Verification of concurrent programs-the automata-theoretic framework. Annals of Pure and Applied Logic 51 ( 1991 ) 79-98.  Moshe Y. Vardi. 1991. Verification of concurrent programs-the automata-theoretic framework. Annals of Pure and Applied Logic 51 ( 1991 ) 79-98.","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"e_1_2_1_45_1","volume-title":"Karp-Miller Trees for a Branching Extension of VASS. Discrete Mathematics & Theoretical Computer Science","author":"Verma Kumar Neeraj","year":"2005","unstructured":"Kumar Neeraj Verma and Jean Goubault-Larrecq . 2005. Karp-Miller Trees for a Branching Extension of VASS. Discrete Mathematics & Theoretical Computer Science Vol. 7 ( 2005 ). Kumar Neeraj Verma and Jean Goubault-Larrecq. 2005. Karp-Miller Trees for a Branching Extension of VASS. Discrete Mathematics & Theoretical Computer Science Vol. 7 ( 2005 )."},{"key":"e_1_2_1_46_1","volume-title":"Silent Transitions in Automata with Storage. ( 2013 ). arXiv:1302.3798 Full version of an article in Proceedings of ICALP","author":"Zetzsche Georg","year":"2013","unstructured":"Georg Zetzsche . 2013. Silent Transitions in Automata with Storage. ( 2013 ). arXiv:1302.3798 Full version of an article in Proceedings of ICALP 2013 . Georg Zetzsche. 2013. Silent Transitions in Automata with Storage. ( 2013 ). arXiv:1302.3798 Full version of an article in Proceedings of ICALP 2013."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434325","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434325","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:47Z","timestamp":1750195907000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434325"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434325"],"URL":"https:\/\/doi.org\/10.1145\/3434325","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}