ARTICLES / PAPERS

Revue / Journal

[1]
Louis Gesbert, Frédéric Gava, Frédéric Loulergue, and Frédéric Dabrowski. Bulk Synchronous Parallel ML with Exceptions. Future Generation Computer Systems, 26:486-490, 2010. [ DOI ]
Bulk Synchronous Parallel ML is a high-level language for programming parallel algorithms. Built upon OCaml and using the BSP model, it provides a safe setting for their implementation, avoiding concurrency related problems (deadlocks, indeterminism). Only a limited set of the features of OCaml can be used in BSML to respect its properties of safety: this paper describes a way to add exception handling to this set by extending and adapting OCaml's exceptions. The behaviour of these new exceptions and the syntactic constructs to handle them, together with their implementation, are described in detail, and results over an example are given.

[2]
Frédéric Gava and Frédéric Loulergue. A Static Analysis for Bulk Synchronous Parallel ML to Avoid Parallel Nesting. Future Generation Computer Systems, 21(5):665-671, 2005. [ DOI ]
The BSMLlib library is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a data structure named parallel vector, which is given by intention. In order to have an execution that follows the BSP model, and to have a simple cost model, nesting of parallel vectors is not allowed. The novelty of this paper is a type system which prevents such nesting. This system is correct w.r.t. the dynamic semantics.

[3]
Frédéric Gava and Frédéric Loulergue. A Functional Language for Departmental Metacomputing. Parallel Processing Letters, 15(3):289-304, 2005. [ DOI ]
We have designed a functional data-parallel language called BSML for programming bulk-synchronous parallel algorithms, a model of computing. Dead-locks and indeterminism are avoided and the execution time can be then estimated. For large scale applications where parallel processing is helpful, more than one parallel machine is needed. One speaks about metacomputing. A major problem in programming parallel application for such platforms is their hierarchical network structures: latency and bandwidth of global ones are orders of magnitude worse than those of local networks. Here we consider how an extention of the well-suited BSP model might be for these kinds of computing and how extended our functional language can be for this.

[4]
Frédéric Loulergue, Frédéric Gava, Myrto Arapinis, and Frédéric Dabrowski. Semantics and Implementation of Minimally Synchronous Parallel ML. International Journal of Computer and Information Science, 5(3):182-199, 2004.
This paper presents a new functional parallel language: Minimally Synchronous Parallel ML (MSPML). The execution time can be estimated, dead-locks and indeterminism are avoided. Programs are written as usual ML programs but using a small set of additional functions. Provided functions are used to access the parameters of the parallel machine and to create and operate on a parallel data structure. It follows the execution and cost model of the Message Passing Machine model (MPM). It shares with Bulk Synchronous Parallel ML its syntax and high-level semantics but it has a minimally synchronous distributed semantics. Experiments have been run on a cluster of PC using an implementation of the Diffusion algorithmic skeleton.

[5]
Gaétan Hains, Frédéric Loulergue, and John Mullins. Concrete data structures and functional parallel programming. Theoretical Computer Science, 258(1-2):233-267, 2001. [ DOI ]
A framework is presented for designing parallel programming languages whose semantics is functional and where communications are explicit. To this end, Brookes and Geva's generalized concrete data structures are specialized with a notion of explicit data layout to yield a CCC of distributed structures called arrays. Arrays' symmetric replicated structures, suggested by the data-parallel SPMD paradigm, are found to be incompatible with sum types. We then outline a functional language with explicitly-distributed (monomorphic) concrete types, including higher-order, sum and recursive ones. In this language, programs can be as large as the network and can observe communication events in other programs. Such flexibility is missing from current data-parallel languages and amounts to a fusion with their so-called annotations, directives or meta-languages.

[6]
Frédéric Loulergue. Distributed Evaluation of Functional BSP Programs. Parallel Processing Letters, (4):423-437, 2001. [ DOI ]
The BSlambda_p-calculus is a calculus of functional bulk synchronous parallel (BSP) programs. It is the basis for the design of a bulk synchronous parallel ML language. For data-parallel languages, there are two points of view: the programming model where a program is seen as a sequence of operations on parallel vectors, and the execution model where the program is a parallel composition of programs run on each processor of the parallel machine. BSP algorithms are defined by data-parallel algorithms with explicit (physical) processes in order to allow their parallel execution time to be estimated. We present here a distributed evaluation minimally synchronous for BSP execution (which corresponds to the execution model). This distributed evaluation is correct w.r.t. the call-by-value strategy of the BSlmabda_p-calculus (which corresponds to the programming model).

[7]
Frédéric Loulergue, Gaétan Hains, and Christian Foisy. A Calculus of Functional BSP Programs. Science of Computer Programming, 37(1-3):253-277, 2000. [ DOI ]
An extension of the lambda-calculus called BSlambda is introduced as a formal basis for functional languages expressing bulk synchronous parallel algorithms. A confluence result is shown. The application of the calculus is illustrated by examples of program proofs and the associated notion of parallel reduction. The reduction process is interpreted in the BSP cost model.

Chapitre de livre / Book Chapter

[1]
Gaétan Hains and Frédéric Loulergue. Functional Bulk Synchronous Parallel Programming using the BSMLlib Library. In S. Gorlatch and C. Lengauer, editors, Constructive Methods for Parallel Programming, Advances in Computation: Theory and Practice, pages 165-178. Nova Science Publishers, august 2002.
BSMLlib is a functional data-parallel library for programming bulk-synchronous parallel (BSP) algorithms in Objective CAML. This article demonstrates the expressivity of BSMLlib operations on elementary algorithms. Other operations, on a type of parallel sets, illustrate how BSP exchange phases are written as small, simple programs. A longer example, inspired by parallel join algorithms for relational databases, demonstrates the advantage of using BSMLlib's explicit processes for dynamic load balancing. Finally, suggestions are made for extending the library and building a complete BSML language with the same operations.

Numéro spécial de revue / Special Issue

[1]
Frédéric Loulergue and A. Tiskin. Preface: Special Issue on High-Level Parallel Programming and Applications. Parallel Processing Letters, 18(1), 2008.
[2]
Anne Benoit and Frédéric Loulergue. Special Issue on Practical Aspects of High-Level Parallel Programming. Scalable Computing: Practice and Experience, 8, 2007. Selected extended and revised papers from the Third International Workshop on Practical Aspects of High-Level Parallel Programming (PAPP 2006).
[3]
Frédéric Loulergue. Introduction to the special issue on semantics and costs models for high-level parallel programming. Computer Languages, Systems and Structures, 33(3-4):79-81, 2007.
[4]
Frédéric Loulergue. Special Issue on Practical Aspects of High-Level Parallel Programming. Scalable Computing: Practice and Experience, 7(3), September 2006. Selected extended and revised papers from the Second International Workshop on Practical Aspects of High-Level Parallel Programming (PAPP 2005). [ The paper ]
[5]
Frédéric Loulergue. Special Issue on Practical Aspects of High-Level Parallel Programming. Scalable Computing: Practice and Experience, 6(4), December 2005. Selected extended and revised papers from the First International Workshop on Practical Aspects of High-Level Parallel Programming (PAPP 2004). [ The paper ]
[6]
Gaétan Hains and Frédéric Loulergue. Preface: Special Issue on High-Level Parallel Programming and Applications. Parallel Processing Letters, 13(3), 2003.

Colloque international avec publication des actes / International Conference with Published Proceedings

[1]
Noman Javed and Frédéric Loulergue. Verification of a Heat Diffusion Simulation written with Orléans Skeleton Library. In 9th International Conference on Parallel Processing and Applied Mathematics (PPAM 2011), volume 7204 of LNCS, pages 91-100. Springer, 2012. [ DOI ]
Orléans Skeleton Library (OSL) provides a set of algorithmic skeletons as a C++ library on top of MPI. The parallel programming approach of OSL is a structure one, which eases the reasoning about the performance and correctness of the programs. In this paper we present the verification of a heat diffusion simulation program, written in OSL, using the Coq proof assistant. The specification used in proving the correctness is a discretisation of the heat equation.

