{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,26]],"date-time":"2026-04-26T03:50:29Z","timestamp":1777175429179,"version":"3.51.4"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ONR","award":["503353"],"award-info":[{"award-number":["503353"]}]},{"name":"European Research Council","award":["695412"],"award-info":[{"award-number":["695412"]}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF1544542, CCF1318227, CCF1618732"],"award-info":[{"award-number":["CCF1544542, CCF1318227, CCF1618732"]}],"id":[{"id":"10.13039\/100000001","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":[[2018,1]]},"abstract":"<jats:p>High-performance dynamic language implementations make heavy use of speculative optimizations to achieve speeds close to statically compiled languages. These optimizations are typically performed by a just-in-time compiler that generates code under a set of assumptions about the state of the program and its environment. In certain cases, a program may execute code compiled under assumptions that are no longer valid. The implementation must then deoptimize the program on-the-fly; this entails finding semantically equivalent code that does not rely on invalid assumptions, translating program state to that expected by the target code, and transferring control. This paper looks at the interaction between optimization and deoptimization, and shows that reasoning about speculation is surprisingly easy when assumptions are made explicit in the program representation. This insight is demonstrated on a compiler intermediate representation, named sourir, modeled after the high-level representation for a dynamic language. Traditional compiler optimizations such as constant folding, unreachable code elimination, and function inlining are shown to be correct in the presence of assumptions. Furthermore, the paper establishes the correctness of compiler transformations specific to deoptimization: namely unrestricted deoptimization, predicate hoisting, and assume composition.<\/jats:p>","DOI":"10.1145\/3158137","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Correctness of speculative optimizations with dynamic deoptimization"],"prefix":"10.1145","volume":"2","author":[{"given":"Olivier","family":"Fl\u00fcckiger","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriel","family":"Scherer","sequence":"additional","affiliation":[{"name":"Northeastern University, USA \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming-Ho","family":"Yee","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aviral","family":"Goel","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Vitek","sequence":"additional","affiliation":[{"name":"Northeastern University, USA \/ Czech Technical University, Czechia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349303"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869517"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2016.15.2.a1"},{"key":"e_1_2_2_4_1","unstructured":"Project Chromium. 2017. V8 JavaScript Engine. https:\/\/chromium.googlesource.com\/v8\/v8.git .  Project Chromium. 2017. V8 JavaScript Engine. https:\/\/chromium.googlesource.com\/v8\/v8.git ."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854061"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535866"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2647508.2647521"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2542142.2542143"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2003.1191549"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542528"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926450"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143114"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/353171.353191"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706313"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2005.32"},{"key":"e_1_2_2_18_1","unstructured":"Michael Paleczny Christopher Vick and Cliff Click. 2001. The Java Hotspot Server Compiler. In Java Virtual Machine Research and Technology (JVM). http:\/\/www.usenix.org\/events\/jvm01\/full_papers\/paleczny\/paleczny.pdf  Michael Paleczny Christopher Vick and Cliff Click. 2001. The Java Hotspot Server Compiler. In Java Virtual Machine Research and Technology (JVM). http:\/\/www.usenix.org\/events\/jvm01\/full_papers\/paleczny\/paleczny.pdf"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2414740.2414743"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291155"},{"key":"e_1_2_2_22_1","unstructured":"Sunil Soman and Chandra Krintz. 2006. Efficient and General On-Stack Replacement for Aggressive Program Specialization. In Software Engineering Research and Practice (SERP).  Sunil Soman and Chandra Krintz. 2006. Efficient and General On-Stack Replacement for Aggressive Program Specialization. In Software Engineering Research and Practice (SERP)."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.321"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.30"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158137","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158137","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158137","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158137"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":24,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158137"],"URL":"https:\/\/doi.org\/10.1145\/3158137","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}