Salle 206
20 September 2018 - 14h00
Extending the CompCert certified compiler for a VLIW processor of Kalray
by Cyril Six from Kalray & Verimag
Abstract: VLIW (Very Long Word Instruction) processors [Fisher, 1983], are designed to give assembly programs control over resources parallelization at each instruction. In other words, a VLIW instruction represents some aggregate of atomic computations running in parallel on the computing units of the processor. With respect to standard high performance architectures (for example, modern x86) which reorder and parallelize instructions at runtime, such a processor offers more computing power, using fewer resources (space and energy consumption), and simplifies static bounding of running times (e.g. WCET).
The counterpart of this simplicity in the design of the processor is that it requires more complex compilers to benefit from this potential. Such a compiler must indeed find an efficient way to decompose the behavior of the high-level program (typically in C) into a sequence of parallel atomic computations.
CompCert [Leroy et al., 2006-2018] is an optimizing C compiler, developed and certified in Coq, used in the industry of critical embedded systems since 2015. This compiler generates assembly program for different targets. But, currently, it only supports assembly semantics without parallelism.
Cyril Six starts a Phd thesis in order to develop a certified backend for CompCert, targeting the next VLIW processor of Kalray. He will present the scientific context of his thesis at the crossroads of three domains: VLIW processors, optimizing compilers, and software certification.
