TY - GEN
T1 - Verified compilation on a verified processor
AU - Lööw, Andreas
AU - Kumar, Ramana
AU - Tan, Yong Kiam
AU - Myreen, Magnus O.
AU - Norrish, Michael
AU - Abrahamsson, Oskar
AU - Fox, Anthony
N1 - Publisher Copyright:
© 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.
PY - 2019/6/8
Y1 - 2019/6/8
N2 - Developing 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 complex, realistic system components, including compilers (software) and processors (hardware), to date these verification efforts have not been compatible to the point of enabling a single end-to-end correctness theorem about running a verified compiler on a verified processor. In this paper we show how to extend the trustworthy development methodology of the CakeML project, including its verified compiler, with a connection to verified hardware. Our hardware target is Silver, a verified proof-of-concept processor that we introduce here. The result is an approach to producing verified stacks that scales to proving correctness, at the hardware level, of the execution of realistic software including compilers and proof checkers. Alongside our hardware-level theorems, we demonstrate feasibility by hosting and running our verified artefacts on an FPGA board.
AB - Developing 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 complex, realistic system components, including compilers (software) and processors (hardware), to date these verification efforts have not been compatible to the point of enabling a single end-to-end correctness theorem about running a verified compiler on a verified processor. In this paper we show how to extend the trustworthy development methodology of the CakeML project, including its verified compiler, with a connection to verified hardware. Our hardware target is Silver, a verified proof-of-concept processor that we introduce here. The result is an approach to producing verified stacks that scales to proving correctness, at the hardware level, of the execution of realistic software including compilers and proof checkers. Alongside our hardware-level theorems, we demonstrate feasibility by hosting and running our verified artefacts on an FPGA board.
KW - Compiler verification
KW - Hardware verification
KW - Program verification
KW - Verified stack
UR - http://www.scopus.com/inward/record.url?scp=85067695144&partnerID=8YFLogxK
U2 - 10.1145/3314221.3314622
DO - 10.1145/3314221.3314622
M3 - Conference contribution
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 1041
EP - 1053
BT - PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - McKinley, Kathryn S.
A2 - Fisher, Kathleen
PB - Association for Computing Machinery
T2 - 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019
Y2 - 22 June 2019 through 26 June 2019
ER -