Revue / Journal
- [j1]
-
Frédéric Loulergue, Wadoud Bousdira, Julien Tesson
Calculating Parallel Programs in Coq using List Homomorphisms.
International Journal of Parallel Programming.
Springer Verlag (Germany)
2015.
SyDPaCC is a set of libraries for the Coq
proof assistant. It allows to write naive functional programs
(i.e. with high complexity) that are considered as specifications,
and to transform them into more efficient versions. These more
efficient versions can then be automatically parallelised before
being extracted from Coq into source code for the functional
language OCaml together with calls to the Bulk Synchronous
Parallel ML (BSML) library. In this paper we present a new core
version of SyDPaCC for the development of parallel programs
correct-by-contruction using the theory of list homomorphisms and
algorithmic skeletons implemented and verified in Coq. The
framework is illustrated on the the maximum prefix sum problem.
[ HAL |
DOI ]
- [j2]
-
Victor Allombert, Frédéric Gava, Julien Tesson
Multi-ML: Programming Multi-BSP Algorithms in ML. International Journal of Parallel Programming.
International Journal of Parallel Programming.
Springer Verlag (Germany)
2015.
The multi-bsp model is an extension of the
well known bsp bridging model. It brings a tree based view of
nested components to represent hierarchical architectures. In the
past, we designed bsml for programming bsp algorithms in ml. We
now propose the multi-ml language as an extension of bsml for
programming multi-bsp algorithms in ml.
[ HAL ]
Colloque International / International Conference
- [ic9]
-
Kento Emoto, Frédéric Loulergue, Julien Tesson
A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction.
Interactive Theorem Proving.
LNAI volume 8558, pages 258-274.
Springer,
Vienna, Autriche. 2014.
The integration of the generate-and-test paradigm and semi-rings for the aggregation of results provides a parallel programming framework for large scale data-intensive applications. The so-called GTA framework allows a user to define an inefficient specification of his/her problem as a composition of a generator of all the candidate solutions, a tester of valid solutions, and an aggregator to combine the solutions. Through two calculation theorems a GTA specification is transformed into a divide-and-conquer efficient program that can be implemented in parallel. In this paper we present a verified implementation of this framework in the Coq proof assistant: efficient bulk synchronous parallel functional programs can be extracted from naive GTA specifications. We show how to apply this framework on an example, including performance experiments on parallel machines.
[ DOI ]
- [ic8]
-
Frédéric Loulergue, Simon Robillard,
Julien Tesson, Joeffrey Legaux, Zhenjiang Hu
Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem.
ACM Symposium on Applied Computing (SAC),pages 1577-1584.
Gyeongju, Republic of Korea. 2014.
The All Nearest Smaller Values (ANSV) problem is an important problem for parallel programming as it can be used to solve several problems and is one of the phases of several other parallel algorithms. We formally develop by construction a functional parallel program for solving the ANSV problem using the theory of Bulk Synchronous Parallel (BSP) homomorphisms within the Coq proof assistant. The performances of the Bulk Synchronous Parallel ML program obtained from Coq is compared to a version derived without software support (pen-and-paper) and implemented using the Orléans Skeleton Library of algorithmic skeletons, and to a (unproved correct) direct implementation of the BSP algorithm of He and Huang.
[ DOI ]
- [ic7]
-
Frédéric Loulergue, Virginia Niculescu, Julien Tesson.
Implementing powerlists with Bulk Synchronous Parallel ML.
2014 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)
Timisoara, Romania, 2014.
The latest developments of the computation systems impose using tools and methodologies able to simplify the development process of parallel software, but also to assure a high level of performance and robustness. Powerlists and their variants are data structures that can be successfully used in a simple, provably correct, functional description of parallel programs, which are divide and conquer in nature. They represent one of the high-level algebraic theories which are appropriate to be used as fundamentals for a model of parallel computation that assures correctness proving. The paper presents how programs defined based on powerlists could be transformed to real code in the functional language OCaml plus calls to the parallel functional programming library Bulk Synchronous Parallel ML. BSML functions follow the BSP model requirements, and so its advantages are introduced in OCaml parallel code. The transformations are based on a framework that assures: simple, correct, efficient implementation. Examples are given and concrete experiments for their executions are conducted. The results emphasise the utility and the efficiency of the framework.
[ PDF | DOI ]
- [ic6]
-
Joeffrey Legaux, Zhenjiang Hu, Frédéric
Loulergue, Kiminori Matsuzaki, Julien Tesson.
Programming with BSP Homomorphisms.
Euro-Par 2013 Parallel Processing
LNCS Volume 8097, pp 446-457.
Springer,
2013.
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.
[ DOI ]
- [ic5]
-
Wadoud Bousdira, Frédéric Loulergue, Julien Tesson.
A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays.
ICA3PP 2012,
LNCS Volume 7439, pp 218-232.
Springer,
2012.
[ DOI ]
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.
- [ic4]
-
Julien Tesson, Frédéric Loulergue.
A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation.
11th International Conference on Computational Science (ICCS 2011),
Procedia Computer Science 4,
Elsevier.
2011.
[ DOI ]
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 a simulation application based on heat equation.
- [ic3]
-
Noman Javed, Frédéric Loulergue, Julien Tesson, Wadoud Bousdira
Prototyping a Library of Algorithmic Skeletons with Bulk Synchronous Parallel ML.
(PDPTA'11), International Conference on Parallel and Distributed Processing Techniques and Applications,
CSREA Press.
2011.
- [ic2]
-
Louis Gesbert, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, Julien Tesson.
Systematic Development of Correct Bulk Synchronous Parallel Programs.
The 11th International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT2010),
2010.
[ Draft |
DOI |
slides ]
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.
- [ic1]
-
Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi.
Program Calculation in Coq.
Algebraic Methodology and Software Technology - 13th International
Conference, AMAST 2010, Lac-Beauport, QC, Canada.
LNCS 6486,
Springer.
2011.
[ Draft |
DOI ]
Program calculation, being a programming
technique that derives programs from specification by means of
formula manipulation, is a challenging activity. It requires human
insights and creativity, and needs systems to help human to focus on
clever parts of the derivation by automating tedious ones and
verifying correctness of transformations. Different from many
existing systems, we show in this paper that Coq, a popular theorem
prover, provides a cheap way to implement a powerful system to
support program calculation, which has not been recognized so
far. We design and implement a set of tactics for the Coq proof
assistant to help the user to derive programs by program calculation
and to write proofs in calculational form. The use of these tactics
is demonstrated through program calculations in Coq based on the
theory of lists.
Tutoriels / Tutorials
- [t1]
-
Frédéric Loulergue, Julien Tesson
Certified Parallel Program Calculation in Coq:
A Tutorial
International Conference on High
Performance Computing and Simulation (HPCS), Bologna,
Italy.
2014
Colloque national / National Conferences
- [nc2]
-
Frédéric Loulergue, Simon Robillard,
Julien Tesson, Joeffrey Legaux, Zhenjiang Hu.
Dérivation formelle et extraction d'un programme data-parallèle pour le problème des valeurs inférieures les plus proches.
Approches Formelles dans l'Assistance au D{\'e}veloppement de Logiciels (AFADL),
Paris, France, 2014
Le problème des valeurs inférieures les plus proches est un problème important pour la programmation parallèle car il peut être utilisé pour résoudre plusieurs problèmes plus spécifiques et est l'une des phases d'algorithmes plus complexes. Avec l'assistant de preuve Coq, nous développons formellement par construction un programme parallèle fonctionnel pour résoudre ce problème, en utilisant la théorie des homomorphismes parallèles quasi synchrones. Les performances du programme parallèle fonctionnel obtenu par extraction sont comparées avec une version dérivée sans support logiciel et implantées avec la bibliothèque C++ de squelettes algorithmiques OSL, et avec une implantation d'un algorithme non vérifié du à He et Huang.
- [nc1]
-
Hideki Hashimoto, Zhenjiang Hu, Julien Tesson, Frédéric Loulergue, Masato Takeichi.
A Coq Library for Program Calculation.
JSSST Conference on Software Science and Technology,
Shimane University, Shimane : Japon, 2009
Program calculation, being a programming
technique that derives programs from specification by means of
formula manipulation, is a challenging activity. It requires human
insights and creativity, and needs systems to help human to focus
on clever parts of the derivation by automating tedious ones and
verifying correctness of transformations. Different from many
existing systems, we show in this paper that Coq, a popular
theorem prover, provides a cheap way to implement a powerful
system to support program calculation, which has not been
recognized so far. We design and implement a set of tactics for
the Coq proof assistant to help the user to derive programs by
program calculation and to write proofs in calculational form. The
use of these tactics is demonstrated through program calculations
in Coq based on the theory of lists.
Atelier international / International Workshop
- [w1]
-
J. Tesson and F. Loulergue.
Formal Semantics of DRMA-Style Programming in
BSPlib.
Seventh International Conference
on Parallel Processing and Applied Mathematics (PPAM 2007), Workshop
on Language-Based Parallel Programming Models,
J. Weglarz, R. Wyrzykowski, and B. Szymanski.
LNCS 4967,
Springer.
2008.
[ pdf ]
BSPlib is a programming library for C and
Fortran which supports bulk synchronous parallelism (BSP). This
paper is about a formal semantics for the DRMA programming style
of the BSPlib library. The aim is to study the behavior of BSPlib
programs and to propose some syntactic characterizations used to
provide guarantees on semantic properties. This work is the basis
for future tools dedicated to the validation of BSPlib programs.
Mémoire / Thesis
- [t1]
-
Julien Tesson.
Environnement pour le développement et la preuve de
correction systématiques de programmes parallèles fonctionnels.
PhD thesis, LIFO, University of Orléans, November 2011.
[ pdf | slides ]
Concevoir et implanter des programmes parallèles est une tâche complexe, sujette aux erreurs. La vérification des programmes parallèles est également plus difficile que celle des programmes séquentiels. Pour permettre le développement et la preuve de correction de programmes parallèles, nous proposons de combiner le langage parallèle fonctionnel quasi-synchrone BSML, les squelettes algorithmiques - qui sont des fonctions d'ordre supérieur sur des structures de données réparties offrant une abstraction du parallélisme - et l'assistant de preuve Coq, dont le langage de spécification est suffisamment riche pour écrire des programmes fonctionnels purs et leurs propriétés. Nous proposons un plongement des primitives BSML dans la logique de Coq sous une forme modulaire adaptée à l'extraction de programmes. Ainsi, nous pouvons écrire dans Coq des programmes BSML, raisonner dessus, puis les extraire et les exécuter en parallèle. Pour faciliter le raisonnement sur ceux-ci, nous formalisons le lien entre programmes parallèles, manipulant des structures de données distribuées, et les spécifications, manipulant des structures séquentielles. Nous prouvons ainsi la correction d'une implantation du squelette algorithmique BH, un squelette adapté au traitement de listes réparties dans le modèle de parallélisme quasi synchrone. Pour un ensemble d'applications partant d'une spécification d'un problème sous forme d'un programme séquentiel simple, nous dérivons une instance de nos squelettes, puis nous extrayons un programme BSML avant de l'exécuter sur des machines parallèles.
Exposé / Talk
- [e5]
-
Environnement pour le développement et la
preuve de correction de programmes parallèles fonctionnels.
Workgroup LaMHA - GDR GPL,Orsay.
November, 2011
- [e4]
-
Environnement pour le développement et la
preuve de correction de programmes parallèles fonctionnels.
Workgroup LTP - GDR GPL, Rennes.
October 27, 2011
- [e3]
-
Systematic Development of Correct Bulk
Synchronous Parallel Programs.
PAPDAS Meeting, LIFO,Orléans.
March 23, 2011
- [e2]
-
Environnement pour le développement et la preuve de correction systématiques de programmes parallèles fonctionnels.
Workgroup LTP - GDR GPL, Paris.
October, 2009
- [e1]
-
Operational semantics of an imperative BSP mini-language in Coq.
Theorem Proving and Provers meeting, Tohoku University, Sendaï.
November, 2008
Version Française