Date prévisible d'embauche : dès que possible, au plus tard octobre 2010

Type de contrat : Contrat à durée déterminé de 3 ans, proposé par la société Bull, dans le cadre d'une thèse CIFRE en collaboration avec l'équipe VASY de l'INRIA (Institut National de Recherche en Informatique) et du LIG (Laboratoire d'Informatique de Grenoble)

Rémunération : environ 29000 EUR brut annuel

Lieu de travail :

Cette thèse se déroulera principalement sur le site de Bull aux Clayes-sous-Bois (Yvelines), avec des déplacements réguliers sur le site de l'INRIA à Montbonnot (Isère), à une dizaine de kilomètres de Grenoble. Les frais de transport engendrés par ces déplacements seront pris en charge.

Sujet de la thèse : « Vérification de protocoles de cohérence de caches pour les calculateurs à haute performance »

Objectifs de la thèse :

La fabrication et la commercialisation d'ordinateurs destinés au calcul scientifique à haute performance (HPC: High-Performance Computing) est un axe stratégique de l'activité de Bull (1er fournisseur global en systèmes d'information d'origine européenne). Les futures générations d'ordinateurs HPC 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, chaque processeur étant équipé d'un cache mémoire.

Un tel degré de parallélisme ouvre de nombreux défis. L'un d'eux consiste à 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.

La thèse vise à améliorer les méthodes de développement utilisées par Bull. L'objectif est de proposer des solutions au problème de cohérence de caches, 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, commune à l'INRIA et au LIG, 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.

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, Murphi, ...) et/ou des assistants de preuve (PVS, Coq, ...), 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 lien direct 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 versions de ses protocoles de cohérence de cache.

Courtesy of Bull

Compétences et profil attendus :

• Connaissance des méthodes formelles (model-checking, démonstration, etc.)

• Programmation

• Bonne maîtrise du français et de l'anglais

• Bonne capacité d'assimilation et de synthèse, rigueur, méthodologie, autonomie, esprit d'équipe, intérêt pour travailler en milieu industriel

• Formation de Master 2 Recherche en informatique ou en mathématiques appliquées

• Un stage de master en méthodes formelles serait un plus

Contacts :

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

	M. Ghassan Chehaibar Platforms Hardware R&D Bull Rue Jean Jaurès 78340 Les Clayes Sous Bois E-mail : Ghassan.Chehaibar@bull.net
	M. Frédéric Lang INRIA Rhône-Alpes /VASY Inovallée 655, avenue de l'Europe 38330 Montbonnot Saint-Martin Tel : +33 (0)4 76 61 55 11 E-mail : Frederic.Lang@inria.fr

Composition du dossier de candidature :

• lettre de motivation

• curriculum vitæ

• les éventuelles références ou lettres de recommandation

• les éventuelles publications scientifiques ou techniques

Envoi du dossier de candidature :

Les candidatures doivent être adressées directement à Ghassan Chehaibar et Frédéric Lang, de préférence par e-mail, en indiquant le numéro de l'emploi #2010A. La date limite de réception des dossiers est fixée au 30 juin 2010.