All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

Correctness of speculative optimizations with dynamic deoptimization

The result's identifiers

  • Result code in IS VaVaI

    <a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F18%3A00330698" target="_blank" >RIV/68407700:21240/18:00330698 - isvavai.cz</a>

  • Result on the web

    <a href="http://dx.doi.org/10.1145/3158137" target="_blank" >http://dx.doi.org/10.1145/3158137</a>

  • DOI - Digital Object Identifier

    <a href="http://dx.doi.org/10.1145/3158137" target="_blank" >10.1145/3158137</a>

Alternative languages

  • Result language

    angličtina

  • Original language name

    Correctness of speculative optimizations with dynamic deoptimization

  • Original language description

    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.

  • Czech name

  • Czech description

Classification

  • Type

    J<sub>ost</sub> - Miscellaneous article in a specialist periodical

  • CEP classification

  • OECD FORD branch

    10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Result continuities

  • Project

  • Continuities

    R - Projekt Ramcoveho programu EK

Others

  • Publication year

    2018

  • Confidentiality

    S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Data specific for result type

  • Name of the periodical

    Proceedings of the ACM on Programming Languages (PACMPL)

  • ISSN

    2475-1421

  • e-ISSN

  • Volume of the periodical

    2

  • Issue of the periodical within the volume

    49

  • Country of publishing house

    US - UNITED STATES

  • Number of pages

    28

  • Pages from-to

  • UT code for WoS article

  • EID of the result in the Scopus database