Anthony Fox
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.
- F. Besson, S. Blazy, and P. Wilke. A concrete memory model for CompCert. In C. Urban and X. Zhang, editors, Interactive Theorem Proving (ITP), LNCS. Springer, 2015.Google Scholar
Cross Ref
- A. Chlipala. A verified compiler for an impure functional language. In M. V. Hermenegildo and J. Palsberg, editors, Principles of Programming Languages (POPL). ACM, Jan. 2010. Google ScholarDigital Library
- A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In Programming Language Design and Implementation (PLDI). ACM, 2011. Google ScholarDigital Library
- A. Chlipala. The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In International Conference on Functional Programming (ICFP). ACM, 2013. Google ScholarDigital Library
- A. C. J. Fox. Improved tool support for machine-code decompilation in HOL4. In C. Urban and X. Zhang, editors, Interactive Theorem Proving (ITP), LNCS, 2015.Google Scholar
- R. Kumar, M. O. Myreen, M. Norrish, and S. Owens. CakeML: a verified implementation of ML. In S. Jagannathan and P. Sewell, editors, Principles of Programming Languages (POPL). ACM, 2014. Google ScholarDigital Library
- X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7), 2009. Google ScholarDigital Library
- X. Leroy, A. W. Appel, S. Blazy, and G. Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012.Google Scholar
- J. S. Moore. A mechanically verified language implementation. Journal of Automated Reasoning, 5(4):461–492, 1989. Google ScholarDigital Library
- E. Mullen, D. Zuniga, Z. Tatlock, and D. Grossman. Verified peephole optimizations for CompCert. In C. Krintz and E. Berger, editors, Programming Language Design and Implementation (PLDI). ACM, 2016. Google ScholarDigital Library
- Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. SIGPLAN Not., 41(1), Jan. 2006. Google ScholarDigital Library
- Google Scholar
- S. Owens, M. O. Myreen, R. Kumar, and Y. K. Tan. Functional bigstep semantics. In P. Thiemann, editor, European Symposium on Programming (ESOP), LNCS. Springer, 2016.Google ScholarDigital Library
- T. A. L. Sewell, M. O. Myreen, and G. Klein. Translation validation for a verified OS kernel. In Programming Language Design and Implementation (PLDI). ACM, 2013. Google ScholarDigital Library
- Y. K. Tan, M. O. Myreen, R. Kumar, A. Fox, S. Owens, and M. Norrish. A new verified compiler backend for CakeML. In J. Garrigue, G. Keller, and E. Sumii, editors, International Conference on Functional Programming (ICFP). ACM, 2016. Google Scholar
Index Terms
- Verified compilation of CakeML to multiple machine-code targets
Recommendations
Verified compilation on a verified processor
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and ImplementationDeveloping technology for building verified stacks, i.e., computer systems with comprehensive proofs of correctness, is one way the science of programming languages furthers the computing discipline. While there have been successful projects verifying ...
A new verified compiler backend for CakeML
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingWe 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 ...
A new verified compiler backend for CakeML
ICFP '16We 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 ...
Comments