diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-12-06 14:31:50 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-12-06 14:31:50 +0100 |
| commit | dede57ca2de03dd3fee4fa0cb5cc4c5bfec056ce (patch) | |
| tree | 9421d437129ebb3c7f455e7d2b2cb7e4f32cc046 | |
| parent | 3316fc1f4f9c6ca11a49ab836bbacb20d2b0e52a (diff) | |
| download | compcert-kvx-dede57ca2de03dd3fee4fa0cb5cc4c5bfec056ce.tar.gz compcert-kvx-dede57ca2de03dd3fee4fa0cb5cc4c5bfec056ce.zip | |
authors and papers links for the CPP'22 version
| -rw-r--r-- | README.md | 14 | ||||
| -rw-r--r-- | README_Kalray.md | 2 |
2 files changed, 14 insertions, 2 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 (CPP'22)](https://www-verimag.imag.fr/~boulme/CPP_2022/). * [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 diff --git a/README_Kalray.md b/README_Kalray.md index 86c49ad1..33b41cf5 100644 --- a/README_Kalray.md +++ b/README_Kalray.md @@ -18,7 +18,7 @@ Please follow the instructions in `INSTALL.md` ## Documentation of the Coq sources -The documentation is available [online](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx). +The documentation of this CPP'2022 release is available [online](https://www-verimag.imag.fr/~boulme/CPP_2022/). You may also generate it locally from `make documentation` (after installation via `INSTALL.md`): the entry-point is in `doc/index-kvx.html`. ## Testing |