Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem

Abstract : The All Nearest Smaller Values (ANSV) problem is an important problem for parallel programming as it can be used to solve several problems and is one of the phases of several other parallel algorithms. We formally develop by construction a functional parallel program for solving the ANSV problem using the theory of Bulk Synchronous Parallel (BSP) homomorphisms within the Coq proof assistant. The performances of the Bulk Synchronous Parallel ML program obtained from Coq is compared to a version derived without software support (pen-and-paper) and implemented using the Orléans Skeleton Library of algorithmic skeletons, and to a (unproved correct) direct implementation of the BSP algorithm of He and Huang.
Type de document :
Communication dans un congrès
ACM. ACM Symposium on Applied Computing (SAC), 2014, Gyeongju, South Korea. 2014
Liste complète des métadonnées

https://hal.inria.fr/hal-00905950
Contributeur : Frédéric Loulergue <>
Soumis le : mardi 19 novembre 2013 - 08:46:11
Dernière modification le : jeudi 11 janvier 2018 - 06:19:28

Identifiants

  • HAL Id : hal-00905950, version 1

Collections

Citation

Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, Zhenjiang Hu. Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem. ACM. ACM Symposium on Applied Computing (SAC), 2014, Gyeongju, South Korea. 2014. 〈hal-00905950〉

Partager

Métriques

Consultations de la notice

285