We extend the CompCert certified compiler with a backend for the K1C 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 K1c is a very large instruction word (VLIW) in-order core. We extend CompCert for the K1c core. For this, we need some optimizations such as instruction scheduling.

Contact | Site Map | Site powered by SPIP 3.1.12 + AHUNTSIC [CC License]

info visites 1674409