Séminaire APRRSS

Programmation BSP à la ML : exemples, utilisation pour la vérification de codes et perspectives pour les architectures hiérarchiques


20/03/2015
Intervenant(s) : Frédéric Gava
Dans cet exposé, nous présenterons la programmation à la ML d'algorithmes BSP ainsi que les travaux qui ont été réalisés autours de la vérification de codes et le mode checking. Le modèle de parallélisme quasi-synchrone BSP est un modèle structuré de parallélisme qui permet la portabilité des programmes tout en offrant une prévision réaliste de leurs performances sur une grande variété d'architectures. Nous présenterons comment programmer ce modèle en ML, les sémantiques sous-jacentes, l'implémentation ainsi que la génération de programmes BSP certifiés grâce à l'assistant de preuve Coq. Nous décrirons aussi brièvement une extension BSP de l'outil de vérification déductive WHY et ses possibilités pour la vérification d'algorithmes de model-checking. Nous discuterons aussi de l'ajout de primitives de composition parallèle (qui permet aussi la programmation d'algorithmes «diviser-pour-régner» parallèles). Finalement, nous présenterons l'avenir de ce travail pour les architectures hiérarchiques à l'aide d'une extension de BSP appelée Multi-BSP et sa programmation en ML associée.
 Mentions légales
Carte du site |