|
|
|
|
| Directeur de l'action | Massimo Zendri (Bull) |
| Projets INRIA | VASY (Grenoble)
PAMPA (Rennes) |
| Personnels INRIA | Hubert Garavel (Chargé de Recherche)
Radu Mateescu (Chargé de Recherche) César Viho (Maître de conférences) |
| Personnels CNRS | Claude Jard (Chargé de Recherche) |
| Ingénieurs Experts | Marc Herbert (à partir d'avril 1999)
Solofo Ramangalahy (à partir de septembre 1999) |
Depuis 1995, l'INRIA et BULL entretiennent une collaboration de longue durée dans le domaine des méthodes formelles. Cette collaboration, à laquelle participent les projets PAMPA (Rennes) et VASY (Grenoble), est coordonnée par un ingénieur BULL (M. Zendri) installé dans les locaux de l'Unité de Recherche INRIA Rhône-Alpes. Elle vise à démontrer que les méthodes formelles et les outils développés à l'INRIA pour la validation et le test des protocoles de télécommunications peuvent aussi être appliqués avec succès aux architectures multi-processeurs développées par BULL. L'objectif à long terme est d'offrir une chaîne complète et intégrée d'outils pour la spécification formelle, la simulation, le prototypage rapide, la vérification, la génération de tests et leur exécution.
Une première étape de cette collaboration a pris fin en 1998 avec l'achèvement de l'action VASY de DYADE, consacrée à deux études de cas successives : le protocole d'arbitrage de bus de l'architecture POWERSCALE et le protocole de cohérence de caches de l'architecture multiprocesseurs POLYKID. Le résultat de ces expérimentations a été jugé positif : la faisabilité de l'approche proposée a été démontrée et BULL a manifesté son intérêt à poursuivre l'application de cette approche sur de nouvelles architectures.
Depuis octobre 1998, les efforts portent sur FAME, une architecture multi-processeurs CC-NUMA basée sur des processeurs INTEL de nouvelle génération développée au centre BULL des Clayes-sous-Bois (France). D'abord informelle, cette collaboration a été officialisée en 1999 par le comité de pilotage et le comité de direction de DYADE sous la forme d'une nouvelle action intitulée FORMALFAME.
L'action FORMALFAME cherche à promouvoir l'utilisation de méthodes formelles pour la vérification et le test d'architectures multiprocesseurs. La méthodologie utilisée consiste à établir un modèle de référence de l'architecture visée en utilisant le langage de description formelle LOTOS. Les outils de simulation et de vérification CADP sont ensuite utilisés pour s'assurer de la correction du modèle de référence. Finalement, l'outil TGV est employé pour produire des jeux de tests "abstraits" déduits du modèle de référence ; ces tests abstraits sont ensuite traduits automatiquement en tests exécutables qui, appliqués dans l'environnement de test utilisé par BULL, serviront à valider l'implémentation du produit final.
En 1999, les travaux de FORMALFAME ont porté sur les points suivants :
En janvier 1999, nous avons achevé les travaux entrepris en 1998 pour traduire en LOTOS une description de FAME fournie sous la forme d'un programme écrit dans le langage d'entrée de l'outil MURPHI développé à l'Université Stanford. Bien que nous ayions montré la faisabilité d'une traduction systématique de MURPHI vers LOTOS, nous n'avons pas poursuivi cette approche car, à l'usage, la description de FAME en MURPHI s'est révélée difficile à faire évoluer et insuffisamment détaillée pour permettre la génération de tests pertinents.
De février à septembre 1999, nous avons concentré nos efforts sur le circuit CCS (Core Chip Set) de FAME qui, pour un groupe de quatre processeurs, implémente les fonctions de gestion mémoire, d'arbitrage de bus et de crossbar. L'objectif de notre travail était le test fonctionnel de l'implantation du composant CCS --- c'est-à-dire de son modèle VHDL au niveau RTL (Register Transfer Level) --- en ciblant notamment les aspects relatifs à la correction du protocole de cohérence de caches.
Nous avons élaboré une description LOTOS (1200 lignes, 10 processus) constituant un modèle de référence du circuit CCS et de son environnement. Pour décrire cet environnement, nous avons modélisé le comportement des deux bus, du circuit réseau et de deux microprocesseurs INTEL accédant au bus.
En appliquant l'outil TGV à cette description LOTOS, nous avons pu produire diverses suites de tests : 21 tests de base (temps de génération : 1 mn/test), 50 tests de collision (15 mn/test) et une suite de tests avec objectif de test généralisé (1 journée). En collaboration avec Solofo Ramangalahy (projet PAMPA), un traducteur écrit en LEX/YACC a été développé pour convertir les tests "abstraits" produits par TGV en des tests directement exécutables dans l'environnement de test utilisé par BULL (c'est-à-dire en programmes C dans lesquels les émissions/réceptions de signaux sont effectuées par des appels à des fonctions définies dans des interfaces de programmation spécialisées).
A partir d'octobre 1999, nous nous sommes intéressés au circuit NCS (Network Chip Set) de FAME qui assure les communications réseau. Nous avons élaboré une description LOTOS (1200 lignes, 16 processus) modélisant trois circuits NCS placés dans un environnement comportant quatre bus et trois processeurs INTEL. A partir de cette description LOTOS, l'outil TGV a produit 50 tests de base (temps de génération : 30 secondes/test). Enfin, le traducteur de tests abstraits en tests exécutables développé pour le circuit CCS a été étendu pour permettre le test du modèle RTL du circuit NCS.
En 1999, le code C généré par le compilateur CAESAR.ADT pour les types de données complexes (tuples, listes, arbres, ensembles, etc.) a été amélioré de manière significative. Auparavant, tous ces types étaient implémentés comme pointeurs vers des structures ou des unions avec discriminants, ce qui entraînait un surcoût en mémoire de 4 octets par valeur mémorisée.
La nouvelle version de CAESAR.ADT implémente tous les types LOTOS non-récursifs directement comme des structures ou des unions avec discriminants, ce qui permet d'économiser l'espace mémoire précédemment consommé par les pointeurs. Dans le cas des types LOTOS directement ou mutuellement récursifs (listes, arbres, etc.), la nouvelle version de CAESAR.ADT met en oeuvre des heuristiques visant à implémenter comme pointeurs un nombre minimal de types, de façon à "casser" toutes les dépendances cycliques entre les types. L'utilisateur a la possibilité de choisir lui-même l'implémentation des types en imposant que certains types soient implémentés avec pointeurs, ou bien sans pointeur.
Ces améliorations, qui ont nécessité des changements importants dans le compilateur CAESAR.ADT (ajout de contrôles sémantiques et algorithmes d'ordonnancement des définitions de types en langage C), ont permis d'obtenir des réductions parfois spectaculaires de l'espace mémoire pour les types de données couramment utilisés dans les protocoles de communication (structures, paquets, unités de transfert de données, etc.). Le gain est très tangible en vérification énumérative, où il est souvent nécessaire de mémoriser simultanément un nombre important de valeurs (plusieurs millions) représentant le contenu de tous les états du système.
En 1999, nous avons travaillé à généraliser le modèle réseau utilisé par le compilateur CAESAR pour traduire les définitions de processus présentes dans une description LOTOS.
La définition formelle de ce modèle réseau est donnée dans la thèse d'Hubert Garavel : il s'agit d'un réseau de Petri étendu par des variables d'état typées, dans lequel chaque transition est étiquetée par divers attributs construits à partir des informations présentes dans la description LOTOS, notamment une porte correspondant à un point de communication, une offre qui est une liste d'expressions typées correspondant aux valeurs émises ou reçues sur la porte, et une action qui est un bloc d'instructions séquentielles pouvant comporter des affectations (qui modifient la valeur d'une variable d'état), des itérations (qui font prendre a` une variable toutes les valeurs possibles dans un domaine fini) et des conditions (gardes booléennes pouvant empêcher le franchissement de la transition). En 1992, afin de réduire le nombre d'états des graphes produits en vérification exhaustive, ce modèle avait été enrichi en attachant à chaque transition une liste de variables devant être réinitialisées (par défaut, à zéro) lorsque la transition est franchie.
Dans le modèle réseau de CAESAR, l'action d'une transition est executée avant que les expressions de l'offre de la transition ne soient évaluées. Afin d'obtenir des réseaux plus compacts, il est apparu souhaitable que certaines actions (affectations ou réinitialisations de variables) puissent aussi être effectuées après l'évaluation de l'offre. Nous avons introduit cette extension dans le modèle réseau de CAESAR et généralisé en conséquence les diverses phases de construction et d'optimisation opérant sur ce modèle.
Sur de nombreux exemples LOTOS, ces modifications ont permis de réduire le nombre de places, de transitions et de variables des réseaux produits par CAESAR. Dans de nombreux cas, ces réductions sont significatives. Ainsi, sur un exemple fourni par Elie Najm (Ecole Nationale Supérieure des Télécommunications), le nombre de places passe de 17 à 4, le nombre de transitions passe de 60 à 47 et le nombre de variables passe de 16 à 1.
La réduction de la taille des réseaux entraîne fréquemment une réduction de la taille des graphes correspondants. Souvent, le facteur de réduction est d'un ordre de grandeur, mais il peut être bien supérieur dans certains cas, comme sur l'exemple d'Elie Najm pour lequel la taille du graphe passe de 304_305 états et 1_434_070 transitions à 83 états et 364 transitions.
La vitesse de génération des graphes a aussi été améliorée : sur des exemples LOTOS étudiés par Fabrice Baray (laboratoire ISIMA/LIMOS), la nouvelle version de CAESAR est, en moyenne, 150 fois plus rapide que la précédente (la taille des graphes produits restant sensiblement la même).
Toutefois, l'amélioration n'est pas systématique car, sur quelques exemples, l'un des paramètres du réseau (par exemple, le nombre de variables) peut augmenter alors que les autres paramètres (par exemple, le nombre de places et de transitions) diminuent ; sur d'autres exemples, le nombre d'états du graphe peut diminuer tandis que le nombre de transitions augmente. Ces questions restent à approfondir.
En 1999, l'outil TGV a bénéficié d'un "lifting" complet en vue de sa distribution au sein de la boîte à outils CADP. L'architecture de TGV a été repensée complètement pour refléter la découpe fonctionnelle et permettre une plus grande modularité. Les fonctionnalités ont été améliorées, notamment en généralisant l'utilisation des expressions régulières pour donner une plus grande expressivité aux objectifs de tests et aux fichiers de masquage et de renommage. Le calcul de temporisations a été simplifié et incorporé au coeur de TGV. Le calcul des postambules a été affiné par la notion d'état stable. L'outil TGV accepte désormais le format de graphe BCG à la fois en entrée et en sortie. Un nouveau module appelé VTS (Verification of Test Suites) pouvant se substituer au module principal de TGV permet maintenant de vérifier et corriger à la volée des cas de test. Ceci peut servir à corriger des tests écrits manuellement, mais sert également à tester TGV lui-même en vérifiant les tests qu'il produit. Enfin, en plus de la version Solaris, il existe désormais une version Linux de TGV et une version Windows NT est en préparation.
L'activité de FORMALFAME a été jugé satisfaisante et il est prévu que la collaboration se poursuive en l'an 2000.
Back to the VASY Home Page