diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-12-06 15:30:13 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-12-06 15:30:13 +0100 |
| commit | 86fa4cc62f34f8fda7ea324c692101a97b4b8166 (patch) | |
| tree | 08f1b2c0bce3371ce8ce307f1ec7e49785e7d214 /README.md | |
| parent | 2f46b5c2420fec2d349a1ac192c8877d7737b72e (diff) | |
| download | compcert-kvx-86fa4cc62f34f8fda7ea324c692101a97b4b8166.tar.gz compcert-kvx-86fa4cc62f34f8fda7ea324c692101a97b4b8166.zip | |
update info on authors/papers
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 14 |
1 files changed, 13 insertions, 1 deletions
@@ -20,6 +20,7 @@ the [user's manual](https://compcert.org/man/). 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. +* Scheduling passes for ARMv8 (aarch64) and RISC-V. * Some general-purpose optimization phases (e.g. profiling). * see [`PROFILING.md`](PROFILING.md) for details on the profiling system @@ -28,13 +29,24 @@ The people responsible for this version are * Sylvain Boulmé (Grenoble-INP, Verimag) * David Monniaux (CNRS, Verimag) * Cyril Six (Kalray) +* Léo Gourdin (UGA, Verimag) + +with contributions of: + +* Justus Fasse (M2R UGA, now at KU Leuven). +* Pierre Goutagny and Nicolas Nardino (L3 ENS-Lyon). ## 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)). +* [the documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx). * [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) +* [Formally Verified Superblock Scheduling](https://hal.archives-ouvertes.fr/hal-03200774), a CPP'22 paper, by Six, Gourdin, Boulmé, Monniaux, Fasse and Nardino. +* [Optimized and formally-verified compilation for a VLIW processor](https://hal.archives-ouvertes.fr/tel-03326923), Phd Thesis of Cyril Six in 2021. +* [Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) -- Chapters 1 to 3](https://hal.archives-ouvertes.fr/tel-03356701), Habilitation Thesis of Sylvain Boulmé in 2021. +* [Code Transformations to Increase Prepass Scheduling Opportunities in CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/FASSE-Justus-MSc-Thesis_2021.pdf), MSc Thesis of Justus Fasse in 2021. +* [Register-Pressure-Aware Prepass-Scheduling for CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/NARDINO-Nicolas-BSc-Thesis_2021.pdf), BSc Thesis of Nicolas Nardino in 2021. ## License CompCert is not free software. This non-commercial release can only |