Julien TESSON - Publications

Version Française

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. SYNASC Timisoara, Romania, 2014. to Appear. 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.
[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.

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.pdfslides ] 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