An Abstract Interpretation-based Model of Tracing Just-In-Time
Compilation
S. Dissegna, F. Logozzo, and F. Ranzato. (2014)cite arxiv:1411.7839Comment: To appear in ACM Transactions on Programming Languages and Systems.
Abstract
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. We provide a formal model of tracing JIT
compilation of programs using abstract interpretation. Hot path detection
corresponds to an abstraction of the trace semantics of the program. The
optimization phase corresponds to a transform of the original program that
preserves its trace semantics up to an observation modeled by some abstraction.
We provide a generic framework to express dynamic optimizations and 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 based on operational bisimulations.
Description
An Abstract Interpretation-based Model of Tracing Just-In-Time
Compilation
%0 Generic
%1 dissegna2014abstract
%A Dissegna, Stefano
%A Logozzo, Francesco
%A Ranzato, Francesco
%D 2014
%K php
%T An Abstract Interpretation-based Model of Tracing Just-In-Time
Compilation
%U http://arxiv.org/abs/1411.7839
%X 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. We provide a formal model of tracing JIT
compilation of programs using abstract interpretation. Hot path detection
corresponds to an abstraction of the trace semantics of the program. The
optimization phase corresponds to a transform of the original program that
preserves its trace semantics up to an observation modeled by some abstraction.
We provide a generic framework to express dynamic optimizations and 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 based on operational bisimulations.
@misc{dissegna2014abstract,
abstract = {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. We provide a formal model of tracing JIT
compilation of programs using abstract interpretation. Hot path detection
corresponds to an abstraction of the trace semantics of the program. The
optimization phase corresponds to a transform of the original program that
preserves its trace semantics up to an observation modeled by some abstraction.
We provide a generic framework to express dynamic optimizations and 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] based on operational bisimulations.},
added-at = {2017-12-30T11:19:12.000+0100},
author = {Dissegna, Stefano and Logozzo, Francesco and Ranzato, Francesco},
biburl = {https://www.bibsonomy.org/bibtex/215367b8502db07f83c572f56ab4adbb8/s_bergmann},
description = {An Abstract Interpretation-based Model of Tracing Just-In-Time
Compilation},
interhash = {b2752b6a2bebd3e0a5f216401472b06d},
intrahash = {15367b8502db07f83c572f56ab4adbb8},
keywords = {php},
note = {cite arxiv:1411.7839Comment: To appear in ACM Transactions on Programming Languages and Systems},
timestamp = {2017-12-30T11:19:12.000+0100},
title = {An Abstract Interpretation-based Model of Tracing Just-In-Time
Compilation},
url = {http://arxiv.org/abs/1411.7839},
year = 2014
}