{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T16:51:54Z","timestamp":1771951914693,"version":"3.50.1"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T00:00:00Z","timestamp":1451865600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"University of Padova under the PRAT projects BECOM and ANCORE"},{"name":"Microsoft Research Software Engineering Innovation Foundation 2013","award":["SEIF 2013"],"award-info":[{"award-number":["SEIF 2013"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2016,1,4]]},"abstract":"<jats:p>Tracing just-in-time compilation is a popular compilation technique for the efficient implementation of dynamic languages, which is commonly used for JavaScript, Python, and PHP. It relies on two key ideas. First, it monitors program execution in order to detect so-called hot paths, that is, the most frequently executed program paths. Then, hot paths are optimized by exploiting some information on program stores that is available and therefore gathered at runtime. The result is a residual program where the optimized hot paths are guarded by sufficient conditions ensuring some form of equivalence with the original program. The residual program is persistently mutated during its execution, for example, to add new optimized hot paths or to merge existing paths. Tracing compilation is thus fundamentally different from traditional static compilation. Nevertheless, despite the practical success of tracing compilation, very little is known about its theoretical foundations. We provide a formal model of tracing compilation of programs using abstract interpretation. The monitoring phase (viz., hot path detection) corresponds to an abstraction of the trace semantics of the program that captures the most frequent occurrences of sequences of program points together with an abstraction of their corresponding stores, for example, a type environment. The optimization phase (viz., residual program generation) corresponds to a transform of the original program that preserves its trace semantics up to a given observation as modeled by some abstraction. We provide a generic framework to express dynamic optimizations along hot paths and to prove them correct. We instantiate it to prove the correctness of dynamic type specialization and constant variable folding. We show that our framework is more general than the model of tracing compilation introduced by Guo and Palsberg [2011], which is based on operational bisimulations. In our model, we can naturally express hot path reentrance and common optimizations like dead-store elimination, which are either excluded or unsound in Guo and Palsberg\u2019s framework.<\/jats:p>","DOI":"10.1145\/2853131","type":"journal-article","created":{"date-parts":[[2016,4,11]],"date-time":"2016-04-11T13:34:08Z","timestamp":1460381648000},"page":"1-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["An Abstract Interpretation-Based Model of Tracing Just-in-Time Compilation"],"prefix":"10.1145","volume":"38","author":[{"given":"Stefano","family":"Dissegna","sequence":"first","affiliation":[{"name":"University of Padova, Padova, Italy"}]},{"given":"Francesco","family":"Logozzo","sequence":"additional","affiliation":[{"name":"Facebook Inc., WA, USA"}]},{"given":"Francesco","family":"Ranzato","sequence":"additional","affiliation":[{"name":"University of Padova, Padova, Italy"}]}],"member":"320","published-online":{"date-parts":[[2016,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660199"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349303"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(99)00042-3"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784740"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869517"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993508"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929501.1929508"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1565824.1565827"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237776"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80168-9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00313-3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503290"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535866"},{"key":"e_1_2_1_16_1","volume-title":"ECMAScript 2015 Language Specification","author":"International Ecma","unstructured":"Ecma International. 2015. Standard ECMA-262, ECMAScript 2015 Language Specification (6th ed.). Retrieved from http:\/\/www.ecma-international.org\/ecma-262\/6.0.","edition":"6"},{"key":"e_1_2_1_17_1","volume-title":"The HipHop Virtual Machine. (Oct","author":"Facebook Inc. 2013.","year":"2013","unstructured":"Facebook Inc. 2013. The HipHop Virtual Machine. (Oct. 2013). https:\/\/www.facebook.com\/hhvm."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542528"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542528"},{"key":"e_1_2_1_20_1","volume-title":"A New Crankshaft for V8. (Dec","author":"Google Inc. 2010.","year":"2010","unstructured":"Google Inc. 2010. A New Crankshaft for V8. (Dec. 2010). The Chromium Blog. http:\/\/blog.chromium.org\/2010\/12\/new-crankshaft-for-v8.html."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926450"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"M. Handjieva and S. Tzolovski. 1998. Refining static analyses by trace-based partitioning using control flow. In Proceedings of the 5th International Static Analysis Symposium (SAS\u201998) Lecture Notes in Computer Science Vol. 1503. Springer Berlin 200--214. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-49727-7_12","DOI":"10.1007\/3-540-49727-7_12"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2093157.2093176"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2579673"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2011.5764692"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2005.01.001"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/225494"},{"key":"e_1_2_1_28_1","unstructured":"Mozilla Foundation. 2010. TraceMonkey. (Oct. 2010). MozillaWiki. https:\/\/wiki.mozilla.org\/JavaScript:TraceMonkey."},{"key":"e_1_2_1_29_1","unstructured":"Mozilla Foundation. 2013. IonMonkey. (May 2013). MozillaWiki. https:\/\/wiki.mozilla.org\/IonMonkey."},{"key":"e_1_2_1_30_1","unstructured":"M. Pall. 2005. The LuaJIT Project. (2005). http:\/\/luajit.org."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964002"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007734417713"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/937563.937565"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103136"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2853131","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2853131","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:04:30Z","timestamp":1750273470000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2853131"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,4]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,1,4]]}},"alternative-id":["10.1145\/2853131"],"URL":"https:\/\/doi.org\/10.1145\/2853131","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1,4]]},"assertion":[{"value":"2014-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}