|
|
|
|
| Directeur de l'action | Massimo Zendri (BULL) (jusqu'au 31 mars 2000)
Nicolas Zuanon (BULL) (depuis le 15 mai 2000) |
| 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, jusqu'au 11 avril 2000) |
| Ingénieurs Experts | Marc Herbert (jusqu'au 30 septembre 2000)
Frédéric Perret (depuis le 20 novembre 2000) Solofo Ramangalahy |
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 (Massimo Zendri, puis Nicolas Zuanon) 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 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 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 [1] et le protocole de cohérence de caches de l'architecture multiprocesseurs POLYKID [2] [3] [4]. 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 travaux portent sur FAME, une architecture multiprocesseurs CC-NUMA développée par BULL et basée sur des processeurs INTEL ITANIUM 64 bits. D'abord informelle, la collaboration a été officialisée en 1999 sous la forme d'une nouvelle action DYADE, intitulée FORMALFAME, menée en collaboration avec l'équipe d'Anne Kaszynski au centre BULL des Clayes-sous-Bois (France).
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.
Pour la simulation et la vérification, l'action FORMALFAME utilise les méthodes énumératives mises en oeuvre dans la boite à outils CADP développée notamment par le projet VASY. Pour la génération automatique de tests, elle utilise l'outil TGV développé notamment par le projet PAMPA.
Depuis décembre 1999, les travaux de FORMALFAME portent sur une nouvelle version de l'architecture FAME à base de processeurs Intel Itanium et, plus précisément, sur la validation d'un circuit appelé B-SPS qui implémente le protocole de cohérence de caches de l'architecture FAME. Le fonctionnement de ce protocole 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. L'implémentation du circuit B-SPS est décrite par un modèle en langage VERILOG. Un simulateur logiciel en langage C++ de ce circuit est également disponible pour valider les résultats générés par le modèle VERILOG.
En 2000, les travaux de FORMALFAME ont concerné les points suivants :
Description formelle du protocole de cohérence de caches
Massimo Zendri a d'abord réalisé une modélisation simplifiée du circuit B-SPS et de son environnement (processeurs). Cette modélisation, qui ne traitait pas les collisions d'accès à une même adresse dues à la concurrence des transactions, a ensuite été reprise et complétée par Nicolas Zuanon pour prendre en compte les dernières évolutions du protocole, ainsi que le traitement des collisions. La description complète comporte 12 processus concurrents (5000 lignes de code LOTOS).
Dans un second temps, une variante plus abstraite de cette description LOTOS a été développée. Comportant 7 processus LOTOS (4500 lignes de code), cette variante est destinée à la validation des traces (voir ci-après) ; elle se concentre sur le fonctionnement observable du circuit B-SPS en faisant abstraction de l'environnement (processeurs) et de certains aspects d'implémentation.
Simulation et vérification des descriptions formelles
La mise au point des deux descriptions LOTOS a été facilitée par l'existence, dans la boîte à outils CADP, du simulateur graphique OCIS (Open/Caesar Interactive Simulator) mis à notre disposition à partir de mars 2000. L'action FORMALFAME a joué un rôle significatif pour le test en vraie grandeur et la mise au point de cet outil développé par le projet VASY.
Une vérification par model-checking des descriptions LOTOS développées dans FORMALFAME a été brièvement tentée, mais s'est heurtée au problème de l'explosion d'états. Faute de temps, cette vérification n'a pas pu être poursuivie ; néanmoins, les améliorations des outils de vérification compositionnelle de CADP effectuées par le projet VASY en collaboration avec le laboratoire VERIMAG devraient permettre de surmonter cet obstacle à l'avenir.
Génération automatique de tests
Un des objectifs initiaux de l'action FORMALFAME consistait à générer des cas de test grâce à l'outil TGV en les dérivant automatiquement de la description LOTOS. Cette tâche a été retardée du fait des délais liés au remplacement de Massimo Zendri. En effet, à la date d'embauche de Nicolas Zuanon, l'écriture manuelle des tests par l'équipe BULL aux Clayes-sous-Bois avait atteint les objectifs fixés (plus de 30.000 cas de test exécutés). En conséquence, l'action FORMALFAME s'est réorientée vers des objectifs plus prioritaires.
En parallèle, les projets PAMPA et VASY ont terminé l'intégration de l'outil TGV dans l'interface graphique de CADP, ce qui facilitera son utilisation ultérieure.
Vérification automatique de traces d'exécution
L'action FORMALFAME a travaillé à l'analyse automatisée des traces d'exécution produites soit par le modèle VERILOG, soit par le simulateur C++ du circuit B-SPS. 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 des propriétés de correction sur les traces en utilisant la logique temporelle acceptée par l'outil de vérification EVALUATOR 3.0. 700 propriétés de séquencement ont ainsi été spécifiées et vérifiées. Ce résultat a été rendu possible grâce à plusieurs améliorations apportées aux outils CADP pour réduire le temps de vérification :
Les primitives de lecture du format binaire BCG dans lequel sont encodées les traces ont été rendues plus rapides ;
L'outil EVALUATOR 3.0 a été optimisé pour prendre en compte les graphes sans circuit (dont les traces sont un cas particulier) ;
Un outil prototype appelé SEQ.OPEN a été développé pour permettre de manipuler, via l'interface de programmation OPEN/CAESAR, des traces encodées simplement en format ASCII.
soit la trace à vérifier est encodée comme une expression régulière dont on détermine l'acceptation grâce à l'outil EXHIBITOR de CADP,
soit la trace à vérifier est encodée comme une formule de logique temporelle (comportant des expressions régulières) et évaluée grâce à l'outil EVALUATOR 3.0.
Les résultats obtenus par FORMALFAME en 2000 ont été jugés positifs. Le travail de modélisation formelle a soulevé 10 questions qui, adressées aux développeurs de l'architecture FAME, ont contribué à éliminer divers proble`mes (imprécisions, ambiguïtés, incomplétudes ou incohérences) dans la description informelle du protocole de cohérence de caches. De plus, la vérification des traces a mis en évidence un problème majeur (ambiguïté dans la spécification informelle du protocole, également détectée par le simulateur C++ du circuit B-SPS) qui a confirmé l'intérêt des travaux menés dans l'action FORMALFAME.
Back to the VASY Home Page