Changes between Version 5 and Version 6 of FraDeCoPP-2


Ignore:
Timestamp:
Nov 20, 2012, 9:05:55 AM (6 years ago)
Author:
frederic.loulergue@…
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • FraDeCoPP-2

    v5 v6  
    1313* 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. 
    1414 
    15 * 11h15-12h00 Julien Tesson (LIFO, Université d'Orléans), '''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.  
     15* 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.  
    1616 
    1717* 12h00-14h00 '''Déjeuner / Lunch (Restaurant l'Agora)'''