Différences
Ci-dessous, les différences entre deux révisions de la page.
| Les deux révisions précédentes Révision précédente Prochaine révision | Révision précédente | ||
|
fr:research:bsp [2018/03/29 17:15] apeiron |
— (Version actuelle) | ||
|---|---|---|---|
| Ligne 1: | Ligne 1: | ||
| - | Ce travail a démarré fin 2016, et a été réalisé en collaboration avec Frédéric Gava, maître de conférences à l'Université Paris-Est Créteil. Bien qu'il n'ait pas été financé par contrat, j'ai été affilié au Laboratoire d’Algorithmique, Complexité et Logique pendant que j'exerçais mon activité de chercheur bénévole. | ||
| - | ====== Versions ====== | ||
| - | |||
| - | **An ASM Thesis for BSP** (Yoann Marquer, Frédéric Gava), le {{ :fr:research:bsp-asm.pdf |premier rapport technique}}, est disponible sur [[https://hal.archives-ouvertes.fr/hal-01717647|HAL]]. | ||
| - | |||
| - | **Algorithmic Completeness of BSP Languages** (Yoann Marquer, Frédéric Gava), le {{ :fr:research:bsp-while.pdf |second rapport technique}}, est disponible sur [[https://hal.archives-ouvertes.fr/hal-01742406|HAL]]. | ||
| - | |||
| - | |||
| - | |||
| - | ====== Résumé ====== | ||
| - | |||
| - | La thèse de Gurevich énonce que l'ensemble des algorithmes séquentiels sont capturés par ses trois postulats. De plus, il a prouvé que ces trois postulats définissent le même ensemble que ses Abstract State Machines. Ainsi, nous avons que ASM = Algo. Cela montre que l'approche axiomatique des postulats est équivalente à l'approche opérationnelle des ASMs. | ||
| - | |||
| - | Dans [[fr:research:fi-while|cet article]], j'ai montré que les langages impératifs usuels sont non seulement Turing-complets mais aussi algorithmiquement complets. Cela a été fait en prouvant qu'un langage impératif minimal While est **algorithmiquement équivalent** aux ASMs de Gurevich. Ainsi, nous avons While ≃ ASM, ce qui signifie plus précisément que les exécutions des deux modèles de calcul sont les mêmes, à variables fraîches et dilatation temporelle près. Donc nous avons While ≃ Algo, ce qui montre que tout langage de programmation contenant les commandes de While est algorithmiquement complet (pour les algorithmes séquentiels). | ||
| - | |||
| - | Dans le contexte HPC (High Performance Computing), un résultat similaire paraît difficile à obtenir. Le problème principal est le manque de définition pour ce qu'est formellement un calcul HPC, ou dit autrement, la communauté HPC manque d'une définition consensuelle de ce qu'est la classe des algorithmes HPC. Utiliser un **modèle pont**((Voir l'article de Valiant : A Bridging Model for Parallel Computation)) peut être vu comme un premier pas dans cette direction, qui fournit un pont conceptuel entre l'implémentation physique de la machine, et l'abstraction possible pour le programmeur. Cela simplifie également la tâche de la conception d'algorithme, leur programmation, et assure une meilleure portabilité d'un système à l'autre. Et, plus important encore, cela permet de raisonner sur le coût même des algorithmes. | ||
| - | |||
| - | Plus précisément, BSP (Bulk Synchronous Parallelism) est un modèle de programmation parallèle consistant en la séquentialisation de **super-étapes** divisées en trois phases : | ||
| - | - Chaque processeur effectue des calculs locaux, en n'utilisant que les valeurs stockées dans sa propre mémoire. | ||
| - | - Puis les processeurs envoient ou reçoivent des données. | ||
| - | - Enfin, une barrière de synchronisation a lieu quand les communications sont terminées, et rend les données échangées disponibles aux mémoires locales des processeurs. | ||
| - | |||
| - | Le but est de rendre les programmes simples à écrire, indépendants des architectures, et que les performances d'un programme sur une architecture donné soit prévisible. Pour cela, les algorithmes BSP sont associés à un modèle de coût : le coût (en temps) d'une super-étape est **w + h×g + l**, où w est le nombre maximum de calculs fait par un processeur durant la super-étape, h est le nombre maximum de messages envoyés ou reçus, g mesure la perméabilité du réseau et l est le coût de la barrière de synchronisation. | ||
| - | |||
| - | Jusqu'à maintenant, il y a eu de nombreux langages de programmation ou bibliothèques pour programmer des algorithmes BSP, comme la BSPLIB pour le langage C ou Java, BSML, Pregel pour le big-data, etc. Mais pour l'instant il n'y a pas de définition explicite faisant consensus. | ||
| - | |||
| - | Notre but a été de faire un travail similaire à celui de Gurevich pour définir axiomatiquement les **algorithmes BSP**, de prouver que ces algorithmes peuvent être vus comme une extension naturelle du modèle des ASMs, et enfin de montrer une **équivalence algorithmique** de ces ASMs étendues avec un langage de programmation impératif. Ainsi, ce langage est caractéristique des algorithmes BSP, et peut être pris comme définition opérationnelle des algorithmes séquentiels. | ||
| - | |||
| - | Dans le premier rapport technique, nous avons axiomatisé l'ensemble Algo-BSP des algorithmes BSP en étendant les trois postulats de Gurevich d'un seul processeur à un p-uplet de processeurs travaillant simultanément, et en ajoutant un **quatrième postulat** pour tenir compte des super-étapes dans le modèle BSP, c'est à dire l'alternance dans un algorithme BSP entre phase de calcul (où les processeurs font leurs calculs de manière indépendante) et phase de communication. | ||
| - | |||
| - | Puis nous avons étendu le modèle de calcul ASM à des p-uplet de processeurs en appliquant le même programme ASM en même temps à chaque processeur durant les phases de calcul, et durant les phases de communication en supposant l'existence d'une fonction de communication abstraite (afin que le résultat ne dépende pas d'une implémentation particulière des communications). Nous avons prouvé que cette extension ASM-BSP est bien la contrepartie opérationnelle des algorithmes BSP définis de manière axiomatique, c'est à dire que ASM-BSP = Algo-BSP. | ||
| - | |||
| - | Comme dans [[fr:research:fi-while|mon article sur While]] nous pensons qu'un langage impératif est plus pratique qu'une simple fonction de transition pour déterminer des classe en temps ou en espace, ou tout simplement pour être comparé à des langages de programmation plus usuels. Ainsi, nous avons défini dans le deuxième rapport technique la sémantique opérationnelle d'un langage impératif minimal While-BSP travaillant sur des p-uplets de processeurs. Enfin, nous avons prouvé que While-BSP et ASM-BSP pouvaient se simuler l'un l'autre d'un point de vue algorithmique: While-BSP ≃ ASM-BSP. | ||
| - | |||
| - | De ces deux rapports techniques, nous pouvons donc déduire que While-BSP ≃ Algo-BSP, et donc que notre langage impératif minimal est bien algorithmiquement complet (pour les algorithmes BSP). | ||