Sujet de stage 2018 – Utiliser la compilation pour aider la vérification formelle

Contact

Responsable : Emmanuelle Saillard
Téléphone : 05.24.57.41.24
Courriel :
emmanuelle.saillard@inria.fr

Ce stage est en collaboration avec l’Inria Rennes.

Présentation du sujet

Comprendre et analyser le comportement d’une application HPC est un travail difficile. Il existe des initiatives, comme l’Inria Project Lab HAC-SPECIS, qui vise à trouver des solutions pour aider les programmeurs à corriger et optimiser leurs applications. Une des pistes envisagées est de simuler l’exécution d’un programme afin de prédire son comportement pour une valeur fixée des données d’entrées [1]. SimGrid est un outil qui utilise cette méthode pour détecter des erreurs dans les applications distribuées. Il est basé sur une approche dite de vérification formelle dynamique.

La vérification formelle permet de prouver la correction d’un programme, modélisé sous forme mathématique pour exprimer toutes ses exécutions possibles. Cette modélisation vaut pour un jeu de valeurs d’entrée et est conforme à une spécification (propriété qui sert de référence pour la vérification). La difficulté de cette approche est de représenter tous les états d’exécution du programme.

Par le biais d’une analyse dite statique, le compilateur est en mesure de fournir des informations relatives au comportement d’un programme. C’est par exemple le cas des analyses de flot de données, qui ont la possibilité de détecter si à partir d’un point du programme, la valeur d’une variable sera utilisée. Ce genre d’analyse est souvent utilisé pour la détection d’erreurs dans un programme mais peut également aider la vérification formelle en réduisant l’espace d’états à considérer.

L’objectif de ce stage est d’aider la vérification formelle à l’aide de la compilation. Deux pistes sont possibles :

  1. Développement d’une analyse statique pour détecter toutes les variables non initialisées (quelque soit leur type) d’un programme afin de les initialiser
    Ce travail présente deux avantages : (1) Il complémente les méthodes ad hoc développées dans SimGrid [2]. Il est possible de réduire l’espace d’états en ré-initialisant des variables dont la valeur n’a pas d’importance (parce qu’elles seront ré-affactées avant leur utilisation). (2) L’utilisation d’une variable non initialisée est une erreur de programmation fréquente. Cette erreur peut provoquer des résultats incorrects, des accès à des mémoires indéterminées ou nulles ou encore conduire à des comportements imprévisibles du programme. Détecter ces variables éviterait l’apparition de telles erreurs.
  2. Développement d’une analyse statique pour récupérer des informations de typage sur les données stockées dans le tas
    En cas d’aliasing des blocs du tas (accès à une même mémoire), on souhaite obtenir les différents types utilisés, de façon à simplifier l’introspection automatique de la mémoire du processus lors de l’exécution.

Dans les deux cas, l’analyse sera développée dans le compilateur LLVM sous forme d’une passe [3].

Mot-clés : Calcul haute performance, vérification formelle, LLVM

Commentaires

Des connaissances en compilation sont souhaitables pour aborder le sujet dans de bonnes conditions.

Références

Équipe Storm: https://team.inria.fr/storm

[1] Simulating MPI applications : the SMPI approach, Augustin Degomme, Arnaud Legrand, Georges Markomanolis, Martin Quinson, Mark Stillwell, et Frédéric Suter.
[2] System-level State Equality Detection for the Formal Dynamic Verification of Legacy Distributed Applications, Marion Guthmuller, Martin Quinson, et Gabriel Corona.
[3] https ://llvm.org/docs/WritingAnLLVMPass.html

Comments are closed.