En attendant de pouvoir se retrouver en présentiel, nous vous proposons 4 séminaires CLAP virtuels d’ici la fin de l’année.
Jeudi 23 septembre 2021
Orateurs
-
- Cyril Six, Kalray
-
- Emmanuelle Saillard, Inria
Planning
-
- 10h-10h15 : café CLAP sur gather.town
Lien: https://gather.town/app/7giEyr3CTKAwe3Or/cafeCLAP
-
- 10h15-12h15 : séminaire sur zoom
10h20-11h00 – Cyril Six, Kalray
Titre: Introducing Basic-block and Superblock Scheduling in CompCert for a VLIW Processor
Résumé :
CompCert is the first commercial formally verified C compiler. Machine-checked with the Coq proof assistant, it ensures a property of semantic preservation by composing transformation passes, each having their own formal proof.
Because of the complexity involved in formally proving compiler optimizations, CompCert only features a limited number of them. The most advanced of those are constant propagation and common-subexpression elimination.
We introduced scheduling optimizations in CompCert, that are essential to have for in-order processors, and in particular VLIW targets. We performed basic-block scheduling after register allocation, superblock scheduling before register allocation, and we also introduced branch prediction, loop-invariant code motion, loop unrolling and loop rotation. These transformations are formally-verified using a posteriori verification and symbolic execution techniques.
Our optimizations can be used for many targets with little effort involved. We introduced these optimizations for the Kalray KV3 Coolidge VLIW core, the ARM Cortex A-53 in-order core and the Risc-V Rocket core. We measured the impact of these optimizations on these processors on benchmarks, including Polybench and TACLeBench. Thanks to our newly introduced optimizations, our version of CompCert is now only 16% slower (respectively 12% and 30%) than GCC -O2 on the KV3 (respectively A-53 and Rocket), instead of 50% (respectively 38% and 45%).
CompCert is the first commercial formally verified C compiler. Machine-checked with the Coq proof assistant, it ensures a property of semantic preservation by composing transformation passes, each having their own formal proof.
Because of the complexity involved in formally proving compiler optimizations, CompCert only features a limited number of them. The most advanced of those are constant propagation and common-subexpression elimination.
We introduced scheduling optimizations in CompCert, that are essential to have for in-order processors, and in particular VLIW targets. We performed basic-block scheduling after register allocation, superblock scheduling before register allocation, and we also introduced branch prediction, loop-invariant code motion, loop unrolling and loop rotation. These transformations are formally-verified using a posteriori verification and symbolic execution techniques.
Our optimizations can be used for many targets with little effort involved. We introduced these optimizations for the Kalray KV3 Coolidge VLIW core, the ARM Cortex A-53 in-order core and the Risc-V Rocket core. We measured the impact of these optimizations on these processors on benchmarks, including Polybench and TACLeBench. Thanks to our newly introduced optimizations, our version of CompCert is now only 16% slower (respectively 12% and 30%) than GCC -O2 on the KV3 (respectively A-53 and Rocket), instead of 50% (respectively 38% and 45%).
11h00-11h40 – Emmanuelle Saillard, Inria
Titre: PARCOACH, a tool that combines static and dynamic analyses to detect misuse of MPI communications.
Résumé :
The advent to exascale requires more scalable and efficient techniques to help developers to locate, analyze and correct errors in parallel applications. PARallel COntrol flow Anomaly CHecker (PARCOACH) is a framework that detects MPI collective errors using a static/dynamic analysis. The static phase studies the control- and data-flow of a program to detect potential errors while the dynamic phase uses compile-time information to verify the potential errors. Recently, PARCOACH has been extended to detect misuse of MPI nonblocking and persistent communications. The new analysis adds the detection of four new error classes related to these types of communications.
Informations utiles
- Plateforme : zoom
https://u-bordeaux-fr.zoom.us/j/81969164370?pwd=YmcxYmFYMjRSMEpwYTJPUDBuTGhFZz09
ID de réunion : 819 6916 4370
Code secret : 440764
- Contact : Emmanuelle Saillard, emmanuelle.saillard@inria.fr
Les prochains séminaires
- Dates des séminaires : 23/09, 21/10, 18/11 et 16/12
Organisateurs
- Kevin Martin, Université de Bretagne-Sud/Lab-STICC
- Emmanuelle Saillard, Inria
- Frédéric Dabrowski, Université d’Orléans
- Ludovic Henrio, CNRS