Repository logo
 

Verified Compilation of CakeML to Multiple Machine-Code Targets

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Myreen, MO 
Tan, YK 
Kumar, R 

Abstract

This paper describes how the latest CakeML compiler supports verified compilation down to multiple realistically modelled target architectures. In particular, we describe how the compiler definition, the various language semantics, and the correctness proofs were organised to minimize target-specific overhead. With our setup we have incorporated compilation to four 64-bit architectures, ARMv8, x86-64, MIPS-64, RISC-V, and one 32-bit architecture, ARMv6. Our correctness theorem allows interference from the environment: the top-level correctness statement takes into account execution of foreign code and per-instruction interference from external processes, such as interrupt handlers in operating systems. The entire CakeML development is formalised in the HOL4 theorem prover.

Description

Keywords

Compiler verification, ML, verified assembly

Journal Title

CPP 2017 Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

Conference Name

6th ACM SIGPLAN Conference on Certified Programs and Proofs

Journal ISSN

Volume Title

Publisher

ACM
Sponsorship
Engineering and Physical Sciences Research Council (EP/K008528/1)
Engineering and Physical Sciences Research Council (EPSRC); Swedish Research Council