logo EDITE Sujets de doctorat

Analyse statique de programmes parallèles avec variables numériques

Résumé rédigé par
Directeur de thèse:
Doctorant: Vincent BOTBOL
Unité de recherche UMR 7606 Laboratoire d'informatique de Paris 6

Projet

L’analyse statique des programmes parallèles demande de résoudre plusieurs problèmes, tant théoriques que pratiques. Dans le cadre de cette thèse, nous étudierons la possibilité de faire des analyses statiques en considérant un modèle de systèmes concurrents suffisamment expressif pour permettre:

• le calcul arithmétique sur les entiers; • la communication entre processus de valeurs de type entier (variables partagées et/ou canaux de communication FIFO); • la création dynamique de processus; • le calcul des pires temps d’exécution grâce à une abstraction du matériel sur lequel s’exécutent les processus.

Un premier travail consistera a ` d ́efinir un algorithme efficace de calcul de point fixe sur ce mod`ele, en supposant dans un premier temps l’existence de primitives de synchronisation. Cet algorithme permettra de d ́efinir une analyse statique pour d ́eterminer la valeur des variables et le pire temps d’ex ́ecution du programme. Nous explorerons dans un second temps la possibilit ́e de relacher les conditions de synchronisation. Un second travail consistera `a utiliser ce mod`ele et les r ́esultats obtenus en lien avec la plateforme Frama-C (greffon Mthread) d ́evelopp ́ee par le CEA LIST. Ce travail demandera d’extraire des propri ́et ́es de concurrence `a partir de programmes C (annot ́es et/ou utilisant une biblioth`eque sp ́ecifique pour le parall ́elisme), et de traduire les r ́esultats de l’analyseur statique pour produire du code C lui aussi annot ́e. Nous traiterons ́egalement les programmes parall`eles ́ecrits dans un langage fonctionnel de type ML. Les r ́esultats de cette th`ese seront donc aussi bien th ́eoriques que pratiques. Ils permet- trons d’am ́eliorer les outils actuellement d ́evelopp ́es par les deux laboratoires qui accueilleront le doctorant (le CEA LIST et le LIP6).