Dérivation formelle et extraction d'un programme data-parallèle pour le problème des valeurs inférieures les plus proches - Archive ouverte HAL Access content directly
Conference Papers Year : 2014

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

(1) , (1) , (2) , (3) , (4, 5)
1
2
3
4
5

Abstract

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.
Not file

Dates and versions

hal-00979092 , version 1 (15-04-2014)

Identifiers

  • HAL Id : hal-00979092 , version 1

Cite

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⟩
166 View
0 Download

Share

Gmail Facebook Twitter LinkedIn More