Représentations Intermédiaires et Sémantiques de la Concurrence pour les Compilateurs Vérifiés – DISCOVER

L'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 nécessité pour aboutir à des techniques de preuves qui passent à l'échelle, en taille et en difficultéde preuve.

Le middle-end CompCertSSA, basé sur le compilateur C vérifié CompCert est notre plateforme privilégiée d'expérimentation. Nous y avons développé et intégré plusieurs de nos résultats portant sur les techniques de preuves d'optimisation sur la forme SSA : un test rapide et vérifié de dominance, propriété sémantique de non-interférence entre certaines variables d'un programme SSA, qui permet des optimisations importantes (réutilisation de variables) lors de la destruction de la forme SSA, et une boîte à outils de lemmes pour raisonner à propos de la relation de dominance par induction sur les chemins d'exécutions du programme.
Nous avons réalisé une preuve formelle pour un Garbage Collector Concurrent, programmé dans une représentation intermédiaire fournissant des mécanismes d'abstraction sur l'environnement d'exécution. La preuve est conduite dans une logique de programme Rely-Guarantee que nous avons conçue pour être concise, automatisable, et incrémentale.
Nous avons défini des modèles sémantiques formels pour des représentations intermédiaires plus souples que des graphes de flot de contrôle (Sea-of-Nodes et Monadic Gated SSA), qui abstraient certaines dépendances non essentielles entre les instructions du programme.

Nous avons atteint un nombre significatif de résultats sur les représentations intermédiaires utilisées par les compilateurs optimisants, ainsi que sur des outils formels pour raisonner à propos de la correction fonctionnelle de composants de l'environnement d'exécution de programmes haut niveau concurrents. En particulier, la preuve du Garbage Collector concurrent est un résultat important. La formalisation de Sea-of-Nodes est aussi une brique importante pour la construction de modèles sémantiques supportant à la fois des optimisations de code agressives, mais aussi des principes de preuve qui restent structurés par la représentation du programme.
Nous envisageons que cette étude sémantique, ainsi que celle de Monadic Gated SSA, étendue à des instructions de manipulation mémoire, mènent à une compréhension plus profonde des relaxations mémoire observables qui sont induites par les optimisations réalisées à la compilation.

- Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, et al.. Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology. Journal of Automated Reasoning, Springer Verlag, 2018
- Delphine Demange, Yon Ferna´ndez de Retana, David Pichardie. Semantic reasoning about the sea of nodes. CC 2018 - 27th International Conference on Compiler Construction, Feb 2018, Vienna, Austria.
- Yannick Zakowski, David Cachera, Delphine Demange, David Pichardie. Verified Compilation of Linearizable Data Structures: Mechanizing Rely Guarantee for Semantic Refinement. SAC 2018 - The 33rd ACM/SIGAPP Symposium On Applied Computing, Apr 2018, Pau, France.
- Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, et al.. Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology. ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil.
- Delphine Demange, Yon Fernandez de Retana, Mechanizing conventional SSA for a verified destruction with coalescing. 25th International Conference on Compiler Construction, Mar 2016, Barcelona, Spain.
- Delphine Demange, David Pichardie, Léo Stefanesco. Verifying Fast and Sparse SSA-based Optimizations in Coq. 24th International Conference on Compiler Construction, CC 2015, 2015, London, United Kingdom.
- Sandrine Blazy, Delphine Demange, David Pichardie. Validating Dominator Trees for a Fast, Verified Domainance Test. Dominance Test. Interactive Theorem Proving, Aug 2015, Nanjing, China.
- Gurvan Cabon, David Cachera, David Pichardie. An extended Buffered Memory Model with Full Reorderings. Reorderings. FtFjp - Ecoop workshop, Jul 2016, Rome, Italy.
- Yon Fernandez de Retana. Vers la compilation vérifiée de Sea-of-Nodes : propriétés et raisonnement sémantiques. Manuscrit de thèse, Université Rennes 1, 2018. Français.

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.