Seminar Room 2, ground floor (Building IMAG)
12 December 2023 - 09h30
Formal Validation of Intra-Procedural Transformations by Defensive Symbolic Simulation (Phd Defense)
by Leo Gourdin from VERIMAG
Abstract: Compilers are highly complex software systems and may, therefore, contain bugs. These bugs can result in errors during the compilation process, or, much more annoyingly, in the generation of incorrect code. Bugs that subtly alter the semantics of generated programs are often very insidious and challenging to trace. In certain applications, particularly in embedded, safety-critical systems subject to stringent regulations and requirements (e.g. avionics, trains, etc.), eliminating these bugs is of paramount importance.
Although most of these bugs are typically found in optimization passes, disabling optimizations is not a viable option in many applications. In fact, simply turning off optimizations is insufficient to guarantee bug-free code. Regulatory standards often necessitate the use of simple, predictable processors, heavily reliant on the compiler for performance.
An alternative solution is to employ a certified compiler, mechanically proven correct in a proof assistant. Such a compiler ensures that the generated assembly code faithfully preserves the source code's semantics. CompCert belongs to this category, and stands as the first formally verified C compiler widely used in the industry. However, proving the correctness of intricate optimizations remains a challenge. This is why certified compilers, including CompCert, produce code that is significantly less performant compared to mainstream compilers like GCC or LLVM.
Translation validation offers a technique where only the result of an optimization is verified, rather than proving the correctness of its implementation. The optimization algorithm, referred to as an oracle, remains untrusted. Nevertheless, its results are always subjected to validation by a proven validator designed to reject any errors.
In this thesis, we delve into the concept of guided translation validation. The principle is to allow oracles to guide the validator by providing hints that reduce the search space, thereby minimizing the complexity of the validation process. Specifically, we propose a formally verified symbolic interpreter capable of validating an entire class of transformations. Our tool requests program invariants from oracles as hints to drive the symbolic simulation of both the original and optimized code. The proven simulation test defensively validates the applied optimizations, ensuring consistency with the unoptimized code.
We have successfully validated several new transformations using this approach, including some that had never been formally verified before, thanks to the communication between oracles and their validator. Notably, we verify a strength-reduction optimization targeting 64-bit RISC-V architectures, which show promise in the context of safety-critical embedded systems. In addition to strength-reduction, our symbolic simulation framework also supports partial redundancy elimination, dead code elimination, code motion, scheduling, and weak software pipelining with renaming.
We have integrated our validation mechanism into a fork of CompCert through the development of a new intermediate language called Block Transfer Language, BTL. Translations to and from BTL are also defensively validated, accomplished with a separate, formally verified checker capable of validating code duplication and factorization as control-flow graph morphisms. To rigorously assess the impact of our optimizations and the overhead introduced by their validation, we conducted multiple experimental measurements of both compilation time and runtime performance. Platform specific optimizations were tested on both AArch64 and RISC-V architectures. Results show a significant improvement of the runtime performance while maintaining a reasonable compilation time.
In the future, this same method could potentially be applied to validate other transformations, such as the automatic insertion of security countermeasures. Our designs appear to be applicable beyond CompCert.
Slides of the Presentation.
Phd defense of Léo Gourdin.
See https://lgourd.in/defense.html for more information (e.g. remote link).
