Dérivation formelle et extraction d'un programme data-parallèle pour le problème des valeurs inférieures les plus proches

Résumé : Le problème des valeurs inférieures les plus proches est un problème important pour la programmation parallèle car il peut être utilisé pour résoudre plusieurs problèmes plus spécifiques et est l'une des phases d'algorithmes plus complexes. Avec l'assistant de preuve Coq, nous développons formellement par construction un programme parallèle fonctionnel pour résoudre ce problème, en utilisant la théorie des homomorphismes parallèles quasi synchrones. Les performances du programme parallèle fonctionnel obtenu par extraction sont comparées avec une version dérivée sans support logiciel et implantées avec la bibliothèque C++ de squelettes algorithmiques OSL, et avec une implantation d'un algorithme non vérifié du à He et Huang.
Type de document :
Communication dans un congrès
Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2014, Paris, France. 2014
Liste complète des métadonnées

https://hal.inria.fr/hal-00979092
Contributeur : Frédéric Loulergue <>
Soumis le : mardi 15 avril 2014 - 11:52:59
Dernière modification le : mercredi 12 décembre 2018 - 15:21:58

Identifiants

  • HAL Id : hal-00979092, version 1

Collections

Citation

Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, Zhenjiang Hu. Dérivation formelle et extraction d'un programme data-parallèle pour le problème des valeurs inférieures les plus proches. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2014, Paris, France. 2014. 〈hal-00979092〉

Partager

Métriques

Consultations de la notice

246