Le  projet  TSAR  vise  la  définition  et  l’implantation  d’une  machine  multiprocesseurs  à  mémoire  partagée.  L’architecture  doit  être  pouvoir  supporter  jusqu’à  4000  processeurs  implantés  en clusters de 4 processeurs, interconnectés par un réseau de communication distribué (DSPIN). La mémoire est physiquement distribuée dans les différents clusters et elle est logiquement partagée par  l’ensemble des processeurs : l’espace d’adressage est commun à  tous, et  les données sont accessibles par  le biais de  fonctions de  lecture et d’écriture. Cette architecture  induit des  temps accès aux données non uniformes: selon la localisation relative du processeur réalisant un accès et  la  donnée  accédée,  le  temps  d’accès  est  variable.  La  hiérarchie  mémoire  permettant  de rapprocher  les  données  des  processeurs  induit  une  possible  réplication  des  données  dans différents  caches.  La  cohérence  des  différentes  copies  d’une même  donnée  est  implantée  en matériel au travers d’un protocole write-through original.

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 formellement 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 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 la technique du model-checking, applicable pour des architectures intégrant un faible nombre de composants. 

Le model-checking consiste à parcourir symboliquement l’espace d’état du système, et à déterminer automatiquement, lors de ce parcours, si la structure de l’espace d’états est conforme aux propriétés désirées. Une première étude a permis de construire des modèles exécutables et vérifiables formellement des éléments  constitutifs du protocole DHCCP ; la vérification complètement automatique se heurte au problème d’explosion combinatoire de l’espace d’états du système à analyser. Le présent projet utilise des représentations symboliques d'espace d'états très efficaces sur les systèmes hiérarchiques pour contourner ces phénomènes d'explosion combinatoire.

 

Objectif:

L’objectif du projet est de proposer une démarche de vérification permettant l’analyse de propriétés de sûreté du protocole. Cette démarche repose sur la nature hiérarchique du protocole DHCCP, ainsi que sur la structure modulaire de l’architecture multi-processeur.

 

Le projet comprend plusieurs étapes :

1. Identification des niveaux hiérarchiques du protocole. Modélisation des entités constitutives du protocole (processeur, cache L1, contrôleur mémoire, mémoire, différents réseaux de communication).

2.  Construction d'une plate-forme permettant l'activation de tous les mécanismes du protocole

3. Identification des propriétés à vérifier (sûreté et vivacité).

4. Vérification des propriétés et analyse des résultats.

 

Connaissances souhaitées:

Modélisation des comportements d’un système numérique par automate et/ou analyse par exploration de l’espace d’états.

 

Ce projet permettra à l’étudiant de se former aux problèmes de cohérence de caches dans les architectures multiprocesseurs, aux méthodes et outils de modélisation et de vérification fonctionnelle de systèmes concurrents.

 

Outil:

Model-checker PNSDD développé au LIP6

 

Encadrants:

Emmanuelle Encrenaz : emmanuelle.encrenaz@lip6.fr

Yann Thierry-Mieg : yann.thierry-mieg@lip6.fr

 

Rémunération:

420 euros/mois (sous réserve de financement , réponse début janvier)

 

Bibliographie:

 

Vérification de logiciels : Méthodes et Outils du Model-Checking, P. Schnoebelen et al. Vuibert, 1999.

 

Documentation de l’architecture TSAR, A. Greiner et al. Rapport interne LIP6, 2009.

 

Building Efficient Model Checkers using Hierarchical Set Decision Diagrams and Automatic Saturation. A. Hamez, F. Kordon, Y. Thierry-Mieg, Fundamenta Informaticae Petri Nets (2008) 1–25 IOS Press

 

Modélisation et Vérification du Protocole de Cohérence de Caches de la Machine TSAR : Propriété de deadlock. A. Mansour. Rapport de projet Master 1. 2012. Université Pierre et Marie Curie. LIP6.

 

Efficient Methods for Formally Verifying Safety Properties of Hierarchical Cache Coherence Protocols. X. Chen, Y. Yang, G. Gopalakrishnan, C. Chou. Formal Methods in System Designs, vol 36, pp 37-64, 2010