| 22 | | * 9h30-10h10: Kiminori Matsuzaki, ''Functional Models of Hadoop !MapReduce and Their Application to Scan'' |
| 23 | | * 10h10-10h50: Kento Emoto, Frédéric Loulergue, and Julien Tesson, ''A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction''[[BR]]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 talk 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. |
| 24 | | * 10h50-11h10: ''Coffee Break'' |
| 25 | | * 11h10-11h50: Kiminori Matsuzaki and Reina Miyazaki, ''Parallel Tree Accumulations on !MapReduce'' |
| 26 | | * 11h50-12h30: Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, and Zhenjiang Hu. ''Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem''[[BR]]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. |
| | 22 | * 9h30-10h10: Kiminori Matsuzaki, '''Functional Models of Hadoop !MapReduce and Their Application to Scan''' |
| | 23 | * 10h10-10h50: Kento Emoto, Frédéric Loulergue, and Julien Tesson, '''A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction'''[[BR]]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 talk 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. |
| | 24 | * 10h50-11h10: '''Coffee Break''' |
| | 25 | * 11h10-11h50: Kiminori Matsuzaki and Reina Miyazaki, '''Parallel Tree Accumulations on !MapReduce''' |
| | 26 | * 11h50-12h30: Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Legaux, and Zhenjiang Hu. '''Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem'''[[BR]]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. |
| 32 | | * 14h00-15h00: ''Invited talk'' |
| 33 | | * 15h00-15h40: Kento Emoto, Kiminori Matsuzaki, ''The !SkeTo Library'' |
| 34 | | * 15h40-16h20: Joeffrey Légaux, Noman Javed, Sylvain Jubertie, and Frédéric Loulergue, ''OSL: The Orléans Skeleton Library''[[BR]]Structured parallel models such as algorithmic skeletons offer a global view of the parallel program in contrast with the fragmented view of the SPMD style. This makes program easier to write and to read for users, and offer additional opportunities for optimisation done by the libraries, compilers and/or run-time systems. Algorithmic skeletons are or can be seen as patterns or higher-order functions implemented in parallel, often manipulating distributed data structures. Orléans Skeleton Library (OSL) is a library of parallel algorithmic skeletons, written in C++ on top of MPI, which uses meta-programming techniques for optimisation. This talk will present the recent work on OSL: skeletons used to manage arbitrary distributions of distributed arrays, support for BSP homomorphisms, an exception mechanism that ensures the global coherence of the system after exceptions are caught. |
| 35 | | * 16h20-16h40: ''Coffee Break'' |
| 36 | | * 16h40-17h20: Shigeyuki Sato, Kiminori Matsuzaki, ''A Generic Implementation of Tree Skeletons'' |
| 37 | | * 17h20-18h00: Wadoud Bousdira (Presenter), Frédéric Loulergue, Julien Tesson, Vitor Rodrigues, and Sylvain Dailler, ''A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays''[[BR]]To make parallel programming as widespread as parallel architectures, more structured parallel programming paradigms are necessary. One of the possible approaches are Algorithmic skeletons that are abstract parallel patterns. They can be seen as higher order functions implemented in parallel. Algorithmic skeletons offer a simple interface to the programmer without all the details of parallel implementations as they abstract the communications and the synchronisations of parallel activities. To write a parallel program, users have to combine and compose the skeletons. Orléans Skeleton Library (OSL) is an efficient meta-programmed C++ library of algorithmic skeletons that manipulate distributed arrays. A prototype implementation of OSL exists as a library written with the function parallel language Bulk Synchronous Parallel ML. In this paper we are interested in verifying the correctness of a subset of this prototype implementation. To do so, we give a functional specification (i.e. without the parallel details) of a subset of OSL and we prove the correctness of the BSML implementation with respect to this functional specification, using the Coq proof assistant. |
| | 32 | * 14h00-15h00: '''Invited talk''' |
| | 33 | * 15h00-15h40: Kento Emoto, Kiminori Matsuzaki, '''The !SkeTo Library''' |
| | 34 | * 15h40-16h20: Joeffrey Légaux, Noman Javed, Sylvain Jubertie, and Frédéric Loulergue, '''OSL: The Orléans Skeleton Library'''[[BR]]Structured parallel models such as algorithmic skeletons offer a global view of the parallel program in contrast with the fragmented view of the SPMD style. This makes program easier to write and to read for users, and offer additional opportunities for optimisation done by the libraries, compilers and/or run-time systems. Algorithmic skeletons are or can be seen as patterns or higher-order functions implemented in parallel, often manipulating distributed data structures. Orléans Skeleton Library (OSL) is a library of parallel algorithmic skeletons, written in C++ on top of MPI, which uses meta-programming techniques for optimisation. This talk will present the recent work on OSL: skeletons used to manage arbitrary distributions of distributed arrays, support for BSP homomorphisms, an exception mechanism that ensures the global coherence of the system after exceptions are caught. |
| | 35 | * 16h20-16h40: '''Coffee Break''' |
| | 36 | * 16h40-17h20: Shigeyuki Sato, Kiminori Matsuzaki, '''A Generic Implementation of Tree Skeletons''' |
| | 37 | * 17h20-18h00: Wadoud Bousdira (Presenter), Frédéric Loulergue, Julien Tesson, Vitor Rodrigues, and Sylvain Dailler, '''A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays'''[[BR]]To make parallel programming as widespread as parallel architectures, more structured parallel programming paradigms are necessary. One of the possible approaches are Algorithmic skeletons that are abstract parallel patterns. They can be seen as higher order functions implemented in parallel. Algorithmic skeletons offer a simple interface to the programmer without all the details of parallel implementations as they abstract the communications and the synchronisations of parallel activities. To write a parallel program, users have to combine and compose the skeletons. Orléans Skeleton Library (OSL) is an efficient meta-programmed C++ library of algorithmic skeletons that manipulate distributed arrays. A prototype implementation of OSL exists as a library written with the function parallel language Bulk Synchronous Parallel ML. In this paper we are interested in verifying the correctness of a subset of this prototype implementation. To do so, we give a functional specification (i.e. without the parallel details) of a subset of OSL and we prove the correctness of the BSML implementation with respect to this functional specification, using the Coq proof assistant. |
| 45 | | * 09h30-10h30: ''Invited Speaker'' |
| 46 | | * 10h30-10h50: ''Coffee Break'' |
| 47 | | * 10h50-11h30: Thomas Pinsard, Frédéric Dabrowski, Frédéric Loulergue, ''Nested Atomic Sections with Thread Escape: From a Formal Definition to Verified Compilation'' |
| 48 | | * 11h30-12h10: Sylvain Dailler, Frédéric Dabrowski, ''Modular Verified Compilation for Parallel Languages'' |
| | 45 | * 09h30-10h30: '''Invited Speaker''' |
| | 46 | * 10h30-10h50: '''Coffee Break''' |
| | 47 | * 10h50-11h30: Thomas Pinsard, Frédéric Dabrowski, Frédéric Loulergue, '''Nested Atomic Sections with Thread Escape: From a Formal Definition to Verified Compilation''' |
| | 48 | * 11h30-12h10: Sylvain Dailler, Frédéric Dabrowski, '''Modular Verified Compilation for Parallel Languages''' |
