diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-04 16:42:54 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-11-04 16:42:54 +0100 |
commit | 9b6758f42ba80caed80b6f25371140a45cc88340 (patch) | |
tree | 37722a21d4674558512fb403587b0e057838d99d | |
parent | b7c2d3f693c8cef940bb6151c228059ffde0304a (diff) | |
parent | 2ebe7e342cc56486e28c28f6a7a2678f67778229 (diff) | |
download | compcert-kvx-9b6758f42ba80caed80b6f25371140a45cc88340.tar.gz compcert-kvx-9b6758f42ba80caed80b6f25371140a45cc88340.zip |
Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
-rw-r--r-- | README.md | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -31,7 +31,8 @@ The people responsible for this version are ## 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. +* [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) |