diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-12-02 16:15:31 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-12-02 16:15:31 +0100 |
| commit | bf791c9795c86af025cf85ad87663630e79911f3 (patch) | |
| tree | 3136242f1b1d20fa5046a491752ed1fcdeeb2d78 | |
| parent | 40c36e4e43fa5608d91a0d6ddd46eafbf5ced45c (diff) | |
| download | compcert-kvx-bf791c9795c86af025cf85ad87663630e79911f3.tar.gz compcert-kvx-bf791c9795c86af025cf85ad87663630e79911f3.zip | |
update for CPP_2022 publication
| -rw-r--r-- | doc/index-kvx.html | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/doc/index-kvx.html b/doc/index-kvx.html index daa4cdc4..bbda781a 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,11 @@ 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é 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). </p> <font color=gray> @@ -389,7 +390,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> |