Trustworthy Systems

Verified compilation of CakeML to multiple machine-code targets

Authors

Anthony Fox, Magnus Myreen, Yong Kiam Tan and Ramana Kumar

University of Cambridge

Chalmers University of Technology

Carnegie Mellon University

Data61
CSIRO

Abstract

This paper describes how the latest CakeML compiler sup- ports 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 places particular emphasis on pos- sible interference from the external environment: the top- level correctness statement takes into account execution of foreign code and per-instruction interference from external processes, such as that of interrupt handlers in operating sys- tems. The entire CakeML development is formalised in the HOL4 theorem prover.

BibTeX Entry

  @inproceedings{Fox_MTK_17,
    address          = {Paris, France},
    author           = {Fox, Anthony and Myreen, Magnus and Tan, Yong Kiam and Kumar, Ramana},
    booktitle        = {International Conference on Certified Programs and Proofs},
    keywords         = {cakeml},
    month            = jan,
    pages            = {125--137},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9510.pdf},
    title            = {Verified Compilation of {CakeML} to Multiple Machine-Code Targets},
    year             = {2017}
  }

Download