|
|
|
| Directeur de l'action | Solofo Ramangalahy (BULL) (depuis le 1er juin 2001) |
| Projets INRIA | VASY (Grenoble) |
| Personnels INRIA | Hubert Garavel (Directeur de Recherche)
Radu Mateescu (Chargé de Recherche) |
| Ingénieur Expert | Bruno Ondet (jusqu'au 31 décembre 2002) |
Depuis 1995, nous entretenons une collaboration de longue durée avec BULL, collaboration à laquelle l'ex-projet PAMPA a participé jusqu'en décembre 2000. Il s'agit de 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écommunication peuvent aussi être appliqués avec succès aux architectures multiprocesseurs 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 eu lieu entre 1995 et 1998 dans le cadre de l'action VASY du GIE BULL-INRIA DYADE. Elle a été 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 multiprocesseur POLYKID. Le résultat 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 la collaboration avec de nouvelles architectures.
Depuis octobre 1998, nos travaux portent sur FAME, une architecture multiprocesseur CC-NUMA développée par BULL et basée sur des processeurs INTEL ITANIUM 64 bits. D'abord informelle, cette collaboration a été officialisée en 1999 sous la forme d'une action DYADE, intitulée FORMALFAME, qui a duré jusqu'à la fin du GIE DYADE en mars 2001. Depuis cette date, la collaboration se poursuit sous la forme d'un contrat BULL-INRIA, pour lequel nous avons conservé le nom de FORMALFAME. Ce contrat réunit le projet VASY et l'équipe de Sylvie Lesmanne (qui a succédé à Anne Kaszynski en mars 2002) au centre BULL des Clayes-sous-Bois (France), la coordination étant assurée par un ingénieur BULL (M. Zendri, puis N. Zuanon, puis S. Ramangalahy) installé dans les locaux de l'Unité de Recherche INRIA Rhône-Alpes.
FORMALFAME cible ses efforts sur les composants critiques de l'architecture FAME, successivement : le circuit CCS qui gère les communications pour un groupe de quatre processeurs, le circuit NCS qui gère les communications réseau et, depuis décembre 1999, le circuit BSPS qui implémente le protocole de cohérence de caches. Pour chacun de ces composants, une description LOTOS a été élaborée et sert de modèle de référence pour la vérification et le test.
En 2002, les résultats obtenus par FORMALFAME concernent, d'une part, la validation et le test du circuit BSPS et, d'autre part, l'amélioration des différents outils de CADP.
Depuis octobre 1998, nous collaborons avec BULL dans le cadre du contrat FORMALFAME qui cherche à promouvoir l'utilisation de méthodes formelles pour la vérification et le test d'architectures multiprocesseurs. Nos travaux portent sur FAME, une architecture CC-NUMA développée au centre BULL des Clayes-sous-Bois (France) et basée sur des processeurs 64 bits INTEL ITANIUM. Nous nous concentrons sur la validation et le test d'un circuit complexe (appelé BSPS) ayant une double fonctionnalité : il effectue le routage entre les processeurs et les noeuds d'entrées/sorties et il implémente le protocole de cohérence de caches de l'architecture FAME. La complexité de ce circuit provient à la fois du parallélisme interne inhérent au routage et des accès multiples aux données partagées dont il convient de préserver l'intégrité.
Le fonctionnement du circuit BSPS est décrit par un document de référence (100 pages) combinant des spécifications informelles en langue naturelle avec des tables états/transitions. Le circuit lui-même est réalisé par un modèle en langage VERILOG. Un modèle logiciel en langage C++ du circuit BSPS permet, soit d'émuler le comportement attendu du circuit, soit de valider le comportement du modèle VERILOG. Dans le cadre de FORMALFAME, une description formelle en LOTOS du circuit BSPS a été développée en 2000.
Les travaux conduits dans FORMALFAME introduisent des aspects formels dans la méthodologie de validation et de test utilisée par BULL. En 2002, les travaux ont porté sur trois points:
Description formelle du protocole de cohérence de caches
La description formelle en LOTOS du circuit BSPS est désormais maintenue au centre BULL des Clayes-sous-Bois qui l'améliore et la fait évoluer en fonction des révisions du protocole de cohérence de caches. En 2002, Jacques Abily et Romain Henry ont développé de nouvelles descriptions LOTOS détaillées pour deux parties du circuit BSPS (le bloc PRR et l'unité ILU) afin d'expérimenter la méthodologie FORMALFAME au niveau des blocs et des unités (c'est-à-dire à un niveau plus bas que le niveau système correspondant à la totalité du circuit BSPS).
Génération automatique de tests
L'un des objectifs de FORMALFAME consiste à dériver automatiquement des cas de test à partir de la description LOTOS, ce qui garantit la correction des tests par rapport à la modélisation formelle. Ainsi, l'effort investi dans la modélisation trouve son utilité non seulement pour la vérification, mais aussi pour la génération automatique de tests qui s'ajoutent aux tests écrits manuellement.
En 2002, l'approche dont nous avions montré la faisabilité en 2001 a été approfondie au centre BULL des Clayes-sous-Bois. Dans cette approche, basée sur l'utilisation du compilateur CAESAR en mode "génération de code" (EXEC/CAESAR), les tests sont obtenus par des exécutions aléatoires de la description LOTOS selon diffeérentes distributions de probabilité. Le code C produit par EXEC/CAESAR a été connecté à la plate-forme de test de BULL (outil TESTBUILDER de la société CADENCE) afin que celle-ci soit directement pilotée par la description LOTOS. L'expérimentation de cette approche pour le bloc PRR et l'unité ILU a été entreprise.
Vérification automatique de traces d'exécution
Nous avons poursuivi nos travaux sur la validation automatique des traces d'exécution produites soit par le modèle VERILOG, soit par l'émulateur C++ du circuit BSPS. Ces traces sont issues de scénarios de test (déterministes ou aléatoires) et peuvent comporter plusieurs dizaines de milliers de messages, ce qui rend leur analyse manuelle par relecture prohibitive, surtout dans le cas de transactions imbriquées.
En 2002, nous avons finalisé la méthode consistant à spécifier en logique temporelle des propriétés de correction sur les traces et à vérifier ces propriétés grâce aux outils EVALUATOR 3.0 et SEQOPEN de CADP. Les propriétés sont produites automatiquement à partir des tables états/transitions figurant dans la spécification de référence du circuit BSPS. Les résultats de la vérification permettent de mesurer précisément la couverture fonctionnelle (déterminée en fonction de la spécification de référence) par un ensemble de traces considéré. Cette couverture, différente de la couverture structurelle (évaluée par rapport au modèle Verilog, n'était pas mesurable objectivement avec les méthodes de test utilisées antérieurement par BULL.
Cette méthode de test (qui avait permis de détecter des erreurs et de rajouter des tests manquants) a été transférée à BULL. Elle est désormais appliquée systématiquement lors de chaque révision du circuit BSPS. Les améliorations de l'outil SEQOPEN effectuées en 2002 ont permis des gains en temps appréciables (d'environ 30%) par rapport à 2001. Ainsi, le temps nécessaire pour effectuer, sur une machine standard (processeur Pentium III 700 MHz avec 1 giga-octet de mémoire vive), 7,4 millions de vérifications unitaires (c'est-à-dire, vérification d'une propriété sur une trace) a été ramené de 31 heures à 23 heures.
Suite à ces résultats, le contrat FORMALFAME devrait être prolongé pour l'année 2003.
Back to the VASY Home Page