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

Kento Emoto Frédéric Loulergue 1, * Julien Tesson 2
* Corresponding author
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.
Liste complète des métadonnées

https://hal.inria.fr/hal-00964061
Contributor : Frédéric Loulergue <>
Submitted on : Monday, March 24, 2014 - 3:59:28 AM
Last modification on : Thursday, January 17, 2019 - 3:06:06 PM

Identifiers

  • 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〉

Share

Metrics

Record views

312