Raffinement temporel et exécution parallèle dans un langage synchrone fonctionnel

Cédric Pasteur

Thèse de doctorat de l'université Paris 6, 2013


Nous nous intéressons dans ce manuscrit au langage ReactiveML, qui est une extension de ML avec des constructions inspirées des langages synchrones. L'idée de ces langages est de diviser l'exécution d'un programme en une suite d'instants logiques discrets. Cela permet de proposer un modèle de concurrence déterministe que l'on peut compiler vers du code séquentiel impératif. La principale application de ReactiveML est la simulation discrète, par exemple de réseaux de capteurs. Nous cherchons ici à programmer des simulations à grande échelle, ce qui pose deux questions: sait-on les programmer de façon simple et modulaire? sait-on ensuite exécuter ces programmes efficacement?
Nous répondons à la première question en proposant une extension du modèle synchrone appelée domaines réactifs. Elle permet de créer des instants locaux invisibles de l'extérieur. Cela rend possible le raffinement temporel, c'est-à-dire le remplacement d'une approximation d'un système par une version plus détaillée sans changer son comportement externe. Nous développons dans ce manuscrit la sémantique formelle de cette construction ainsi que plusieurs analyses statiques, sous forme de systèmes de types-et-effets, garantissant la sûreté des programmes dans le langage étendu.
Enfin, nous montrons également plusieurs implémentations parallèles du langage pour tenter de répondre à la question du passage à l'échelle des simulations. Nous décrivons tout d'abord une implémentation avec threads communiquant par mémoire partagée et basée sur le vol de tâches, puis une seconde implémentation utilisant des processus lourds communiquant par envoi de messages.

La thèse a été encadrée par Marc Pouzet (Professeur ENS/UPMC) et Louis Mandel (Maitre de conférence Collège de France).
Les rapporteurs sont Florence Maraninchi (Professeur Grenoble INP/VERIMAG) et Jean-Bernard Stefani (Directeur de recherche INRIA). Le jury est présidé par Christian Queinnec (Professeur UPMC) et contient également Gérard Berry (Professeur Collège de France), Bruno Pagano (Directeur scientifique Esterel Technologies) et Didier Rémy (Directeur de recherche INRIA).

Ressources