diff options
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 23 |
1 files changed, 23 insertions, 0 deletions
@@ -16,6 +16,26 @@ features, installation instructions, using the compiler, etc), please refer to the [Web site](https://compcert.org/) and especially the [user's manual](https://compcert.org/man/). +## Verimag-Kalray version +This is a special version with additions from Verimag and Kalray : + +* A backend for the KVX processor: see [`README_Kalray.md`](README_Kalray.md) for details. +* Some general-purpose optimization phases (e.g. profiling). + * see [`PROFILING.md`](PROFILING.md) for details on the profiling system + +The people responsible for this version are + +* Sylvain Boulmé (Grenoble-INP, Verimag) +* David Monniaux (CNRS, Verimag) +* Cyril Six (Kalray) + +## Papers, docs, etc on this CompCert version + +* [a 5-minutes video](http://www-verimag.imag.fr/~boulme/videos/poster-oopsla20.mp4) by C. Six, presenting the postpass scheduling and the KVX backend +(also on [YouTube if you need subtitles](https://www.youtube.com/watch?v=RAzMDS9OVSw)). +* [Certified and Efficient Instruction Scheduling](https://hal.archives-ouvertes.fr/hal-02185883), an OOPSLA'20 paper, by Six, Boulmé and Monniaux. +* [the documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx) + ## License CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. @@ -29,6 +49,7 @@ The CompCert verified compiler is Copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and AbsInt Angewandte Informatik GmbH. +The additions are Copyright Grenoble-INP, CNRS and Kalray. ## Contact General discussions on CompCert take place on the @@ -37,3 +58,5 @@ mailing list. For inquiries on the commercial version of CompCert, please contact info@absint.com + +For inquiries on the Verimag-specific additions, contact the researchers. |