[2]
Frédéric Loulergue, Frédéric Gava, Nikolai Kosmatov, and Matthieu Lemerre. Towards Verified Cloud Computing Environments. In International Conference on High Performance Computing and Simulation (HPCS). IEEE, 2012. to appear.
As the usage of cloud becomes pervasive in our lives, it is needed to ensure the reliability, safety and security of cloud environments. In this paper we study a usual software stack of a cloud environment from the perspective of formal verification. We argue that most of the layers could be practically formally verified, even if the work to verify all levels is huge.

[3]
Noman Javed and Frédéric Loulergue. Parallel Programming and Performance Predictability with Orléans Skeleton Library. In International Conference on High Performance Computing and Simulation (HPCS), pages 257-263. IEEE, 2011. [ DOI ]
Orléans Skeleton Library (OSL) is a library of parallel algorithmic skeletons in C++ on top of MPI. It provides a structured approach towards parallel programming. Skeletons in OSL are based over the bulk synchronous parallelism model. Applications can be developed using different combinations and compositions of the skeletons. This paper illustrates the expressivity and performance predictability of OSL with two applications: a two dimensional heat diffusion simulation, and an exact n-body simulation. Experiments using these applications are performed on parallel machines.

[4]
Noman Javed and Frédéric Loulergue. A Formal Programming Model of Orléans Skeleton Library. In Victor Malyshkin, editor, 11th International Conference on Parallel Computing Technologies (PaCT), LNCS 6873, pages 40-52. Springer, 2011. [ DOI ]
Orléans Skeleton Library (OSL) is a library of parallel algorithmic skeletons in C++ on top of MPI. It provides a structured approach towards parallel programming. Skeletons in OSL are based on the bulk synchronous parallelism model. In this paper we present formal semantics of OSL: a programming model and its properties proved with the Coq assistant.

[5]
Noman Javed, Frédéric Loulergue, Julien Tesson, and Wadoud Bousdira. Prototyping a Library of Algorithmic Skeletons with Bulk Synchronous Parallel ML. In The 2011 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'11), pages 520-526. CSREA Press, 2011.
Algorithmic skeletons are a high-level approach to parallel programming that can be combined with widely used programming languages such as Java, C and C++. In this paper we show that prototyping such a library with a structured parallel functional language, namely Bulk Synchronous Parallel ML, provides a parallel implementation with which experiments can be performed and gives some hints about the formal semantics of the library as well.

[6]
Julien Tesson and Frédéric Loulergue. A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation. In International Conference on Computational Science (ICCS), Procedia Computer Science, pages 36-45. 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.

[7]
Louis Gesbert, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, and Julien Tesson. Systematic Development of Correct Bulk Synchronous Parallel Programs. In International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), pages 334-340. IEEE, 2010. [ DOI ]
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.

