Attention! L'offre d'emploi ci-dessous n'est plus valable, le poste en question ayant été pourvu depuis.
Ce sujet de thèse CIFRE est proposé conjointement par la société Bull (1er fournisseur global en systèmes d'information d'origine européenne) et l'équipe VASY de l'INRIA (Institut National de Recherche en Informatique).
Il prend place au sein du projet Multival du pôle de compétitivité Minalogic. Institués en 2005 par le gouvernement, les pôles de compétitivité ont pour objectif une politique industrielle de grande envergure. Ils se concrétisent par le lancement d'ambitieux projets de recherche et développement, qui mettent en oeuvre des collaborations entre centres de recherche et entreprises reconnus mondialement dans leurs domaines d'excellence respectifs.
Les performances d'un supercalculateur dépendent de son architecture matérielle et de la couche logicielle qui offre l'interface de programmation parallèle. Ainsi le constructeur de multiprocesseurs destinés au calcul scientifique haute performance (HPC: High-Performance Computing) doit optimiser les bibliothèques de programmation parallèle pour l'architecture de ses serveurs. Dans le cadre du projet FAME2, Bull construit des multiprocesseurs à mémoire distribuée partagée avec protocole de cohérence de caches CC-DSM (Cache-Coherent Distributed Shared Memory) et fournit une implémentation de la bibliothèque de programmation parallèle MPI (Message Passing Interface).
MPI implémente le modèle de programmation parallèle, très répandu, par passage de messages : les processus ne partagent pas de données mais communiquent au moyen de primitives send/receive et utilisent des barrières pour se synchroniser. Le concepteur d'applications parallèles peut optimiser la décomposition de l'algorithme et l'usage des primitives de synchronisation. Cependant, le coût des primitives de synchronisation résulte de l'implémentation de MPI - algorithmes implémentant les primitives (send, receive, barrier) - et de l'architecture matérielle sous-jacente sur laquelle s'exécute le logiciel.
Dans les communications entre processus, on utilise des tampons de communication et éventuellement des verrous pour gérer les exclusions d'accès à ces tampons. Dans une architecture CC-DSM, ces structures de communications sont implantées en mémoire cohérente et leurs accès sont régis par le protocole de cohérence des caches. Ceci implique des transferts entre les caches et les mémoires et entre les différents caches qui dépendent de l'implantation physique de ces structures et du protocole : ces transferts déterminent la performance des communications et synchronisations inter-processus. Ainsi les performances de l'implémentation de MPI dépendent de 3 paramètres: 1) la succession d'accès définie par l'algorithme des primitives de communications, 2) le protocole de cohérence de caches qui détermine les changements d'états dans les caches et les transferts entre caches et mémoires, 3) la topologie de l'architecture du multiprocesseur qui détermine les latences des transferts.
L'objet de la thèse est de fournir un outil permettant d'évaluer et d'optimiser une implémentation de la bibliothèque MPI en fonction de l'architecture matérielle et du protocole de cohérence de caches : en entrée, on a l'algorithme implémentant une primitive MPI et un modèle de l'architecture matérielle et de son protocole de caches ; en sortie, on obtient : la latence d'exécution de la primitive, les poids relatifs des instructions de l'algorithme (pour savoir ce qu'il faut optimiser) et le débit de données que permet la primitive (par exemple dans le cas d'un send ou receive). On peut aussi avoir en entrée l'algorithme d'un benchmark qui est un processus composé d'appels à des primitives.
L'idée est de ramener tout algorithme à un processus fait de lectures (load) et d'écritures (store) mémoire. Il s'agit alors de construire un modèle LOTOS augmenté de latences et résultant de la composition de 3 modèles :
L'intérêt d'une telle approche est de pouvoir faire varier ces 3 aspects de façon indépendante : on peut modifier l'algorithme en conservant la même architecture matérielle, ou modifier les transitions du protocole de cache (M → S au lieu de M → I sur une lecture, par exemple) ou modifier la topologie.
Le travail de thèse comprend :
Les modèles LOTOS annotés avec des informations permettant l'analyse des performances (débits, latences, etc.) seront produits selon l'approche proposée en [GH02], qui permet de combiner les aspects fonctionnels (comportement parallèle) et les aspects quantitatifs (débits, latences) au sein d'une même spécification LOTOS. Cette approche, basée sur un modéle sémantique défini en [Her02], présente l'avantage de fournir une spécification unique qui sert de support à la vérification fonctionnelle au moyen des outils basés sur les logiques temporelles et les équivalences (EVALUATOR et BISIMULATOR) et aussi à l'évaluation de performances au moyen des outils spécialisés (BCG_MIN, BCG_STEADY, BCG_TRANSIENT, DETERMINATOR) disponibles dans la boîte à outils CADP de l'INRIA.
La thèse sera co-encadrée par Bull et l'INRIA. Elle se déroulera principalement sur le site de Bull Les Clayes-sous-Bois (Yvelines), avec des déplacements réguliers à Dijon et/ou Grenoble.
Des échanges réguliers avec le professeur H. Hermanns (Université de la Sarre) sont également prévus.
Les candidatures peuvent être déposées par le biais du formulaire http://vasy.inria.fr/jobs/candidature ou adressées directement à Ghassan Chehaibar et Radu Mateescu comme indiqué ci-dessous, en indiquant la référence #2006G.
Toutes questions concernant cette thèse CIFRE doivent être adressées aux deux personnes suivantes: