Systematic Development of Functional Bulk Synchronous Parallel Programs

Abstract : With the current generalization of parallel architectures arises the concern of applying formal methods to parallelism, which allows specifications of parallel programs to be precisely stated and the correctness of an implementation to be verified. However, the complexity of parallel, compared to sequential, programs makes them more error-prone and difficult to verify. This calls for a strongly structured form of parallelism, which should not only ease programming by providing abstractions that conceal much of the complexity of parallel computation, but also provide a systematic way of developing practical programs from specification. Bulk Synchronous Parallelism (BSP) is a model of computation which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism. We propose a framework for refining a sequential specification toward a functional BSP program, the whole process being done with the help of a proof assistant. The main technical contributions of this paper are as follows: We define BH, a new homomorphic skeleton, which captures the essence of BSP computation in an algorithmic level, and also serves as a bridge in mapping from high level specification to low level BSP parallel programs ; We develop a set of useful theories in Coq for systematic and formal derivation of programs in BH from specification, and we provide a certified parallel implementation of BH in the parallel functional language Bulk Synchronous Parallel ML so that a certified BSP parallel program can be automatically extracted from the proof ; We demonstrate with an example that our new framework can be very useful in practice to develop certified BSP parallel programs.
Type de document :
Rapport
[Research Report] RR-2010-01, 2010, pp.21
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00465838
Contributeur : Frédéric Loulergue <>
Soumis le : mardi 23 mars 2010 - 08:11:45
Dernière modification le : jeudi 11 janvier 2018 - 06:19:28
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 12:20:12

Fichier

RR-2010-01.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00465838, version 2

Collections

Citation

Julien Tesson, Zhenjiang Hu, Kiminori Matsuzaki, Frédéric Loulergue, Louis Gesbert. Systematic Development of Functional Bulk Synchronous Parallel Programs. [Research Report] RR-2010-01, 2010, pp.21. 〈inria-00465838v2〉

Partager

Métriques

Consultations de la notice

212

Téléchargements de fichiers

118