Evaluation des performances de benchmarks MPI sur des ...
2
pages
Français
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
2
pages
Français
Ebook
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
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 de0 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 leMeriem.Zidouni@bull.net
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 ...
Voir
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
||type CC-DSM
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 leMeriem.Zidouni@bull.net
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 ...
9iÈme Atelier en Evaluation de Performances Aussois, du 1 au 4 juin 2008
notre Étude est la composition parallÈle de deux processusP0etP1, qui s’envoient alternativement un seul message À la fois : Evaluation des performances de benchmarks MPI sur desping_pong(P0,P1) = architectures multiprocesseur de<send(P0→P1) ;receive(P0←P1)> || type CC-DSM <receive(P1←P0) ;send(P1→P0)> 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 Meriem.Zidouni@bull.net 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 desNous avons modÉlisÉ de faÇon indÉpendante, en ÉlÉments d’analyse nÉcessaires pour comprendrelangage LOTOS, les 3 aspects qui dÉfinissent les les mesures faites au moment de la validation de laperformances d’une implÉmentation de MPI dans machine rÉelle. Nous dÉfinissons et expÉrimentonsune architecture CC-DSM : une telle mÉthode, À travers l’Étude de cas d’un1. lasuccession d’accÈs dÉfinie par l’algorithme benchmark de MPI (ping-pong). Notre mÉthode dedes 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 boteetreceivequi 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.comcomportement 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 chanÉ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 (unNous envisageons de poursuivre nos recherches sendsuivi d’unreceive) et le nombre demisseffec- suivantplusieurs directions. PremiÈrement, nous tuÉs sur chaque variable de l’algorithme pendantallons 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 deshÉ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Élaisnexion 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 demachines. DeuxiÈmement, nous souhaitons mettre lecture et d’Écriture, ÉvaluÉes durant la gÉnÉrationen oeuvre une traduction automatique entre la des-du modÈle du ping-pong en LOTOS. Ensuite, ilcription 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 exemplerespondante, augmentÉe de latences. Cela permet-qu’elle prÉserve la concurrence des processus pa-trait de disposer d’une chane complÈte de modÉli-rallÈles dans le temps, et d’autre part, qu’elle nesation et Évaluation de performances qui assiste-perturbe pas le comportement fonctionnel de larait 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Ésultatstional 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
© 2010-2024 YouScribe
