A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction

Kento Emoto Frédéric Loulergue 1, * Julien Tesson 2
* Auteur correspondant
1 PaMDA
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
Abstract : The integration of the generate-and-test paradigm and semi-rings for the aggregation of results provides a parallel programming framework for large scale data-intensive applications. The so-called GTA framework allows a user to define an inefficient specification of his/her problem as a composition of a generator of all the candidate solutions, a tester of valid solutions, and an aggregator to combine the solutions. Through two calculation theorems a GTA specification is transformed into a divide-and-conquer efficient program that can be implemented in parallel. In this paper we present a verified implementation of this framework in the Coq proof assistant: efficient bulk synchronous parallel functional programs can be extracted from naive GTA specifications. We show how to apply this framework on an example, including performance experiments on parallel machines.
Type de document :
Communication dans un congrès
Interactive Theorem Proving, 2014, Vienna, Austria. Springer, 2014
Liste complète des métadonnées

https://hal.inria.fr/hal-00964061
Contributeur : Frédéric Loulergue <>
Soumis le : lundi 24 mars 2014 - 03:59:28
Dernière modification le : jeudi 11 janvier 2018 - 06:19:28

Identifiants

  • HAL Id : hal-00964061, version 1

Collections

Citation

Kento Emoto, Frédéric Loulergue, Julien Tesson. A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. Interactive Theorem Proving, 2014, Vienna, Austria. Springer, 2014. 〈hal-00964061〉

Partager

Métriques

Consultations de la notice

298