Vérification optimisée de systèmes distribués par décomposition de la relation d'indépendance

Contexte

Le model checking est une méthode formelle de vérification des systèmes informatiques basée sur l'exploration exhaustive de toutes les évolutions possibles d'un modèle du système à vérifier. Cette méthode est plus facile à utiliser qu'un assistant de preuve, qui demande à l'utilisateur d'inventer des objectifs intermédiaires quand l'objectif initial est hors de portée. La vérification formelle de logiciels (software model checking -- SMC) vise à utiliser les méthodes de model checking directement sur un logiciel à vérifier, sans modélisation préalable.

Cela laisse envisager des outils entièrement automatiques, capables de démontrer formellement des propriétés sur des programmes sans intervention de l'utilisateur, en testant de manière exhaustive les exécutions possibles du programme [CACM11].

Mc SimGrid est un tel programme [McSimGrid17], capable de vérifier des propriétés de sûreté sur des programmes écrits en C, C++ ou Fortran avec l’interface de communication MPI, prédominante dans le domaine du calcul intensif.

La mise au point de ces outils pose cependant de nombreux problèmes intéressants. Du point de vue algorithmique la difficulté réside dans l'explosion combinatoire qui résulte de l'exploration exhaustive de l'espace d'états du système: n processus séquentiels finis mis en parallèle ont un graphe d'état de taille exponentielle par rapport à la taille de chaque processus. Pire, la taille peut être infinie si les données (e.g. fifo, variables) sont non bornées. Cela rend souvent impossible en pratique l'exploration de systèmes réels même de taille modérée. Depuis quelques décennies, une recherche foisonnante vise à réduire cet espace d'états, en exploitant par exemple des propriétés de redondance, de symétrie, etc.

Par exemple, DPOR (dynamic partial ordering reduction) est une technique classique qui réduit l’espace d’états à explorer grâce au fait que deux événements causalement indépendants n’ont aucune influence mutuelle. On peut alors assurer une couverture exhaustive du graphe d’états sans explorer plusieurs exécutions du système ne différant que par l’ordre d’événements indépendants adjacents.

Objectif du stage

La littérature récente propose des méthodes extrêmement efficaces pour réduire la quantité de traces à explorer, tout en limitant le temps nécessaire pour calculer précisément la relation d’indépendance [ODPOR].

Ce projet de recherche vise à accélérer encore cette exploration DPOR, cette fois en raffinant progressivement la relation de dépendance (négation de l'indépendance) afin d'accélérer le calcul des traces à explorer, sans augmenter le nombre de ces traces.

Une première approche est de ne considérer initialement qu'une partie de cette relation (par exemple, seulement les dépendances des interactions entre deux acteurs donnés) afin de trouver rapidement les bugs qui existent dans cette première approximation rapide à explorer. Si cette approximation du système ne contient pas de bug caractérisable, on la raffinera pour construire des abstractions plus fines et plus lentes à construire, mais contenant progressivement plus de traces distinctes (mais moins de comportements), jusqu'à contenir exactement les comportements du système (les traces effectivement disctinctes).

Une seconde approche consiste à déterminer des parties du programme clairement indépendantes entre elles de par la sémantique du modèle de calcul, et exploiter les indépendances entre ces meta-blocs. Cette approche semble particulièrement prometteuse dans le cas des communications collectives du modèle MPI.

Travail attendu

Après une étude bibliographique complémentaire pour mieux cerner le problème, le·a stagiaire devra proposer des algorithmes d'exploration SMC optimisés par la décomposition de la relation de dépendance.

Il s'agira dans un premier temps de formaliser ces algorithmes pour démontrer leur correction, avant de les implémenter en pratique dans McSimGrid pour évaluer leur efficacité sur des cas réels.

Ce projet constitue donc une bonne application pratique de concepts théoriques.

Bibliographie

[CACM11] Formal Analysis of MPI-Based Parallel Programs, Gopalakrishnan et Al. Communication of the ACM, 2011. https://cacm.acm.org/magazines/2011/12/142546-formal-analysis-of-mpi-based-parallel-programs/fulltext

[McSimGrid17] Verifying MPI Applications with Mc SimGrid, T. A. Pham, T. Jéron, M. Quinson. Workshop on Software Correctness for HPC Applications (Correctness’17) https://hal.inria.fr/hal-01632421

[ODPOR] Optimal dynamic partial order reduction, Abdulla, Aronis, Jonsson, Sagonas - ACM Symposium on Principles of Programming Languages (POPL’14). https://user.it.uu.se/~bengt/Papers/Full/popl14.pdf