{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:34:22Z","timestamp":1784241262889,"version":"3.55.0"},"reference-count":79,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100014086","name":"Fondation Sciences Math\u00e9matiques de Paris","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100014086","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-09-SEGI-016"],"award-info":[{"award-number":["ANR-09-SEGI-016"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:p>We propose a general formal model of isolated hierarchical parallel computations, and identify several fragments to match the concurrency constructs present in real-world programming languages such as Cilk and X10. By associating fundamental formal models (vector addition systems with recursive transitions) to each fragment, we provide a common platform for exposing the relative difficulties of algorithmic reasoning. For each case we measure the complexity of deciding state reachability for finite-data recursive programs, and propose algorithms for the decidable cases. The complexities which include PTIME, NP, EXPSPACE, and 2EXPTIME contrast with undecidable state reachability for recursive multithreaded programs.<\/jats:p>","DOI":"10.1145\/2518188","type":"journal-article","created":{"date-parts":[[2013,11,12]],"date-time":"2013-11-12T15:29:09Z","timestamp":1384270149000},"page":"1-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Analysis of Recursively Parallel Programs"],"prefix":"10.1145","volume":"35","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[{"name":"LIAFA, Universit\u00e9 Paris Diderot"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Emmi","sequence":"additional","affiliation":[{"name":"LIAFA, Universit\u00e9 Paris Diderot"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788796"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229428.1229471"},{"key":"e_1_2_1_3_1","volume-title":"Sun Microsystems","author":"Allen E.","unstructured":"Allen, E., Chase, D., Luchangco, V., Maessen, J.-W., Ryu, S., Steele Jr., G. L., and Tobin-Hochstadt, S. 2006. The fortress language specification. Tech. rep., Sun Microsystems, Inc."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201908)","volume":"2","author":"Atig M. F.","unstructured":"Atig, M. F., Bouajjani, A., and Touili, T. 2008. Analyzing asynchronous programs with preemption. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201908). Leibniz International Proceedings in Informatics, vol. 2, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 37--48."},{"key":"e_1_2_1_6_1","first-page":"4","article-title":"Context-bounded analysis for concurrent programs with dynamic creation of threads","volume":"7","author":"Atig M. F.","year":"2011","unstructured":"Atig, M. F., Bouajjani, A., and Qadeer, S. 2011. Context-bounded analysis for concurrent programs with dynamic creation of threads. Logic. Methods Comput. Sci. 7, 4.","journal-title":"Logic. Methods Comput. Sci."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694462"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_11"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_36"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869515"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1177\/1094342007078442"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094852"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328460"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Clarke E. M. and Emerson E. A. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs Lecture Notes in Computer Science vol. 131 Springer 52--71.","DOI":"10.5555\/648063.747438"},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Clarke E. M. Grumberg O. and Peled D. 2001. Model Checking. MIT Press.","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 2nd International Symposium on Programming. 106--130","author":"Cousot P.","unstructured":"Cousot, P. and Cousot, R. 1976. Static determination of dynamic properties of programs. In Proceedings of the 2nd International Symposium on Programming. 106--130."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694620"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201909)","volume":"4","author":"Demri S.","unstructured":"Demri, S., Jurdzinski, M., Lachish, O., and Lazic, R. 2009. The covering and boundedness problems for branching vector addition systems. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201909). Leibniz International Proceedings in Informatics Series, vol. 4, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 181--192."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393652"},{"key":"e_1_2_1_23_1","first-page":"244","article-title":"Decidability issues for Petri nets - A survey","volume":"52","author":"Esparza J.","year":"1994","unstructured":"Esparza, J. and Nielsen, M. 1994. Decidability issues for Petri nets - A survey. Bull. Euro. Assoc. Theor. Comput. Sci. 52, 244--262.","journal-title":"Bull. Euro. Assoc. Theor. Comput. Sci."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325697"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926443"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00139-1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1188455.1188543"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003329"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1767111.1767125"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480895"},{"key":"e_1_2_1_33_1","volume-title":"-F","author":"Geeraerts G.","year":"2012","unstructured":"Geeraerts, G., Heu\u00dfner, A., and Raskin, J.-F. 2012. Queue-dispatch asynchronous systems. CoRR abs\/1201.4871. http:\/\/www.swt-bamberg.de\/aheussner\/files\/heussner-a-2013--a.pdf."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.001"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733618"},{"key":"e_1_2_1_37_1","unstructured":"Gray J. 1985. Why do computers stop and what can be about it? http:\/\/www.hpl.hp.com\/techreports\/tandem\/TR-85.7.pdf."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926424"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/4472.4478"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_27"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190266"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.45"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229545"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802201"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.16"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_54"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Larus J. R. and Rajwar R. 2006. Transactional Memory. Morgan & Claypool. http:\/\/www.morganclaypool.com\/doi\/abs\/10.2200\/S00070ED1V01Y200611CAC002.","DOI":"10.1007\/978-3-031-01719-3_3"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.180"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1693453.1693459"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640106"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926421"},{"key":"e_1_2_1_55_1","volume-title":"The reachability problem requires exponential space. Tech. rep. 62","author":"Lipton R. J.","unstructured":"Lipton, R. J. 1976. The reachability problem requires exponential space. Tech. rep. 62, Yale University."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/800076.802477"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Nielson F. Nielson H. R. and Hankin C. 1999. Principles of program analysis. Springer.","DOI":"10.5555\/555142"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_60_1","volume-title":"Computational Complexity","author":"Papadimitriou C. H.","unstructured":"Papadimitriou, C. H. 1993. Computational Complexity. Addison Wesley."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1988915.1988918"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996845"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/647325.721668"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","unstructured":"Randall K. H. 1998. Cilk: Efficient multithreaded computing. Ph.D. thesis Department of Electrical Engineering and Computer Science Massachusetts Institute of Technology.","DOI":"10.5555\/928053"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the 1st International Workshop on Future Architectural Support for Parallel Programming.","author":"Segulja C.","unstructured":"Segulja, C. and Abdelrahman, T. S. 2011. Synchronization-free and deterministic coarse-grain parallelism: Architectural support and programming model. In Proceedings of the 1st International Workshop on Future Architectural Support for Parallel Programming."},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/645394.651904"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_94"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_29"},{"key":"e_1_2_1_75_1","first-page":"189","article-title":"Two approaches to interprocedural data-flow analysis. In Program Flow Analysis: Theory and Applications, S. S. Muchnick and N. D. Jones Eds., Prentice-Hall","volume":"7","author":"Sharir M.","year":"1981","unstructured":"Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data-flow analysis. In Program Flow Analysis: Theory and Applications, S. S. Muchnick and N. D. Jones Eds., Prentice-Hall, Chapter 7, 189--234.","journal-title":"Chapter"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.5555\/524279"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263928"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.46298\/dmtcs.350"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2518188","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2518188","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:13Z","timestamp":1750277653000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2518188"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":79,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1145\/2518188"],"URL":"https:\/\/doi.org\/10.1145\/2518188","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,11]]},"assertion":[{"value":"2012-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}