{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:17:34Z","timestamp":1790813854917,"version":"4.1.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"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":"publisher","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"name":"European Research Council","award":["610150"],"award-info":[{"award-number":["610150"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>Thread pooling is a common programming idiom in which a fixed set of worker threads are maintained to execute tasks concurrently. The workers repeatedly pick tasks and execute them to completion. Each task is sequential, with possibly recursive code, and tasks communicate over shared memory. Executing a task can lead to more new tasks being spawned. We consider the safety verification problem for thread-pooled programs. We parameterize the problem with two parameters: the size of the thread pool as well as the number of context switches for each task. The size of the thread pool determines the number of workers running concurrently. The number of context switches determines how many times a worker can be swapped out while executing a single task---like many verification problems for multithreaded recursive programs, the context bounding is important for decidability.<\/jats:p>\n          <jats:p>We show that the safety verification problem for thread-pooled, context-bounded, Boolean programs is EXPSPACE-complete, even if the size of the thread pool and the context bound are given in binary. Our main result, the EXPSPACE upper bound, is derived using a sequence of new succinct encoding techniques of independent language-theoretic interest. In particular, we show a polynomial-time construction of downward closures of languages accepted by succinct pushdown automata as doubly succinct nondeterministic finite automata. While there are explicit doubly exponential lower bounds on the size of nondeterministic finite automata accepting the downward closure, our result shows these automata can be compressed. We show that thread pooling significantly reduces computational power: in contrast, if only the context bound is provided in binary, but there is no thread pooling, the safety verification problem becomes 3EXPSPACE-complete. Given the high complexity lower bounds of related problems involving binary parameters, the relatively low complexity of safety verification with thread-pooling comes as a surprise.<\/jats:p>","DOI":"10.1145\/3498678","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Context-bounded verification of thread pools"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9371-0807","authenticated-orcid":false,"given":"Pascal","family":"Baumann","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9926-0931","authenticated-orcid":false,"given":"Ramanathan S.","family":"Thinniyam","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_11"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15579-1_37"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_7"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_25"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2020.111"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434325"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ESA.2017.27"},{"key":"e_1_2_2_8_1","first-page":"178","article-title":"On constructing obstruction sets of words","volume":"44","author":"Courcelle Bruno","year":"1991","unstructured":"Bruno Courcelle . 1991 . On constructing obstruction sets of words . Bulletin of the EATCS , 44 (1991), 178 \u2013 186 . Bruno Courcelle. 1991. On constructing obstruction sets of words. Bulletin of the EATCS, 44 (1991), 178\u2013186.","journal-title":"Bulletin of the EATCS"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-65306-6_20"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_2_2_12_1","volume-title":"The mathematical theory of context free languages","author":"Ginsburg Seymour","unstructured":"Seymour Ginsburg . 1966. The mathematical theory of context free languages . McGraw Hill . Seymour Ginsburg. 1966. The mathematical theory of context free languages. McGraw Hill."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_16"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"H. Gruber M. Holzer and M. Kutrib. 2009. More on the Size of Higman-Haines Sets: Effective Constructions. Fundam. Inf. 91(1) (2009) 105\u2013121.  H. Gruber M. Holzer and M. Kutrib. 2009. More on the Size of Higman-Haines Sets: Effective Constructions. Fundam. Inf. 91(1) (2009) 105\u2013121.","DOI":"10.3233\/FI-2009-0035"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0021-9800(69)80111-0"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190266"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12200-2_10"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785796"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3190508.3190552"},{"key":"e_1_2_2_24_1","volume-title":"The reachability problem is exponential-space hard","author":"Lipton Richard","year":"1976","unstructured":"Richard Lipton . 1976. The reachability problem is exponential-space hard . Yale University , Department of Computer Science, Report, 62 ( 1976 ). Richard Lipton. 1976. The reachability problem is exponential-space hard. Yale University, Department of Computer Science, Report, 62 (1976)."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72016-2_24"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.12"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80009-2"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90006-1"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_29"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(78)90156-5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498678","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498678","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498678"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":34,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498678"],"URL":"https:\/\/doi.org\/10.1145\/3498678","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}