Inline Caching and Unboxing Optimization for Interpreters

Martin Desharnais 🌐

December 7, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This Isabelle/HOL formalization builds on the VeriComp entry of the Archive of Formal Proofs to provide the following contributions:
  • an operational semantics for a realistic virtual machine (Std) for dynamically typed programming languages;
  • the formalization of an inline caching optimization (Inca), a proof of bisimulation with (Std), and a compilation function;
  • the formalization of an unboxing optimization (Ubx), a proof of bisimulation with (Inca), and a simple compilation function.
This formalization was described in the CPP 2021 paper Towards Efficient and Verified Virtual Machines for Dynamic Languages

License

BSD License

History

June 25, 2021
proved conditional completeness of compilation
June 14, 2021
refactored function definitions to contain explicit basic blocks

Topics

Session Interpreter_Optimizations

Depends on

Cite

× 
@article{Interpreter_Optimizations-AFP,
  author  = {Martin Desharnais},
  title   = {Inline Caching and Unboxing Optimization for Interpreters},
  journal = {Archive of Formal Proofs},
  month   = {December},
  year    = {2020},
  note    = {\url{https://isa-afp.org/entries/Interpreter_Optimizations.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: