Safety-critical applications are generally deployed on microcontrollers or specialized processors, and incur specific procedures for validation and qualification. General-purpose compilers, such as gcc or clang, may occasionally miscompile programs. CompCert is a formally verified compiler for the C programming language, in the sense that there is a machine-checked proof that, when compilation succeeds, it produces assembly code whose execution matches that of the source code. Correctness is not everything. Safety-critical systems must generally meet real-time specifications. Compiler optimizations result in faster code capable of meeting these specifications. At present CompCert is only moderately optimizing. At Verimag, we have already added various optimizations to CompCert (prepass and postpass scheduling, global common subexpression elimination, loop-invariant code motion, strength reduction…). Yet, there is still much to do for certain kinds of applications and certain target platforms, in particular 32-bit ARM, which is popular for embedded applications. The purpose of the internship is to investigate which optimizations CompCert is missing on certain classes of programs, and how to implement and prove them correct.
This topic may be taken as a master 1 or 2 internship. In the case of master 2, it may be followed by a CIFRE (part-time in industry) thesis. We may also recruit directly in CIFRE if conditions are right.
