{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:25:37Z","timestamp":1779074737043,"version":"3.51.4"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["772568 and 695412"],"award-info":[{"award-number":["772568 and 695412"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1544542 and 1618732"],"award-info":[{"award-number":["1544542 and 1618732"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Czech Operational Programme Research, Development and Education","award":["CZ.02.1.01\/0.0\/0.0\/15_003\/0000421"],"award-info":[{"award-number":["CZ.02.1.01\/0.0\/0.0\/15_003\/0000421"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>Just-in-time compilers for dynamic languages routinely generate code under assumptions that may be invalidated at run-time, this allows for specialization of program code to the common case in order to avoid unnecessary overheads due to uncommon cases. This form of software speculation requires support for deoptimization when some of the assumptions fail to hold. This paper presents a model just-in-time compiler with an intermediate representation that explicits the synchronization points used for deoptimization and the assumptions made by the compiler's speculation. We also present several common compiler optimizations that can leverage speculation to generate improved code. The optimizations are proved correct with the help of a proof assistant. While our work stops short of proving native code generation, we demonstrate how one could use the verified optimization to obtain significant speed ups in an end-to-end setting.<\/jats:p>","DOI":"10.1145\/3434327","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T17:34:24Z","timestamp":1609781664000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Formally verified speculation and deoptimization in a JIT compiler"],"prefix":"10.1145","volume":"5","author":[{"given":"Aur\u00e8le","family":"Barri\u00e8re","sequence":"first","affiliation":[{"name":"University of Rennes, France \/ Inria, France \/ CNRS, France \/ IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0189-0223","authenticated-orcid":false,"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[{"name":"University of Rennes, France \/ Inria, France \/ CNRS, France \/ IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0512-9607","authenticated-orcid":false,"given":"Olivier","family":"Fl\u00fcckiger","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[{"name":"University of Rennes, France \/ Inria, France \/ CNRS, France \/ IRISA, France"}],"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":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/857076.857077"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2016.15.2.a1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/304065.304113"},{"key":"e_1_2_1_4_1","unstructured":"Project Chromium. 2020. V8 JavaScript Engine. https:\/\/chromium.googlesource.com\/v8\/v8.git.  Project Chromium. 2020. V8 JavaScript Engine. https:\/\/chromium.googlesource.com\/v8\/v8.git."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854061"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2542142.2542143"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359619.3359744"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158137"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542528"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926450"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143114"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/191080.191116"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451512.2451541"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706313"},{"key":"e_1_2_1_18_1","unstructured":"Michael Paleczny Christopher Vick and Clif 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 Clif 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_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371091"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434327","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434327","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434327","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:47Z","timestamp":1750195907000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434327"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":20,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434327"],"URL":"https:\/\/doi.org\/10.1145\/3434327","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}