Séminaire CLAP - 23/09/21
Le séminaire CLAP du 23 septembre de 10h15 à 12h15 portera sur le thème "compilation et verification". Le séminaire se fera en visio sur zoom (cf ci-dessous pour les info de connexion). Vous êtes également conviés à un café CLAP de 10h à 10h15 sur gather.town (https://gather.town/app/7giEyr3CTKAwe3Or/cafeCLAP). Les talks se feront en français.
Le planning est le suivant:
- 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%).
- 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.
Merci de nous contacter (à l’adresse emmanuelle.saillard@inria.fr) si vous souhaitez présenter vos travaux lors des prochains séminaires (21/10, 18/11 et 16/12). Les doctorants sont fortement encouragés à le faire
à bientôt,
Les responsables du GT CLAP
Kevin Martin, Ludovic Henrio, Frederic Dabrowski, Laure Gonnord & Emmanuelle Saillard
Participer à la réunion Zoom
https://u-bordeaux-fr.zoom.us/j/81969164370?pwd=YmcxYmFYMjRSMEpwYTJPUDBuTGhFZz09
ID de réunion : 819 6916 4370
Code secret : 440764
Une seule touche sur l’appareil mobile
+12532158782,,81969164370#,,,,*440764# États-Unis (Tacoma)
+13017158592,,81969164370#,,,,*440764# États-Unis (Washington DC)
Composez un numéro en fonction de votre emplacement
+1 253 215 8782 États-Unis (Tacoma)
+1 301 715 8592 États-Unis (Washington DC)
+1 312 626 6799 États-Unis (Chicago)
+1 346 248 7799 États-Unis (Houston)
+1 669 900 6833 États-Unis (San Jose)
+1 929 205 6099 États-Unis (New York)
ID de réunion : 819 6916 4370
Code secret : 440764
Trouvez votre numéro local : https://u-bordeaux-fr.zoom.us/u/kd09wkMTT2
Participer à l’aide d’un protocole SIP
81969164370@zoomcrc.com
Participer à l’aide d’un protocole H.323
162.255.37.11 (États-Unis (Ouest))
162.255.36.11 (États-Unis (Est))
213.19.144.110 (Amsterdam Pays-Bas)
213.244.140.110 (Allemagne)
Code secret : 440764
ID de réunion : 819 6916 4370
Date:
Jeudi, 23 Septembre, 2021