Evaluation des performances de benchmarks MPI sur des ...

Description

9ième Atelier en Evaluation de Performances
Aussois, du 1 au 4 juin 2008
notre étude est la composition parallèle de deux
processus P et P , qui s’envoient alternativement0 1
un seul message à la fois :Evaluation des performances de
benchmarks MPI sur des ping_pong(P ,P ) =0 1
architectures multiprocesseur de 0 1 0 1
||type CC-DSM
1 0 1 0
Meriem Zidouni Dans une implémentation MPICH pour une archi-
tecture CC-DSM, les primitives send et receive uti-
Bull S.A.
lisent des tampons de messages et éventuellementPlatforms Hardware R&D
des verrous pour gérer l’exclusion d’accès aux tam-Architecture & Verification
pons, en tant que mécanisme de communication.Rue Jean Jaurès
Ces structures de communication résident dans la78340 Les Clayes Sous Bois, FRANCE
mémoire distribuée et leurs accès sont régis par [e-mail]
protocole de cohérence de caches qui assure l’in-
tégrité des données, et implique l’emplacement de
1. Introduction
leur valeur valide à un moment donné.
Comme le programme contient des processus quiDans le cadre de son offre de serveurs haut de
1 s’exécutent en parallèle et accèdent à des variablesgamme, Bull conçoit des multiprocesseurs à mé-
partagées, un accès d’un processus aura une la-moire distribuée partagée avec un protocole de co-
tence qui ne peut pas être déterminée statique-hérence de caches CC-DSM (Cache-Coherent Distri-
ment, puisqu’elle dépend de l’entrelacement desbuted Shared ...

Sujets

• D'une ombre à l'autre
• Primitives de fonctions rationnelles
• Comité de Surveillance et de Suivi
• Modélisation des données
• Verrou
• Variables d'échelle de Bjorken

Informations

• Publié par: Udwue
• Nombre de lectures: 74
• Langue: Français

Extrait

9iÈme Atelier en Evaluation de Performances Aussois, du 1 au 4 juin 2008

notre Étude est la composition parallÈle de deux processusP 0 etP 1 , qui s’envoient alternativement un seul message À la fois : Evaluation des performances de benchmarks MPI sur des ping_pong(P 0 ,P 1 ) = architectures multiprocesseur de <send(P 0 →P 1 ) ;receive(P 0 ←P 1 )> || type CC-DSM <receive(P 1 ←P 0 ) ;send(P 1 →P 0 )> Meriem Zidouni Dans une implÉmentation MPICH pour une archi- tecture CC-DSM, les primitivessendetreceiveuti- Bull S.A. lisent des tampons de messages et Éventuellement Platforms Hardware R&D des verrous pour gÉrer l’exclusion d’accÈs aux tam- Architecture & Verification pons, en tant que mÉcanisme de communication. Rue Jean JaurÈs Ces structures de communication rÉsident dans la 78340 Les Clayes Sous Bois, FRANCE mÉmoire distribuÉe et leurs accÈs sont rÉgis par le [e-mail] protocole de cohÉrence de caches qui assure l’in- tÉgritÉ des donnÉes, et implique l’emplacement de 1. Introduction leur valeur valide À un moment donnÉ. Comme le programme contient des processus qui Dans le cadre de son offre de serveurs haut de 1 s’exÉcutent en parallÈle et accÈdent À des variables gamme, BullconÇoit des multiprocesseurs À mÉ- partagÉes, un accÈs d’un processus aura une la- moire distribuÉe partagÉe avec un protocole de co- tence qui ne peut pas tre dÉterminÉe statique- hÉrence de caches CC-DSM (Cache-Coherent Distri- ment, puisqu’elle dÉpend de l’entrelacement des buted Shared Memory) et fournit une implÉmenta- actions qui auront prÉcÉdÉ cet accÈs. Par consÉ- tion de la bibliothÈque de programmation paral- quent, l’accÈs À une variable peut avoir diffÉ- lÈle MPI (Message Passing Interface). Le but de notre rentes latences possibles correspondant aux Éven- recherche est de fournir une mÉthode et ses ou- tuels transferts entre l’emplacement de la donnÉe tils associÉs, permettant l’Évaluation et l’optimisa- valide (mÉmoire locale ou distante, ou cache d’un tion de cette implÉmentation en fonction de l’archi- processeur distant ) par rapport au processeur de- tecture matÉrielle : topologie d’interconnexion et mandeur. La latence de ces transferts dÉtermine la protocole de cohÉrence de caches. Ceci permettra, performance des communications et des synchro- d’une part, de faire les bons choix d’architecture nisations inter-processus. matÉrielle et d’implÉmentation logicielle au mo- ment de la conception, et d’autre part, fournira des Nous avons modÉlisÉ de faÇon indÉpendante, en ÉlÉments d’analyse nÉcessaires pour comprendre langage LOTOS, les 3 aspects qui dÉfinissent les les mesures faites au moment de la validation de la performances d’une implÉmentation de MPI dans machine rÉelle. Nous dÉfinissons et expÉrimentons une architecture CC-DSM : une telle mÉthode, À travers l’Étude de cas d’un 1. lasuccession d’accÈs dÉfinie par l’algorithme benchmark de MPI (ping-pong). Notre mÉthode de des primitives de communication : dans notre modÉlisation est basÉe sur la thÉorie des IMC (In- cas de ping-pong, il s’agit des primitivessend teractive Markov Chains), implÉmentÉe dans la bote etreceivequi correspondent À des suites d’ac- À outils CADP [1]. Elle consiste À modÉliser le sys- cÈs aux variables pour des opÉrations de lec- tÈme en langage LOTOS [2], puis À vÉrifier formel- ture (load) et d’Écriture (store) ; lement sa correction fonctionnelle, et finalement À 2. leprotocole de cohÉrence de caches qui rÉgit Évaluer ses performances aprÈs l’avoir augmentÉ les changements des États des caches (suivant avec des informations quantitatives (latences). le protocole MESI classique), et les transferts entre caches et mÉmoires, et entre caches ; 2. ModÉlisationet vÉrification du benchmark 3. latopologie d’interconnexion de l’architecture ping-pong multiprocesseur, qui dÉtermine la latence des transferts suivant le niveau de distance entre Le benchmark ping-pong consiste en des envois les mÉmoires et les processeurs et entre les alternÉs de messages entre processus via les processeurs. primitivessendetreceive. Celui considÉrÉ dans Nous avons vÉrifiÉ la correction fonctionnelle du 1 http ://www.bull.com comportement donnÉ par la spÉcification LOTOS

du ping-pong avec les outils de CADP. Pour– ladistance entre les processeurs dans le rÉseau Établir la correction de l’algorithme ping-pong,d’interconnexion de l’architecture : on considÈre nous avons employÉ la vÉrification visuelle (vi-trois niveaux diffÉrents de distance entre les pro- sual checkingcesseurs sur lesquels s’exÉcute le ping-pong ;) en utilisant les outils BCG_MIN et BCG_EDIT. Pour analyser le protocole de cohÉ-– leprotocole de cohÉrence de caches : on Étudie rence de caches et la gestion des verrous, nousdeux protocoles de cohÉrence de caches dont la avons utilisÉ la vÉrification par logiques tempo-diffÉrence rÉside dans le changement des États relles (model checkingdes caches ;) À l’aide de l’outil EVALUA- TOR. –les primitivessendetreceive: on considÈre deux sortes de primitives : celles qui utilisent des listes chanÉes avec des verrous, et celles qui utilisent 3. Evaluation des performances du benchmark des tampons sans verrous. ping-pong Le but de notre Étude est d’Évaluer les perfor- 5. Conclusionet perspectives mances du benchmark ping-pong, ce qui consiste À calculer la latence d’un Échange de message (un Nous envisageons de poursuivre nos recherches sendsuivi d’unreceive) et le nombre demiss effec- suivantplusieurs directions. PremiÈrement, nous tuÉs sur chaque variable de l’algorithme pendant allons focaliser nos efforts sur la modÉlisation en cet Échange. Pour cela, nous avons adoptÉ l’ap- LOTOS de plusieurs variantes de protocoles de co- proche proposÉe en [3] basÉe sur la thÉorie des hÉrence de caches, ainsi que d’autres primitives de IMC. Elle consiste À enrichir la spÉcification LO- communication et de synchronisation de MPI. Ces TOS, dont les propriÉtÉs fonctionnelles ont ÉtÉ dÉjÀ modÈles, groupÉs dans des bibliothÈques rÉutili- vÉrifiÉes, par des informations quantitatives appe- sables et paramÉtrÉes par la topologie d’intercon- lÉesdÉlais Markoviens. Dans notre cas, ces dÉlais nexion des processeurs, permettraient de modÉ- Markoviens correspondent aux latences des trans- liser facilement des configurations diffÉrentes de ferts d’accÈs aux variables par les opÉrations de machines. DeuxiÈmement, nous souhaitons mettre lecture et d’Écriture, ÉvaluÉes durant la gÉnÉration en oeuvre une traduction automatique entre la des- du modÈle du ping-pong en LOTOS. Ensuite, il cription de l’algorithme distribuÉ et des primitives faut vÉrifier, d’une part, que cette insertion est sÉ- de communication et la modÉlisation LOTOS cor- mantiquement correcte, en s’assurant par exemple respondante, augmentÉe de latences. Cela permet- qu’elle prÉserve la concurrence des processus pa- trait de disposer d’une chane complÈte de modÉli- rallÈles dans le temps, et d’autre part, qu’elle ne sation et Évaluation de performances qui assiste- perturbe pas le comportement fonctionnel de la rait de maniÈre utile les concepteurs de logiciels spÉcification originelle. Nous avons appliquÉ l’ou- distribuÉs sur les machines multiprocesseurs. til BCG_STEADY de CADP pour le calcul des per- formances sur le modÈle Markovien du ping-pong. Bibliographie C’est un outil qui permet de calculer, de maniÈre 1. H.Garavel, F. Lang, R. Mateescu, and W. Serwe. – itÉrative, À l’État d’Équilibre la distribution de pro- CADP 2006 : A Toolbox for the Construction and babilitÉ À long terme (de ce fait, on obtient la la- Analysis of Distributed Processes. – Proceedings of tence d’un Échange de message), et de fournir des the 19th International Conference on Computer Ai- mesures de dÉbit pour chacune des Étiquettes de ded Verification CAV’2007 (Berlin, Germany), vol. transitions (on obtient le nombre demisseffectuÉs 4590 of Lecture Notes in Computer Science, pp. sur chaque variable pendant l’Échange d’un mes- 158-163. Springer Verlag, July 2007. sage). 2. ISO/IEC.– LOTOS : A Formal Description Tech- nique based on the Temporal Ordering of Observa- 4. RÉsultats tional Behaviour. – International Standard ISO/IEC 8807, 1989. Cette approche nous a permis d’obtenir des la- 3. H. Garavel and H. Hermanns. – On Combining tences moyennes d’Échange d’un message confor- Functional Verification and Performance Evalua- tÉes par les mesures expÉrimentales, et de les ana- tion using CADP. – Proceedings of the 11th Inter- lyser avec le nombre demisseffectuÉ sur les diffÉ- national Symposium on Formal Methods Europe rentes variables pendant cet Échange. FME’2002 (Copenhague, Denmark), vol. 2391 of Nous avons Également ÉvaluÉ et analysÉ les perfor- Lecture Notes in Computer Science, pp. 410-429. Springer Verlag, July 2002. mances du ping-pong en faisant varier des aspects matÉriels et logiciels :

2