OBJECTIF

L’architecture TSAR vise la définition et l’implémentation d’une architecture de processeur many-cores utilisable dans des ordinateurs de type serveurs, c'est-à-dire une architecture matérielle supportant la mémoire virtuelle, et fournissant un mécanisme de cohérence des caches garantie par le matériel. Cette architecture NUMA (Non Uniform memory Access) supporte des systèmes d’exploitation généralistes de type UNIX (ou LINUX). Elle a été conçue pour être réellement scalable (pour atteindre plusieurs milliers de coeurs sur une seule puce), tout en fournissant une mémoire partagée cohérente. Un protocole hiérarchique de cohérence des caches hiérarchique a été proposé, nommé DHCCP (Directory-Based Hierarchical Coherency Cache Protocol).

Une première version de l’architecture TSAR, comportant 512 cÅ“urs a été modélisée en langage SystemC, en utilisant la plate-forme de prototypage virtuel SOCLIB et un style de modélisation « au cyle près Â» Différentes applications logicielles  ont pu être déployées et exécutées (en simulation) sur ce prototype virtuel, démontrant la scalabilité du protocole de cohérence DHCCP. Néanmoins, la validation de ce protocole reste à réaliser.

La définition de protocoles de cohérence de caches est une tâche particulièrement difficile car elle fait intervenir de nombreux processus concurrents asynchrones partageant certaines données critiques. Du fait de la complexité du protocole, des défauts de conception peuvent être introduits, qui sont très difficiles à mettre en évidence. Il faut prouver que ce protocole garantit bien (1) les propriétés de cohérence (par ex. on ne peut pas répercuter une donnée incohérente en mémoire centrale, la liste et la localisation des copies sont cohérentes, …) et (2) qu’il est exempt de blocage (par ex. le système pourra toujours traiter une nouvelle requête de lecture ou d’écriture).

 

La preuve formelle de tels protocoles a fait l’objet de nombreuses recherches, et en fait peu de solutions satisfaisantes sont applicables à de nouveaux protocoles. Nous proposons dans ce stage de vérifier des propriétés de cohérence et d’absence de blocage en utilisant des techniques d’observation dynamique, intégrées à une plate-forme de prototypage virtuel. 

TRAVAIL PROPOSE

Ce stage porte sur l’instrumentation d’un prototype virtuel de l’architecture TSAR, permettant de tester dynamiquement, à la volée, les propriétés de sûreté que doit respecter le protocole DHCCP. Les modèles des composants élémentaires de la plate-forme sont disponibles et décrits « au cycle près Â». La spécification du protocole DHCCP est plus abstraite (niveau échange de messages représentant les commandes / réponses des différentes entités du protocole).

Ce stage se déroulera en plusieurs étapes

1.      étude de l’architecture TSAR et du modèle de simulation au cycle près

2.   Ã©tude de la spécification du protocole DHCCP, identification des points de contrôle et des invariants à contrôler dynamiquement,

3.    proposition d’un modèle d’observateur permettant le suivi de plusieurs lignes de caches simultanément, et intégrant un mécanisme de conversion des transferts de la plate-forme au cycle près en messages du protocole

4.    implantation des observateurs dans une plate-forme comprenant deux clusters de quatre cÅ“urs.

5.  simulation et test de la plate-forme instrumentée, rapport d’analyse des observateurs

 

ENCADREMENT :

Emmanuelle Encrenaz  (Emmanuelle.Encrenaz(at)lip6(.)fr) et Alain Greiner Alain.Greiner(at)lip6(.)fr

Ce stage s’inscrit dans le cadre du projet Européen SHARP piloté par BULL, dont les partenaires Français sont THALES, le LIP6 et le CEA/LETI.