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 | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 3985140