Dérivation formelle et extraction d’un programme data parallele pour le probleme des valeurs inférieures les plus proches

Le probleme des valeurs inférieures les plus proches (All Nearest Smaller Values ou ANSV) est un probleme important pour la programmation parallele [1] car il peut être utilisé pour résoudre plusieurs problemes plus spécifiques et il est également l’une des phases d’algorithmes plus complexes. Le probleme est le suivant: soit xs=[x1; x2;...; xn] une liste d’éléments d’un domaine totalement ordonné, pour chaque xi, trouver la valeur la plus prochea gauche de xi et la valeur la plus prochea droite de xi qui sont inférieuresax i. S’il n’y a pas de telle valeur, indiquer⊥a la place.Partant d’une spécification naıve, sous forme d’un programme fonctionnel inefficace, nous dérivons pas-a-pas un programme fonctionnel séquentiel plus efficace. Cette derniere formulation utilise une fonction d’ordre supérieure appelée homomorphisme quasi synchrone, dont nous fournissons une implantation parallele vérifiée. La dérivation et la vérification de l’implantation parallele sont conduitesa l’aide de l’assistant de preuve Coq [4]. Nous utilisons finalement la fonctionnalité d’extraction de code de Coq pour obtenir un programme OCaml avec des appelsa la bibliotheque de programmation parallele Bulk Synchronous Parallel ML. Les performances du programme parallele fonctionnel obtenu par extraction sont comparées avec une version implantée avec la bibliotheque C++ de squelettes algorithmiques OSL [3], et avec une implantation d’un algorithme non vérifié dûa He et Huang [2].