CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Verified compilation of CakeML to multiple machine-code targets

Anthony C. J. Fox ; Magnus O. Myreen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Yong Kiam Tan ; Ramana Kumar
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, {CPP} 2017 p. 125-137. (2017)
[Konferensbidrag, refereegranskat]

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.

Nyckelord: Compiler verification, ML, Verified assembly



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2017-02-01. Senast ändrad 2017-08-16.
CPL Pubid: 247963