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:bsp [2018/03/29 16:39]
apeiron 		fr:research:bsp [2018/03/29 17:10]
apeiron [Résumé]
Ligne 26: Ligne 26:
 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. 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).