Vérification d'applications multithreadées
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) 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]. La mise au point de tels outils pose cependant plusieurs difficultés.
La première, d'ordre algorithmique, 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.
Une seconde difficulté est d'ordre technique. Contrôler finement l'exécution du système vérifié demande de combiner des techniques de virtualisation niveau OS, d'interception d'exécution et d'inspection de la mémoire. Un outil de vérification dynamique peut être vu comme une machine virtuelle capable d'inspecter le programme comme gdb, puis d'influer automatiquement sur l'exécution. Certaines techniques sont inspirées d'attaques de sécurité.
Mc SimGrid est un tel programme [McSimGrid17], capable de vérifier des propriétés de sûreté et de vivacité sur des programmes écrits en C, C++ ou Fortran avec l'interface de communication MPI, prédominante dans le domaine du calcul intensif. Les techniques de réduction de l'espace d'états proposées sont relativement classiques sans être à la pointe de l'état de l'art.
L'objectif de ce stage est d'apporter une contribution à ce logiciel. Deux sujets sont proposés, mais le stagiaire devra choisir l'un d'entre eux au préalable.
[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
Objectifs du stage
Mc SimGrid est actuellement incapable de vérifier des applications multithreadées utilisant l'interface pthread, car l'outil ne "voit" pas les actions liées aux threads. On peut rendre visibles les fonctions impliquées [sThread], mais observer les accès mémoire du programme reste plus difficile. Une piste serait d'augmenter un outil de debug dédié à ces applications comme ThreadSanitizer [TSan]. Interfacer ces outils avec Mc SimGrid permettrait de réaliser une exploration exhaustive d'applications multithreadées, en utilisant leurs capacités d'observation.
Ces outils instrumentent tous les accès mémoire de l'application, et déterminent si une zone est accédée par plusieurs threads de façon concurrente sans protection par un mutex. L'approche suivie par Helgrind est de clusteriser les zones mémoires proches [Helgrind], tandis que TSan travaille par sampling des accès mémoire [TSan]. Combinée à l'exploration exhaustive offerte par Mc SimGrid, cette capacité d'analyse s'avèrerait particulièrement utile pour trouver des conditions de compétition dans les programmes analysés.
Ce sujet est relativement technique et sa mise en oeuvre nécessite une bonne compréhension des outils impliqués (SimGrid, LLVM). L'objectif est de réaliser un outil utilisable en pratique pour vérifier à la fois des applications multithreadées et des applications distribuées, ce qui serait une première.
[sThread] Sthread: In-Vivo Model Checking of Multithreaded Programs. Cooperman, Quinson. The Art, Science, and Engineering of Programming, 2020. https://hal.inria.fr/hal-02449080
[TSan] Dynamic race detection with LLVM compiler, K Serebryany et Al. Conference on Runtime Verification (RV'11). https://research.google/pubs/pub37278.pdf
[Helgrind] Efficient Data Race Detection for C/C++ Programs Using Dynamic Granularity, Young Wn Song et Al. 28th International Parallel and Distributed Processing Symposium (IPDPS'14) https://ieeexplore.ieee.org/abstract/document/6877300