Improving Thunks in the Verified PureCake Compiler

Abstract

Compiler construction is a research area that is constantly being developed, as the need for faster and more correct programming languages and implementations is steadily growing. While much work has been done to ensure compilers output efficient and semantically intact code, the complexity and size of the current optimising compilers lead to bugs that can be hard to find and diagnose. Situations where correctness is critical has therefore led to the development of formally verified compilers, that guarantee the correctness of the generated code. The price paid for developing verified compilers is that every step in the compilation process must be carefully implemented and formalised in order for the verification system to accept it, which makes optimisation pipelines much harder to implement.

This project’s work is based on the PureCake verified compiler for pure, lazy functional languages. PureCake is an extension of the CakeML project, which itself is a verified compiler for strict functional languages, both developed using the HOL4 formal verification system. The PureCake compiler is already a complete verified compiler, but it lacks the optimisations that would make its generated code as efficient as the generated code of optimising non-verified compilers for lazy languages such as GHC. This project’s goal is to enhance PureCake’s and CakeML’s language with features that will enable critical optimisations to be implemented in order to close the gap between verified and non-verified compilers for lazy languages in terms of runtime efficiency.

In this thesis, we take on the task of improving the quality of PureCake’s generated code, by optimising the handling of thunks by the PureCake and CakeML compilers. We first target the representation of thunks inside PureCake, by enriching the semantics of the operations responsible for handling thunks and by proving these changes correct. Then, we implement thunks in CakeML and lay the foundations for future optimisations in the runtime. This work will help bring PureCake up to par with unverified compilers in terms of the generated executable’s performance, while also making sure that the soundness of the compilation process remains intact.