Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
Prochaine révision 		Révision précédente
Prochaine révision Les deux révisions suivantes
fr:research:projects [2017/04/25 13:01]
apeiron 		fr:research:projects [2021/04/05 18:04]
apeiron
Ligne 3: Ligne 3:
 ====== Recherche en cours ====== ====== Recherche en cours ======
  
-===== Caractérisation impérative des algorithmes BSP =====+TODO
  
-L'​article soumis pour [[https://​hlpp2017.infor.uva.es/​|HLPP 2017, 10th International Symposium on High-Level Parallel Programming and Applications]] est disponible {{ :​fr:​research:​bsp1.pdf |ici}}.+====== Projets de recherche ======
  
-Bulk Synchronous Parallelism est un modèle de programmation parallèle consistant en la séquentialisation de \textbf{super-étapes} divisées en trois phases : +===== Caractérisation fonctionnelle ​des algorithmes ​en temps polynomial =====
-  - 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 : +Avec mon ancien directeur ​de thèse Pierre Valarcher, professeur ​à l'​Université Paris-Est Créteil, nous avons travaillé sur la [[fr:​research:​models-computation#​algorithmes_sequentiels|caractérisation impérative ​des algorithmes en temps polynomial]] c'est à dire sur la preuve ​que d'​une ​part notre langage ​de programmation impératif PLoopC ​est bien en temps polynomial, et d'autre part que tout algorithme séquentiel peut être simulé par PLoopC.
-$$\text{cost of a superstep} = \max_{\text{processes}}w_i + \max_{\text{processes}}h_i \times g + \ell$$ +
-où $w_i$ est le temps nécessaire au processeur $i$ pour faire ses calculs locaux, $h_i$ est le nombre de communications envoyées ou reçues par le processeur $i$, $g$ est une mesure de la perméabilité du réseau, et $\ell$ est le coût d'une barrière de synchronisation.+
  
-Différents langages de programmation((Comme l'adoption par Google ​de Pregel et MapReduce, des projets libres ​de programmation avec de grandes performances comme Apache Hama ou Apache Giraph, des langages ​spécifiques ​comme BSML, ou et des implémentations ​de la BSPLib comme la Paderborn University BSP library ou la Oxford BSP Toolset de Jonathan Hill.)) ont tenté d'​implémenter ​les algorithmes ​BSP, mais pour l'​instant il n'y a pas de définition explicite faisant consensus.+Pour faire cette preuve nous avons utilisé les ASMs, c'est à dire une présentation impérative des algorithmes,​ mais d'​autres modèles ont été présentés dans un cadre fonctionnel,​ comme les récurseurs ​de Moschovakis. De plus, de nombreux ​langages ​(comme le langage LPL de Patrick Baillot, Marco Gaboardi ​et Virgile Mogbil) essayant ​de caractériser ​les algorithmes ​polynomiaux sont des langages fonctionnels.
  
-Notre but avec Frédéric Gava, maître de conférences à l'​Université Paris-Est Créteil, ​est de faire un travail similaire à celui de Gurevich pour définir **axiomatiquement** les algorithmes BSP avant de prouver que ces algorithmes peuvent être vus comme une extension naturelle du modèle des ASMs, et enfin de montrer une **équivalence algorithmique** des ces ASMs étendues avec un langage de programmation impératif. Ainsi, ce langage sera caractéristique des algorithmes BSP, et pourra être pris comme définition opérationnelle de ces algorithmes.+Notre but est donc de créer une version fonctionnelle ​de notre langage, et de prouver l'équivalence algorithmique ​entre la version impérative et la version fonctionnelle, ce qui permettra ensuite de comparer la version fonctionnelle aux modèles ​et langages existants.
  
-===== Caractérisation fonctionnelle des algorithmes ​en temps polynomial ​=====+===== Equivalence algorithmique ​en PLoopC et LPL =====
  
-====== Projets de recherche ======+Le langage LPL de Patrick Baillot, Marco Gaboardi et Virgile Mogbil est un langage de programmation fonctionnel,​ qui est en temps polynomial en s'​assurant syntaxiquement de la réduction des termes dans les définitions,​ et en contraignant la récursion par un système de type issu de la logique linéaire. 
 + 
 +Ce langage possède des caractéristiques proches de notre langage PLoopC comme l'​utilisation de fonctions de base pour écrire les algorithmes (approche oraculaire) et des schémas de récursion syntaxiquement très souples, qui lui permettent notamment d'​obtenir le minimum de Colson. Aussi, Pierre Valarcher et moi soupçonnons qu'il soit possible de prouver l'​équivalence algorithmique entre LPL et la future version fonctionnelle de notre langage PLoopC. 
 + 
 +Cela permettrait de faire un pont entre la communauté de la **complexité implicite** et la communauté de la **complexité par typage,** tout en fournissant une paire de langages capables de mettre fin à la quête d'un langage caractérisant les algorithmes polynomiaux. 
 + 
 +===== Séries divergentes ​=====
  
 +Comme indiqué dans [[fr:​vulgarisation:​series-divergentes|mon article sur les séries divergentes]],​ le travail fait par Lê (de la chaîne Science4All) et moi pourrait mener à une caractérisation des séries divergentes sommables de façon unique par linéarité,​ stabilité et régularité. Mais pour cela il faudrait que je me mette à jour sur l'​état de l'art (toute aide serait la bienvenue) puis faire la preuve rigoureusement avant de la soumettre quelque part (je ne connais pas cette communauté,​ encore une fois toute aide serait la bienvenue ^^).