Projet ANR-14-CE28-0004 – DISCOVER : Représentations Intermédiaires et Sémantiques de la Concurrence pour les Compilateurs Vérifiés
Programme : Sciences et technologies logicielles (DS0704)
Année de financement : 2014
Coordinateur du projet : Madame Delphine Demange (Institut de recherche en informatique et systèmes aléatoires / Université de Rennes 1)
Partenaires : Laboratoire public
Montant : 301649.0 euros
Date de début : 2014
Durée : 60 mois
Résumé : DISCOVERDevising Intermediate representations and Semantics of COncurrency for Verified compilERs
Enjeux et objectifsLe projet DISCOVER vise à tirer parti des avancées récentes en vérification formelle dans les assistants de preuve pour concevoir, mettre en oeuvre et vérifier les techniques de compilation utilisées pour les langages de programmation de haut-niveau concurrents et managés. Le but ultime de DISCOVER est de concevoir de nouveaux formalismes et techniques de preuve capables de passer à l'échelle de la preuve de correction mécanisée d'un compilateur optimisant, repoussant ainsi les frontières de l'état de l'art en compilation vérifiée.
Méthode et approcheL'approche particulière que nous employons dans le projet DISCOVER est la conception et formalisation de mécanismes d'abstraction appropriés, en se basant principalement sur des techniques de langages de programmation, et de représentations intermédiaires, pour la conception de modèles sémantiques, et la vérification mécanisée de programmes et de transformations de programmes. Nous soutenons que c'est une necessité pour aboutir à des techniques de preuves qui passent à l'échelle (en taille et en difficulté de preuve).
Résumé de la soumission : La concurrence à mémoire partagée est omniprésente dans les logiciels et les systèmes matériels multiprocesseurs modernes, mais ce paradigme de programmation et d'exécution reste un véritable défi. Les multiprocesseurs standards (x86, Power, ARM etc) et langages de programmation traditionnels (C, C++, Java) ont des modèles de mémoire subtiles et faiblement cohérents, qui exposent des comportements complexes et contre-intuitifs. Cette complexité est due à l'agressivité des optimisations des compilateurs et matérielles (executions out-of-order), et rend l'activité de programmation particulièrement propice aux erreurs. Le besoin d'établir la correction des programmes est donc accru.Dans ce contexte, les techniques traditionnelles de vérification, telles qu'utilisées dans l'industrie des systèmes critiques ne sont pas applicables: l'inspection manuelle des codes sources et binaires est difficilement envisageable, et le test des applications multithread est particulièrement difficile, car les relaxations exposées par les modèles de mémoire faibles ne sont presque jamais reproductibles. Ainsi, la preuve statique de correction de programmes (par analyse statique, preuve déductive, model checking) apporterait de plus forte garanties, de part sa couverture exhaustive des exécutions possibles. Les récents progrès en formalisation de modèles de mémoire faibles sont considérables, et des techniques de vérification, basées sur des logiques de programmes, commencent même à émerger. Mais ces outils concernent le plus souvent le programme source, et une mauvaise compilation (un bug dans le compilateur) pourraient invalider ces garanties durement acquises. Comparée au cas séquentiel et les avancées majeures de Leroy et al. dans le cadre du compilateur C vérifié CompCert, la compilation vérifiée pour la concurrence à mémoire partagée reste un problème largement ouvert. En effet, outre les défis que pose la concurrence en vérification de transformation de programmes, des composants runtime peuvent aussi s'exécuter en concurrence avec les threads de l'application, améliorant la performance, mais au prix d'une complexité supplémentaire. Leurs interactions sont généralement régies par du code injecté par le compilateur, pour tracer et mettre à jour des informations utiles à l'exécution du programme (allocation mémoire, barrières d'écriture et de lecture, barrières mémoire etc). Ces idiomes sont très sophistiqués, peuvent contenir des data-races (i.e. des accès mémoires simultanés conflictuels à la mémoire partagée), et leur correction fonctionnelle doit être assurée dans un environnement sujet à des transformations de programmes.Le projet DISCOVER vise à tirer parti des avancées récentes sur la vérification formelle dans les assistants de preuve pour concevoir, mettre en oeuvre et vérifier les techniques de compilation utilisées pour les langages de programmation de haut-niveau concurrents et managés. Le but ultime de DISCOVER est de concevoir de nouveaux formalismes et techniques de preuve capables de passer à l'échelle de la preuve de correction mécanisée d'un compilateur optimisant, repoussant ainsi les frontières de l'état de l'art en compilation vérifiée.À la lumière de travaux récents en compilation optimisante pour les langages de haut-niveau, les représentations intermédiaires (IR) à base de graphes de flot de contrôle semblent trop rigides. Ces analyses et optimisations travaillent sur des IRs plus abstraites, à base de dépendances de données et de contrôle. Un exemple phare est la forme la sea-of-nodes, qui a d'ailleurs mené à la complexité du modèle de mémoire Java. DISCOVER propose d'aborder le problème de la compilation vérifiée pour la concurrence à mémoire partagée avec une approche résolument basée langages, et d'explorer la formalisation d'IRs adéquates et des techniques de preuve de correction associées.
Résultats : - Technique de preuve basée sur la dominance. Nous avons proposé un cadre générique de preuve formelle pour la vérification de correction sémantique d'optimisations sur la forme SSA. Ce cadre guide le processus de vérification en factorisant les étapes (et propriétés importantes) d'un raisonnement basé sur les régions dominées (dans un graphe de flot de contôle SSA), et fournit une boîte à outil de lemmes pour raisonner à propos de dominance par induction sur les chemins d'executions.
- Propriétés essentielles pour les optimisations de programmes. Les implémentations modernes d'optimisations reposent sur l'utilisation de propriétés structurelles et sémantiques importantes des représentations de programmes. Plusieurs de nos résultats montrent que ces techniques à l'état de l'art ont toute leur place dans un compilateur vérifié. Nous avons conçu un test rapide et vérifié de dominance, et nous avons formalisé (et prouvé) une propriété sémantique de non-interference entre certaines variables d'un programme SSA, qui permet des optimisations non négligeables (réutilisation de variables) lors de la destruction de la forme SSA.
- Le middle-end CompCertSSA, basé sur le compilateur C vérifié CompCert est notre plateforme d'expérimentation, sur laquelle nous basons, et dans laquelle nous avons intégré, les résultats mentionnés plus haut.
Perspectives : A ce point du projet, la prochaine étape est de d'étudier des représentations de programmes basées sur les dépendances de données et de contrôle, plutôt que sur de simples graphes de flôts de contrôle. Nous aimerions formaliser leur sémantique de sorte à exprimer élégamment les (in)-dépendances des instructions d'accès mémoire, et ainsi espérer capturer certaines des relaxations exhibées lors des optimisations de code existantes.
En parallèle, nous mettons également au point des logiques de programmes, vérifiées en Coq, et adaptées à la vérification d'implémentations de service runtimes servant à la mise en oeuvres des langages haut-niveaux concurrents.
Publications et brevets : - Mechanizing Conventional SSA for a Verified Destruction with Coalescing. D. Demange, Y. Fernandez de Retana. CC 2016.
- Verifying Fast and Sparse SSA-based Optimizations in Coq. D. Demange, D. Pichardie and L. Stefanesco. CC 2015.
- Validating Dominator Trees for a Fast, Verified Dominance Test. S. Blazy, D. Demange and D. Pichardie. ITP 2015.