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 Les deux révisions suivantes
fr:research:bsp [2018/03/29 16:39]
apeiron
fr:research:bsp [2018/03/29 17:08]
apeiron [Résumé]
Ligne 25: Ligne 25:
  
 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.