|
|
|
|
| Directeur de l'action | Nicolas Zuanon (BULL) (jusqu'au 30 avril 2001)
Solofo Ramangalahy (BULL) (depuis le 1er juin 2001) |
| Projets INRIA | VASY (Grenoble) |
| Personnels INRIA | Hubert Garavel (Chargé de Recherche)
Radu Mateescu (Chargé de Recherche) |
| Ingénieurs Experts | Bruno Ondet (depuis le 1er septembre 2001)
Frédéric Perret (jusqu'au 31 décembre 2001) |
Depuis 1995, VASY entreteint 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 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 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 multiprocesseurs 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 multi-processeurs 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, auquel nous avons conservé le nom de FORMALFAME. Prévu jusqu'à fin 2002, ce contrat réunit le projet VASY et l'équipe d'Anne Kaszynski 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, qui sert de modèle de référence pour la vérification et le test.
En 2001, 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.
L'action FORMALFAME cherche à promouvoir l'utilisation de méthodes formelles pour la vérification et le test d'architectures multiprocesseurs. Plusieurs méthodologies sont explorées. Toutes se basent sur l'établissement d'un modèle de référence de l'architecture visée grâce au langage de description formelle LOTOS.
Nos travaux portent sur FAME, une nouvelle architecture multi-processeurs CC-NUMA développée au centre BULL des Clayes-sous-Bois (France) et basée sur des processeurs INTEL ITANIUM 64 bits. Nous nous concentrons actuellement 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.
Sur la base du document de référence, BULL a également développé un modèle du circuit BSPS en langage C++. Celui-ci permet, soit d'émuler le comportement attendu du circuit, soit de valider le comportement produit par le modèle VERILOG.
Cette approche pragmatique est complétée par les travaux de FORMALFAME qui, en s'appuyant sur une description formelle en LOTOS du circuit BSPS développée en 2000, introduisent des aspects formels dans la méthodologie de validation et de test utilisée par BULL.
En 2001, les travaux de FORMALFAME ont concerné les aspects suivants :
Vérification automatique de traces d'exécution
Nous avons poursuivi nos travaux sur l'analyse 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. Leur analyse manuelle par relecture étant prohibitive, surtout dans le cas de transactions imbriquées, nous avons proposé et mis en oeuvre deux méthodes de validation automatique basées sur les outils CADP :
La première méthode consiste à spécifier en logique temporelle des propriétés de correction sur les traces. Jusqu'alors, ces propriétés étaient codées manuellement à partir des tables états/transitions de la spécification informelle du protocole, puis vérifiées sur les traces (préalablement converties dans un format acceptable par les outils de CADP) au moyen de l'outil EVALUATOR 3.0.
En 2001, cette procédure a été complètement automatisée grâce au développement de nouveaux outils (environ 5000 lignes de Perl et de shell script) qui, à partir des tables états/transitions et d'un ensemble de traces, génèrent automatiquement les propriétés en logique temporelle et les vérifient sur chaque trace.
Les résultats de ces vérifications fournissent une mesure précise de la couverture fonctionnelle du protocole (évaluée par rapport à la spécification) par l'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 dans FORMALFAME.
La deuxième méthode consiste à vérifier que les traces d'exécution fournies par BULL sont acceptées par la description LOTOS du protocole de cohérence de caches. Pour cela, chaque trace est traduite vers une formule de logique temporelle comportant des expressions régulières, qui est vérifiée (à la volée) sur la description LOTOS grâce à l'outil EVALUATOR 3.0.
Ces deux méthodes d'analyse ont été appliquées sur différents types de traces fournies par BULL et préalablement validées par l'implémentation en C++ du circuit BSPS :
Pour les traces dites de collision, nous avons analysé plus de 130 méga-octets de traces produites par le modèle VERILOG (représentant environ 24000 transactions effectuées entre le circuit BSPS et les autres modules) sans découvrir d'erreur dans le protocole de cohérence de caches. Naturellement, ceci ne constitue pas une garantie absolue, compte-tenu du nombre élevé de cas possibles.
Pour les traces dites d'interface, l'objectif n'était pas de valider le circuit lui-même, mais de déterminer si les tests écrits manuellement par BULL assuraient une couverture exhaustive par rapport aux tables états/transitions. Sur les traces correspondant à ces tests, 761 propriétés temporelles ont été vérifiées, dont 216 n'étaient satisfaites par aucune trace. Après interprétation de ces résultats conjointement avec les concepteurs de FAME, il est apparu que ces propriétés non vérifiées se réduisaient à 24 situations ``réelles'' qui n'étaient pas testées. Ceci a permis de rajouter 2 nouveaux tests pour couvrir les 24 cas manquants.
De même, pour les traces dites directory, 518 propriétés ont été vérifiées, dont 196 n'étaient pas satisfaites par l'ensemble de traces. Après analyse, ceci a permis de rajouter un test supplémentaire pour couvrir les cas manquants.
Grâce aux améliorations des outils CADP (en particulier, l'évaluation optimisée des propriétés sur les traces), l'ensemble de ces vérifications peut désormais être effectué en une nuit sur une machine standard (processeur Pentium III 700 MHz avec 1 giga-octet de mémoire vive).
Génération automatique de tests
Un autre objectif de FORMALFAME consiste à générer des cas de test en les dérivant automatiquement 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 viennent compléter les tests écrits manuellement.
Initialement, il était prévu d'utiliser l'outil TGV afin de produire des tests déterministes. Toutefois, l'écriture manuelle des tests déterministes par l'équipe BULL aux Clayes-sous-Bois ayant atteint les objectifs fixés, nous avons orienté nos travaux vers la production de tests aléatoires.
En 2001, nous avons conçu et étudié la faisabilité d'une approche basée sur le compilateur CAESAR en mode ``génération de code'' (EXEC/CAESAR). Dans cette approche, les tests sont obtenus par des exécutions aléatoires de la description LOTOS selon différentes distributions de probabilité.
Nos premières expérimentations concluent à la possibilité de connecter le code C produit par EXEC/CAESAR à la plate-forme de test de BULL afin que celle-ci puisse être directement pilotée par la description LOTOS.
Les résultats de FORMALFAME en 2001 ont été jugés positifs par BULL. Outre l'amélioration de la spécification informelle du protocole de cohérence de caches par la correction de deux imprécisions, les outils de vérification de CADP ont permis de mesurer précisément la couverture fonctionnelle des tests et de rajouter des cas de test manquants pour atteindre la totalité des objectifs du plan de test de l'architecture FAME.
Suite à ces résultats, l'équipe BULL des Clayes-sous-Bois a adopté la technologie basée sur LOTOS et CADP (en particulier, l'analyse automatique des traces d'exécution) afin de l'intégrer à sa propre méthodologie de validation utilisée pour l'architecture FAME.
Back to the VASY Home Page