Verified Compilation for Sequential Programs
We have constructed three verified compilers, which are implemented and verified in the Coq proof assistant.
- Pilsner compiles programs written in an ML-like source language into an idealized RISC-style assembly language, and incorporates a number of optimisation passes. It is the first multi-pass compiler for a higher-order imperative language to be compositionally verified.
- Zwickel is a simpler single-pass compiler from the same ML-like source language that Pilsner supports into the same idealized RISC-style assembly target language. The two compilers are (provably) fully interoperable. If part of a program is compiled by Pilsner and the remainder is compiled by Zwickel, the two parts may be linked together and will produce the same output as if they were compiled by either one of the compilers.
- SepCompCert is an extension of the well-known CompCert verified compiler that compiles C programs into x86, Power, and ARM assembly and has performance roughly comparable to gcc at optimisation level 1. Unlike the base CompCert 2.4 compiler, SepCompCert is correct also for separate compilation: that is, where the compiler is run on each input C file separately and the resulting object files are linked together.
The source code for these compilers is available at the links above.
Compilation under Weak Memory Models
We have also studied the correctness of compilation under weak memory models. Specifically:
- We have studied the C/C++ 2011 memory model and considered the soundness of program optimisations under it, uncovering a number of errors in the 2011 C and C++ standards, and proposing fixes to the model. (The proofs associated with this work have been carried out in Coq and are available here together with a detailed description of the errors in the original C/C++11 model.)
- We have proposed Strong Release-Acquire (SRA) consistency, a sound strengthening of the release-acquire fragment of the C/C++ 2011 memory model and have proved that the expected program optimisations and compilation schemes to TSO and POWER are sound. (The proofs associated with this work have been carried out in Coq and are available here.)
- We have constructed a translation validator for the LLVM compiler infrastructure targetting the optimisation of atomic accesses at the "opt" level of the compiler. Our validator was used to uncover a few serious compilation bugs in LLVM version 3.6. (For further details and to download the validator, please follow this link.)