Efficient language translation, optimized code generation, and runtime memory layout are cornerstones of modern computer language compilers. Squeezing a user’s data structures, especially with C++ multiple inheritance, into fewer but efficiently accessed bits leads to smaller footprints needed for newer mobile and embedded applications. However, proving that the compiler is managing the correct bit layout has been lacking for C++.
This paper provides a formal verification approach based on semantic foundations that justify new layout optimizations. It introduces families of various memory layout algorithms and describes them by means of an operational semantics notation that is complex but still independent of the target architecture. These extensive formal layout details, provided using the Coq proof tools and the resulting semantic preservation correctness proofs, are a valuable contribution to the compiler field.
Compiler technology has come a long way from the classic optimization steps of the basic language for implementation of system software (BLISS) compiler or the famous Nicholas Wirth Pascal compilers (with comments written in German). Though this paper provides some overview of previous C++ memory layout solutions, the authors’ main contribution is their formal semantic proofs for complex multiple inheritance memory layouts.