[Pl-seminar] Seminar Tomorrow 6/15: Aurèle Barriere: "Proving Just in Time Compilation Correct"

[Amal Ahmed]

This talk is TOMORROW at 10am.  Apologies for the late notice; there was an issue with the talk announcement last week.


NUPRL Seminar Presents

Aurèle Barriere
IRISA
aurele.barriere at irisa.fr

10:00AM to 11:30AM
Monday, June 15th, 2020
Zoom: https://northeastern.zoom.us/my/jvroom <https://northeastern.zoom.us/my/jvroom>

Proving Just in Time Compilation Correct

Abstract

Just-in-Time compilation consists in interleaving program interpretation and compilation at run-time, to achieve better performance than standard interpretation. While some of the execution time is spent compiling, a JIT compiler can leverage run-time information to make speculative optimizations. These optimizations create optimized versions of functions given some assumptions. While static compilers have been the topic of many formal verification works, few have tackled JIT compilation verification. We discuss our work about the formal and mechanized verification of a Just-in-Time compiler middle-end. We first present an intermediate representation designed for speculation. We show how we can adapt the proof methodology from verified static compilers, such as CompCert, to prove in Coq the correctness of dynamic and speculative optimizations on this intermediate representation. Our verified model of a JIT compiler can then be extracted and run.

Host: Jan Vitek


-------------- next part --------------
HTML attachment scrubbed and removed