Contexte et objectifs du stage

Le projet TSAR vise la définition et l’implantation d’une machine multiprocesseur à mémoire partagée. L’architecture supporte jusqu’à 4096 processeurs organisés en clusters de 4 processeurs, interconnectés par un réseau de communication distribué. La mémoire est physiquement distribuée dans 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.

Dans une telle machine multiprocesseur, la synchronisation des processus impose l’utilisation d’opérations atomiques. Une opération atomique est composée d’une lecture de la mémoire suivie d’une modification et d’une écriture de la valeur lue en mémoire en assurant qu’entre la lecture et l’écriture aucune autre modification n’a été apportée à la valeur contenue dans la mémoire. Dans le processeur Mips, la mise en œuvre des opérations atomiques est assurée par le couple d’instructions LL (Linked Load) et SC (Store Condidtional). L’instruction LL fait la lecture et l’instruction SC réalise l’écriture. Si, entre la lecture et l’écriture, une autre modification s’est opérée, la mémoire refuse d’effectuer l’écriture et signale l’échec de l’instruction SC au processeur.

Dans le cadre du projet TSAR, nous avons mis au point un mécanisme matériel pour assurer la prise en charge des instructions LL-SC. Ce mécanisme est particulièrement adapté aux machines multiprocesseurs à grande échelle et fonctionne avec une quantité limitée de matériel. L’objectif du stage est de vérifier, de façon formelle, que ce mécanisme assure effectivement le bon fonctionnement de ces instructions.

Le stage se déroulera en plusieurs étapes :

1. Compréhension du problème d’atomicité dans les machine multiprocesseur

2.      Etude du mécanisme matériel proposé

3.      Abstraction et modélisation du mécanisme dans un langage de vérification formelle

4.      Description des propriétés à vérifier

5.      Vérification à l’aide d’un outil de vérification formelle

 

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.

 

Encadrants

Emmanuelle Encrenaz : Emmanuelle.Encrenaz(at)lip6(.)fr

Pirouz Bazargan Sabet : Pirouz.Bazargan-Sabet(at)lip6(.)fr

 

Références

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

Mécanisme LL-SC scalable, A. Joannou, Rapport de stage M2 – 2011