Formal Verification of Just-in-Time Compilation

Thesis dissertation

Watching the Defense

December 19th 2022, 15h (3pm, GMT+1).
At IRISA Rennes, room Petri-Turing.

Please send me an email if you wish to attend live. You can also watch the defense online using the link below.

During the presentation, please turn off your video if you are not a member of the jury
Pendant la présentation, merci de couper votre caméra si vous ne faites pas partie du jury.

Webex Link

PhD Jury

  • Sandrine Blazy. Professeur des Universités, Université de Rennes 1. Directrice de thèse.
  • David Pichardie. Chercheur, Meta. Co-encadrant de thèse.
  • Andrew Appel. Professor, Princeton University. Reviewer.
  • Xavier Leroy. Professeur, Collège de France. Reviewer.
  • Stephan Merz. Directeur de Recherche, INRIA.
  • Magnus Myreen. Associate Professor, Chalmers University of Technology.
  • Alan Schmitt. Directeur de Recherche, INRIA.
  • Manuel Serrano. Directeur de Recherche, INRIA.

Abstract

Just-in-Time compilation is a technique to execute programs, where execution is interleaved with optimizations. Just-in-Time compilers often produce fast executions, but are particularly complex. For instance, they reuse various existing techniques: some contain both interpreters to execute programs and traditional compilers to generate optimized machine code. They also use ad hoc techniques like speculation, which consists in predicting the future behavior of the program to generate specialized code that executes particularly fast if the prediction holds.

This great complexity can lead to bugs. This thesis tackles their formal verification, to develop Just-in-Time compilers in such a way that one can formally prove that they behave as prescribed by the semantics of the program they execute. We present correctness proofs for their main features, including speculation, dynamic optimizations and machine code generation. We reuse proof techniques from formally verified traditional compilers like CompCert. All our proofs have been mechanized in the Coq proof assistant.