Direction de recherche : Michèle SORIA

Co-encadrement : PESCHANSKI Fréderic

Analyse statique de programmes concurrents et dynamiques

Les programmes et systèmes informatiques ont un besoin grandissant d'accès à des ressources dynamiques : moyens de communication alloués puis détruits à volonté, connexions à des bases de données, espaces mémoire, ressources de calcul, etc. On s'intéresse dans ce travail aux analyses qualitatives ainsi que quantitatives de telles ressources pour les systèmes concurrents et dynamiques.
Notre étude repose sur le langage de programmation prototype Piccolo, développé dans le cadre de cette thèse. Il permet de programmer des machines multi-coeurs, par le moyen de constructions basées sur l'algèbre de processus pi-calcul. Les programmes Piccolo sont alors très proches de modèles exprimés en pi-calcul, qui peuvent être analysés au moyen d'outils de vérification automatique.
Dans ce travail, nous abordons tout d'abord les difficultés liées à la construction d'espaces d'états explicites pour les processus en pi-calcul. Etant donné l'expressivité du formalisme, il s'agit d'un problème complexe, en particulier si l'on considère le cas des sémantiques à transitions étiquetées. Nous proposons un nouvel algorithme (ainsi qu'un outil prototype) basé sur les transitions symboliques plutôt que sur la sémantique précoce. Nous constatons alors expérimentalement une importante réduction des espaces d'états ainsi générés. Nous introduisons également une variante du pi-calcul, nommée slice-pi, qui fournit un intermédiaire entre une sémantique à transitions étiquetées et une sémantique de réductions. Elle permet à la demande d'"ouvrir" certaines parties d'un système tout en conservant "fermées" les autres parties.
La partie centrale de cette thèse concerne le développement d'une boîte à outils algorithmiques pour l'analyse de ressources pour les systèmes concurrents et dynamiques. Ce framework est fondé, au niveau théorique, sur un nouveau modèle d'automates, les nu-automates, qui sont une variantes des automates à mémoire finie. Ils permettent de modéliser le comportement des systèmes du point de vue de leur utilisation de ressources. Nous montrons comment construire un nu-automate depuis un modèle en pi-calcul, ou en slice-pi, mais leur usage n'est pas limité à ces applications. Sur ce socle théorique, nous développons des algorithmes pour l'analyse quantitative des ressources dans les nu-automates, et donc dans les systèmes qu'ils modélisent. En particulier, nous introduisons le ramasse-miettes omniscient (OGC) qui permet de calculer une borne minimale, au pire cas, pour la consommation en ressources d'un système. Un outil prototype a été développé afin d'évaluer les algorithmes d'analyse en pratique.

Publications 2014-2016

• 2016
  • A. Deharbe : “Analyse statique de programmes concurrents et dynamiques”, soutenance de thèse, soutenance 21/09/2016, direction de recherche Soria, Michèle, co-encadrement : Peschanski, Fréderic (2016)
• 2014
  • A. Deharbe, F. Peschanski : “The Omniscient Garbage Collector : a Resource Analysis Framework”, ACSD 2014 - 14^th International Conference on Application of Concurrency to System Design, La Marsa, Tunisia, pp. 102-111, (IEEE) (2014)
  • A. Deharbe, F. Peschanski : “The Omniscient Garbage Collector: a Resource Analysis Framework”, (2014)