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.
Liste complète des métadonnées

https://hal.inria.fr/hal-00979092
Contributor : Frédéric Loulergue <>
Submitted on : Tuesday, April 15, 2014 - 11:52:59 AM
Last modification on : Thursday, January 17, 2019 - 3:10:02 PM

Identifiers

  • HAL Id : hal-00979092, version 1

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. ⟨hal-00979092⟩

Share

Metrics

Record views

256