A New Verified Compiler Backend for CakeML
View / Open Files
Publication Date
2016-09-04Journal Title
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
ISSN
1523-2867
Publisher
Association for Computing Machinery
Pages
60-73
Language
English
Type
Article
This Version
AM
Metadata
Show full item recordCitation
Tan, Y., Myreen, M., Kumar, R., Fox, A., Owens, S., & Norrish, M. (2016). A New Verified Compiler Backend for CakeML. Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 60-73. https://doi.org/10.1145/2951913.2951924
Abstract
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.
Keywords
compiler verification, ML, verified optimisations
Sponsorship
Engineering and Physical Sciences Research Council
Funder references
EPSRC (EP/K008528/1)
Identifiers
External DOI: https://doi.org/10.1145/2951913.2951924
This record's URL: https://www.repository.cam.ac.uk/handle/1810/261357
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved