51 | | * 16h50-17h30: Wadoud Bousdira, 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. |
52 | | |
53 | | * 17h30-18h10: Shigeyuki Sato, Kiminori Matsuzaki, '''A Generic Implementation of Tree Skeletons'''[[BR]]In data-parallel skeleton libraries, the implementation of skeletons is usually tightly-coupled with that of data structures. However, a loose coupling between both like C++ STL will improve modularity and flexibility of skeletons and data structures. This flexibility is particularly valuable for tree skeletons. To achieve such a loose coupling, we present an iterator-based interface of trees for tree skeletons. We have implemented tree skeletons on the basis of our interface; we present their design and implementation. This paper also reports the results of preliminary experiments. |
| 51 | * 16h50-17h30: Shigeyuki Sato, Kiminori Matsuzaki, '''A Generic Implementation of Tree Skeletons'''[[BR]]In data-parallel skeleton libraries, the implementation of skeletons is usually tightly-coupled with that of data structures. However, a loose coupling between both like C++ STL will improve modularity and flexibility of skeletons and data structures. This flexibility is particularly valuable for tree skeletons. To achieve such a loose coupling, we present an iterator-based interface of trees for tree skeletons. We have implemented tree skeletons on the basis of our interface; we present their design and implementation. This paper also reports the results of preliminary experiments. |