We have developed and mechanically verified a new compiler backend for CakeML. Our new compiler features a sequence of intermediate languages that allows it to incrementally compile away high-level features and enables verification at the right levels of semantic detail. In this way, it resembles mainstream (unverified) compilers for strict functional languages. The compiler supports efficient curried multi-argument functions, configurable data representations, exceptions that unwind the call stack, register allocation, and more. The compiler targets several architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V.
In this paper, we present the overall structure of the compiler, including its 12 intermediate languages, and explain how everything fits together. We focus particularly on the interaction between the verification of the register allocator and the garbage collector, and memory representations. The entire development has been carried out within the HOL4 theorem prover.
Mon 19 SepDisplayed time zone: Osaka, Sapporo, Tokyo change
13:40 - 14:55
|A New Verified Compiler Backend for CakeML|
Yong Kiam Tan IHPC at A*STAR, Singapore, Magnus O. Myreen Chalmers University of Technology, Sweden, Ramana Kumar Data61 at CSIRO, Australia, Anthony Fox University of Cambridge, UK, Scott Owens University of Kent, UK, Michael Norrish Data61 at CSIRO, AustraliaDOI
|Sequent Calculus as a Compiler Intermediate Language|
Paul Downen University of Oregon, USA, Luke Maurer University of Oregon, USA, Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft Research, UKDOI
|Refinement through Restraint: Bringing Down the Cost of Verification|
Liam O'Connor UNSW, Australia, Zilin Chen UNSW, Australia, Christine Rizkallah University of Pennsylvania, USA, Sidney Amani UNSW, Australia, Japheth Lim Data61, Australia, Toby Murray University of Melbourne, Australia, Yutaka Nagashima Data61, Australia, Thomas Sewell UNSW, Australia, Gerwin Klein UNSW, AustraliaDOI