[8]
Julien Tesson, H. Hashimoto, Zhenjiang Hu, Frédéric Loulergue, and Masato Takeichi. Program Calculation in Coq. In Thirteenth International Conference on Algebraic Methodology And Software Technology (AMAST2010), LNCS 6486, pages 163-179. Springer, 2010. [ 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.

[9]
Noman Javed and Frédéric Loulergue. OSL: Optimized Bulk Synchronous Parallel Skeletons on Distributed Arrays. In Y. Don, R. Gruber, and J. Joller, editors, 8th international Conference on Advanced Parallel Processing Technologies (APPT'09), LNCS 5737, pages 436-451. Springer, 2009. [ DOI ]
The existing solutions to program parallel architectures range from parallelizing compilers to distributed concurrent programming. Intermediate approaches propose a more structured parallelism: Algorithmic skeletons are higher-order functions that capture the patterns of parallel algorithms. The user of the library has just to compose some of the skeletons to write her parallel application. When one is designing a parallel program, the parallel performance is important. It is thus very interesting for the programmer to rely on a simple yet realistic parallel performance model such as the Bulk Synchronous Parallel (BSP) model. We present OSL, the Orléans Skeleton Library: it is a library of BSP algorithmic skeletons in C++. It offers data-parallel skeletons on arrays as well as communication oriented skeletons. The performances of OSL are demonstrated with two applications: heat equation and FFT.

[10]
Louis Gesbert and Frédéric Loulergue. Semantics of an Exception Mechanism for Bulk Synchronous Parallel ML. In International Conference on Parallel and Distributed Computing, Applications and Technologies (PDCAT), pages 201-208. IEEE Computer Society, 2007. [ DOI ]
Bulk Synchronous Parallel ML is a high-level language for programming parallel algorithms. Built upon OCaml and using the BSP model, it provides a safe setting for their implementation, avoiding concurrency related problems (deadlocks, indeterminism). Only a limited set of the features of OCaml can be used in BSML to respect its properties of safety: this paper describes a way to add exception handling to this set by extending and adapting OCaml's exceptions. After a precise definition of the problems that arise and an informal description of the solutions, an extension of BSML is proposed. Formal semantics define the behaviour in all possible cases, followed by a short description of the implementation.

[11]
Louis Gesbert, Frédéric Gava, Frédéric Loulergue, and Frédéric Dabrowski. Bulk Synchronous Parallel ML with Exceptions. In Peter Kacsuk, Thomas Fahringer, and Zsolt Nemeth, editors, Distributed and Parallel Systems (DAPSYS 2006), pages 33-42. Springer, 2006. [ DOI ]
Bulk Synchronous Parallel ML is a high-level language for programming parallel algorithms. Building upon OCaml and using the BSP model, it provides a safe setting for their implementation, avoiding concurrency related problems (deadlocks, indeterminism). Only a limited set of the features of OCaml can be used in BSML to respect its safety: this paper describes a way to add exception handling to this set by extending and adapting OCaml's exceptions. The behaviour of these new exceptions and the syntactic constructs to handle them, together with their implementation, are described in detail, and results over an example are given.

[12]
Frédéric Loulergue, Radia Benheddi, Frédéric Gava, and Dimitri Louis-Regis. Bulk Synchronous Parallel ML: Semantics and Implementation of the Parallel Juxtaposition. In International Computer Science Symposium in Russia (CSR 2006), volume 3967 of LNCS, pages 475-486. Springer, 2006. [ DOI ]
The Bulk Synchronous Parallel ML (BSML) library is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the lambda-calculus by parallel operations on a parallel data structure named parallel vector. This paper presents the execution model, given as a distributed semantics, of the parallel juxtaposition, a primitive of parallel composition for BSML. It also presents an implementation, which follows the semantics, and experiments using the parallel juxtaposition.

[13]
Frédéric Loulergue, Frédéric Gava, and D. Billiet. Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction. In Vaidy S. Sunderam, Gaétan Dick van Albada, Peter M. A. Sloot, and Jack Dongarra, editors, International Conference on Computational Science (ICCS), LNCS 3515, pages 1046-1054. Springer, 2005. [ DOI ]
The BSMLlib is a library for parallel programming with the functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector. The execution time can be estimated, dead-locks and indeterminism are avoided. Programs are written as usual functional programs (in Objective Caml) but using a small set of additional functions. Provided functions are used to access the parameters of the parallel machine and to create and operate on parallel vectors. It follows the execution and cost model of the Bulk Synchronous Parallel model. The paper presents the lastest implementation of this library and experiments of performance prediction.

[14]
Frédéric Loulergue. Optimizing Bulk Synchronous Parallel ML. In Chao Lu and Roger Lee, editors, 6th ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing (SNPD 2005), pages 294-299. IEEE Computer Society, 2005.
Bulk Synchronous Parallel ML is a functional parallel language based on the Bulk Synchronous Parallelism model of computation. Deadlocks are avoided and programs are deterministic. The performance of programs can be accurately predicted. This paper addresses the optimization of BSML programs through the compilation of BSML primitives to Objective Caml code with calls to a low level library rather than their direct implementation as a high level library.

[15]
Frédéric Gava and Frédéric Loulergue. Semantics of a Functional Bulk Synchronous Parallel Language with Imperative Features. In Gaétan Joubert, W. Nagel, Frédéric Peters, and W. Walter, editors, Parallel Computing: Software Technology, Algorithms, Architectures and Applications, Proceedings of the 10th ParCo Conference, pages 95-102, Dresden, 2004. North Holland/Elsevier.
The Bulk Synchronous Parallel ML (BSML) is a functional language for Bulk Synchronous Parallel (BSP) programming, on top of the sequential functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector, which is given by intention. The Objective Caml language is a functional language but it also offers imperative features. This paper presents formal semantics of BSML with references, assignment and dereferencing.

[16]
Frédéric Loulergue. A Calculus of Functional BSP Programs with Explicit Substitution. In Gaétan Joubert, W. Nagel, Frédéric Peters, and W. Walter, editors, Parallel Computing: Software Technology, Algorithms, Architectures and Applications, Proceedings of the 10th ParCo Conference, pages 127-134, Dresden, 2004. North Holland/Elsevier.
The BSlambdasigmaUparrow-calculus calculus is a calculus of functional BSP programs with enumerated parallel vectors and explicit substitution. This confluent calculus is defined and proved confluent. These results constitute the core of a formal design for a Bulk Synchronous Parallel dialect of ML (BSML) as well as a framework for proving parallel abstract machine which can evaluate BSML programs.

[17]
Frédéric Loulergue. An Event Oriented Functional Parallel Language. In Gaétan Joubert, W. Nagel, Frédéric Peters, and W. Walter, editors, Parallel Computing: Software Technology, Algorithms, Architectures and Applications, Proceedings of the 10th ParCo Conference, pages 79-86, Dresden, 2004. North Holland/Elsevier.
This paper presents the design of the core of a parallel programming language called CDS*. It is based on explicitly-distributed concrete data structures and features compositional semantics, higher-order functions and explicitly distributed objects. The denotational semantics is outlined, the (equivalent) operational semantics is presented and a new realization of the latter is given as a rewriting system. Simulated execution of examples illustrates the language's flexibility and explicit control of data layout on the parallel network.

[18]
Frédéric Loulergue. Management of Communication Environments for Minimally Synchronous Parallel ML. In Z. Juhasz, P. Kacsuk, and D. Kranzimuller, editors, Distributed and Parallel Systems (DAPSYS 2004), pages 185-192. Springer, 2004.
Minimally Synchronous Parallel ML is a functional parallel language whose execution time can then be estimated and dead-locks and indeterminism are avoided. Programs are written as usual ML programs but using a small set of additional functions. Provided functions are used to access the parameters of the parallel machine and to create and operate on a parallel data structure. It follows the cost model of the Message Passing Machine model (MPM). In the current implementation, the asynchrony is limited by a parameter called the asynchrony depth. When processes reach this depth a global synchronization occurs. This is necessary to avoid memory leak. In this paper we propose a mechanism to avoid such synchronization barriers. This mechanism relies on a more complex management of the communication environments but with a small and parametrized overhead.

[19]
Frédéric Loulergue. Communication Primitives for Minimally Synchronous Parallel ML. In M. Bubak, D. van Albada, P. Sloot, and J. Dongarra, editors, The International Conference on Computational Science (ICCS 2004), Part I, LNCS, pages 411-414. Springer Verlag, 2004. [ DOI ]
Minimally Synchronous Parallel ML is a functional parallel language whose execution time can then be estimated and dead-locks and indeterminism are avoided. Programs are written as usual ML programs but using a small set of additional functions. Provided functions are used to access the parameters of the parallel machine and to create and operate on a parallel data structure. It follows the cost model of the Message Passing Machine model (MPM). This paper explore the writing of an additional communication function using this small set of primitives. It could also be considered as a primitive rather than a function written using primitives. So we developed a low-level implementation of this function and compared it with the high-level implementation in terms of efficiency.

[20]
Myrto Arapinis, Frédéric Loulergue, Frédéric Gava, and Frédéric Dabrowski. Semantics of Minimally Synchronous Parallel ML. In W. Dosch and R. Y. Lee, editors, 4th International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing (SNPD'03), pages 260-267. ACIS, 2003.
This paper presents a new functional parallel language: Minimally Synchronous Parallel ML. It shares with Bulk Synchronous Parallel ML its syntax and high-level semantics but it has a minimally synchronous distributed semantics. It follows the cost model of the Message Passing Machine model (MPM).

[21]
Frédéric Dabrowski and Frédéric Loulergue. Functional Bulk Synchronous Programming in C++. In 21st IASTED International Multi-conference, Applied Informatics (AI 2003), Symposium on Parallel and Distributed Computing and Networks, pages 462-467. ACTA Press, february 2003.
This paper presents the BSFC++ library for functional bulk synchronous parallel programming in C++. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector, which is given by intention. This guarantees the determinism and the absence of deadlock. Broadcast algorithms are implemented using the core library.

[22]
Frédéric Dabrowski, Frédéric Loulergue, and Frédéric Gava. Pattern Matching of Parallel Values in Bulk Synchronous Parallel ML. In W. Dosch and R. Y. Lee, editors, 4th International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing (SNPD'03), pages 301-308. ACIS, 2003.
This paper presents an extension of the functional parallel language BSML (Bulk Synchronous Parallel ML) and of the BSlambda-calculus (a calculus of functional bulk synchronous parallel programs) with pattern matching of parallel values.

[23]
Frédéric Gava and Frédéric Loulergue. A Parallel Virtual Machine for Bulk Synchronous Parallel ML. In Peter M. A. Sloot and al., editors, International Conference on Computational Science (ICCS 2003), Part I, number 2657 in LNCS, pages 155-164. Springer Verlag, june 2003. [ DOI ]
We have designed a functional data-parallel language called BSML for programming bulk-synchronous parallel (BSP) algorithms in so-called direct mode. In a direct-mode BSP algorithm, the physical structure of processes is made explicit. The execution time can then be estimated and dead-locks and indeterminism are avoided. The BSMLlib library has been implemented for the Objective Caml language. But there is currently no full implementation of such a language and an abstract machine is needed to validate such an implementation. Our approach is based on a bytecode compilation to a parallel abstract machine performing exchange of data and synchronous requests derived from the ZAM, the efficient abstract machine of the Objective Caml language.

[24]
Frédéric Gava and Frédéric Loulergue. A Polymorphic Type System for Bulk Synchronous Parallel ML. In V. Malyshkin, editor, Seventh International Conference on Parallel Computing Technologies (PaCT 2003), number 2763 in LNCS, pages 215-229. Springer Verlag, 2003. [ DOI ]
The BSMLlib library is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a data structure named parallel vector, which is given by intention. In order to have an execution that follows the BSP model, and to have a simple cost model, nesting of parallel vectors is not allowed. The novelty of this paper is a type system which prevents such nesting. This system is correct w.r.t. the dynamic semantics which is also presented.

[25]
Frédéric Gava, Frédéric Loulergue, and Frédéric Dabrowski. A Parallel Categorical Abstract Machine for Bulk Synchronous Parallel ML. In W. Dosch and R. Y. Lee, editors, 4th International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing (SNPD'03), pages 293-300. ACIS, 2003.
We have designed a functional data-parallel language called BSML for programming bulk-synchronous parallel (BSP) algorithms in so-called direct mode. In a direct-mode BSP algorithm, the physical structure of processes is made explicit. The execution time can then be estimated and dead-locks and indeterminism are avoided. The BSMLlib library has been implemented for the Objective Caml language. But there is currently no full implementation of such a language and an abstract machine is needed to have a certified implementation. Our approach is based on a byte-code compilation to a parallel abstract machine performing exchange of data and synchronous requests derived from the abstract machine of the Caml language.

[26]
Frédéric Loulergue. Parallel Juxtaposition for Bulk Synchronous Parallel ML. In H. Kosch, L. Boszorményi, and H. Hellwagner, editors, Euro-Par 2003, number 2790 in LNCS, pages 781-788. Springer Verlag, 2003. [ DOI ]
The BSMLlib library is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector. An attempt to add a parallel composition to this approach led to a non-confluent calculus and to a restricted form of parallel composition. This paper presents a new, simpler and more general semantics for parallel composition, renamed here parallel juxtaposition, as well as an associated cost model derived from the BSP cost model.

[27]
Frédéric Loulergue. Parallel Superposition for Bulk Synchronous Parallel ML. In Peter M. A. Sloot and al., editors, International Conference on Computational Science (ICCS 2003), LNCS 2659, pages 223-232. Springer Verlag, 2003. [ DOI ]
The BSMLlib library is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector, which is given by intention. Those operations are flat and allow BSP programming in direct mode but it is impossible to express directly divide-and-conquer algorithms. This paper presents a new construction for the BSMLlib library which can express divide-and-conquer algorithms. It is called parallel superposition because it can be seen as the parallel composition of two BSP threads which can each use all the processors. An associated cost model derived from the BSP cost model is also given.

[28]
Frédéric Loulergue. Implementation of a Functional Bulk Synchronous Parallel Programming Library. In 14th IASTED International Conference on Parallel and Distributed Computing Systems, pages 452-457. ACTA Press, 2002.
The BSMLlib is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the lambda-calculus by parallel operations on a parallel data structure named parallel vector, which is given by intention. A first implementation of this library was based on the BSPlib library, which is not longer supported nor updated. Being the basis of a framework for Grid computing, a new implementation of the BSMLlib based on MPI has been designed. Experimental results on a cluster of PCs are presented.

[29]
Frédéric Loulergue. Parallel Composition and Bulk Synchronous Parallel Functional Programming. In S. Gilmore, editor, Trends in Functional Programming, Volume 2, pages 77-88. Intellect Books, 2001.
The work described here is part of our research program to investigate new paradigms for declarative parallel programming through special interpretations of standard semantics. Our approach is a purely functional approach to programming of BSP algorithms. An attempt to add a parallel composition to this approach led to a non-confluent calculus. This paper presents a solution for adding the parallel composition to the weak call-by-value strategy of the BSlambda_p and to the BSMLlib library.

[30]
Olivier Ballereau, Frédéric Loulergue, and Gaétan Hains. High-level BSP Programming: BSML and BSλ. In Gaétan Michaelson and Ph. Trinder, editors, Trends in Functional Programming, pages 29-38. Intellect Books, 2000.
A functional data-parallel language called BSML is designed for programming bulk-synchronous parallel (BSP) algorithms in so-called direct mode. Its aim is to combine the generality of languages like NESL with the predictable performance of direct-mode BSP algorithms. The BSML operations are motivated and described. Experiments with a library implementation of BSML show the possibility and limitations of parallel performance prediction in this framework.

[31]
Frédéric Loulergue. BSλp: Functional BSP Programs on Enumerated Vectors. In J. Kazuki, editor, International Symposium on High Performance Computing, number 1940 in LNCS, pages 355-363. Springer, October 2000. [ DOI ]
The BSlambda_p calculus is a calculus of functional BSP programs on enumerated parallel vectors. This confluent calculus is defined and a parallel cost model is associated with a weak call-by-value strategy. These results constitute the core of a formal design for a BSP dialect of ML.

[32]
Frédéric Loulergue and Gaétan Hains. Parallel functional programming with explicit processes: Beyond SPMD. In C. Lengauer, M. Griebl, and S. Gorlatch, editors, Euro-Par'97 Parallel Processing, number 1300 in LNCS, pages 530-537, Passau, Germany, August 1997. Springer.
This paper presents the design for a purely functional parallel language with higher-order functions. Data layout is explicit in the language and arbitrary synchronizations can be specified in the non-standard type system based on concrete data structures. We present its denotational semantics, operational semantics, full abstraction property and program examples to illustrate its key features.

Exposé à un colloque international / Talk at an International Conference without Proceedings

[1]
Frédéric Loulergue. On the Formal Verification of Computer Simulations. In 5th Models and Simulations conference (MS5), The Finnish Centre of Excellence in the Philosophy of the Social Sciences, Helsinki, Finland, June 2012.

Colloque national / National Conference

[1]
Wadoud Bousdira, Louis Gesbert, and Frédéric Loulergue. Syntaxe et sémantique de Revised Bulk Synchronous Parallel ML. In S. Conchon and A. Mahboubi, editors, Journées Francophones des Langages Applicatifs (JFLA), Studia Informatica Universalis, pages 117-146. Hermann, 2011.
Bulk Synchronous Parallel ML (BSML) est une extension du langage fonctionnel Objective Caml, fondé sur un modèle structuré de parallélisme, le modèle BSP. Ce modèle assure au programmeur BSML la sûreté d'exécution tout en lui laissant le strict contrôle des processeurs. Le modèle de prévision de performances de BSML est simple et réaliste. Le parallélisme est exprimé en utilisant un ensemble de primitives fonctionnelles pures sur une structure de données parallèle appelée vecteur parallèle. Cependant, les programmes sont souvent difficiles à écrire et leur mise au point peut être fastidieuse. Nous proposons dans cet article une nouvelle syntaxe et une sémantique associée dans le but d'écrire des programmes plus courts et plus lisibles. Nous formalisons la syntaxe et la sémantique classiques ainsi que les nouvelles syntaxe et sémantique, puis nous les modélisons en Coq. Leur confluence est établie.

[2]
H. Hashimoto, Zhenjiang Hu, Julien Tesson, Frédéric Loulergue, and Masato Takeichi. A Coq Library for Program Calculation. In JSSST Conference on Software Science and Technology, Shimane University, Shimane, Japan, 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.

[3]
Radia Benheddi and Frédéric Loulergue. Composition parallèle pour MSPML. In P.-E. Moreau and T. Hardin, editors, Journées Francophones des Langages Applicatifs (JFLA), pages 101-116. INRIA, 2006.
Cet article présente l'ajout, à un langage fonctionnel parallèle appelé Minimally Synchronous Parallel ML (MSPML), d'une primitive pour la composition parallèle, appelée juxtaposition. MSPML est un langage fonctionnel parallèle basé sur un petit nombre de primitives sur une structure de données parallèle. Les programmes sont écrits comme des programmes ML usuels en utilisant ce petit ensemble de fonctions. MSPML est déterministe et sans déblocages. Le temps d'exécution des programmes peut étre estimé. Il a une sémantique asynchrone, c'est-à-dire sans barrière de synchronisation globale. Cette propriété s'avère intéressante pour des programmes non équilibrés à chaque étape. Toutefois il ne permettait pas d'écrire des algorithmes diviser-pour-règner parallèles qui sont courants dans la littérature. La juxtaposition remédie à cette limitation.

[4]
Frédéric Gava and Frédéric Loulergue. Synthèse de types pour Bulk Synchronous Parallel ML. In J.C. Filliatre, editor, Journées Francophones des Langages Applicatifs (JFLA 2003), pages 153-168, january 2003.
The BSMLlib library is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a data structure named parallel vector, which is given by intention. In order to have an execution that follows the BSP model, and to have a simple cost model, nesting of parallel vectors is not allowed. The novelty of this paper is a type system which prevents such nesting. An algorithm for type inference is also presented.

[5]
A. Merlin, Gaétan Hains, and Frédéric Loulergue. A SPMD Environment Machine for Functional BSP Programs. In Proceedings of the Third Scottish Functional Programming Workshop, august 2001.
A functional data-parallel language called BSML has been designed for programming bulk-synchronous parallel (BSP) algorithms in so-called direct mode. Its aim is to offer predictable and scalable performance for BSP algorithms written as functional programs. The current implementation of BSML is a library and has not been validated w.r.t the language's formal definition. As a library, it does not allow static tools to support performance management. As a first step in the construction of a complete BSML language, we have defined a parallel environment machine from our language's evaluation semantics and begun testing the scalability and predictability of its performance. This paper presents the machine design and the results of our experiments.

[6]
Frédéric Loulergue. Parallel Composition and Bulk Synchronous Parallel Functional Programming. In Stephen Gilmore, editor, Proceedings of the second Scottish Functional Programming Workshop, St Andrews, July 2000.
The work described here is part of our research program to investigate new paradigms for declarative parallel programming through special interpretations of standard semantics. Our approach is a purely functional approach to programming of BSP algorithms. An attempt to add a parallel composition to this approach led to a non-confluent calculus. This paper presents a solution for adding the parallel composition to the weak call-by-value strategy of the BSlambda_p and to the BSMLlib library.

[7]
Olivier Ballereau, Frédéric Loulergue, and Gaétan Hains. High-level BSP Programming: BSML and BSλ. In P Trinder and Gaétan Michaelson, editors, Proceedings of the first Scottish Functional Programming Workshop, number Techinal Report RM/99/9, pages 43-52, Edinburgh, august 1999. Heriot-Watt University.
BSMLlib is a functional data-parallel library for programming bulk-synchronous parallel (BSP) algorithms in Objective CAML. The definition of BSMLlib and performance prediction for elementary operations have been discussed in Sfp2000. This article demonstrates the expressivity of operations on elementary algorithms. Other operations, on a type of parallel sets, illustrate the advantage of explicit BSP exchange phases: the possibility of predicting and minimising communication and synchronization costs. A more complex example, inspired by parallel join algorithms for relational databases, demonstrates the advantage of using BSMLlib's explicit processes for dynamic load balancing. Finally, suggestions are made for extending the library and building a complete BSML language with the same operations.

[8]
Frédéric Loulergue. Extension du BSλ-calcul. In P. Weis, editor, JFLA'99 : Journées Francophones des Langages Applicatifs, pages 93-112, Morzine-Avoriaz, February 1999.
Après une présentation du calcul confluent BSλ, extension du λ-calcul par des opérations parallèles permettant l'expression d'algorithmes BSP, nous proposons trois nouvelles opérations parallèles étendant le calcul. Le calcul et cette nouvelle extension sont illustrés par différentes algorithmes de diffusion donnés dans une syntaxe à la ML.

[9]
Frédéric Loulergue. BSML : Programmation BSP purement fonctionnelle. In D. Méry and Gaétan-R. Perrin, editors, Dixièmes Rencontres Francophones du Parallélisme (Renpar'10), pages 243-246, Strasbourg, june 1998.
Nous d'efinissons une extension minimale du langage fonctionnel Caml par des op'erations parall`eles BSP, d'eriv'ees d'un mod`ele d'enotationel simple avec processus explicites et statiques. Le langage obtenu, BSML, pr'eserve la s'emantique compositionnelle et permet des pr'evisions pr'ecises de performances gr^ace au mod`ele de co^uts BSP. Nous l'illustrons sur des algorithmes parall`eles de base et montrons comment un simulateur BSML permet,a`l'aide des param`etres BSP des machines, de pr'evoir les performances r'eelles.

[10]
Frédéric Loulergue and G Hains. Programmation fonctionnelle parallèle en processus statiques: Une approche dénotationnelle. In M. Gengler and C. Queinnec, editors, Journées Francophones des Langages Applicatifs JFLA'97. INRIA, 1997.
This paper presents the design for a purely functional parallel language with higher-order functions. It is based on specialisation of a non-standard model of lambda calculus (concrete data structure): array data structures. We present its denotational semantics, operational semantics, full abstraction property and program examples to illustrate its key features.

Atelier international / International Workshop

[1]
Mohamad Al Hajj Hassan, Mostafa Bamha, and Frédéric Loulergue. An Efficient Skew-insensitive Algorithm for Join Processing on Grid Architectures. In 5th ACM SIGPLAN workshop on High-Level Parallel Programming and Applications, pages 11-18. ACM, 2011. [ DOI ]
Scientific experiments in many domains generate a huge amount of data whose size is in the range of hundreds of megabytes to petabytes. These data are stored on geographically distributed and heterogeneous resources. Researchers who need to analyze and have a fast access to such data are also located all over the globe. Queries executed by these researchers may require the transfer of huge amount of data over the wide area network in a reasonable time. Due to these emerging needs, the grid infrastructure which connects widely geographically distributed and heterogeneous computing and storage resources was born. In this paper, we are interested in treating join queries on the grid. We propose a new parallel algorithm allowing to reduce communication and disk Input/Output costs to minimum.

[2]
Frédéric Gava, Louis Gesbert, and Frédéric Loulergue. Type System for a Safe Execution of Parallel Programs in BSML. In 5th ACM SIGPLAN workshop on High-Level Parallel Programming and Applications, pages 27-34. ACM, 2011. [ DOI ]
BSML, or Bulk Synchronous Parallel ML, is a high-level language based on ML and dedicated to parallel computation. In this paper, an extended type system that guarantees the safety of parallel programs is presented. It prevents non-determinism and deadlocks by ensuring that the invariants needed to preserve the structured parallelism are verified. Imperative extensions (references, exceptions) are included, and the system is designed for compatibility with modules.

[3]
Wadoud Bousdira, Frédéric Gava, Louis Gesbert, Frédéric Loulergue, and Guillaume Petiot. Functional Parallel Programming with Revised Bulk Synchronous Parallel ML. In Koji Nakano, editor, First International Conference on Networking and Computing (ICNC 2010), 2nd International Workshop on Parallel and Distributed Algorithms and Applications (PDAA), pages 191-196. IEEE Computer Society, 2010. [ DOI ]
Bulk Synchronous Parallel ML or BSML is a high-level language for programming parallel algorithms. Built upon the Objective Caml language, it provides a safe setting for implementing Bulk Synchronous Parallel (BSP) algorithms. It avoids concurrency related problems: deadlocks and non- determinism. BSML is based on a very small core of parallel primitives that extended functional sequential programming to functional BSP programming with a parallel data structure and operations to manipulate it. However, in practice the primitives for writing the parallel non-communicating parts of the program are not so easy to use. Thus we designed a new syntax that makes programs easier to write and read. Revised BSML is presented and its expressiveness and performance are illustrated through an application example.

[4]
Radia Benheddi and Frédéric Loulergue. Divide-and-Conquer Programming with Minimally Synchronous Parallel ML. In J. Weglarz, R. Wyrzykowski, and B. Szymanski, editors, Seventh International Conference on Parallel Processing and Applied Mathematics (PPAM 2007), Workshop on Language-Based Parallel Programming Models, number 4967 in LNCS, pages 1078-1085. Springer, 2008. [ DOI ]
Minimally Synchronous Parallel ML (MSPML) is a functional parallel programming language. It is based on a small number of primitives on a parallel data structure. MSPML programs are written like usual sequential ML program and use this small set of functions. MSPML is deterministic and deadlock free. The execution time of the programs can be estimated. Divide-and-conquer is a natural way of expressing parallel algorithms. MSPML is a flat language: it is not possible to split the parallel machine in order to implement divide-and-conquer parallel algorithms. This paper presents an extension of MSPML to deal with this kind of algorithms: a parallel composition primitive.

[5]
Julien Tesson and Frédéric Loulergue. Formal Semantics for the DRMA Programming Style Subset of the BSPlib Library. In J. Weglarz, R. Wyrzykowski, and B. Szymanski, editors, Seventh International Conference on Parallel Processing and Applied Mathematics (PPAM 2007), Workshop on Language-Based Parallel Programming Models, number 4967 in LNCS, pages 1122-1129. Springer, 2008. [ DOI ]
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.

[6]
Frédéric Loulergue. A Calculus of Functional BSP Programs with Projection. In International Parallel & Distributed Processing Symposium, 8th Workshop on Advances in Parallel and Distributed Computational Models. IEEE Computer Society Press, 2006. [ DOI ]
Bulk Synchronous Parallel ML (BSML) is an extension of the functional language Objective Caml to program Bulk Synchronous Parallel (BSP) algorithms. It is deterministic, deadlock free and performances are good and predictable. Parallelism is expressed with a set of 4 primitives on a parallel data structure called parallel vector. These primitives are pure functional ones: they have no side-effect. It is thus possible, and we did it, to prove the correctness of BSML programs using a proof assistant like Coq. The BSλ-calculus is an extension of the λ-calculus which models the core semantics of BSML. Nevertheless some principles of BSML are not well captured by this calculus. This paper presents a new calculus, with a projection primitive, which provides a better model of the core semantics of BSML.

[7]
Frédéric Gava and Frédéric Loulergue. A Functional Language for Departmental Metacomputing. In S. Gorlatch, editor, 4th Workshop on Constructive Methods for Parallel Programming, pages 63-80. Westfälische Wilheims-Universitët Münster, 2004.
We have designed a functional data-parallel language called BSML for programming bulk-synchronous parallel algorithms, a model of computing. Dead-locks and indeterminism are avoided and the execution time can be then estimated. For large scale applications where parallel processing is helpful, more than one parallel machine is needed. One speaks about metacomputing. A major problem in programming parallel application for such platforms is their hierarchical network structures: latency and bandwidth of global ones are orders of magnitude worse than those of local networks. Here we consider how an extention of the well-suited BSP model might be for these kinds of computing and how extended our functional language can be for this.

[8]
Gaétan Hains and Frédéric Loulergue. Functional Bulk Synchronous Parallel Programming using the BSMLlib Library. In S. Gorlatch, editor, Second International Workshop on Constructive Methods for Parallel Programming (CMPP'2000), Research Report MIP-2000-07, June 2000.
BSMLlib is a functional data-parallel library for programming bulk-synchronous parallel (BSP) algorithms in Objective CAML. The definition of BSMLlib and performance prediction for elementary operations have been discussed in Sfp2000. This article demonstrates the expressivity of operations on elementary algorithms. Other operations, on a type of parallel sets, illustrate the advantage of explicit BSP exchange phases: the possibility of predicting and minimising communication and synchronization costs. A more complex example, inspired by parallel join algorithms for relational databases, demonstrates the advantage of using BSMLlib's explicit processes for dynamic load balancing. Finally, suggestions are made for extending the library and building a complete BSML language with the same operations.

[9]
Frédéric Loulergue, Gaétan Hains, and Christian Foisy. A Calculus of Recursive-Parallel BSP Programs. In S. Gorlatch, editor, First International Workshop on Constructive Methods for Parallel Programming (CMPP'98), Research Report MIP-9805, pages 59-70. University of Passau, May 1998.
An extension of the lambda-calculus called BSlambda is introduced as a formal basis for functional languages expressing bulk synchronous parallel algorithms. A local confluence result is explained and a call-by-value evaluation strategy is defined. The operational meaning of the calculus is illustrated by two programs defining the binary fold algorithm, one flat and one parallel-recursive.

Rapport de recherche / Research Report

[1]
Noman Javed and Frédéric Loulergue. Parallel Programming with Orléans Skeleton Library. Technical Report RR-2011-05, LIFO, University of Orléans, March 2011.
Orleans Skeleton Library (OSL) is a library of parallel algorithmic skeletons in C++ on top of MPI. It provides a structured approach towards parallel programming. Skeletons in OSL are based over the bulk synchronous parallelism model. Applications can be developed using different combinations and compositions of the skeletons. This paper illustrates the expressivity of OSL with two applications: a two dimensional heat diffusion simulation, and an exact n-body simulation. Experiments using these applications are performed on parallel machines.

[2]
Noman Javed and Frédéric Loulergue. A Formal Programming Model of Orléans Skeleton Library. Technical Report RR-2011-06, LIFO, University of Orléans, April 2011.
Orléans Skeleton Library (OSL) is a library of parallel algorithmic skeletons in C++ on top of MPI. It provides a structured approach towards parallel programming. Skeletons in OSL are based on the bulk synchronous parallelism model. In this paper we present formal semantics of OSL: a programming model and its properties proved with the Coq assistant.

[3]
Julien Tesson, H. Hashimoto, Zhenjiang Hu, Frédéric Loulergue, and Masato Takeichi. Program Calculation in Coq. Technical Report RR-2009-07, LIFO, University of Orléans, 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.

[4]
Frédéric Loulergue, Zhenjiang Hu, and K. Kakehi. A Tutorial Implementation of the Diffusion Algorithmic Skeleton with the BSMLlib Library. Technical Report METR-2004-06, Department of Mathematical Informatics, University of Tokyo, 2004.
Skeleton programming enables programmers to build parallel programs easier by providing efficient ready-made parallel algorithms. The diffusion skeleton was proposed (associated with a method for program derivation) to abstract a good combination of primitive skeletons, such as map, parallel reduction and parallel prefix sum (scan). The BSMLlib library whose design is based on formal semantics is a library for the Objective Caml language to support Bulk Synchronous Parallelism. It offers a small set of primitives which permits to write any deterministic BSP algorithm. In this paper we study the implementation of the diffusion parallel skeleton using the BSMLlib library in a tutorial way.

[5]
Frédéric Loulergue. Communication Primitives for Minimally Synchronous Parallel ML. Technical Report 2004-02, University of Paris 12, LACL, 2004.
Minimally Synchronous Parallel ML is a functional parallel language whose execution time can then be estimated and dead-locks and indeterminism are avoided. Programs are written as usual ML programs but using a small set of additional functions. Provided functions are used to access the parameters of the parallel machine and to create and operate on a parallel data structure. It follows the cost model of the Message Passing Machine model (MPM). This paper explore the writing of an additional communication function using this small set of primitives. It could also be considered as a primitive rather than a function written using primitives. So we developed a low-level implementation of this function and compared it with the high-level implementation in terms of efficiency.

[6]
Frédéric Gava and Frédéric Loulergue. Verifying Functional Bulk Synchronous Parallel Programs Using the Coq System. Technical Report 187, University of Freiburg, D. Basin and B. Wolff editor, TPHOLS'03, Emerging Trends, september 2003.
The Bulk Synchronous Parallel ML (BSML) is a functional language for Bulk Synchronous Parallel (BSP) programming. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector, which is given by intention. We present the formal proofs of correctness of BSML programs in the Coq proof assistant. Such development demonstrates the usefulness of higher-order logic in the process of software certification and parallel applications. They also show that proof of rather complex parallel algorithms may be made with inductive types by using the certified programs.

[7]
Frédéric Gava and Frédéric Loulergue. A Parallel Virtual Machine for Bulk Synchronous Parallel ML. Technical Report 2003-01, University of Paris Val-de-Marne, LACL, january 2003.
We have designed a functional data-parallel language called BSML for programming bulk-synchronous parallel (BSP) algorithms in so-called direct mode. In a direct-mode BSP algorithm, the physical structure of processes is made explicit. The execution time can then be estimated and dead-locks and indeterminism are avoided. The BSMLlib library has been implemented for the Objective Caml language. But there is currently no full implementation of such a language and an abstract machine is needed to validate such an implementation. Our approach is based on a bytecode compilation to a parallel abstract machine performing exchange of data and synchronous requests derived from the ZAM, the efficient abstract machine of the Objective Caml language.

[8]
Frédéric Gava and Frédéric Loulergue. Verifying Functional Bulk Synchronous Parallel Programs Using the Coq System. Technical Report 2003-02, University of Paris 12, LACL, 2003.
The Bulk Synchronous Parallel ML (BSML) is a functional language for Bulk Synchronous Parallel (BSP) programming. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector, which is given by intention. We present the formal proofs of correctness of BSML programs in the Coq proof assistant. Such development demonstrates the usefulness of higher-order logic in the process of software certification and parallel applications. They also show that proof of rather complex parallel algorithms may be made with inductive types by using the certified programs.

[9]
Frédéric Dabrowski and Frédéric Loulergue. Efficiency of Bulk Synchronous Parallel Programming using C++, BSCF++ and BSMLlib. Technical Report 2002-10, University of Paris Val-de-Marne, LACL, june 2002.
The BSMLlib library is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector, which is given by intention. The BSFC++ library is a library for Functional Bulk Synchronous Parallel programming in C++ which is based on the FC++ library. We present those libraries and give experimental results. For comparaison, MPI/C++ versions of the same programs were also ran on our cluster of PCs.

[10]
Frédéric Loulergue. Implementation of the BSMLlib Library v0.2. Technical Report 2002-11, University of Paris Val-de-Marne, LACL, july 2002.
The BSMLlib is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the λ-calcul by parallel operations on a parallel data structure named parallel vector, which is given by intention. A first implementation of this library was based on the BSPlib library, which is not longer supported nor updated. Being the basis of a framework for Grid computing, a new implementation of the BSMLlib based on MPI has been designed. Experimental results on a cluster of PCs are presented.

[11]
Frédéric Dabrowski and Frédéric Loulergue. Functional Bulk Synchronous Parallel Programming in C++. Technical Report 2002-13, University of Paris Val-de-Marne, LACL, august 2002.
This paper presents the BSFC++ library for functional bulk synchronous parallel programming in C++. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector, which is given by intention. This guarantees the determinism and the absence of deadlock. Broadcast algorithms are implemented using the core library.

[12]
Frédéric Loulergue. Parallel Juxtaposition for Bulk Synchronous Parallel ML. Technical Report 2002-17, University of Paris Val-de-Marne, LACL, november 2002.
The BSMLlib is a library for Bulk Synchronous Parallel (BSP) programming with the functional language Objective Caml. It is based on an extension of the λ-calculus by parallel operations on a parallel data structure named parallel vector, which is given by intention. An attempt to add a parallel composition to this approach led to a non-confluent calculus and to a restricted form of parallel composition. This paper presents a new, simpler and more general semantics for parallel composition, renamed here parallel juxtaposition, as well as an associated cost model derived from the BSP cost model.

[13]
Frédéric Gava and Frédéric Loulergue. A Bulk Synchronous Parallel Categorical Abstract Machine. Technical Report 2002-20, University of Paris Val-de-Marne, LACL, december 2002.
We have designed a functional data-parallel language called BSML for programming bulk-synchronous parallel (BSP) algorithms in so-called direct mode. In a direct-mode BSP algorithm, the physical structure of processes is made explicit. The execution time can then be estimated and dead-locks and indeterminism are avoided. The BSMLlib library has been implemented for the Objective Caml language. But there is currently no full implementation of such a language and an abstract machine is needed to validate such an implementation. Our approach is based on a natural semantics and a bytecode compilation to a parallel abstract machine performing exchange of data and synchronous requests derived from the abstract machine of the Caml language.

[14]
Frédéric Loulergue. Compositionality in Functional Bulk Synchronous Parallelism. Technical Report 2002-21, University of Paris Val-de-Marne, LACL, december 2002.
The BSλp-calculs an extension of the λ-calculus by bulk synchronous parallel (BSP) operations on a parallel data structure named parallel vector. This paper presents how functional composition is preserved in this framework both from the semantics point of view and from the cost model point of view. Those operations are flat and allow BSP programming in direct mode but it is impossible to express directly divide-and-conquer algorithms. This paper also present a new kind of composition, a new construction for the BSλp-calculus which can express divide-and-conquer algorithms. It is called parallel superposition. An associated cost model derived from the BSP cost model is also given.

[15]
Frédéric Loulergue. Confluence of the BSλ-calculus. Technical Report RR99-10, LIFO, Université d'Orléans, May 1999.
The BSlambda-calculus, a formal basis for functional languages expressing bulk synchronous parallel algorithms, is presented. It is then shown to be confluent.

[16]
Frédéric Loulergue and Gaétan Hains. An Introduction to BSλ. Technical Report RR98-09, LIFO, Université d'Orléans, September 1998.
This paper is an introduction to BSlambda a calculus of parallel-recursive BSP programs. The calculus is presented, the confluence of its flat subset is stated and examples are gieven in an ML-like syntax.

Mémoire / Thesis

[1]
Frédéric Loulergue. Functional Programming for Parallel and Meta Computing: Semantics, Systems and Proofs. Habilitation à diriger des recherches thesis, University Paris Val de Marne, december 2004.
[2]
Frédéric Loulergue. Programmation fonctionnelle d'ordinateurs parallèles et de méta-ordinateurs : sémantiques, systèmes et preuves. Mémoire d'habilitation à diriger des recherches, University Paris Val de Marne, décembre 2004.
[3]
Frédéric Loulergue. Conception de langages fonctionnels pour la programmation massivement parallèle. thèse de doctorat, Université d'Orléans, LIFO, 4 rue Léonard de Vinci, BP 6759, F-45067 Orléans Cedex 2, France, January 2000.
Certains problèmes nécessitent des performances que seules les machines massivement parallèles peuvent offrir. Leur programmation demeure néanmoins difficile. Les travaux étudiant le mélange de la programmation fonctionnelle et du parallélisme se répartissent en deux catégories : les extensions explicitement parallèles des langages fonctionnels - mais les langages obtenus sont soit indéterministes soit brisent l'aspect fonctionnel pur - et les implantations parallèles avec sémantique fonctionnelle - mais les langages obtenus n'expriment pas directement les algorithmes parallèles et ne permettent pas la prévision des temps d'exécution. L'approche des langages à patrons, dans lesquels seulement un ensemble fixé d'opérations sont exécutées en parallèle, est intermédiaire. Leur sémantique fonctionnelle est explicite mais leur sémantique opérationnelle parallèle est implicite. L'ensemble de patrons doit étre le plus complet possible mais cet ensemble s'avère dépendant du domaine d'application. Nous approfondissons cette position intermédiaire avec pour objectif de parvenir à des langages universels dans lesquels le code source permet de déterminer le coét. Cette dernière exigence nécessite que soient explicites dans les programmes les lieux du réseau de processeurs de la machine. Une approche dénotationnelle nous a amené à une étude des limites de l'expressivité des langages fonctionnels parallèles à processus explicites. Une approche opérationnelle nous a amené à définir des λ-calculs BSP (le modèle BSP ajoute une notion de processus explicites au parallélisme de données) confluents et universels pour les algorithmes BSP. Nous avons également analysé les conditions précises d'implantation parallèle de tels calculs, expérimenté le style de programmation associé et constaté qu'ils sont suffisamment expressifs et que la prévision des temps d'exécution parallèle y est possible. Abstract: Some problems require performance that only massively parallel computers offer, but their programming is still difficult. Works on functional programming and parallelism can be divided in two categories: explicit parallel extensions of functional languages - where resulting languages are either non-deterministic or non functional - and parallel implementations with functional semantics - where resulting languages don't express parallel algorithms directly and don't allow the prediction of execution times. Algorithmic skeletons languages, in which only a finite set of operations (the skeletons) are run in parallel, constitutes an intermediate approach. Their functional semantics is explicit but their parallel operational semantics is implicit. The set of algorithmic skeletons has to be as complete as possible but it is often dependent on the domain of application. We explore this intermediate position thoroughly in order to obtain universal parallel languages where source code determines execution cost. This last requirement forces the use of explicit processes corresponding to the parallel machine's processors. A denotational approach leads us to study the expressiveness of functional parallel languages with explicit processes. An operational approach leads us to define BSP lambda-calculi (the BSP model adds a notion of explicit process to data-parallelism) that are confluent and universal for BSP algoritms. We also analyze the conditions for parallel implementation of such calculi. We have experimented the associated programming style and have observed that they are sufficiently expressive and allow the prediction of execution times.

[4]
Frédéric Loulergue. Programmation parallèle fonctionnelle en processus statiques: une approche dénotationnelle. Mémoire de DEA d'informatique, LIFO, Université d'Orléans, Septembre 1996.

Poster / Poster

[1]
Noman Javed and Frédéric Loulergue. A Metaprogrammed Bulk Synchronous Parallel Algorithmic Skeleton Library. In International Conference for High Performance Computing, Networking, Storage and Analysis (SC08), Poster, 2008.

Exposé / Talk

[1]
Frédéric Loulergue. Correct Functional Parallel Programs in a Safe Execution Environment. Talk at the National Institute of Informatics (Japan), June 2008.
The design of parallel programs and parallel programming languages is a trade-off. On one hand the programs should be efficient. But the efficiency should not come at the price of non portability and unpredictability of performances. The portability of code is needed to allow code reuse on a wide variety of architectures and to allow the existence of legacy code. The predictability of performances is needed to guarantee that the efficiency will always be achieved on any architecture. Another very important characteristic of parallel programs is the complexity of their semantics. Deadlocks and indeterminism often hinder the practical use of parallelism by a large number of users. To avoid these undesirable properties, a trade-off has to be made between the expressiveness of the language and its structure which could decrease the expressiveness. 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: deadlocks are avoided and indeterminism is limited to very specific cases in the BSPlib. BSP programs are portable across many parallel architectures. The Bulk Synchronous Parallel ML language (BSML) is based on a confluent extension of the λ-calculus. Thus it is deadlock free and deterministic. Being a high-level language, programs are easier to write, to reuse and to compose. It is even possible to certify the correctness of BSML programs with the help of the Coq proof assistant. However the correctness of these programs is ensured with respect to the programming model of BSML. BSML, as data-parallel languages, has a programming model that is a formal or informal semantics of the primitive operations it provides as viewed by the programmer. However the realization of the primitives on parallel architecture, or execution model, is quite different. Thus to guarantee the correct execution of these programs in parallel, it is necessary to verify the equivalence of the programming model and the execution model. This talk presents the Bulk Synchronous Parallel language, several formal semantics of BSML from the programming model to the semantics of an abstract parallel machine, and proof of correctness of BSML programs with the Coq proof assistant.

[2]
F Loulergue. Functional Bulk Synchronous Parallelism in ML. The University of Tokyo, July 2007.
[3]
Radia Benheddi and Frédéric Loulergue. Minimally Synchronous Parallel ML with Parallel Composition. In Seventh Symposium on Trends in Functional Programming (TFP 2006), pages 387-402. Nottingham, UK, 2006.
Parallel divide-and-conquer parallel algorithms are very common in the litterature on parallel algorithms. In order to ease their implementation in Minimally Synchronous Parallel ML (MSPML), we add a new primitive to this asynchronous parallel functional language. MSPML is based on a parallel data structure called parallel vectors and operations to manipulate them. This paper presents semantics and an implementation of MSPML with parallel composition.

[4]
Louis Gesbert and Frédéric Loulergue. Semantics of Bulk Synchronous Parallel ML with Exceptions. In Zoltén Horvéth, editor, Draft proceedings of the 18th International Symposium on Implementation and Application of Functional Languages (IFL'06), 2006.
[5]
Frédéric Loulergue. The PROPAC Project - Certified Parallel Programming. The University of Tokyo, March 2006.
The goal of this project is to produce a programming environment in which certified parallebgl programs can be written, proved and safely executed. More technically, several subgoals are studied to achieve the overall goal of the project: proofs, using the Coq proof assistant, of programs written with the functional parallel languages we developped; certification of the compilers for these languages, from source code to bytecode for parallel virtual machines and the certification of these virtual machines; proofs of imperative bulk synchronous parallel programs first written with a small dedicated language and then with an extension of C or Java; automatic performance prediction of the programs written with these languages.

[6]
Frédéric Loulergue. Functional Parallel Programming with BSML. The University of Tokyo, March 2006.
Bulk Synchronous Parallel ML (BSML) and Minimally Synchronous Parallel ML (MSPML) are two functional languages for parallel programming, based respectively on the Bulk Synchronous Parallel model and the Message Passing Machine model. The execution time can be estimated, dead-locks and indeterminism are avoided. Programs are written as usual ML programs but using a small set of additional functions. Provided functions are used to access the parameters of the parallel machine and to create and operate on a parallel data structure. This tutorial will provide an introduction to both languages and an overview of the research done.

[7]
Frédéric Loulergue and Frédéric Gava. Calcul parallèle: bicephale.univ-paris12.fr et Bulk Synchronous Parallel ML. Séminaire du LACL, February 2005.
Certains problèmes comme la simulation de phénomènes physiques ou chimiques ou la gestion de bases de données de grande taille nécessitent des performances que seules les machines parallèles peuvent offrir. En plus de ces domaines d'application, on utilise les machines parallèles en recherche opérationnelle, en extraction de connaissances, en réalité virtuelle et en vérification. Les machines parallèles servent ainsi à un sous-ensemble important de toutes les applications de l'informatique. Leur programmation demeure néanmoins plus difficile que celle des machines séquentielles et la conception de langages adaptés est un sujet de recherche actif. Cet exposé présentera : - d'une part la machine parallèle du Laboratoire d'Algorithmique, Complexité et Logique (LACL), appelée "bicephale.univ-paris12.fr" qui est de type grappe de PC et les bases de l'utilisation pratique de celle-ci ; - d'autre part le langage de programmation de haut-niveau Bulk Synchronous Parallel ML (BSML) développé au LACL et quelques exemples implémentés avec BSML et qui ont fait l'objet d'expérimentations sur la grappe de PC.

[8]
Frédéric Loulergue. Programmation de méta-ordinateur: de MSPML à DMML. Exposé au Groupe de travail "Programmation", Laboratoire Preuves, Programmes et Systèmes, Paris, March 2005.
De nombreux problèmes comme la simulation de phénomènes physiques ou la manipulation de bases de données de grandes tailles nécessitent des performances que seuls les ordinateurs massivement parallèles, voire les méta-ordinateurs, peuvent fournir.A partir d'un modèle de parallélisme structuré possèdant un modèle de prévision de performances (Bulk Synchronous Parallel ou BSP) nous avons conéu un ensemble d'opérations universelles qui permet la programmation de n'importe quel algorithme de ce modèle. Une approche opérationnelle nous a amené à définir des extensions du lambda-calcul par des primitives BSP. Une bibliothèque basée sur ces calculs, la bibliothèque BSML a été développée pour le langage fonctionnel Objective Caml. La programmation BSML s'appuie sur une structure de données parallèle polymorphe. Les programmes sont des fonctions Objective Caml usuelles mais manipulent cette structure de données parallèle à l'aide d'un petit ensemble d'opérations dédiées. BSML suit le modèle BSP et est donc garanti sans inter-blocage. La confluence des calculs garantit quant à elle le déterminisme de BSML. Un nouvel axe de recherche, présenté dans cet exposé, est d'avoir un langage pour le metacomputing, c'est-à-dire pour la programmation de grappes de machines parallèles (qui sont elles-mémes souvent des grappes de PC) que nous appelons méta-ordinateurs. Pour obtenir ce langage, appelée Departmental Metacomputing ML, nous avons combiné le langage BSML, pour la programmation de chaque noeud parallèle, et notre nouveau langage MSPML (Minimally Synchronous Parallel ML) pour la coordination de l'ensemble. MSPML diffère de BSML par l'absence de barrières de synchronisation globale.

[9]
Frédéric Loulergue. Functional programming of parallel and meta computing. Talk at the Komet Workshop, November 2004.
[10]
Frédéric Loulergue. Compositions parallèles et BSML. Seminaire du LIFO, Orléans, march 2003.
[11]
Frédéric Loulergue. Bulk Synchronous Parallel ML: Safety and Expressivity. Talk at The Tokyo Programming Seminar, November 2003.
[12]
Frédéric Loulergue. Distributed Evaluation of Functional BSP Programs. Talk at the International Workshop on High Level Parallel Programming, Orléans, march 2001.
[13]
Frédéric Loulergue. Conception de langages fonctionnels pour la programation massivement parallèle : de BSlambda à la BSMLlib. Séminaire du LACL, Crétail, october 2000.
[14]
Frédéric Loulergue. Conception de langages fonctionnels pour la programation massivement parallèle : de BSlambda à la BSMLlib. Séminaire du groupe de travail "Programmation", PPS, Paris, may 2000.
[15]
Frédéric Loulergue. Conception de langages fonctionnels pour la programation massivement parallèle. Exposé aux Journées GDR Parallélisme Répartition et Objets, Lille, december 1999.
[16]
Frédéric Loulergue. Un langages fonctionnel pur d'ordre supérieur explicitement parallèle. Exposé aux Journées GDR, Rennes, 1997.