English version

PPS UMR 7126 – Laboratoire
Preuves, Programmes et Systèmes

Accueil · Présentation · Membres · Publications · Séminaire · Groupes de travail · Projets · πr²

Frédéric Loulergue (Université d'Orléans, pi.r2)

Systematic development of programs for parallel and cloud computing

23 avril 2015

The goal of the SyDPaCC framework is to ease the systematic development of correct parallel programs, in particular large scale data-intensive applications. Currently it is provided as a set of Coq libraries and an OCaml library for parallel programming. The users write inefficient (sequential) functional programs and through (partly automated) program transformations based on the theory of list homomorphisms, bulk synchronous parallel homomorphisms or semi-ring homomorphisms, an efficient sequential version is obtained. This version can then be automatically parallelised thanks to type class instance resolution and instances relating specific sequential functions to their parallel counterparts. These parallel functions, also called algorithmic skeletons, are written with a Coq axiomatisation of Bulk Synchronous Parallel ML (BSML) primitives. To obtain the final code, these Coq programs are extracted as OCaml functors and are applied to modules that implement the BSML library in parallel.

I will first present the SyDPaCC framework from a user point of view, then I will present some aspects of its internals, in particular automatic transformation and parallelisation using instance resolution. Finally, I will discuss ongoing work around SyDPaCC.