Static Analysis for BSPlib Programs
La programmation parallèle consiste à utiliser des architectures à multiples unités de traitement, de manière à ce que le temps de calcul soit inversement proportionnel au nombre d unités matérielles. Le modèle de BSP (Bulk Synchronous Parallel) permet de rendre le temps de calcul prévisible. BSPlib...
Gorde:
| Egile nagusia: | |
|---|---|
| Beste egile batzuk: | , , , , , , , , |
| Formatua: | Thèse numérique |
| Hizkuntza: | Anglais Français |
| Argitaratua: |
2019.
|
| Gaiak: | |
| Sarrera elektronikoa: | Accès au texte intégral https://theses.univ-orleans.fr/public/2019ORLE2005_vm.pdf http://www.theses.fr/2019ORLE2005/abes https://theses.hal.science/tel-02920363 |
| Oharra: |
Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) Autre(s) contribution(s) : Emmanuel Chailloux (Président du jury) ; Gaétan Hains, Wadoud Bousdira, Herbert R. Kuchen, Frédéric Dabrowski, Denis Barthou, Wijnand Suijlen (Membre(s) du jury) |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Analyse statique des programmes BSPlib |
| Gaia: | La programmation parallèle consiste à utiliser des architectures à multiples unités de traitement, de manière à ce que le temps de calcul soit inversement proportionnel au nombre d unités matérielles. Le modèle de BSP (Bulk Synchronous Parallel) permet de rendre le temps de calcul prévisible. BSPlib est une bibliothèque pour la programmation BSP en langage C. En BSPlib on entrelace des instructions de contrôle de la structure parallèle globale, et des instructions locales pour chaque unité de traitement. Cela permet des optimisations nes de la synchronisation, mais permet aussi l écriture de programmes dont les calculs locaux divergent et masquent ainsi l évolution globale du calcul BSP. Toutefois, les programmes BSPlib réalistes sont syntaxiquement alignés, une propriété qui garantit la convergence du ot de contrôle parallèle. Dans ce mémoire nous étudions les trois dimensions principales des programmes BSPlib du point de vue de l alignement syntaxique : la synchronisation, le temps de calcul et la communication. D abord nous présentons une analyse statique qui identi e les instructions syntaxiquement alignées et les utilise pour véri er la sûreté de la synchronisation globale. Cette analyse a été implémentée en Frama-C et certi ée en Coq. Ensuite nous utilisons l alignement syntaxique comme base d une analyse statique du temps de calcul. Elle est fondée sur une analyse classique du coût pour les programmes séquentiels. En n nous dé nissons une condition suf sante pour la sûreté de l enregistrement des variables. L enregistrement en BSPlib permet la communication par accès aléatoire à la mémoire distante (DRMA) mais est sujet à des erreurs de programmation. Notre développement technique est la base d une future analyse statique de ce mécanisme. The goal of scalable parallel programming is to program computer architectures composed of multiple processing units so that increasing the number of processing units leads to an increase in performance. Bulk Synchronous Parallel (BSP) is a widely used model for scalable parallel programming with predictable performance. BSPlib is a library for BSP programming in C. In BSPlib, parallel algorithms are expressed by intermingling instructions that control the global parallel structure, and instructions that express the local computation of each processing unit. This lets the programmer ne-tune synchronization, but also implement programs whose diverging parallel control ow obscures the underlying BSP structure. In practice however, the majority of BSPlib program are textually aligned, a property that ensures parallel control ow convergence. We examine three core aspects of BSPlib programs through the lens of textual alignment: synchronization, performanceandcommunication.First,wepresentastaticanalysisthatidenti estextuallyalignedstatements and use it to verify safe synchronization. This analysis has been implemented in Frama-C and certi ed in Coq. Second, we exploit textual alignment to develop a static performance analysis for BSPlib programs, based on classic cost analysis for sequential programs. Third, we develop a textual alignment-based suf cient condition for safe registration. Registration in BSPlib enables communication by Direct Remote Memory Access but is error prone. This development forms the basis for a future static analysis of registration. |
|---|---|
| Alearen deskribapena: | Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) Autre(s) contribution(s) : Emmanuel Chailloux (Président du jury) ; Gaétan Hains, Wadoud Bousdira, Herbert R. Kuchen, Frédéric Dabrowski, Denis Barthou, Wijnand Suijlen (Membre(s) du jury) |
| Formatua: | Configuration requise : un logiciel capable de lire un fichier au format : PDF |