Attention! L'offre d'emploi ci-dessous n'est plus valable.

Vérification de protocoles de cohérence de caches pour les calculateurs à haute performance

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.

Objectifs de la thèse

Bull conçoit, fabrique et commercialise des ordinateurs destinés au calcul scientifique à haute performance (HPC: High-Performance Computing), dont les futures générations intègreront plusieurs centaines de milliers de nœuds de calcul fonctionnant en parallèle. Chaque nœud est lui-même un serveur multiprocesseur à mémoire partagée et répartie sur les processeurs, qui sont équipés chacun d'un cache mémoire.

Un des défis de Bull est de concevoir des protocoles de gestion des caches utilisables à une telle échelle. Pour réduire les coûts et les temps de mise sur le marché, Bull souhaite disposer de méthodes lui permettant de garantir la cohérence de caches, caractérisée par un ensemble de bonnes propriétés telles que l'impossibilité de lire dans un cache une donnée qui n'est pas à jour.

L'objectif de la thèse est de proposer des solutions au problème de cohérence de caches, qui soient basées sur des outils logiciels fondés sur des méthodes formelles. Le candidat disposera de l'expertise des membres de l'équipe-projet VASY de l'INRIA, dont l'activité principale est la conception et le développement de la boîte à outils logiciels CADP, par ailleurs déjà utilisée par Bull [GVZ01].

Travail proposé et résultats attendus

Dans un premier temps, le candidat devra mener une étude approfondie de l'existant en matière de techniques et outils de vérification, en particulier leur utilisation pour valider des protocoles de cohérence de caches ou des problèmes voisins. Cette étude devra déboucher sur une synthèse critique, centrée principalement sur des aspects pratiques, notamment : simplicité de modélisation, adéquation entre pouvoir expressif et besoins spécifiques des protocoles utilisés par Bull, passage à l'échelle, contraintes d'utilisation, types de propriétés vérifiables, disponibilité et robustesse des outils logiciels, etc.

Sur la base de cette synthèse, la suite de la thèse consistera à modéliser et à vérifier les protocoles de Bull, en utilisant des méthodes et des outils existants, tels que des model-checkers (CADP [GLMS07], Murphi [DDHY92], ...) et/ou des assistants de preuve (PVS [OSR92], Coq [BC04], ...), voire en les combinant. L'utilisation de model-checkers nécessitera des techniques (abstraction, approches compositionnelles, utilisation de grappes ou de grilles d'ordinateurs, ...) permettant de repousser le problème de l'explosion combinatoire des états, qui se pose lorsque le nombre d'états du modèle du protocole dépasse les capacités mémoire des ordinateurs disponibles.

Durant cette phase, le candidat travaillera en communication directe avec l'équipe d'architecture de Bull, à qui il fera un rapport détaillé des erreurs identifiées dans les protocoles.

Enfin, le candidat tentera de dégager de cette étude une méthodologie complète, utilisable par Bull pour valider les futures version de ses protocoles de cohérence de cache.

Lieu de travail

La thèse sera co-encadrée par Bull et l'INRIA. Elle se déroulera principalement sur le site de Bull aux Clayes-sous-Bois (Yvelines), avec des déplacements réguliers à Grenoble.

Rémunération

Le montant de la rémunération est d'environ 29000 EUR brut annuel. Les frais de transport engendrés par les déplacements à Grenoble seront pris en charge.

Compétences

Profil

Contacts / Dates

L'objectif est que cette thèse puisse démarrer en novembre ou décembre 2009.

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 Frédéric Lang comme indiqué ci-dessous, en indiquant la référence #2009F.

Toutes questions concernant cette thèse CIFRE doivent être adressées aux deux personnes suivantes:

et

Bibliographie