Merge remote-tracking branch 'origin/CPP_2022' into weak-software-pipelining

3 files changed, 22 insertions, 7 deletions

diff --git a/README.md b/README.md
index 3990048e..0a369265 100644
--- a/README.md
+++ b/README.md
@@ -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
diff --git a/doc/index-kvx.html b/doc/index-kvx.html
index daa4cdc4..909a613f 100644
--- a/doc/index-kvx.html
+++ b/doc/index-kvx.html
@@ -25,7 +25,7 @@ a:active {color : Red; text-decoration : underline; }
 <font color=gray>
 <H1 align="center">The CompCert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 3.8, 2020-11-16</H3>
+<H3 align="center">Version 3.9, 2021-05-10</H3>
 </font>
 <H3 align="center">PATCHED for the Kalray MPPA-KVX VLIW CORE<!--@DATE@--></H3>
 
@@ -36,10 +36,13 @@ a:active {color : Red; text-decoration : underline; }
   The unmodified parts of this table appear in <font color=gray>gray</font>.
   <br>
   <br>
-  A high-level view of this CompCert backend is provided by this OOPSLA'20 paper (of Six, Boulm&eacute; and Monniaux):
-  <div><a href=https://hal.archives-ouvertes.fr/hal-02185883>Certified and Efficient Instruction Scheduling. Application to Interlocked VLIW Processors.</a></div>
+  A high-level view of this CompCert backend is provided by this CPP'22 paper (of Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino):
+  <div><a href=https://hal.archives-ouvertes.fr/hal-03200774>Verified Superblock Scheduling.</a></div>
   <br>
-  See also the <tt>README.md</tt> of our <a href=https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx>GitLab public repository</a>.
+  See also the <tt>README.md</tt> of our <a href=https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx/-/tree/CPP22_main>GitLab public repository</a>
+  (the source code is in branch <tt>CPP22_main</tt> -- the branch <tt>CPP22_if_lifting</tt> being an experimental variant described in the above paper).
+  <br>
+  This pages corresponds to our Kalray MPPA-KVX VLIW backend. For our RISC-V and Aarch64 (ARMv8) backend, see directly the source code (given by the link above).
 </p>
 
 <font color=gray>
@@ -389,7 +392,7 @@ This IR is generic over the processor, even if currently, only used for KVX.
 </TR>
 </TABLE>
 
-<H3>All together (there are many more RTL passes than on vanilla CompCert: their order is specified in Compiler)</H3>
+<H3>All together (there are many more RTL passes than on mainline CompCert: their order is specified in Compiler)</H3>
 
 <UL>
 </font>