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 adopte une démarche compositionnelle pour mener à bien les objectifs de vérification.

 

Objectif:

L’objectif du projet est de proposer une démarche de vérification compositionnelle 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 ; des abstractions des éléments constitutifs sont assemblées pour simplifier la preuve. Si l’abstraction est trop grossière, l’analyse de la trace d’exécution invalidant la propriété est utilisée pour affiner le modèle.

 

Le projet comprend plusieurs étapes :

1.  Identification des niveaux hiérarchiques du protocole. Proposition d’abstraction initiale des composants  de l’architecture.

2.  Proposition d’une stratégie de raffinement des abstractions initiales guidée par le contre-exemple.

3.  Mise en Å“uvre de  la vérification compositionnelle pour vérifier des propriétés de sûreté.

4.  Extension  du  modèle  et  de  la  vérification  aux  primitives  LL/SC  (Linked  Load  /  Store Conditional)  permettant  de  synchroniser  des  processus  sur  l’accès  à  des  ressources partagées (locks).

La quatrième étape est facultative et sa réalisation dépendra de la rapidité avec laquelle les étapes précédentes auront été menées.

 

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 SPIN

 

Encadrant:

Emmanuelle Encrenaz : emmanuelle.encrenaz@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.

 

SPIN user manual. G. Bolzmann, BellLabs, 1997. spinroot.com/spin/whatispin.html

 

Modélisation et Vérification du Protocole de Cohérence de Caches de la Machine TSAR. M. Najem. Rapport de projet Master 1. 2011. 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