= FraDeCoPP-2 -- Second Workshop on Frameworks for the Development of Correct (parallel) Programs =
== Date and Location ==
Monday, November 26, 2012, room "Salle de réunion 1" (2nd floor/1er étage)
LIFO, Orléans ([http://www.univ-orleans.fr/lifo/acces.php?lang=fr&sub=sub4 comment venir])
== Tentative Program ==
* 10h15-10h30 '''Accueil et introduction / Welcome and Introduction'''
* 10h30-11h15 Wadoud Bousdira (LIFO, Université d'Orléans), '''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. To illustrate how the user could use these skeletons, we prove the correctness of two applications implemented with them: a heat diffusion simulation and the maximum segment sum problem.
* 11h15-12h00 Julien Tesson (LACL, Université Paris-Est), '''Systematic Development of Functional Bulk Synchronous Parallel Programs'''[[BR]]With the current generalisation of parallel architectures arises the concern of applying formal methods to parallelism. The complexity of parallel, compared to sequential, programs makes them more error-prone and difficult to verify. Bulk Synchronous Parallelism (BSP) is a model of computation which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism. We propose a framework for refining a sequential specification toward a functional BSP program, the whole process being done with the help of the Coq proof assistant. To do so we define BH, a new homomorphic skeleton, which captures the essence of BSP computation in an algorithmic level, and also serves as a bridge in mapping from high level specification to low level BSP parallel programs.
* 12h00-14h00 '''Déjeuner / Lunch (Restaurant l'Agora)'''
* 14h00-15h15 Virginia Niculescu (Babes-Bolya University of Cluj-Napoca), '''On Granularity in Data-Parallel Programs Development'''[[BR]]One key to attaining good parallel performance is choosing the right granularity for the application. Parallel computation models with high level of abstraction, usually, do not have mechanisms for specifying and building granularity. If such mechanisms are introduced they could be very useful since they allow a better evaluation of the performance, and finally, an easier implementation. It is considered that a model of parallel computation, to be useful, must fulfill a set of requirements: abstractness, software development methodology, architecture independence, cost measures, no preferred scale of granularity, and efficiently implementable. The development of the programs correct by construction is also a very important issue in parallel setting. The normal flow in a derivation is to start from a specification, derive and express it using the chosen model, and then adjust it for implementation. The question that could arise is “When should we care about the granularity?” - only at the mapping phase, or starting from the beginning, in the derivation phase. Some case studies will be presented, and their analysis indicate that if we are able to specify and to build granularity from the first levels of design, then the chances to obtain good improvements of the resulted costs increase very much.
* 15h15-15h45 '''Pause / Coffee Break'''
* 15h45-16h30 Frédéric Loulergue (LIFO, Université d'Orléans), '''Towards a Verified GTA Library'''[[BR]]Joint work in progress with Kento Emoto, Julien Tesson, Frédéric Dabrowski.
* 16h30-16h45 '''Pause / Coffee Break'''
* 16h45-17h30 Frédéric Gava (LACL, Université Paris-Est), '''BSP, bon à toutes les sauces; Application to Functional Programming, Mechanised Verification and Security Protocols'''
* 17h30-18h00 '''Conclusion'''
== Aim and Scope ==
The trend is towards the increase of cores in processors, the number of processors and the need for scalable computing everywhere. But parallel program design and implementation is a complex, error prone task. Thus there is a need for methods to verify parallel programs or insure their correctness by constructive methods.
In the [http://traclifo.univ-orleans.fr/PaPDAS PaPDAS] project we are interested in providing a framework to ease the development of correct parallel programs in a systematic way using constructive algorithmic. That is, in our case, to construct efficient and correct parallel programs by transformation of simple programs towards a combination of algorithmic skeletons. Insuring the correctness of the final implementation '''and''' keeping this implementation efficient means that we need verified efficient implementation of a set of skeletons.
Formal methods like refinement methods, Hoare logics, embedding of languages in a proof assistant, model checking, static analysis, have proved their usefulness to verify different kind of properties of programs. Constructive methods allow to construct efficient correct programs by transformation of simpler programs, insuring the preservation of some properties (usually functional correctness) along the process.
The use of proof assistant or automated tools in the process increases the confidence we can have in derived programs.
The FraDeCoP workshop aims to provide an informal and friendly setting to discuss recent or ongoing works on framework for the development of formally verified programs using programs transformation, programs refinement, or ''a posteriori'' proof of correctness, or experience feedback in the use of such a framework.
While we are interested in seeing such works applied to parallel programs, works on sequential programs will be considered with a great interest.
Topics of interest include but are not limited to:
* Formal framework for:
* programs transformation
* programs refinement
* "Hoare logic" style proofs of programs
* programs analysis
* Experience feedback on the development of "formally proved correct" programs
== Organizers ==
* Frédéric Loulergue, Université d'Orléans
* Julien Tesson, Université Paris-Est
== Past Worshop ==
* [wiki:FraDeCoPP2012]