Julien Sopena

Thèse de doctorat

Titre :

“Algorithmes d'exclusion mutuelle : tolérance aux fautes et adaptation aux grilles.”

Soutenue :

Le 8 Décembre 2008

Directeur :

Pierre SENS, Professeur à l'Université Paris VI (page web)

Encadrante :

Luciana ARANTES, Maître de conférences à l'Université Paris VI (page web)

Rapporteurs :

Roberto BALDONI, Professeur à l'Université Rome I (page web)
Frédéric DESPREZ, Directeur de recherche INRIA - ENS Lyon (page web)

Examinateurs :

Marin BERTIER, Maître de conférences à l'INSA de Rennes (page web)
André SCHIPER, Professeur à l'École Polytechnique Fédérale de Lausanne (page web)
Sebastien TIXEUIL, Professeur à l'Université Paris VI (page web)

Manuscrit :

pdf

Présentation :

1 par page / 8 par page

Positionnement :

Contexte :

Systèmes répartis à grande échelle. L'ensemble de mes travaux prend pour cadre les grands systèmes distribués. Si ces systèmes se sont naturellement imposés pour répondre aux nouveaux besoins en puissance de calcul et en capacité de stockage, ils posent de nouvelles contraintes qui peuvent rendre inefficaces les algorithmes distribués présents dans la littérature. Ainsi, ils imposent la gestion d'un grand nombre de ressources, la prise en compte de l'hétérogénéité des réseaux d'interconnexion et une gestion des pannes dont la fréquence augmente proportionnellement au nombre de machines.

Problématique :

Exclusion mutuelle. Mes travaux portent plus particulièrement sur les algorithmes distribués d'exclusion mutuelle. Ces derniers sont l'une des briques de base pour de nombreuses applications réparties. Celles-ci les utilisent pour protéger les parties de leur code (section critique) qui accèdent à des ressources partagées. On les retrouve, ainsi, implémentés à tous les niveaux des systèmes répartis (middleware, système de partage de données, micro-noyau distribué, etc.).

Approche :

Formelle et expérimentale. Dans l'ensemble de mes travaux, j'ai choisi de considérer ce problème tant sous un aspect formel, en proposant et en prouvant de nouveaux algorithmes, que d'un point de vue système en étudiant la mise en œuvre de ces services de synchronisation dans un cadre réel.

Contributions : Tolérance aux fautes

Algorithme équitable d'exclusion mutuelle tolérant les fautes. Une première série de travaux nous a permis de proposer un nouvel algorithme d'exclusion mutuelle réparti tolérant les fautes. Cet algorithme se distingue de ceux présents dans la littérature par ses bonnes propriétés de passage à l'échelle, à savoir: une complexité moyenne de O(\log n) messages pour un accès à la section critique, une surveillance point à point et limitée aux sites en attente de la section critique, une utilisation réduite de la diffusion dans les mécanismes de recouvrement de fautes et une limitation dans l'annulation des requêtes en attente. De plus, notre algorithme offre de bonnes propriétés d'équité, en garantissant à un site enregistré dans la file d'attente de voir son ordre d'arrivée respecté quels que soient le nombre et le type de défaillance. Cet algorithme a fait l'objet d'une publication dans la conférence internationale [EUROPAR-2005].

Expérimentation avec injections de défaillances. Grâce à la plate-forme générique d'expérimentation gMutex, nous avons évalué notre algorithme tolérant aux défaillances sur le cluster du LIP6 (80 CPU). Dans la plupart des cas, notre algorithme s'est montré à la fois plus rapide et moins coûteux en messages que les algorithmes classiques. De plus, son comportement n'est pas dépendant du degré de parallélisme de l'application. Il conserve de bons temps de recouvrement quelle que soit la fréquence d'accès aux sections critiques. Ceci est particulièrement appréciable pour des applications dont le degré de parallélisme n'est pas constant. Enfin, nous avons montré que notre algorithme résiste à l'usage de temporisateurs agressifs, permettant ainsi d'optimiser le temps de recouvrement. Ces résultats ont fait l'objet d'une publication dans la conférence internationale [SRDS-2006].

Contributions : Adaptation aux topologies de type grille

Algorithme générique de composition. Nous nous sommes aussi intéressés à adapter les algorithmes d'exclusion mutuelle à l'hétérogénéité des réseaux dans les environnements de type grille. Nous avons ainsi proposé un nouvel algorithme générique de composition. Cet algorithme permet de composer plusieurs algorithmes d'exclusion mutuelle, sans les modifier, pour former une nouvelle solution hiérarchique [JOS-2009].

Expérimentation sur GRID'5000. Nous avons implémenté et testé cette solution en grandeur nature sur 9 clusters de la grille française GRID'5000. Les résultats de ces expériences ont permis de vérifier qu'une approche hiérarchique était très efficace. Ils ont aussi mis en évidence l'importance du taux de parallélisme de l'application dans le choix des algorithmes à composer. Ainsi nous proposons trois types de composition adaptés à différents degrés de parallélisme des applications. Ces résultats ont fait l'objet d'une publication dans la conférence internationale [ICPP-2007].

Émulation de plusieurs topologies de grille sur dummynet. Dans une deuxième série d'expériences, nous avons émulé plusieurs topologies de grille et nous avons comparé l'efficacité de la composition suivant différentes répartitions des machines dans la grille. Ces résultats ont montré que les gains offerts étaient déjà intéressants avec une grille composée de deux clusters. Par ailleurs nous avons pu démontrer que la composition offrait des gains optimum pour une grille répartissant n machines dans sqrt(n) clusters. Ces résultats ont été publiés dans la conférence internationale~[EUROPAR-2008].

Vérification formelle de l'algorithme générique de composition. Parallèlement à ces résultats, j'ai collaboré avec Souheib Baarir (Postdoctorant à l'Università del Piemonte Orientale "Amedeo Avogadro", Alessandria, Italie) pour vérifier formellement l'algorithme de composition générique. Ainsi nous l'avons modélisé en utilisant le formalisme des Réseaux de Petri bien-formés stochastiques (RdPBFS). À partir de ce modèle, nous avons vérifié par des techniques de model checking l'expression des propriétés de l'exclusion mutuelle en Logique temporelle linéaire (LTL). Pour limiter l'explosion combinatoire, nous avons cherché à utiliser les propriétés de symétrie. La conservation de ces symétries dans le modèle et dans les propriétés nous a permis d'optimiser le processus de vérification par l'utilisation d'algorithmes spécifiques de model cheking dits de symétrie partielle. Si ce résultat vient en complément d'une preuve formelle, il est une première étape vers une vérification quantitative des propriétés d'équités ainsi que des garanties offertes par la composition. L'ensemble de ce travail a été publié dans la conférence internationale [FORTE-2008] et doit paraître dans un numéro spécial du journal national [TSI-2009].

Designed by OWSD.org. Valid CSS & XHTML
Ce site et l'ensemble de son contenu est mis à disposition sous un contrat Creative Commons.
Creative Commons License