CIFRE 2018-2021

We extend the CompCert certified compiler with a backend for the KVX core and various optimizations to reach high performance (instruction scheduling...).

CompCert is a C compiler with a machine-checked mathematical proof of soundness. The Kalray KVX core is a very large instruction word (VLIW) in-order core. We extend CompCert for the KVX core. For this, we need some optimizations such as instruction scheduling. See the KVX CompCert Compiler

  • PhD Student : Cyril Six
  • Supervisors : David Monniaux, Sylvain Boulmé
  • Kalray : Benoît Dupont de Dinechin

Contact | Plan du site | Site réalisé avec SPIP 3.1.13 + AHUNTSIC [CC License]

info visites 1700282