= FraDeCoPP-3 -- Third Workshop on Frameworks for the Development of Correct (parallel) Programs = == Date and Location == Monday October 7, 2013, 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]) == Program == * 10h20-10h30 '''Accueil et introduction / Welcome and Introduction''' * 10h30-11h15 Julien Tesson (Université Paris Est Créteil) and Joeffrey Legaux (Université d'Orléans), '''[http://frederic.loulergue.eu/ftp/tesson_fradecopp-3.pdf Programming with BSP Homomorphisms]'''[[BR]]Algorithmic skeletons in conjunction with list homomorphisms play an important role in formal development of parallel algorithms. We have designed a notion of homomorphism dedicated to bulk synchronous parallelism. In this paper we derive two application using this theory: sparse matrix vector multiplication and the all nearest smaller values problem. We implement a support for BSP homomorphism in the Orléans Skeleton Library and experiment it with these two applications. * 11h15-12h00 Frédéric Loulergue (Université d'Orléans) , '''[http://frederic.loulergue.eu/ftp/loulergue_fradecopp-3.pdf Parallel Programming in Coq: the Bulk Synchronous Parallel ML Case]'''[[BR]]Bulk Synchronous Parallel ML (BSML) is a structured parallel functional programming language. It extends a functional programming language of the ML family with a polymorphic data structure and a very small set of primitives. In this paper we describe a framework for reasoning about BSML programs using the Coq interactive theorem prover and for extracting actual parallel programs from proofs. This framework is illustrated through applications. * 12h00-14h00 '''Déjeuner / Lunch (Restaurant l'Agora)''' * 14h00-15h00 Thomas Horstmeyer and Rita Loogen (Philipps-Universität Marburg), '''[http://frederic.loulergue.eu/ftp/horstmeyer_fradecopp-3.pdf Parallel Functional Programming in Eden]'''[[BR]]Eden extends Haskell with constructs for the definition and instantiation of parallel processes. Processes evaluate function applications remotely in parallel. The programmer has control over process granularity, data distribution, communication topology, and evaluation site, but need not manage synchronisation and data exchange between processes. The latter are performed by the parallel runtime system through implicit communication channels, transparent to the programmer. Common and sophisticated parallel communication patterns and topologies, so-called algorithmic skeletons, are provided as higher-order functions in a user-extensible skeleton library written in Eden. Eden is geared toward distributed settings, i.e.\ processes do not share any data, but can equally well be used on multicore systems. In the talk, we give an introduction into Eden's language constructs and its skeleton-based programming methodology. * 15h00-16h00 Yolanda Ortega-Mallén (Universidad Complutense de Madrid), '''[http://frederic.loulergue.eu/ftp/ortega-mallen_fradecopp-3.pdf Formal Semantics for the Parallel Language Eden]'''[[BR]]We present two formal semantics for the kernel of the parallel language Eden. First we describe an operational semantics expressed as a two-level transition system. Next we present a denotational semantics based on continuations, suitable for dealing with side-effects and parallelism. We end by comparing both approaches. * 16h00-16h30 '''Pause / Coffee Break''' * 16h30-17h30 Jean Fortin (Université Paris Est Créteil), '''[http://frederic.loulergue.eu/ftp/fortin_fradecopp-3.pdf BSP-Why: a Tool for Deductive Verification of BSP Programs]'''[[BR]]This presentation is based on the author's Doctoral thesis and falls within the formal verification of parallel programs. The aim of formal verification is to ensure that a program will run as it should, without making mistakes, blocking, or terminating abnormally. This is even more important in the parallel computation field, where the cost of calculations can be very high. The BSP model (Bulk Synchronous Parallelism) is a model of parallelism well suited for the use of formal methods. It guarantees a structure in the parallel program, by organising it into super-steps, each of them consisting in a phase of computations, followed by communications between the processes. In this thesis, we chose to extend an existing tool to adapt it for the proof of BSP programs. We based our work on WHY, a VCG (verification condition generator) that has the advantage of being able to interface with several automatic provers and proof assistants to discharge the proof obligations. There are multiple contributions in this thesis. In a first part, we present a comparison of the existing BSP libraries, in order to show the most used BSP primitives, which are the most interesting to formalise. We then present BSP-WHY, our tool for the proof of BSP programs. This tool generates a sequential program to simulate the parallel program in input, thus allowing the use of why and the numerous associated provers to solve the proof obligations. We then show how BSP-WHY can be used to prove the correctness of some basic BSP algorithms. We also present a more complex example, the generation of the state-space (model-checking) of systems, especially for security protocols. Finally, in order to ensure the greatest confidence in the BSP-WHY tool, we give a formalisation of the language semantics, in the coq proof assistant. We also prove the correctness of the transformation used to go from a parallel program to a sequential program. * 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 == Organiser == * Frédéric Loulergue, Université d'Orléans == Past Worshops == * [wiki:FraDeCoPP-2] * [wiki:FraDeCoPP2012]