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.
KALRAY-CompCert
We extend the CompCert certified compiler with a backend for the K1C core and various optimizations to reach high performance (instruction scheduling...).
Browsing
News
- NEWS
- Karine Altisen, Stéphane Devismes, Swan Dubois, and Franck Petit New Book: Introduction to Distributed Self-Stabilizing Algorithms
- Conferences
- November 25-29 2019 Synchron 2019
Seminars
New publications
- Recent Publications
- Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang Yu: The Verified Polyhedron Library: an overview
- Karine Altisen, Stéphane Devismes, Anaïs Durand, Franck Petit: Gradual stabilization
- Nicolas Basset, Marta Z. Kwiatkowska, Clemens Wiltsche: Compositional strategy synthesis for stochastic games with multiple objectives
- Stéphane Devismes, Anissa Lamani, Franck Petit, Sébastien Tixeuil: Optimal torus exploration by oblivious robots
- Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain: Manuel de savoir-prouver à l'usage des roboteux et des distributeux
- Ajoy Kumar Datta, Stéphane Devismes, Colette Johnen, Lawrence L. Larmore: Brief Announcement: Analysis of a Memory-Efficient Self-Stabilizing BFS Spanning Tree Construction
