A VERIFIED LIBRARY OF ALGORITHMIC SKELETONS (V1.0)

To make parallel programming as widespread as parallel architectures, more structured parallel programming paradigms are necessary. One of the possible ap-proaches are algorithmic skeletons. They can be seen as higher order functions implemented in parallel. Algorithmic skeletons offer a simple interface to the pro-grammer 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 imple-mentation of OSL exists as a library written with the function parallel language Bulk Synchronous Parallel ML (BSML). 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 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. To illustrate how the user could use these skeletons, we prove the correctness of two applications implemented with them.