Preuves formelles basées sur des scenarios pour le logiciel concurrent – SCEPROOF

Les logiciels modernes utilisent de plus en plus la programmation concurrente afin d'exploiter les avantages de performances offerts par les architectures multicœurs. La programmation concurrente est cependant notoirement difficile et des bogues de concurrence existent même dans le code écrit par les programmeurs les plus expérimentés. Par conséquent, les chercheurs ont développé des techniques de raisonnement mathématique, dans l'espoir que des preuves pourraient être utilisées pour résoudre ce problème. Malheureusement, de nombreuses techniques de preuve basées sur la logique telles que le rely-guarantee, Owicki-Gries, etc. s'en remettre à l'utilisateur pour fournir des invariants complexes souvent peu intuitifs. En revanche, les concepteurs d'algorithmes de la communauté informatique distribuée fournissent fréquemment des arguments de style plus opérationnel pour la correction de leurs implémentations, qui se concentrent sur les descriptions de scénarios d'entrelacement clés, mais qui se généralisent à un nombre illimité de threads.

Dans ce projet, nous allons combler cette lacune et élever le raisonnement basé sur des scénarios d'arguments intuitifs à des arguments formellement rigoureux qui sont accessibles aux programmeurs et même automatiquement dérivés du code source.

Notre objectif est de développer des techniques fondamentales, des algorithmes et des outils automatisés, démontrant que le raisonnement basé sur des scénarios peut être rigoureux, mais aussi accessible aux programmeurs de tous les jours. Nous formaliserons les scénarios comme, ce que nous appelons, le quotient d'exécution d'un programme, qui capture un petit ensemble d'exécutions entrelacées représentatives qui se généralisent néanmoins --- via la commutativité --- à l'ensemble de toutes les exécutions, même avec un nombre illimité de threads et un espace infini d'états. Nous montrerons que ces quotients peuvent être décrits succinctement dans un langage convenable ; qu'il est possible de dériver automatiquement des quotients directement à partir du code source ; et que les programmeurs peuvent utiliser ces dérivations et les interroger pour mieux comprendre les comportements concurrents de leurs implémentations. Les principales composantes de ce projet seront:
- Établir des bases formelles pour les quotients d'exécution pour un raisonnement basé sur des scénarios.
- Concevoir des langages pour représenter abstraitement des quotients de manière compacte et compréhensible.
- Systématiser le processus de preuve pour montrer qu'une telle abstraction couvre toutes les exécutions possibles du programme, par de nouveaux schemas d'induction combinés avec le raisonnement sur la commutativité.
- Concevoir des algorithmes d'analyse de programme pour dériver automatiquement des abstractions de quotient directement à partir du code source.
- Développer et publier des outils qui automatisent la synthèse des quotients.
- Montrez que des quotients peuvent être fournis et même automatiquement synthétisés pour des programmes concurrents importants tels que des serveurs Web ou des serveurs de base de données.

Nos travaux déboucheront sur des outils de vérification automatisés de logiciels concurrents utilisables par des programmeurs, sans avoir besoin de connaissances en méthodes formelles. Nos nouvelles abstractions et algorithmes élèveront également les arguments de correction informels pour les objets concurrents sur une base formelle. Le projet rendra la vérification plus accessible et, grâce à notre plaidoyer dans le milieu universitaire et dans l'industrie, conduira à l'adoption et, en fin de compte, à des logiciels concurrents plus sûrs.