L'analyse statique de programmes consiste à obtenir automatiquement des propriétés vraies de toutes les exécutions possibles d'un programme : par exemple, prouver qu'on ne va jamais accéder à la mémoire via un pointeur nul, et qu'on ne va pas provoquer de dépassement arithmétique. L'analyse statique par interprétation abstraite est une des approches possibles, notamment utilisée dans des outils industriels comme PolySpace Verifier (développé près de Grenoble), Astrée (dont l'encadrant D. Monniaux était co-développeur) et Absint aIT (auquel l'encadrante C. Maïza a contribué des méthodes). Les utilisateurs de ce type de méthodes sont principalement les développeurs de logiciels embarqués critiques (contrôle-commande d'avions, etc.).
Un analyseur par interprétation abstraite va chercher à calculer des invariants, par exemple que la variable x à la ligne 35 est forcément comprise entre -10 et 10, ou encore que le vecteur (x,y,z) appartient à un certain polyèdre convexe. L'approche classique est de calculer une suite croissante d'objets (p.ex. des polyèdres convexes), ultimement stationnaire vers un invariant. Il faut parfois beaucoup d'itérations, et parfois aussi les invariants calculés sont trop gros pour impliquer les propriétés désirées (p.ex. si on borne x entre -10 et 10, on n'arrive pas à prouver que 1/x ne provoque pas de division par zéro). La recherche en analyse statique vise donc à produire des algorithmes plus rapides et/ou donnant des résultats plus fins.
T. Gawlitza et D. Monniaux ont récemment publié un algorithme mêlant interprétation abstraite et bounded model checking (une autre technique d'analyse). Cet algorithme n'utilise cependant pas le schéma usuel d'itérations en interprétation abstraite, mais plutôt une méthode inspirée de la théorie des jeux, la policy iteration. Elle n'a cependant pas été implémentée en vraie grandeur, et il reste une foule de problèmes à régler avant de pouvoir prétendre qu'elle est vraiment utilisable.
L'objet du stage est donc :
Implémenter la méthode proposée. On pourra s'appuyer sur un outil, déjà développé dans l'équipe, qui transforme des fragments de code en formules logiques.
L'expérimenter
Constater les insuffisances
Remédier à celles-ci
L'analyse statique de programmes consiste à obtenir automatiquement des propriétés vraies de toutes les exécutions possibles d'un programme : par exemple, prouver qu'on ne va jamais accéder à la mémoire via un pointeur nul, et qu'on ne va pas provoquer de dépassement arithmétique. L'analyse statique par interprétation abstraite est une des approches possibles, notamment utilisée dans des outils industriels comme PolySpace Verifier (développé près de Grenoble), Astrée (dont l'encadrant D. Monniaux était co-développeur) et Absint aIT (auquel l'encadrante C. Maïza a contribué des méthodes). Les utilisateurs de ce type de méthodes sont principalement les développeurs de logiciels embarqués critiques (contrôle-commande d'avions, etc.).
Un analyseur par interprétation abstraite va chercher à calculer des invariants, par exemple que la variable x à la ligne 35 est forcément comprise entre -10 et 10, ou encore que le vecteur (x,y,z) appartient à un certain polyèdre convexe. L'approche classique est de calculer une suite croissante d'objets (p.ex. des polyèdres convexes), ultimement stationnaire vers un invariant. Il faut parfois beaucoup d'itérations, et parfois aussi les invariants calculés sont trop gros pour impliquer les propriétés désirées (p.ex. si on borne x entre -10 et 10, on n'arrive pas à prouver que 1/x ne provoque pas de division par zéro). La recherche en analyse statique vise donc à produire des algorithmes plus rapides et/ou donnant des résultats plus fins.
Une approche récemment suggérée (voire p.ex. les travaux de l'équipe d'E. Goubault) consiste à remplacer les itérations évoquées ci-dessus par une recherche de solution d'un problème d'optimisation sous contraintes. Cette approche n'a cependant pas été implémentée en vraie grandeur, et il reste une foule de problèmes à régler avant de pouvoir prétendre qu'elle est vraiment utilisable.
L'objet du stage est donc :
Implémenter la méthode proposée
L'expérimenter
Constater les insuffisances
Remédier à celles-ci
L'optimisation sous contraintes est un classique de la recherche opérationnelle : étant donné une liste de contraintes, maximiser une fonction objectif. Par exemple, si les contraintes sont des inégalités linéaires et la fonction objectif une forme linéaire, cela s'appelle de la programmation linéaire. Et si on veut pouvoir imposer non seulement une conjonction de contraintes, mais plutôt une formule logique quelconque, avec aussi bien opérateurs « ou » que « et » ?
Les deux application envisagées au sein du laboratoire VERIMAG concernant l'analyse statique de programmes. L'analyse statique de programmes consiste à obtenir automatiquement des propriétés vraies de toutes les exécutions possibles d'un programme : par exemple, prouver qu'on ne va jamais accéder à la mémoire via un pointeur nul, et qu'on ne va pas provoquer de dépassement arithmétique. L'analyse statique par interprétation abstraite est une des approches possibles, notamment utilisée dans des outils industriels comme PolySpace Verifier (développé près de Grenoble) et Astrée (dont l'encadrant D. Monniaux était co-développeur). Les utilisateurs de ce type de méthodes sont principalement les développeurs de logiciels embarqués critiques (contrôle-commande d'avions, etc.). Plusieurs problèmes d'analyse statique peuvent se ramener à de l'optimisation sous contraintes :
Recherche d'intervalles de variation de variables
Calcul de temps d'exécution dans le pire cas (WCET). (L'encadrante C. Maïza a notamment contribué des méthodes de calcul de WCET utilisées dans l'outil industriel Absint aiT.)
On peut réduire des problèmes de preuves de théorèmes mathématiques sur les polynômes à des problèmes d'optimisation convexe. Ceci permet d'automatiser certaines recherches de preuves qui sinon seraient extrêmement laborieuses à la main. Cependant, les mathématiciens s'émeuvent de ce que l'on prétende prouver des résultats mathématiques à l'aide de calculs algorithmiques compliqués, qui plus est en virgule flottante. Récemment, des informaticiens et des mathématiciens se sont attelés à produire des résultats de preuve plus précis. Thomas Hales, l'auteur de la preuve informatisée de la conjecture de Kepler, a lancé le projet Flyspeck visant à fournir des preuves formelles pour les lemmes obtenus par calcul informatique.
Par exemple, pour montrer qu'un polynôme est partout positif ou nul, on va chercher à le représenter comme une somme de carrés de polynômes à coefficients rationnels ou, à défaut, un quotient de deux telles sommes de carrés, et réduire cela à un problème numérique de programmation semi-définie. Malheureusement, il se produit alors en général un phénomène de dégénérescence géométrique qui empêche une application directe des techniques numériques.
D. Monniaux et P. Corbineau ont récemment publié une technique permettant de se sortir de ce phénomène, et l'a implémentée. Cette implémentation est cependant un peu naïve (donc inefficace) et mériterait d'être testée sur plus d'exemples. Sur un plan plus théoriques, certains « facteurs d'échelle » assurant la convergence pratique de la méthode ont été réglés à des valeurs arbitraires, et il faudrait essayer de préciser des conditions sur ces facteurs.
Le but du stage est d'étudier des améliorations théoriques et pratiques à cette méthode.
Co-encadrement avec Claire Burguière-Maïza.
De nombreux dispositifs sont actuellement pilotés par des calculateurs informatiques, y compris dans les transports (aviation, trains...). Certains de ces systèmes sont critiques : une panne peut entraîner des pertes humaines ; aussi doit-on garantir leur bon fonctionnement en toute circonstances. Ainsi, si le système est censé réaliser une action en moins de 1 ms, par exemple, il va falloir garantir que le calculateur va en toutes circonstances mettre moins de 1 ms pour effectuer des calculs. Or, sur les microprocesseurs actuels, calculer le temps d'exécution dans le pire cas (WCET) est très difficile, en raison de la présence de dispositifs complexes destinés à améliorer les performances : caches, pipelines, exécution spéculative... On doit donc se contenter de bornes supérieures du WCET obtenues par des analyses délicates et pas forcément très précises.
Les choix d'architecture et de paramétrage de ces dispositifs sont faits pour assurer de bonnes performances moyennes sur des applications pas forcément très représentatives des applications critiques. Ainsi, les PowerPC 755 sont utilisés dans des applications avioniques et spatiales... mais ont été optimisés pour les PowerMac G3. Les accès mémoires réalisés par Photoshop et MacOS X ne sont sans doute pas représentatifs de ces applications critiques !
Une autre différence entre les applications courantes (bureautique...) et les applications embarquées critiques est que dans les premières, on ne maîtrise pas le système, alors que dans les secondes on maîtrise tout, y compris le placement mémoire. Il est possible que les comportements désavantageux des systèmes de cache les plus simples puissent être évités par un placement en mémoire judicieux.
Il s'agit dans ce stage :
D'évaluer les conséquences des choix de l'architecture de cache sur le WCET pour des programmes de type contrôle-commande critique, par une analyse statique sur des modèles d'accès mémoire et/ou à l'aide d'un émulateur de processeur.
D'examiner les possibilités de placement astucieux en mémoire pour éviter les mauvais comportements des caches, ou plutôt obtenir de meilleures bornes supérieures par l'analyse de WCET.
D'étudier l'éventuelle automatisation de ces placements.
Co-encadrement avec Claire
Burguière-Maïza.
Les programmes informatiques qui
pilotent des systèmes critiques comme les avions ou les centrales
nucléaires sont soumis à des normes sévères. Ainsi, si une
boucle de contrôle doit s'exécuter tous les 100e de seconde,
l'industriel doit démontrer aux autorités que le corps de cette
boucle s'exécute effectivement au maximum en un 100e de seconde. On
doit ainsi justifier de bornes dans le pire cas sur le temps
d'exécution (Worst case execution time ou WCET), ce qui nécessite
d'avoir des informations assez précises sur les contenus possibles
des caches du microprocesseur (une lecture de données qui ne sont
pas dans la mémoire cache prend un temps considérablement plus long
qu'une lecture depuis le cache).
Des outils de model-checking
tels que NuSMV permettent de calculer explicitement, mais sous une
forme compacte en mémoire, l'ensemble des états accessibles d'un
système à état fini. L'objet du stage est la traduction de code
assembleur (ou, à défaut, de code LLVM) vers son action sur le
cache d'instructions, afin d'être analysé par des outils de
model-checking.
Suivant la progression du stage, la
modélisation pourra inclure d'autres éléments, par exemple le
pipe-line du processeur.
L'élimination de quantificateurs consiste à transformer une formule logique comprenant des quantificateurs, telle que
Il est possible d'éliminer algorithmiquement les quantificateurs dans l'arithmétique linéaire sur les réels ou dans les entiers (même si c'est, comme d'habitude, plus difficile sur les entiers). Malheureusement, les algorithmes et implémentations existantes sont encore trop lents pour de nombreuses utilisations.
David Monniaux et Nikolaj Bjørner ont publié, respectivement à CAV 2010 et IJCAR 2010, deux articles sur l'élimination de quantificateurs dans l'arithmétique linéaire. Ils ont depuis travaillé sur un algorithme unifié, qui n'est pour le moment qu'à l'état de brouillon. Il s'agirait d'améliorer et d'implémenter cet algorithme.
Une familiarité avec le langage Caml serait utile pour ce stage.
L'analyse statique permet de prouver qu'un programme ne provoque pas de dysfonctionnements. Ainsi, des outils comme PolySpace Verifier ou Astrée sont utilisés dans le développement d'applications critiques (aéronautique...). Pourtant, l'analyseur lui-même ne pourrait-il pas être buggué ? Quelle confiance avoir en ses résultats ?
Le projet VERASCO vise à développer un analyseur statique certifié à brancher sur le compilateur certifié CompCert. Il s'agit, dans ce stage, de chercher à comprendre comment certifier certaines des opérations de cet analyseur, notamment les calculs sur contraintes numériques.
Une expérience préalable avec des outils comme Coq et des connaissances en optimisation convexe (programmation linéaire) sont souhaitables.