A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

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

Kento Emoto
  • Fonction : Auteur
  • PersonId : 954252
Frédéric Loulergue
Connectez-vous pour contacter l'auteur

Résumé

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.
Fichier non déposé

Dates et versions

hal-00964061 , version 1 (24-03-2014)

Identifiants

  • HAL Id : hal-00964061 , version 1

Citer

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. ⟨hal-00964061⟩
194 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More