Soutenance de thèse de Meriem Zidouni

Meriem Zidouni soutiendra le 25 mai 2010 à 14h00
au Grand Amphithéâtre de l'INRIA Grenoble Rhône-Alpes
655, avenue de l'Europe 38330 Montbonnot Saint Martin
(informations d'accès)

une thèse de doctorat de l'Université Joseph Fourier de Grenoble,
spécialité : informatique, intitulée :

"Modélisation et analyse des performances de la bibliothèque MPI en tenant compte de l'architecture matérielle"

Thèse Bull-INRIA préparée dans le Centre de Recherche INRIA Grenoble Rhône-Alpes et au laboratoire LIG (équipe-projet VASY),
sous la direction de M. Ghassan CHEHAIBAR et de M. Radu MATEESCU.

COMPOSITION DU JURY :

  • M. Jean-François MÉHAUT, professeur à l'Université Joseph Fourier de Grenoble (président du jury)
  • M. Jean-Michel FOURNEAU, professeur à l'Université de Versailles (rapporteur)
  • Mme Françoise SIMONOT-LION, professeur à l'INPL / École des Mines de Nancy (rapporteur)
  • Mme Anne BENOÎT, maître de conférences à Ecole Normale Supérieure de Lyon (examinateur)
  • M. Ghassan CHEHAIBAR, architecte senior à Bull S.A.S. (directeur de thèse)
  • M. Radu MATEESCU, chargé de recherche à l'INRIA Grenoble Rhône-Alpes (directeur de thèse)

La soutenance sera naturellement suivie d'un pot, dans la cafétéria de l'INRIA, auquel vous êtes tous cordialement invités.

RESUME :

Dans le cadre de son offre de serveurs haut de gamme, la société Bull conçoit des multiprocesseurs à mémoire distribuée partagée avec un protocole de cohérence de cache CC-DSM (Cache-Coherent Distributed Shared Memory) et fournit une implémentation de la bibliothèque MPI (Message Passing Interface) pour la programmation parallèle. L'évaluation des performances de cette implémentation permettra, d'une part, de faire les bons choix d'architecture matérielle et de la couche logicielle au moment de la conception et, d'autre part, fournira des éléments d'analyse nécessaires pour comprendre les mesures faites au moment de la validation de la machine réelle.

Nous proposons et mettons en oeuvre dans ce travail de thèse une méthodologie permettant d'évaluer les performances des primitives de la bibliothèque MPI (envoi/réception et barrières) en tenant compte de l'architecture matérielle. Cette approche est basée sur l'utilisation des méthodes formelles et consiste en trois étapes principales :

  1. la modélisation en langage LOTOS des aspects matériels (topologie d'interconnexion, protocole de cohérence de caches) et logiciels (primitives MPI et algorithmes de benchmark) ;
  2. la vérification formelle de la correction fonctionnelle du modèle obtenu ;
  3. l'évaluation des performances après l'extension du modèle avec des informations quantitatives (latences des transferts des données) en utilisant des méthodes numériques et de la simulation.

MOTS-CLES :

bibliothèque MPI, architectures multiprocesseurs, méthodes formelles, model checking, évaluation des performances, chaînes de Markov interactives

TITLE:

Modeling and Performance Analysis of the MPI Library by Taking into Account the Hardware Architecture

ABSTRACT:

The range of high-end servers designed and manufactured by Bull includes cache-coherent distributed shared memory (CC-DSM) multiprocessor systems equipped with an implementation of the Message Passing Interface (MPI) library for parallel programming. The evaluation of the performances of this implementation will enable, on the one hand, to make the right choices of the hardware architecture and of the software layer at design time and, will provide, on the other hand, the analysis elements necessary for understanding the experimental measures performed when the real machine is validated.

In this thesis, we propose and develop a methodology allowing to evaluate the performances of MPI library primitives (send/receive and barriers) by taking into account the hardware architecture. This approach is based on formal methods and consists of three main phases:

  1. modeling in the LOTOS language the hardware aspects (interconnection topology, cache coherency protocol) and the software aspects (MPI primitives and benchmark algorithms);
  2. formal verification of the functional correctness of the model obtained;
  3. performance evaluation after extending the model with quantitative information (data transfer latencies) by using numerical methods and simulation.

KEYWORDS:

MPI library, multiprocessor architectures, formal methods, model checking, performance evaluation, interactive Markov chains

Back to the VASY Home Page