{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T17:50:25Z","timestamp":1718905825585},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T00:00:00Z","timestamp":1573603200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["279307"],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P23499-N23, S11407-N23, J-4220"],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"name":"\u00d6sterreichischen Akademie der Wissenschaften","award":["24956"]},{"DOI":"10.13039\/100005801","name":"Facebook","doi-asserted-by":"publisher","award":["PhD Fellowship Program"],"id":[{"id":"10.13039\/100005801","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":[[2019,12,31]]},"abstract":"\n Interprocedural analysis is at the heart of numerous applications in programming languages, such as alias analysis, constant propagation, and so on. Recursive state machines (RSMs) are standard models for interprocedural analysis. We consider a general framework with RSMs where the transitions are labeled from a semiring and path properties are algebraic with semiring operations. RSMs with algebraic path properties can model interprocedural dataflow analysis problems, the shortest path problem, the most probable path problem, and so on. The traditional algorithms for interprocedural analysis focus on path properties where the starting point is\n fixed<\/jats:italic>\n as the entry point of a specific method. In this work, we consider possible multiple queries as required in many applications such as in alias analysis. The study of multiple queries allows us to bring in an important algorithmic distinction between the resource usage of the\n one-time<\/jats:italic>\n preprocessing vs for\n each individual<\/jats:italic>\n query. The second aspect we consider is that the control flow graphs for most programs have constant treewidth.\n <\/jats:p>\n Our main contributions are simple and implementable algorithms that support multiple queries for algebraic path properties for RSMs that have constant treewidth. Our theoretical results show that our algorithms have small additional one-time preprocessing but can answer subsequent queries significantly faster as compared to the current algorithmic solutions for interprocedural dataflow analysis. We have also implemented our algorithms and evaluated their performance for performing on-demand interprocedural dataflow analysis on various domains, such as for live variable analysis and reaching definitions, on a standard benchmark set. Our experimental results align with our theoretical statements and show that after a lightweight preprocessing, on-demand queries are answered much faster than the standard existing algorithmic approaches.<\/jats:p>","DOI":"10.1145\/3363525","type":"journal-article","created":{"date-parts":[[2019,11,14]],"date-time":"2019-11-14T22:07:36Z","timestamp":1573769256000},"page":"1-46","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Faster Algorithms for Dynamic Algebraic Queries in Basic RSMs with Constant Treewidth"],"prefix":"10.1145","volume":"41","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}]},{"given":"Prateesh","family":"Goyal","sequence":"additional","affiliation":[{"name":"MIT, Cambridge MA, USA"}]},{"given":"Rasmus","family":"Ibsen-Jensen","sequence":"additional","affiliation":[{"name":"University of Liverpool, Liverpool, United Kingdom"}]},{"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2019,11,13]]},"reference":[{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"R. Alur M. Benedikt K. Etessami P. Godefroid T. W. Reps and M. Yannakakis. 2005. Analysis of recursive state machines. ACM Trans. Program. Lang. Syst. (2005).","DOI":"10.1145\/1075382.1075387"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.017"},{"key":"e_1_2_1_4_1","volume-title":"Appel and Jens Palsberg","author":"Andrew","year":"2002","unstructured":"Andrew W. Appel and Jens Palsberg. 2002. Modern Compiler Implementation in Java. Cambridge University Press."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(89)90031-0"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264319"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869517"},{"key":"e_1_2_1_8_1","volume-title":"Bender and Mart\u00edn Farach-Colton","author":"Michael","year":"2000","unstructured":"Michael A. Bender and Mart\u00edn Farach-Colton. 2000. The LCA problem revisited. In Proceedings of the Theoretical Informatics (LATIN\u201900). Springer Berlin."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0196-6774(87)90039-3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167488"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2259051.2259052"},{"key":"e_1_2_1_12_1","volume-title":"Graph-Theoretic Concepts in Computer Science","author":"Bodlaender Hans L.","unstructured":"Hans L. Bodlaender. 1994. Dynamic algorithms for graphs with treewidth 2. In Graph-Theoretic Concepts in Computer Science. Springer."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30577-4_1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539795289859"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19488-6_110"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167161"},{"key":"e_1_2_1_17_1","first-page":"1","article-title":"A tourist guide through treewidth","volume":"11","author":"Bodlaender Hans L.","year":"1993","unstructured":"Hans L. Bodlaender. 1993b. A tourist guide through treewidth. Acta Cybern. 11, 1--2 (1993), 1--21. http:\/\/cyber.bibl.u-szeged.hu\/index.php\/actcybern\/article\/view\/3417.","journal-title":"Acta Cybern."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00228-4"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24841-5_6"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/12276.13327"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297280.3297322"},{"key":"e_1_2_1_22_1","volume-title":"Amir Kafshdar Goharshady, and Andreas Pavlogiannis","author":"Chatterjee Krishnendu","year":"2017","unstructured":"Krishnendu Chatterjee, Amir Kafshdar Goharshady, and Andreas Pavlogiannis. 2017. JTDec: A tool for tree decompositions in soot. In Automated Technology for Verification and Analysis, Deepak D\u2019Souza and K. Narayan Kumar (Eds.). Springer International Publishing, Cham, 59--66."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 24th Annual European Symposium on Algorithms (ESA\u201916)","author":"Chatterjee Krishnendu","year":"2016","unstructured":"Krishnendu Chatterjee, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. 2016. Optimal reachability and a space-time tradeoff for distance queries in constant-treewidth graphs. In Proceedings of the 24th Annual European Symposium on Algorithms (ESA\u201916). 28:1--28:17."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676979"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the CAV\u201913","author":"Chatterjee K.","unstructured":"K. Chatterjee and J. Lacki. 2013. Faster algorithms for Markov decision processes with low treewidth. In Proceedings of the CAV\u201913."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676968"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.30"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328460"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s004530010016"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Tong Chen Jin Lin Xiaoru Dai Wei-Chung Hsu and Pen-Chung Yew. 2004. Data dependence profiling for speculative optimizations. In Compiler Construction Evelyn Duesterwald (Ed.). Springer Berlin 57--72.","DOI":"10.1007\/978-3-540-24723-4_5"},{"key":"e_1_2_1_31_1","volume-title":"Handbook of Model Checking","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. 2018. Handbook of Model Checking (1st ed.). Springer Publishing Company, Incorporated.","edition":"1"},{"key":"e_1_2_1_32_1","volume-title":"Engineering a Compiler","author":"Cooper Keith","unstructured":"Keith Cooper and Linda Torczon. 2011. Engineering a Compiler. Elsevier."},{"key":"e_1_2_1_33_1","unstructured":"T. H. Cormen C. E. Leiserson R. L. Rivest and C. Stein. 2001. Introduction to Algorithms. The MIT Press."},{"key":"e_1_2_1_34_1","volume-title":"Handbook of Theoretical Computer Science (Vol. B)","author":"Courcelle Brouno","unstructured":"Brouno Courcelle. 1990. Graph rewriting: An algebraic and logic approach. In Handbook of Theoretical Computer Science (Vol. B). The MIT Press, Cambridge, MA."},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the IFIP\u201977","author":"Cousot P.","year":"1977","unstructured":"P. Cousot and R Cousot. 1977. Static determination of dynamic properties of recursive procedures. In Proceedings of the IFIP\u201977, Formal Description of Programming Concepts, E. J. Neuhold (Ed.)."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01386390"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Evelyn Duesterwald Rajiv Gupta and Mary Lou Soffa. 1995. Demand-driven computation of interprocedural data flow In Proceedings of the POPL\u201995.","DOI":"10.1145\/199448.199461"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the FOCS\u201910","author":"Elberfeld M.","unstructured":"M. Elberfeld, A. Jakoby, and T. Tantau. 2010. Logspace versions of the theorems of Bodlaender and Courcelle. In Proceedings of the FOCS\u201910."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158137"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the 3rd Conference of the European Co-operation in Informatics (ECI\u201981)","author":"Giegerich Robert","year":"1981","unstructured":"Robert Giegerich, Ulrich M\u00f6ncke, and Reinhard Wilhelm. 1981. Invariance of approximate semantics with respect to program transformations. In Proceedings of the 3rd Conference of the European Co-operation in Informatics (ECI\u201981)."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155099"},{"key":"e_1_2_1_42_1","volume-title":"Algorithm Engineering and Experiments","author":"Gustedt Jens","unstructured":"Jens Gustedt, Ole A. M\u00e6hle, and Jan Arne Telle. 2002. The treewidth of Java programs. In Algorithm Engineering and Experiments. Springer."},{"key":"e_1_2_1_43_1","volume-title":"Dynamic algorithms for graphs of bounded treewidth. Algorithmica","author":"Hagerup Torben","year":"2000","unstructured":"Torben Hagerup. 2000. Dynamic algorithms for graphs of bounded treewidth. Algorithmica (2000)."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01917434"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213024"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/222132.222146"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2019.01.027"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55984-1_13"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229545"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2483699.2483707"},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the POPL\u201991","author":"Landi William","unstructured":"William Landi and Barbara G. Ryder. 1991. Pointer-induced aliasing: A problem classification. In Proceedings of the POPL\u201991. ACM."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1022969.1022970"},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the OOPSLA\u201908","author":"Nomair","unstructured":"Nomair A. Naeem and Ondrej Lhot\u00e1k. 2008. Typestate-like analysis of multiple interacting objects. In Proceedings of the OOPSLA\u201908."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_8"},{"key":"e_1_2_1_55_1","volume-title":"Principles of Program Analysis","author":"Nielson Flemming","unstructured":"Flemming Nielson, Hanne R. Nielson, and Chris Hankin. 2015. Principles of Program Analysis. Springer."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_7"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129734"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-2207-2_8"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the ILPS\u201997","author":"Reps Thomas","year":"1997","unstructured":"Thomas Reps. 1997. Program analysis via graph reachability. In Proceedings of the ILPS\u201997."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77050-3_4"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_2_1_63_1","volume-title":"Code inspection: Unused local variable. ReSharper","author":"ReSharper JetBrains","year":"2019","unstructured":"JetBrains ReSharper. 2019. Code inspection: Unused local variable. ReSharper 2019.1 Help. Retrieved from: https:\/\/www.jetbrains.com\/help\/resharper\/UnusedVariable.html."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/0095-8956(84)90013-3"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094817"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2697"},{"key":"e_1_2_1_69_1","volume-title":"Proceedings of the CASCON\u201999","author":"Vall\u00e9e-Rai Raja","year":"1999","unstructured":"Raja Vall\u00e9e-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. 1999. Soot\u2014A Java bytecode optimization framework. In Proceedings of the CASCON\u201999. IBM Press."},{"key":"e_1_2_1_70_1","unstructured":"Genevieve Warren Gordon Hogenson Mike Jones and Saisang Cai. 2016. CA1804: Remove unused locals. Retrieved from: https:\/\/docs.microsoft.com\/en-us\/visualstudio\/code-quality\/ca1804-remove-unused-locals?view=vs-2019."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012962649700036X"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/502874.502888"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594328"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3363525","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T23:16:13Z","timestamp":1707520573000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3363525"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,13]]},"references-count":71,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,12,31]]}},"alternative-id":["10.1145\/3363525"],"URL":"https:\/\/doi.org\/10.1145\/3363525","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,13]]},"assertion":[{"value":"2018-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
