ARTICLES / PAPERS

Revue / Journal

[1]
Hélène Coullon, Ludovic Henrio, Frédéric Loulergue, and Simon Robillard. Component-based distributed software reconfiguration: A verification-oriented survey. ACM Comput. Surv., 56(1):2:1--2:37, may 2024. [ DOI ]
Distributed software built from components has become a mainstay of service-oriented applications, which frequently undergo reconfigurations in order to adapt to changes in their operating environment or their functional requirements. Given the complexity of distributed software and the adverse effects of incorrect reconfigurations, a suitable methodology is needed to ensure the correctness of reconfigurations in component-based systems. This survey gives the reader a global perspective over existing formal techniques that pursue this goal. It distinguishes different ways in which formal methods can improve the reliability of reconfigurations, and lists techniques that contribute to solving each of these particular scientific challenges.
[2]
Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, and Julien Signoles. Sound runtime assertion checking for memory properties via program transformation. Formal Aspects of Computing, 36(1):4:1--4:46, 2024. [ DOI ]
Runtime Assertion Checking (RAC) for expressive specification languages is a non-trivial verification task, that becomes even more complex for memory-related properties of imperative languages with dynamic memory allocation. It is important to ensure the soundness of RAC verdicts, in particular when RAC reports the absence of failures for execution traces. This paper presents a formalization of a program transformation technique for RAC of memory properties for a representative language with pointers and memory operations, including dynamic allocation and deallocation. The generated program instrumentation relies on an axiomatized observation memory model, which is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.
[3]
Virginia Niculescu and Frédéric Loulergue. Transforming powerlist based divide&conquer programs for an improved execution model. Journal of Supercomputing, 76:5016--5037, 2020. [ DOI ]
Powerlists are data structures that can be successfully used for defining parallel programs based on Divide&Conquer paradigm. These parallel recursive data structures and their algebraic theories offer both a methodology to design parallel algorithms and parallel programming abstractions to ease the development of parallel applications. The paper presents a technique for speeding up the parallel recursive programs defined based on powerlists. The improvements are achieved by applying transformation rules that introduce tuple functions and prefix operators, for which a more efficient execution model is defined. Together with the execution model, a cost model is also defined in order to allow a proper evaluation. The treated examples emphasise the fact that the transformation leads to important improvements of the programs. The speeding up is achieved by reducing the number of recursive calls, and also by enable the fusion of splitting/combining operations on different data structures. In addition, enhancing the function that has to be computed to other useful functions using a tuple, could improved the cost reduction even more.
[4]
Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, and Julien Signoles. Soundness of a dataflow analysis for memory monitoring. In Ada Letters, number 2, pages 97--108, Boston, MA, USA, December 2019. ACM. [ DOI ]
An important concern addressed by runtime verification tools for C code is related to detecting memory errors. It requires to monitor some properties of memory locations (e.g. their validity and initialization) along the whole program execution. Static analysis based optimizations have been shown to significantly improve the performances of such tools by reducing the monitoring of irrelevant locations. However, soundness of the verdict of the whole tool strongly depends on the soundness of the underlying static analysis technique. This paper tackles this issue for the dataflow analysis used to optimize the E-ACSL runtime assertion checking tool. We formally define the core dataflow analysis used by E-ACSL and prove its soundness.
[5]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. MMFilter: A CHR-based solver for generation of executions under weak memory models. Comput Lang Syst Str, 53:121--142, 2018. [ DOI ]
With the wide expansion of multiprocessor architectures, the analysis and reasoning for programs under weak memory models has become an important concern. This work presents MMFilter, an original constraint solver for generating program behaviors respecting a particular memory model. It is implemented in Prolog using CHR (Constraint Handling Rules). The CHR formalism provides a convenient generic solution for specifying memory models. It benefits from the existing optimized implementations of CHR and can be easily extended to new models. We present MMFilter design, illustrate the encoding of memory model constraints in CHR and discuss the benefits and limitations of the proposed technique.
[6]
Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. Calculating Parallel Programs in Coq using List Homomorphisms. Int J Parallel Prog, 45:300--319, 2017. [ DOI ]
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.
[7]
Frédéric Loulergue. A BSPlib-style API for Bulk Synchronous Parallel ML. Scalable Computing: Practice and Experience, 18:261--274, 2017. [ DOI ]
Bulk synchronous parallelism (BSP) offers an abstract and simple model of parallelism yet allows to take realistically into account the communication costs of parallel algorithms. BSP has been used in many application domains. BSPlib and its variants are programming libraries for the C language that support the BSP style. Bulk Synchronous Parallel ML (BSML) is a library for BSP programming with the functional language OCaml. It offers parallel operations on a data structure named parallel vector. BSML provides a global view of programs, i.e. BSML programs can be seen as sequential programs working on a parallel data structure (seq of par) while a BSPlib program is written in the SPMD style and understood as a parallel composition of communicating sequential programs (par of seq). The communication styles of BSML and BSPlib are also quite different. The contribution of this paper is a BSPlib-style communication API implemented on top of BSML. It has been designed without extending BSML, but only using the imperative features of the underlying function language OCaml. Programs implemented using this API are very close to programs implemented using a BSPlib library for the C language. It therefore shows that BSML is universal for the BSP model.
[8]
Thibaut Tachon, Chong Li, Gaétan Hains, and Frédéric Loulergue. Automated generation of BSP automata. Parallel Processing Letters, 17(1), 2017. [ DOI ]
Bulk-Synchronous Parallel (BSP) is a bridging model between abstract execution and concrete parallel architectures that retains enough information to model performance scalability. In order to model BSP program executions, Hains adapted the theory of finite automata to the BSP paradigm by introducing BSP automata. In the initial description of the theory, BSP automata had to be explicitly defined as structured sets of states and transitions. The lack of a clean and efficient algorithm for generating them from regular expressions would have prevented this theory from being used in practice. To alleviate this problem we introduce in this paper an algorithm that generates a BSP automaton recognizing a BSP language defined by a BSP regular expression. The main practical use of BSP automata developed in this paper is the parallelization of finite state automata with an explicit distribution and a performance model, that enable parallel matching of regular expressions. Secondarily, BSP regular expressions provide a convenient structure for automatic code generation of imperative BSP program that is also developed in this paper.
[9]
Frédéric Dabrowski, Frédéric Loulergue, and Thomas Pinsard. A formal semantics of nested atomic sections with thread escape. Comput Lang Syst Str, 42:2--21, 2015. [ DOI ]
The multi-core trend is widening the gap between programming languages and hardware. Taking parallelism into account in the programs is necessary to improve performance. Unfortunately, current mainstream programming languages fail to provide suitable abstractions to do so. The most common pattern relies on the use of mutexes to ensure mutual exclusion between concurrent accesses to a shared memory. However, this model is error-prone and scales poorly by lack of modularity. Recent research proposes atomic sections as an alternative. The user simply delimits portions of code that should be free from interference. The responsibility for ensuring interference freedom is left either to the compiler or to the run-time system. In order to provide enough modularity, it is necessary that both atomic sections could be nested and threads could be forked inside an atomic section. In this paper we focus on the semantics of programming languages providing these features. More precisely, without being tied to a specific programming language, we consider program traces satisfying some basic well-formedness conditions. Our main contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. A formalisation of our results in the Coq proof assistant is described.
[10]
Louis Gesbert, Frédéric Gava, Frédéric Loulergue, and Frédéric Dabrowski. Bulk Synchronous Parallel ML with Exceptions. Future Gener Comp Sy, 26(3):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.
[11]
Frédéric Gava and Frédéric Loulergue. A Static Analysis for Bulk Synchronous Parallel ML to Avoid Parallel Nesting. Future Gener Comp Sy, 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.
[12]
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.
[13]
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.
[14]
Gaétan Hains, Frédéric Loulergue, and John Mullins. Concrete data structures and functional parallel programming. Theor Comput Sci, 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.
[15]
Frédéric Loulergue. Distributed Evaluation of Functional BSP Programs. Parallel Processing Letters, 11(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).
[16]
Frédéric Loulergue, Gaétan Hains, and Christian Foisy. A Calculus of Functional BSP Programs. Sci Comput Program, 37(1-3):253--277, 2000. [ DOI | ePub ]
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]
Frédéric Loulergue, Wadoud Bousdira, and Julien Tesson. Calcul de programmes parallèles avec Coq. In Nicolas Ollinger, editor, Informatique Mathématique une photographie en 2015, collection Alpha, pages 87--134. CNRS Éditions, 2015.

Numéro spécial de revue / Special Issue

[1]
Wolfgang Ahrendt, Frédéric Loulergue, and Heike Wehrheim. Introduction to the special collection from the international conference on Tests and Proofs (TAP) 2020 and 2021. 36(1):1:1--1:2, 2024. [ DOI ]
[2]
Virginia Niculescu and Frédéric Loulergue. Guest Editor's Note: High-Level Parallel Programming 2021. Int J Parallel Prog, 51:271--273, 2023. Selected extended and revised papers from the International Symposium on High Level Parallel Programming and Applications (HLPP 2021). [ DOI ]
[3]
Frédéric Loulergue. Special Issue on Practical Aspects of High-Level Parallel Programming. Scalable Computing: Practice and Experience, 18(1), 2017. Selected extended and revised papers from the International Workshop and the ACM SAC track on Practical Aspects of High-Level Parallel Programming. [ http ]
[4]
Frédéric Loulergue and A. Tiskin. Preface: Special Issue on High-Level Parallel Programming and Applications. Parallel Processing Letters, 18(1), 2008. [ DOI ]
[5]
Anne Benoit and Frédéric Loulergue. Special Issue on Practical Aspects of High-Level Parallel Programming. Scalable Computing: Practice and Experience, 8(4), 2007. Selected extended and revised papers from the Third International Workshop on Practical Aspects of High-Level Parallel Programming (PAPP 2006). [ http ]
[6]
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. [ DOI ]
[7]
Frédéric Loulergue. Special Issue on Practical Aspects of High-Level Parallel Programming. Scalable Computing: Practice and Experience, 7(3), 2006. Selected extended and revised papers from the Second International Workshop on Practical Aspects of High-Level Parallel Programming (PAPP 2005). [ http ]
[8]
Frédéric Loulergue. Special Issue on Practical Aspects of High-Level Parallel Programming. Scalable Computing: Practice and Experience, 6(4), 2005. Selected extended and revised papers from the First International Workshop on Practical Aspects of High-Level Parallel Programming (PAPP 2004). [ http ]
[9]
Gaétan Hains and Frédéric Loulergue. Preface: Special Issue on High-Level Parallel Programming and Applications. Parallel Processing Letters, 13(3), 2003. [ DOI ]

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

[1]
Jordan Ischard, Frederic Dabrowski, Jules Chouquet, and Frédéric Loulergue. A Mechanized Formalization of an FRP Language with Effects. In ACM, editor, ACM Symposium on Applied Computing (SAC), Sicily, Italy, March 2025. to appear.
[2]
Téo Bernier, Yani Ziani, Nikolai Kosmatov, and Frédéric Loulergue. Combining Deductive Verification with Shape Analysis. In 27th International Conference on Fundamental Approaches to Software Engineering (FASE), number 14573 in LNCS. Springer, 2024. [ DOI ]
Deductive verification tools can prove a large range of program properties, but often face issues on recursive data structures. Abstract interpretation tools based on separation logic and shape analysis can efficiently reason about such structures but cannot deal with so large classes of properties. This paper presents an ongoing work on combining both techniques. We show how a deductive verifier for C programs, Frama-C/WP, can benefit from a shape analysis tool, MemCAD, where structural and separation properties proved in the latter become assumptions for the former. A case study on selected functions of the tpm2-tss library using linked lists confirms the interest of the approach.
[3]
Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, and Daniel Gracia Pérez. Runtime Verification for High-Level Security Properties: Case Study on the TPM Software Stack. In Tests and Proofs (TAP), LNCS. Springer, 2024. [ DOI ]
The Trusted Platform Module (TPM) is a cryptoprocessor designed to provide hardware-based secure storage and protect integrity of modern computers. Communications with the TPM go through the TPM Software Stack (TSS), a popular implementation of which is the open-source library tpm2-tss. It is thus crucial to ensure that no leak of sensitive data may occur in the TSS during communications between the host platform and the TPM. Recent work on deductive verification of functional and safety properties for this library faced several challenges. The purpose of this case study paper is to focus on high-level security properties, and to propose an alternative validation approach for such properties on the library by using runtime verification. We describe the proposed approach, apply it to specify and verify at runtime some key security properties using the Frama-C verification platform and report on our first evaluation results.
[4]
Frédéric Loulergue and Jordan Ischard. A Framework for the Development of Verified Scalable Parallel Functional Languages. In Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), LNCS. Springer, 2024. [ DOI ]
The SyDPaCC framework supports the development of scalable parallel functional programs with the proof assistant Coq and helps the developers to write correct-by-construction programs with respect to specifications written as simple (and possibly very inefficient) functional programs. Parallel programs are built from specifications using verified program transformations offered by SyDPaCC. Leveraging Coq extraction mechanism, compilable code can be obtained and executed on shared-memory or large scale distributed memory parallel machines.
[5]
Frédéric Loulergue and Ed-Dbali Ali. Verified high performance computing: the SyDPaCC approach. In 16th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS), number 14368 in LNCS. Springer, 2023. [ DOI ]
The SyDPaCC framework for the Coq proof assistant is based on a transformational approach to develop verified efficient scalable parallel functional programs from specifications. These specifications are written as inefficient (potentially with a high computational complexity) sequential programs using some easily understandable predefined sequential function. We obtain efficient parallel programs implemented using algorithmic skeletons that are higher-order functions implemented in parallel on distributed data structures. The output programs are constructed step-by-step by applying transformation theorems. Leveraging Coq type classes, the application of transformation theorems is partly automated. The current version of the framework is presented and exemplified on the development of a parallel program for the maximum segment sum problem. This program is experimented on a parallel machine.
[6]
Olivia Proust and Frédéric Loulergue. Verified scalable parallel computing with Why3. In 21st International Conference on Software Engineering and Formal Methods (SEFM), volume 14323 of LNCS. Springer, 2023. [ DOI ]
BSML is a pure functional library for the multi-paradigm language OCaml. BSML embodies the principles of the Bulk Synchronous Parallel (BSP) model, a model of scalable parallel computing. We propose a formalization of BSML primitives with WhyML, the specification language of Why3 and specify and prove the correctness of most of the BSML standard library. Finally, we develop and verify the correctness of a small BSML application.
[7]
Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue, Daniel Gracia Pérez, and Téo Bernier. Towards Formal Verification of a TPM Software Stack. In 18th International Conference on integrated Formal Methods (iFM), LNCS. Springer, 2023. [ DOI ]
The Trusted Platform Module (TPM) is a cryptoprocessor designed to protect integrity and security of modern computers. Communications with the TPM go through the TPM Software Stack (TSS), a popular implementation of which is the open-source library tpm2-tss. Vulnerabilities in its code could allow attackers to recover sensitive information and take control of the system. This paper describes a case study on formal verification of tpm2-tss using the Frama-C verification platform. Heavily based on linked lists and complex data structures, the library code appears to be highly challenging for the verification tool. We present several issues and limitations we faced, illustrate them with examples and present solutions that allowed us to verify functional properties and the absence of runtime errors for a representative subset of functions. We describe verification results and desired tool improvements necessary to achieve a full formal verification of the target code.
[8]
Virginia Niculescu, Adrian Sterca, and Frédéric Loulergue. Reflections on the design of parallel programming frameworks. In Raian Ali, Hermann Kaindl, and Leszek A. Maciaszek, editors, Evaluation of Novel Approaches to Software Engineering, pages 154--181. Springer International Publishing, 2021. [ DOI ]
Since parallel programming is much more complex and difficult than sequential programming, it is more challenging to achieve the same software quality in a parallel context. High-level parallel programming models, if implemented as software frameworks, could increase productivity and reliability.
[9]
Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, and Julien Signoles. Verified runtime assertion checking for memory properties. In Tests and Proofs (TAP), volume 12165 of LNCS, pages 100--121. Springer, 2020. [ DOI ]
Runtime Assertion Checking (RAC) for expressive specification languages is a non-trivial verification task, that becomes even more complex for memory-related properties of imperative languages with dynamic memory allocation. It is important to ensure the soundness of RAC verdicts, in particular when RAC reports the absence of failures for execution traces. This paper presents a formalization of a program transformation technique for RAC of memory properties for a representative language with memory operations. It includes an observation memory model that is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.
[10]
Virginia Niculescu, Frédéric Loulergue, Darius Bufnea, and Adrian Sterca. Pattern-driven Design of a Multiparadigm Parallel Programming Framework. In 13th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), pages 50--61. ScitePress, 2020. [ DOI ]
Parallel programming is more complex than sequential programming. It is therefore more difficult to achieve the same software quality in a parallel context. High-level parallel programming approaches are intermediate approaches where users are offered simplified APIs. There is a trade-off between expressivity and programming productivity, while still offering good performance. By being less error-prone, high-level approaches can improve application quality. From the API user point of view, such approaches should provide ease of programming without hindering performance. From the API implementor point of view, such approaches should be portable across parallel paradigms and extensible. JPLF is a framework for the Java language based on the theory of Powerlists, which are parallel recursive data structures. It is a high-level parallel programming approach that possesses the qualities mentioned above. This paper reflects on the design of JPLF: it explains the design choices and highlights the design patterns and design principles applied to build JPLF.
[11]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Logic against ghosts: Comparison of two proof approaches for a list module. In ACM Symposium on Applied Computing (SAC), pages 2186--2195. ACM, 2019. Best Paper Award. [ DOI ]
Modern verification projects continue to offer new challenges for formal verification. One of them is the linked list module of Contiki, a popular open-source operating system for the Internet of Things. It has a rich API and uses a particular list representation that make it different from the classical linked list implementations. Being widely used in the OS, the list module is critical for reliability and security. A recent work verified the list module using ghost arrays. This article reports on a new verification effort for this module. Realized in the Frama-C/Wp tool, the new approach relies on logic lists. A logic list provides a convenient high-level view of the linked list. The specifications of all functions are now proved faster and almost all automatically, only a small number of auxiliary lemmas and a couple of assertions being proved interactively in Coq. The proposed specifications are validated by proving a few client functions manipulating lists. During the verification, a more efficient implementation for one function was found and verified. We compare the new approach with the previous effort based on ghost arrays, and discuss the benefits and drawbacks of both techniques.
[12]
Allan Blanchard, Frédéric Loulergue, and Nikolai Kosmatov. Towards Full Proof Automation in Frama-C using Auto-Active Verification. In Nasa Formal Methods, LNCS, pages 88--105. Springer, 2019. [ DOI ]
While deductive verification is increasingly used on real-life code, making it fully automatic remains difficult. The development of powerful SMT solvers has improved the situation, but some proofs still require interactive theorem provers in order to achieve full formal verification. Auto-active verification relies on additional guiding annotations (assertions, ghost code, lemma functions, etc.) and provides an important step towards a greater automation of the proof. However, the support of this methodology often remains partial and depends on the verification tool. This paper presents an experience report on a complete functional verification of several C programs from the literature and real-life code using auto-active verification with the C software analysis platform Frama-C and its deductive verification plugin . The goal is to use automatic solvers to verify properties that are classically verified with interactive provers. Based on our experience, we discuss the benefits of this methodology and the current limitations of the tool, as well as proposals of new features to overcome them.
[13]
Frédéric Loulergue and Jolan Philippe. Automatic Optimization of Python Skeletal Parallel Programs. In Algorithms and Architectures for Parallel Processing (ICA3PP), LNCS, pages 183--197, Melbourne, Australia, 2019. Springer. [ DOI ]
Skeletal parallelism is a model of parallelism where parallel constructs are provided to the programmer as usual patterns of parallel algorithms. High-level skeleton libraries often offer a global view of programs instead of the common Single Program Multiple Data view in parallel programming: A program is written as a sequential program but operates on parallel data structures. Most of the time, skeletons on a parallel data structure have counterparts on a sequential data structure: For example, the map function that applies a given function to all the elements of a sequential collection (e.g., a list) has a map skeleton counterpart that applies a sequential function to all the elements of a distributed collection. Two of the challenges a programmer faces when using a skeleton library that provides a wide variety of skeletons are: which are the skeletons to use, and how to compose them? These design decisions may have a large impact on the performance of the parallel programs. However, skeletons, especially when they do not mutate the data structure they operate on but are rather implemented as pure functions, possess algebraic properties that allow to transform compositions of skeletons into more efficient compositions of skeletons. In this paper, we present such an automatic transformation framework for the Python skeleton library PySke and evaluate it on several example applications.
[14]
Frédéric Loulergue and Jolan Philippe. New List Skeletons for the Python Skeleton Library. In Parallel and Distributed Computing, Applications and Technologies (PDCAT), pages 395--400. IEEE, 2019. [ DOI ]
Algorithmic skeletons are patterns of parallel computations. Skeletal parallel programming eases parallel programming: a program is merely a composition of such patterns. Data-parallel skeletons operate on parallel data-structures that have often sequential counterparts. In algorithmic skeleton approaches that offer a global view of programs, a parallel program has therefore a structure similar to a sequential program but operates on parallel data-structures. PySke is such an algorithmic skeleton library for Python to program shared or distributed memory parallel architectures in a simple way. This paper presents an extension to PySke: new algorithmic skeletons on parallel lists. This extension is evaluated on an application.
[15]
Jolan Philippe and Frédéric Loulergue. PySke: Algorithmic skeletons for Python. In International Conference on High Performance Computing and Simulation (HPCS), pages 40--47. IEEE, 2019.
PySke is a library of parallel algorithmic skeletons in Python designed for list and tree data structures. Such algorithmic skeletons are high-order functions implemented in parallel. An application developed with PySke is a composition of skeletons. It does not follow the Single Program Multiple Data (SPMD) paradigm but offers a global view of parallel programs. All these features make parallel programming with PySke easier. PySke offers a good balance between execution efficiency and programming productivity. In addition to the library, we present experiments performed on a high-performance multicore workstation (shared memory) and a high-performance computing cluster (distributed memory) on a set of example applications developed with PySke.
[16]
Jolan Philippe and Frédéric Loulergue. Parallel programming with Coq: Map and reduce skeletons on trees. In ACM Symposium on Applied Computing (SAC), pages 1578--1581. ACM, 2019. [ DOI ]
SyDPaCC is a set of libraries for the Coq interactive theorem prover. It allows to develop correct functional parallel programs on distributed lists based on the transformation of naive sequential programs that are considered as specifications. To offer the parallelization of functions on other data structures, the first step is to implement a parallel version of the considered data structure and to provide parallel implementations of primitive functions manipulating it. This paper presents such a first step: a binary tree extension which includes new map and reduce pure functional algorithmic skeletons for binary trees. Such algorithmic skeletons are templates of parallel algorithms, realized in a functional context as higher-order functions implemented in parallel. The use of these new primitives is illustrated on example applications.
[17]
Salwa Souaf and Frédéric Loulergue. A first step in the translation of Alloy to Coq. In International Conference on Formal Engineering Methods (ICFEM), LNCS, pages 455--469. Springer, November 2019. [ DOI ]
Alloy is both a formal language and a tool for software modeling. The language is basically first order relational logic. The analyzer is based on instance finding: it tries to refute assertions and if it succeeds it reports a counterexample. It works by translating Alloy models and instance finding into SAT problems. If no instance is found it does not mean the assertion is satisfied. Alloy relies on the small scope hypothesis: examining all small cases is likely to produce interesting counterexamples. This is very valuable when developing a system. However Alloy cannot show their absence. The CompCert compiler or the seL4 kernel have attained a high level of assurance because interactive theorem provers have been used to prove the absence of bugs. In this paper, we propose an approach where Alloy can be used as a first step, and then using a tool we develop, Alloy models can be translated to Coq code to be proved correct interactively.
[18]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C. In Nasa Formal Methods, number 10811 in LNCS, pages 37--53. Springer, 2018. [ DOI ]
Internet of Things (IoT) applications are becoming increasingly critical and require rigorous formal verification. In this paper we target Contiki, a widely used open-source OS for IoT, and present a verification case study of one of its most critical modules: that of linked lists. Its API and list representation differ from the classical linked list implementations, and are particularly challenging for deductive verification. The proposed verification technique relies on a parallel view of a list through a companion ghost array. This approach makes it possible to perform most proofs automatically using the Frama-C/WP tool, only a small number of auxiliary lemmas being proved interactively in the Coq proof assistant. We present an elegant segment-based reasoning over the companion array developed for the proof. Finally, we validate the proposed specification by proving a few functions manipulating lists.
[19]
Frédéric Loulergue, Allan Blanchard, and Nikolai Kosmatov. Ghosts for lists: from axiomatic to executable specifications. In Tests and Proofs (TAP), volume 10889 of LNCS, pages 177--184. Springer, 2018. [ DOI ]
Internet of Things (IoT) applications are becoming increasingly critical and require formal verification. Our recent work presented formal verification of the linked list module of Contiki, an OS for IoT. It relies on a parallel view of a linked list via a companion ghost array and uses an inductive predicate to link both views. A few interactively proved lemmas allow for an automatic proof of other specifications, expressed in the ACSL specification language and proved with the Frama-C/WP tool. In a broader verification context, especially as long as the whole system is not yet formally verified, it would be very useful to use runtime verification, in particular, to test client modules that use the list module. It is not possible with the current specifications, which include an inductive predicate and axiomatically defined functions. In this early-idea paper we show how to define a provably equivalent non-inductive predicate and a provably equivalent non-axiomatic function that belong to the executable subset of ACSL and can be transformed into executable C code. Finally, we propose an extension of Frama-C to handle both axiomatic specifications for deductive verification and executable specifications for runtime verification.
[20]
Frédéric Loulergue and Christopher D. Whitney. Verified programs for frequent itemset mining. In 15th IEEE International Conference on Advanced and Trusted Computing (ATC 2018), pages 1516--1523, Guangzhou, China, 2018. IEEE. [ DOI ]
Frequent itemset mining is one pillar of machine learning and is very important for many data mining applications. There are many different algorithms for frequent itemset mining, but to our knowledge no implementation has been proven correct using computer aided verification. Hu et al. derived on paper an efficient algorithm for this problem, starting from an inefficient functional program and by using program calculation derived an efficient version. Based on their work, we propose a formally verified functional implementation for frequent itemset mining developed with the Coq proof assistant. All the proposed programs are evaluated on classical datasets and are compared to a non verified Java implementation of the Apriori algorithm.
[21]
Salwa Souaf, Pascal Berthomé, and Frédéric Loulergue. A Cloud Brokerage Solution: Formal Methods Meet Security in Cloud Federations. In International Conference on High Performance Computing Simulation (HPCS), pages 691--699. IEEE, 2018. [ DOI ]
Cloud Computing has known in the past few years a fast development, leading to a spike in the number of companies competing on providing the best Cloud services. This makes it harder for potential Cloud customers to chose the adequate provider. Despite its wide adoption, many are still hesitant due to the security issues Cloud Computing poses. In this paper, we propose a brokerage solution that formalizes security properties under the form of inter-VM relations, and gives the possibility of setting these security requirements to its customers from the first steps. This solution uses formal methods and the finite model finder KodKod to verify the consistency of the customer's requirements, and to find a placement for his deployment model.
[22]
Julien Tesson and Frédéric Loulergue. Interactive bulk synchronous parallel functional programming in a browser. In 15th IEEE International Conference on Advanced and Trusted Computing (ATC 2018), pages 1593--1598, Guangzhou, China, 2018. IEEE. [ DOI ]
This paper presents the design and implementation of a sequential simulator for the parallel functional language BSML based on the parallel computation model Bulk Synchronous Parallelism (BSP). This simulator is implemented in sequential, runs in any browser, and provides a graphical representation of the parallel executions. Due to the pure functional nature of BSML, the results obtained by this simulator are the same than the results that could be obtained by executing the program in parallel
[23]
Arvid Jakobsson, Frédéric Dabrowski, Wadoud Bousdira, Frédéric Loulergue, and Gaétan Hains. Replicated Synchronization for Imperative BSP Programs. In International Conference on Computational Science (ICCS), Procedia Computer Science, pages 535--544, Zurich, Switzerland, 2017. Elsevier. [ DOI ]
The BSP model (Bulk Synchronous Parallel) simplifies the construction and evaluation of parallel algorithms, with its simplified synchronization structure and cost model. Nevertheless, imperative BSP programs can suffer from synchronization errors. Programs with textually aligned barriers are free from such errors, and this structure eases program comprehension. We propose a simplified formalization of barrier inference as data flow analysis, which verifies statically whether an imperative BSP program has replicated synchronization, which is a sufficient condition for textual barrier alignment.
[24]
Frédéric Loulergue. A verified accumulate algorithmic skeleton. In Fifth International Symposium on Computing and Networking (CANDAR), pages 420--426, Aomori, Japan, November 19-22 2017. IEEE. [ DOI ]
This paper presents an extension of a library for the Coq interactive theorem prover that enables the development of correct functional parallel programs based on sequential program transformation and automatic parallelization using an algorithmic skeleton named accumulate. Such an algorithmic skeleton is a pattern of a parallel algorithm that is provided as a high-order function implemented in parallel. The use of this framework is illustrated with the bracket matching problem, including experiments on a parallel machine.
[25]
Frédéric Loulergue. Imperative BSPlib-style Communications in Bulk Synchronous Parallel ML. In International Conference on Computational Science (ICCS), Procedia Computer Science, pages 2368--2372, Zurich, Switzerland, 2017. Elsevier. [ DOI ]
Bulk synchronous parallelism (BSP) offers an abstract and simple model of parallelism yet allows to take realistically into account the communication costs of parallel algorithms. BSP has been used in many application domains. BSPlib and its variants are programming libraries for the C language that support the BSP style. Bulk Synchronous Parallel ML (BSML) is a library for BSP programming with the functional language OCaml. It is based on an extension of the lambda-calculus by parallel operations on a data structure named parallel vector. BSML offers a global view of programs, i.e. BSML programs can be seen as sequential programs working on a parallel data structure (seq of par) while a BSPlib program is written in the SPMD style and understood as a parallel composition of communicating sequential programs (par of seq). The communication styles of BSML and BSPlib are also quite different.
[26]
Frédéric Loulergue. Implementing Algorithmic Skeletons with Bulk Synchronous Parallel ML. In Parallel and Distributed Computing, Applications and Technologies (PDCAT), pages 461--468. IEEE, 2017. [ DOI ]
Skeletal parallelism offers a good trade-off between programming productivity and execution efficiency. In this style of parallelism, an application is a composition of algorithmic skeletons. An algorithmic skeleton captures a pattern of parallel algorithm on a distributed data structure, and is also often associated with a sequential algorithm on a sequential data structure that is the counterpart of the parallel data structure. The algorithmic skeleton approach has been inspired by functional programming. It is therefore very natural to embed algorithmic skeletons in a functional programming language. In this paper we present a new algorithmic skeleton library for the statically typed functional language OCaml, and illustrate its use on some applications. This functional skeletal parallel programming library is implemented using the Bulk Synchronous Parallel ML parallel programming library for OCaml.
[27]
Virginia Niculescu, Frédéric Loulergue, Darius Bufnea, and Adrian Sterca. A Java Framework for High Level Parallel Programming using Powerlists. In Parallel and Distributed Computing, Applications and Technologies (PDCAT), pages 255--262. IEEE, 2017. [ DOI ]
Parallel programs based on the Divide&Conquer paradigm could be successfully defined in a simple way using powerlists. These parallel recursive data structures and their algebraic theories offer both a methodology to design parallel algorithms and parallel programming abstractions to ease the development of parallel applications. The paper presents how programs based on powerlists can be implemented in Java using the framework we developed. The design of this framework is based on powerlists theory, but in the same time follows the object-oriented design principles that provide flexibility and maintainability. Examples are given and performance experiments are conducted. The results emphasise the utility and the efficiency of the framework.
[28]
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, and Frédéric Loulergue. conc2seq: A Frama-C plugin for verification of parallel compositions of C programs. In 16th IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM), pages 67--72, Raleigh, NC, USA, 2016. IEEE. [ DOI ]
Frama-C is an extensible modular framework for analysis of C programs that offers different analyzers in the form of collaborating plugins. Currently, Frama-C does not support the proof of functional properties of concurrent code. We present conc2seq, a new code transformation based tool realized as a Frama-C plugin and dedicated to the verification of concurrent C programs. Assuming the program under verification respects an interleaving semantics, conc2seq transforms the original concurrent C program into a sequential one in which concurrency is simulated by interleavings. User specifications are automatically reintegrated into the new code without manual intervention. The goal of the proposed code transformation technique is to allow the user to reason about a concurrent program through the interleaving semantics using existing Frama-C analyzers.
[29]
Frédéric Dabrowski, Frédéric Loulergue, and Thomas Pinsard. Nested atomic sections with thread escape: Compilation to threads and locks. In ACM Symposium on Applied Computing (SAC), pages 2099--2106, Salamanca, Spain, 2015. ACM. [ DOI ]
For the sake of modularity, programming languages with atomic sections should offer nesting and inner parallelism in such sections. The possible escape of a thread created inside a section makes these languages also more expressive. In this paper we address the compilation of such a language towards a language with threads and locks. The design decisions of this compilation pass and of the target language were made with respect to the ultimate goal of a mechanised proof of semantic preservation.
[30]
Asma Guesmi, Patrice Clemente, Frédéric Loulergue, and Pascal Berthomé. Cloud resources placement based on functional and non-functional requirements. In International Conference on Security and Cryptography (SECRYPT), pages 335--324. ScitePress, 2015. [ DOI ]
It is difficult for customers to select the adequate cloud providers which fit their needs, as the number of cloud offerings increases rapidly. Many works thus focus on the design of cloud brokers. Unfortunately, most of them do not consider precise security requirements of customers. In this paper, we propose a methodology defined to place services in a multi-provider cloud environment, based on functional and non-functional requirements, including security requirements. To eliminate inner conflicts within customers requirements, and to match the cloud providers offers with these customers requirements, we use a formal analysis tool: Alloy. The broker uses a matching algorithm to place the required services in the adequate cloud providers, in a way that fulfills all customer requirements. We finally present a prototype implementation of the proposed broker.
[31]
Mohamad Al Hajj Hassan, Mostafa Bamha, and Frédéric Loulergue. Handling Data-skew Effects in Join Operations using MapReduce. In International Conference on Computational Science (ICCS), pages 145--158, Cairns, Australia, 2014. Elsevier. [ DOI ]
For over a decade, MapReduce has become a prominent programming model to handle vast amounts of raw data in large scale systems. This model ensures scalability, reliability and availability aspects with reasonable query processing time. However these large scale systems still face some challenges: data skew, task imbalance, high disk I/O and redistribution costs can have disastrous effects on performance. In this paper, we introduce MRFA-Join algorithm: a new frequency adaptive algorithm based on MapReduce programming model and a randomised key redistribution approach for join processing of large-scale datasets. A cost analysis of this algorithm shows that our approach is insensitive to data skew and ensures perfect balancing properties during all stages of join computation. These performances have been confirmed by a series of experimentations.
[32]
Frédéric Dabrowski, Frédéric Loulergue, and Thomas Pinsard. Nested Atomic Sections with Thread Escape: A Formal Definition. In ACM Symposium on Applied Computing (SAC), pages 1585--1592, Gyeongju, Korea, 2014. ACM. [ DOI | The paper ]
We consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. A formalisation of our results in the Coq proof assistant is also available.
[33]
Kento Emoto, Frédéric Loulergue, and Julien Tesson. A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction. In Interactive Theorem Proving (ITP), number 8558 in LNCS, pages 258--274, Wien, Austria, 2014. Springer. [ DOI ]
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.
[34]
Joeffrey Légaux, Sylvain Jubertie, and Frédéric Loulergue. Development Effort and Performance Trade-off in High-Level Parallel Programming. In International Conference on High Performance Computing and Simulation (HPCS), pages 162--169, Bologna, Italy, 2014. IEEE. [ DOI ]
Research on high-level parallel programming approaches systematically evaluate the performance of applications written using these approaches and informally argue that high-level parallel programming languages or libraries increase the productivity of programmers. In this paper we present a methodology that allows to evaluate the trade-off between programming effort and performance of applications developed using different programming models. We apply this methodology on some implementations of a function solving the all nearest smaller values problem. The high-level implementation is based on a new version of the BSP homomorphism algorithmic skeleton.
[35]
Frédéric Loulergue, Virginia Niculescu, and Julien Tesson. Implementing powerlists with Bulk Synchronous Parallel ML. In Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pages 325--332, Timisoara, Romania, 2014. IEEE. [ DOI ]
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.
[36]
Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Légaux, and Zhenjiang Hu. Formal Derivation and Extraction of a Parallel Program for the All Nearest Smaller Values Problem. In ACM Symposium on Applied Computing (SAC), pages 1577--1584, Gyeongju, Korea, 2014. ACM. [ DOI | The paper ]
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.
[37]
Frédéric Dabrowski, Frédéric Loulergue, and Thomas Pinsard. Nested Atomic Sections with Thread Escape: An Operational Semantics. In Parallel and Distributed Computing, Applications and Technologies (PDCAT), pages 29--35, Taiwan, 2013. IEEE. [ DOI ]
We consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our contribution is a formal operational semantics of this language that satifies a specification on execution traces designed in a companion paper.
[38]
Joeffrey Légaux, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, and Julien Tesson. Programming with BSP Homomorphisms. In Euro-Par Parallel Processing, number 8097 in LNCS, pages 446--457, Aachen, Germany, 2013. Springer. [ DOI ]
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.
[39]
Joeffrey Légaux, Frédéric Loulergue, and Sylvain Jubertie. Managing Arbitrary Distributions of Arrays in Orléans Skeleton Library. In International Conference on High Performance Computing and Simulation (HPCS), pages 437--444, Helsinki, Finland, 2013. IEEE. [ DOI ]
Structured parallel models such as algorithmic skeletons offer a global view of the parallel program in contrast with the fragmented view of the SPMD style. This makes program easier to write and to read for users, and offer additional opportunities for optimisation done by the libraries, compilers and/or run-time systems. Algorithmic skeletons are or can be seen as patterns or higher-order functions implemented in parallel, often manipulating distributed data structures. Orléans Skeleton Library (OSL) is a library of parallel algorithmic skeletons, written in C++ on top of MPI, which uses meta-programming techniques for optimisation. Often such libraries have no or limited support for arbitrary distributions of the data structures. In this paper we detail the new OSL skeletons used to manage arbitrary distributions of distributed arrays. We present a parallel regular sampling sort application as an example of application that requires such skeletons.
[40]
Joeffrey Légaux, Frédéric Loulergue, and Sylvain Jubertie. OSL: an algorithmic skeleton library with exceptions. In International Conference on Computational Science (ICCS), pages 260--269, Barcelona, Spain, 2013. Elsevier. [ DOI ]
Exception handling is a traditional and natural mechanism to manage errors and events that disrupt the normal flow of program instructions. In most concurrent or parallel systems, exception handling is done locally or sequentially, and cannot guarantee the global coherence of the system after an exception is caught. Working with a structured parallel model is an advantage in this respect. Algorithmic skeletons, that are patterns of parallel algorithms on distributed data structures, offer such a structured model. However very few algorithmic skeleton libraries provide a specific parallel exception mechanism, and no C++-based library. In this paper we propose the design of an exception mechanism for the C++ Orléans Skeleton Library that ensures the global coherence of the system after exceptions are caught. We explain our design choices, experiment on the performance penalty of its use, and we illustrate how to purposefully use this mechanism to extract the results in the course of some algorithms.
[41]
Frédéric Loulergue, Virginia Niculescu, and Simon Robillard. Powerlists in Coq: Programming and Reasoning. In First International Symposium on Computing and Networking (CANDAR), pages 57--65, Matsuyama, Japan, 2013. IEEE Computer Society. [ DOI ]
For parallel programs, correctness by construction is an essential feature since debugging is almost impossible. Building correct programs by construction is not a simple task, and usually the methodologies used for this purpose are rather theoretical and based on a pen-and-paper style. A better approach could be based on tools and theories that allow a user to develop an efficient parallel application by easily implementing simple programs satisfying conditions, ideally automatically proved. Powerlists theory and its variants represent a good theoretical base for such an approach, and the Coq proof assistant is a tool that could be used for automatic proofs. The goal of this paper is to model the powerlist theory in Coq, and to use this modelling to program and reason about parallel programs in Coq. This represents the first step in building a framework to ease the development of correct and verifiable parallel programs.
[42]
Wadoud Bousdira, Frédéric Loulergue, and Julien Tesson. A Verified Library of Algorithmic Skeletons on Evenly Distributed Arrays. In Algorithms and Architectures for Parallel Processing (ICA3PP), number 7439 in LNCS, pages 218--232, Fukuoka, Japan, 2012. Springer. [ 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.
[43]
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), number 7204 in LNCS, pages 91--100, Torun, Poland, 2012. Springer. [ 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.
[44]
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), pages 91--97, Madrid, Spain, 2012. IEEE. [ DOI ]
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.
[45]
Joeffrey Légaux, Sylvain Jubertie, and Frédéric Loulergue. Experiments in Parallel Matrix Multiplication on Multi-Core Systems. In Algorithms and Architectures for Parallel Processing (ICA3PP), number 7439 in LNCS, pages 362--376, Fukuoka, Japan, 2012. Springer. [ DOI ]
[46]
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, Istanbul, Turkey, 2011. IEEE. [ 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.
[47]
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, Kazan, Russia, 2011. Springer. [ 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.
[48]
Julien Tesson and Frédéric Loulergue. A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation. In International Conference on Computational Science (ICCS), pages 36--45, Singapore, 2011. Elsevier. [ 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.
[49]
Louis Gesbert, Zhenjiang Hu, Frédéric Loulergue, Kiminori Matsuzaki, and Julien Tesson. Systematic Development of Correct Bulk Synchronous Parallel Programs. In 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.
[50]
Julien Tesson, H. Hashimoto, Zhenjiang Hu, Frédéric Loulergue, and Masato Takeichi. Program Calculation in Coq. In Algebraic Methodology And Software Technology (AMAST), 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.
[51]
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.
[52]
Louis Gesbert and Frédéric Loulergue. Semantics of an Exception Mechanism for Bulk Synchronous Parallel ML. In 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.
[53]
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.
[54]
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.
[55]
Frédéric Loulergue, Frédéric Gava, and David Billiet. Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction. In International Conference on Computational Science (ICCS), volume 3515 of LNCS, 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.
[56]
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.
[57]
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.
[58]
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.
[59]
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.
[60]
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.
[61]
Frédéric Loulergue. Communication Primitives for Minimally Synchronous Parallel ML. In International Conference on Computational Science (ICCS), 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.
[62]
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).
[63]
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.
[64]
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.
[65]
Frédéric Gava and Frédéric Loulergue. A Parallel Virtual Machine for Bulk Synchronous Parallel ML. In International Conference on Computational Science (ICCS), 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.
[66]
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.
[67]
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.
[68]
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.
[69]
Frédéric Loulergue. Parallel Superposition for Bulk Synchronous Parallel ML. In International Conference on Computational Science (ICCS), number 2659 in LNCS, 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.
[70]
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.
[71]
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.
[72]
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. [ ePub ]
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.
[73]
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. [ ePub ]
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.
[74]
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 | ePub ]
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.
[75]
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. [ ePub ]
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.

Article de tutoriel / Tutorial Paper

[1]
Victor Allombert, Mathias Bourgoin, and Frédéric Loulergue. Parallel programming with OCaml: A tutorial. In International Conference on High Performance Computing and Simulation (HPCS), pages 3--11, Orléans, France, 2018. IEEE. [ DOI ]
OCaml is a multi-paradigm (functional, imperative, object-oriented) high level sequential language. Types are statically inferred by the compiler and the type system is expressive and strong. These features make OCaml a very productive language for developing efficient and safe programs. In this tutorial we present three frameworks for using OCaml to program scalable parallel architectures: BSML, Multi-ML and Spoc.
[2]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. A lesson on verification of IoT software with Frama-C. In International Conference on High Performance Computing and Simulation (HPCS), pages 21--30, Orléans, France, 2018. IEEE. [ DOI ]
This paper is a tutorial introduction to Frama-C, a framework for the analysis and verification of sequential C programs, and in particular its EVA, WP, and E-ACSL plugins. The examples are drawn from Contiki, a lightweight operating system for the Internet of Things.

Tutoriel / Tutorial

[1]
Frédéric Loulergue. Collaborative analysis and verification of C programs with Frama-C. In 38th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2023. [ http ]
While ensuring the correctness of an implementation based on a formal functional specification provides the strongest guarantee, it can be prohibitively expensive to achieve. In practice, a combination of formal methods is commonly employed to attain an appropriate level of assurance. This includes static analyses to ensure the absence of runtime errors, deductive verification for functional correctness, and dynamic verification for components that cannot be proven through deductive verification. Frama-C is a source code analysis platform designed for the verification of large-scale programs written in ISO C source code. It offers comprehensive support for the integration of formal methods, offering users a set of plug-ins that facilitate static and dynamic analysis of safety-critical and security-critical software. Furthermore, the collaborative verification capabilities are achieved through the integration of these plug-ins on a shared kernel and their adherence to a standardized specification language known as ACSL (ANSI/ISO C Specification Language). This tutorial is an introduction, including hands-on sessions, to the analysis and verification of C programs using Frama-C. The main plug-ins of Frama-C are presented, as well as their combination in a verification project. We illustrate these plug-ins on several examples taken from Contiki, a lightweight operating system for the Internet of Things.
[2]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Towards reliable things: Formal verification of IoT software with Frama-C. 29th IEEE International Symposium on Software Reliability Engineering (ISSRE), 2018.
Abstract Among distributed systems, connected devices and services, also referred to as the Internet of Things (IoT), have proliferated very quickly in the past years. There are now billions of interconnected devices, and this number is growing. It is anticipated that by 2021, about 46 billions of devices will be in use. Some of these devices are in service in safety and security critical domains, and even in domains that are not necessarily critical, privacy issues may arise with devices collecting and transmitting a lot of personal information. Formal methods have been used successfully for years in highly critical domains, now they can help to bring security into the IoT field. In practice it is common to rely on a combination of formal methods to achieve an appropriate degree of guarantee: static analyses to guarantee the absence of runtime errors, deductive verification of functional correctness, dynamic verification for parts that cannot be proved using deductive verification. This tutorial is focused on Frama-C, which is a source code analysis platform that aims at conducting verification of industrial-size programs written in ISO C99 source code. Frama-C fully supports the combination of formal methods approach, by providing to its users with a collection of plug-ins that perform static and dynamic analysis for safety and security critical software. Moreover collaborative verification across cooperating plugins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language ACSL. Recently Frama-C has been applied to the verification of software in the context of the Internet of Things.
[3]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Secure your things: Secure development of IoT software with Frama-C. In IEEE Cybersecurity Development Conference (SecDev), pages 126--127. IEEE, 2018. [ DOI ]
Among distributed systems, connected devices and services, also referred to as the Internet of Things (IoT), have proliferated very quickly in the past years. There are now billions of interconnected devices, and this number is growing. It is anticipated that by 2021, about 46 billions of devices will be in use. Some of these devices are in service in security critical domains, and even in domains that are not necessarily critical, privacy issues may arise with devices collecting and transmitting a lot of personal information. Moreover insufficiently secured devices may be used for example for massive distributed denial of service attacks. This raises important security challenges. Formal methods have been used successfully for years in highly critical domains, now they can help to bring security into the IoT field. While the correctness of an implementation with respect to a formal functional specification provides the strongest form of guarantee, it can be very costly to achieve. In practice it is therefore more common to rely on a combination of formal methods to achieve an appropriate degree of guarantee: static analyses to guarantee the absence of runtime errors, deductive verification of functional correctness, dynamic verification for parts that cannot be proved using deductive verification. Frama-C is a source code analysis platform that aims at conducting verification of industrial-size programs written in ISO C99 source code. Frama-C fully supports the combination of formal methods approach, by providing to its users with a collection of plug-ins that perform static and dynamic analysis for safety and security critical software. Moreover collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language: ACSL . Recently Frama-C has been applied to the verification of software in the context of the Internet of Things, more specifically the verification of modules of Contiki, an open source operating system for the IoT.
[4]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Towards secure things, or how to verify IoT software with Frama-C. Zooming Innovation in Consumer Electronics International Conference (ZINC), 2018.
It is commonly said the "S" in Internet of Things (IoT) stands for "Security": when it is not absent, it is at least unnoticeable. However, security in IoT becomes an important concern since in both the industry and everyday life, it is gaining wider and wider adoption. Thus, IoT is now targeting more critical domains, and making domains that were not critical, until now, collect and transmit a lot of personal data. For years, this kind of challenges have been successfully addressed in highly critical domains using formal methods. Now, formal methods can help to bring security in the IoT field. Frama-C is a source code analysis platform used to conduct verification of industrial-size programs written in ISO C99. It provides a collection of plug-ins that perform static and dynamic analysis for safety and security critical software. These plug-ins can collaborate to the verification task thanks to their integration on top of a shared kernel and their compliance to ACSL, a specification language for C. Participants will learn how to use different Frama-C analyzers and how to combine their results. During the tutorial, several examples and use-cases will give them a clear practical vision of possible usages of the underlying static and dynamic analyses in their everyday work. The presented code fragments are part of Contiki, a realworld lightweight operating system for the IoT. Each part consists of a presentation using slides and live demonstration, and a session of exercises. The attendees will be provided a virtual machine image for VirtualBox containing all the tools ready to use, to work on the exercises. We will also provide additional exercises and we will be available during the conference (and after) to help the attendees who may want to go beyond the tutorial material.
[5]
Frédéric Loulergue. Systematic Development of Programs for Scalable Computing Using Coq (tutorial). In International Conference on High Performance Computing and Simulation (HPCS), Genoa, Italy, 2017. IEEE. [ DOI ]
The SyDPaCC system is a set of libraries for the pr oof assistant Coq that allows to write naive (i.e. inef fi cient) functional programs then to transform them into ef fi cient versions that could be automatically parallelized within the framework before being extracted from Coq to code in the functional language OCaml plus calls to the parallel functional programming library Bulk Synchronous Parallel ML. These goals of the tutorial are to provide an introduction to the development of correct-by-construction parallel programs, and to able the attendees to develop functio nal parallel programs using the SYDPACC system and the Coq proof assistant.
[6]
Frédéric Loulergue. Development of correct-by-construction functional parallel programs (tutorial). In ACM Symposium on Applied Computing (SAC). ACM, 2016. [ http ]
The SyDPaCC system is a set of libraries for the pr oof assistant Coq that allows to write naive (i.e. inef fi cient) functional programs then to transform them into ef fi cient versions that could be automatically parallelized within the framework before being extracted from Coq to code in the functional language OCaml plus calls to the parallel functional programming library Bulk Synchronous Parallel ML. These goals of the tutorial are to provide an introduction to the development of correct-by-construction parallel programs, and to able the attendees to develop functio nal parallel programs using the SYDPACC system and the Coq proof assistant.
[7]
Frédéric Loulergue and Julien Tesson. Certified Parallel Program Calculation in Coq: A Tutorial. In International Conference on High Performance Computing and Simulation (HPCS). IEEE, 2014. [ DOI ]
With the current generalization of parallel architectures and increasing requirement of parallel computation arises the concern of applying formal methods, which allow specifications of parallel and distributed programs to be precisely stated and the conformance of an implementation to be verified using mathematical techniques. However, the complexity of parallel programs, compared to sequential ones, makes them more error-prone and difficult to verify. This calls for a strongly structured form of parallelism which should not only be equipped with an abstraction or model that conceals much of the complexity of parallel computation, but also provide a systematic way of developing such parallelism from specifications for practically nontrivial examples. Transformational programming is a methodology that offers some scope for making the construction of efficient programs more mathematical. Program calculation is a kind of program transformation based on the theory of constructive algorithmics. An efficient program is derived step-by-step through a sequence of transformations that preserve the meaning and hence the correctness. With suitable data-structures, program calculation can be used for writing parallel programs. However, once an efficient (and correct with respect to the initial specification) formulation of the program is obtained through transformations, the program is then implemented using a parallel library of algorithmic skeletons most of the time written in C++ with calls to a communication library such as MPI. There is no formal correspondence between the efficient program obtained by transformation and the C++ skeletal program. Moreover the transformation itself is usually a pen-and-paper process that could contain errors. The SyDPaCC system is a set of libraries for the Coq proof assistant that allows to write naive functional programs then to transform them into efficient versions that could be automatically parallelised within the framework before being extracted from Coq to real code in the functional language OCaml plus calls to the parallel functional programming library Bulk Synchronous Parallel ML The tutorial is an introduction to the Coq proof assistant and the SyDPaCC system for the systematic development of correct and verified parallel programs.

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

[1]
Frédéric Loulergue and Julien Tesson. Verified parallel programming in Coq with Bulk Synchronous Parallel homomorphisms. In High Level Parallel Programming and Applications (HLPP), Pisa, Italy, 2024.
In this paper, we use the Coq interactive theorem prover to develop a formally verified heat diffusion simulation. To do so, we follow a transformational approach: from a specification using some easily understandable predefined sequential function we obtain an efficient parallel program based on the BH algorithmic skeleton, that is a higher-order function implemented in parallel on a distributed data structure. The obtained program is experimented on a parallel machine.
[2]
Virginia Niculescu and Frédéric Loulergue. Transforming powerlist based divide&conquer programs for an improved execution model. In High Level Parallel Programming and Applications (HLPP), Orléans, France, 2018.
Divide&Conquer (DC) represents an important design pattern for parallel programs. Powerlists are data structures that could be successfully used for defining parallel programs based on this paradigm. These parallel recursive data structures and their algebraic theories offer both a methodology to design parallel algorithms and parallel programming abstractions to ease the development of parallel applications. The paper presents an improvement of the parallel recursive programs defined based on powerlists. The improvements is achieved by applying transformation rules that introduce tuple functions and prefix operators, for which a more efficient execution model is defined. Together with the execution model, a cost model is also defined in order to allow a proper evaluation. The treated examples emphasize the fact that the transformation leads to important improvements of the programs, by reducing their theoretical time-complexities, and the number of recursive calls, and also by allowing splitting and combining of different data structures to be packed together. Also, enhancing the function that has to be computed to other useful functions using a tuple, could improved the cost reduction even more.
[3]
Thibaut Tachon, Gaétan Hains, Frédéric Loulergue, and Chong Li. Automated generation of BSP automata. In High Level Parallel Programming and Applications (HLPP), Münster, Germany, 2016.
Bulk-Synchronous Parallel (BSP) is a bridging model between abstract execution and concrete parallel architecture. In order to model BSP program executions Hains adapted the finite automata theory to the BSP paradigm by introducing BSP automata theory. Benefit provided by BSP automata is twofold: modeling BSP program control and parallelizing finite state automata. The lack of generation algorithm of BSP automata and the illusory lack of application of this theory has been preventing this theory from being used. We propose in this paper an algorithm that generates a BSP automaton recognizing a defined BSP language. In order to demonstrate the usefulness of BSP automata and help to design its use, two applications of the BSP automata theory are provided. The parallel recognition of an expression and debugging of a BSP program.
[4]
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.

Atelier international / International Workshop

[1]
Farid Arfi, Hélène Coullon, Frédéric Loulergue, Jolan Philippe, and Simon Robillard. A Maude formalization of the distributed reconfiguration language Concerto-D. In 17th Interaction and Concurrency Experience (ICE), Electronic Proceedings in Theoretical Computer Science, 2024. [ DOI ]
[2]
Frédéric Loulergue and Jolan Philippe. Towards verified scalable parallel computing with Coq and Spark. In Proceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP), pages 11--17, New York, NY, USA, 2023. ACM. [ DOI ]
SyDPaCC (Systematic Development of programs for Parallel and Cloud Computing) is a framework for the Coq interactive theorem prover. It allows to systematically develop correct parallel programs from specifications via verified and automated program transformations. The obtained programs are scalable, i.e. able to run on numerous processors. SyDPaCC produces programs written in the multi-paradigm and functional programming language OCaml with calls to the BSML (Bulk Synchronous parallel ML) parallel programming library. In this paper we present ongoing work towards an extension of SyDPaCC to be able to produce Scala programs using Apache Spark for parallel processing.
[3]
Salwa Souaf and Frédéric Loulergue. Teaching code analysis and verification using Frama-C. In 1st International Workshop on Applicable Formal Methods (appFM), Beijing, China, November 2021. Electronic Proceedings in Theoretical Computer Science. [ DOI ]
Formal methods provide systematic and rigorous techniques for software development. We strongly believe that they must be taught in computer science curricula. In this paper we present the pedagogic rationale and the concrete implementation of two courses on the use of formal methods, sharing some material. These courses promote the usage of formal verification to ensure safety and security of software, exemplified in the domain of the Internet of Things.
[4]
Allan Blanchard, Frédéric Loulergue, and Nikolai Kosmatov. From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation. In Alexei Lisitsa, Andrei P. Nemytykh, and Maurizio Proietti, editors, Proceedings Fifth International Workshop on Verification and Program Transformation, Uppsala, Sweden, 29th April 2017, volume 253 of Electronic Proceedings in Theoretical Computer Science, pages 109--123. Open Publishing Association, 2017. [ DOI ]
Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed conc2seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program transformation principle behind conc2seq, and present an effort towards the full mechanization of both the for- malization and proofs with the proof assistant Coq.
[5]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. A CHR-Based Solver for Weak Memory Behaviors. In 7th Workshop on Constraint Solvers in Testing, Verification, and Analysis (CSTVA), pages 15--22. CEUR Workshop Proceedings, 2016. [ .pdf ]
With the wide expansion of multiprocessor architectures, the analysis and reasoning for programs under weak memory models has become an important concern. This work presents an original constraint solver for detecting program behaviors respecting a particular memory model. It is implemented in Prolog using CHR (Constraint Handling Rules). The CHR formalism provides a convenient generic solution for specifying memory models, that benefits from the existing optimized implementations of CHR and can be easily extended to new models. We briefly present the solver design, illustrate the encoding of memory model constraints in CHR and discuss the benefits and limitations of the proposal.
[6]
Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, and Frédéric Loulergue. A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C. In International Workshop on Formal Methods for Industrial Critical Systems (FMICS), LNCS, pages 15--30, Oslo, Norway, June 2015. Springer. [ DOI ]
Cloud hypervisors are critical software whose formal verification can increase our confidence in the reliability and security of the cloud. This work presents a case study on formal verification of the virtual memory system of the cloud hypervisor Anaxagoros, a microkernel designed for resource isolation and protection. The code under verification is specified and proven in the Frama-C software verification framework, mostly using automatic theorem proving. The remaining properties are interactively proven with the Coq proof assistant. We describe in detail selected aspects of the case study, including parallel execution and counting references to pages, and discuss some lessons learned, benefits and limitations of our approach.
[7]
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.
[8]
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.
[9]
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.
[10]
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.
[11]
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.
[12]
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.
[13]
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.
[14]
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.
[15]
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.

Colloque national / National Conference

[1]
Jérémy Damour, Allan Blanchard, Loïc Correnson, and Frédéric Loulergue. Formalisation d'une analyse de région pour Frama-C/WP. In Journées Francophones des Langages Applicatifs (JFLA), 2025.
La preuve déductive en logique de Hoare de programmes avec des pointeurs nécessite une modélisation logique de la mémoire. Pour définir un modèle mémoire performant pour la preuve, il est nécessaire de faire des compromis entre pouvoir d'expression du modèle et complexité des preuves. Dans Frama-C/WP, un outil mature et utilisé industriellement pour la preuve de programmes C, nous sommes à la recherche d'un nouveau modèle mémoire s'appuyant sur une cartographie des accès mémoires. Nous avons besoin d'une analyse d'alias enrichie par des meta-données sur la nature des accès. Une analyse modulaire est nécessaire, avec des annotations pour en adapter la précision ainsi que des fondations sémantiques solides pour en démontrer la correction. Cet article présente le cœur de calcul de notre analyse de région, son implémen- tation, sa formalisation ainsi que sa preuve de correction sémantique. C'est une analyse d'alias et de forme, incrémentale, qui peut être vue comme un système de d'inférence de type. L'analyseur, sa formalisation et la preuve de correction sémantique sont entièrement développés dans l'assistant de preuve Coq. C'est un travail en cours de développement mais qui montre d'ores et déjà le rôle et la nécessité de conditions de vérifications additionnelles, généralement éludées dans la littérature, pour en garantir la correction.
[2]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. La logique contre les fantômes: comparaison de deux approches pour la preuve d'un module de listes chaînées. In 18e journées Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), June 2019.
[3]
Wadoud Bousdira, Louis Gesbert, and Frédéric Loulergue. Syntaxe et sémantique de Revised Bulk Synchronous Parallel ML. In Sylvain Conchon and Assia 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.
[4]
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.
[5]
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.
[6]
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.
[7]
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.
[8]
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.
[9]
Olivier Ballereau, Frédéric Loulergue, and Gaétan Hains. High-level BSP Programming: BSML and BSλ. In P Trinder and Greg Michaelson, editors, Proceedings of the first Scottish Functional Programming Workshop, number RM/99/9 in Technical Report, 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.
[10]
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. [ ePub ]
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.
[11]
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. [ ePub ]
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.
[12]
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. [ ePub ]
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.

Rapport de recherche / Research Report

[1]
Allan Blanchard, Nikolai Kosmatov, and Frédéric Loulergue. Concurrent Program Verification by Code Transformation: Correctness. Research Report RR-2017-03, LIFO, Université d'Orléans, 2017. [ .pdf ]
Frama-C is a framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugin do not support concurrency. We have proposed conc2seq a plugin that handles concurrent C programs, based on program transformation to leverage the existing huge code base of plugins. In this paper we formalize and sketch the correctness of the program transformation principle behind conc2seq, and present an effort towards the full mechanization of both the formalization and proofs with the proof assistant Coq
[2]
Arvid Jakobsson, Frédéric Dabrowski, Wadoud Bousdira, Frédéric Loulergue, and Gaétan Hains. Replicated Synchronization for Imperative BSP Programs. Research Report RR-2017-04, LIFO, Université d'Orléans, 2017. [ .pdf ]
The BSP model (Bulk Synchronous Parallel) simplifies the construction and evaluation of parallel algorithms, with its simplified synchronization structure and cost model. Nevertheless, imperative BSP programs can suffer from synchronization errors. Programs with textually aligned barriers are free from such errors, and this structure eases program comprehension. We propose a simplified formalization of barrier inference as data flow analysis, which verifies statically whether an imperative BSP program has replicated synchronization, which is a sufficient condition for textual barrier alignment.
[3]
Frédéric Dabrowski, Frédéric Loulergue, and Thomas Pinsard. Nested Atomic Sections with Thread Escape: A Formal Definition. Technical Report RR-2013-05, LIFO, Université d'Orléans, 2013. [ .pdf ]
We consider a simple imperative language with fork/join parallelism and lexically scoped nested atomic sections from which threads can escape. In this context, our contribution is the precise definition of atomicity, well-synchronisation and the proof that the latter implies the strong form of the former. A formalisation of our results in the Coq proof assistant is also available.
[4]
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.
[5]
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.
[6]
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.
[7]
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.
[8]
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.
[9]
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.
[10]
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.
[11]
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.
[12]
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.
[13]
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.
[14]
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.
[15]
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.
[16]
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.
[17]
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.
[18]
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.
[19]
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]
Jolan Philippe and Frédéric Loulergue. Towards automatically optimizing PySke programs (poster). In International Conference on High Performance Computing and Simulation (HPCS), pages 1045--1046. IEEE, 2019. [ DOI ]
[2]
Jolan Philippe and Frédéric Loulergue. Towards the generation of correct Java programs (poster). In International Conference on High Performance Computing and Simulation (HPCS), pages 1055--1056, Orléans, France, 2018. IEEE. [ DOI ]
[3]
Salwa Souaf and Frédéric Loulergue. Strong security guarantees: from Alloy to Coq (poster). In International Conference on High Performance Computing and Simulation (HPCS), pages 1057--1058, Orléans, France, 2018. IEEE. [ DOI ]
[4]
Jolan Philippe, Frédéric Loulergue, and Wadoud Bousdira. Formalization of a Big Graph API in Coq (Poster). In International Conference on High Performance Computing and Simulation (HPCS), pages 893--894, Genoa, Italy, 2017. IEEE. [ DOI ]
[5]
Christopher D. Whitney and Frédéric Loulergue. Towards a Verified Parallel Implementation of Frequent Itemset Mining (Poster). In International Conference on High Performance Computing and Simulation (HPCS), pages 889--890, Genoa, Italy, 2017. IEEE. [ DOI ]
[6]
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, Mostafa Bamha, and Mohamad Al Hajj Hassan. Handling Data-skew Effects in Join Operations using MapReduce. Journées nationales du GdR GPL, GdT LaMHA, juin 2014.
For over a decade, MapReduce has become a prominent programming model to handle vast amounts of raw data in large scale systems. This model ensures scalability, reliability and availability aspects with reasonable query processing time. However these large scale systems still face some challenges: data skew, task imbalance, high disk I/O and redistribution costs can have disastrous effects on performance. In this paper, we introduce MRFA-Join algorithm: a new frequency adaptive algorithm based on MapReduce programming model and a randomised key redistribution approach for join processing of large-scale datasets. A cost analysis of this algorithm shows that our approach is insensitive to data skew and ensures perfect balancing properties during all stages of join computation. These performances have been confirmed by a series of experimentations.
[2]
Frédéric Loulergue. Systematic Development of Correct Programs for Parallel Computing. Faculty of Mathematics and Informatics, Babes-Bolyai University of Cluj-Napoca, Romania, February 2014.
With parallel machines being now the norm (from smart-phones to super-computers) and no longer restricted to a niche, concurrent and parallel programming has also to become widespread. To do so, it has to move to structured paradigms, in the same way sequential programming did more than forty years ago. Moreover the concern of applying formal methods arises, which allow specifications of parallel and distributed programs to be precisely stated and the conformance of an implementation to be verified using mathematical techniques. However, the complexity of parallel programs, compared to sequential ones, makes them more error-prone, difficult to verify and almost impossible to debug. Parallel programs correctness by construction is thus an essential feature. To build correct programs by constructions is not a simple task, and usually the methodologies used for this purpose are rather theoretical based on a pen-and-paper style. Such theoretical methodologies are usually based on parallel recursive structures. They are named “parallel” because their recursive nature makes them very suitable for divide-and-conquer and thus parallelism. However when one writes an application using parallel recursive structures, it is not yet implemented in parallel. A realisation of parallel recursive structures and their basic operations should be implemented using more concrete (and actually more “flat” than recursive) parallel programming languages. Moreover, a better approach could be based on software tools and formalised theories that allow a user to develop an efficient parallel application by implementing easily simple programs satisfying conditions, ideally automatically, proved. For this purpose proof assistants make the reasoning checkable by a machine, may provide some automation in reasoning, and actual programs may be extracted from developments within these proof assistants. This talk will present an effort for providing a framework based on the Coq proof assistant for the systematic development of correct programs for parallel computing.
[3]
Frédéric Loulergue. PaPDAS: Parallel Program Development with Algorithmic Skeletons. Journée MTV2/MFDL du GDR GPL, Grenoble, Janvier 2014.
Le projet PaPDAS a pour objectif de fournir un environnement pour le développement systématique de programmes parallèles se basant sur l'algorithmique constructive (théorie des listes) et permettant soit d'exécuter très efficacement les programmes obtenus, soit de les compiler avec un compilateur vérifié gérant le parallélisme. Dans cet exposé je présente la dérivation formelle et l'extraction depuis Coq d'un programme parallèle fonctionnel pour le problème All Nearest Smaller Values (ANSV) et la comparaison avec une implantation directe non vérifiée d'un autre algorithme pour résoudre le même problème.
[4]
Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Légaux, and Zhenjiang Hu. Dérivation formelle et extraction d'un programme data-paralléle pour le problème des valeurs inférieures les plus proches. AFADL, juin 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.
[5]
Frédéric Loulergue. Towards a Verified GTA Library in Coq. Deuxième Journée Informatique en Nuage à Orléans (JINO-2), January 2013.
The goal of this work is threefold. First we aim at modelling the algebraic structures used in the GTA framework and prove the lemma used to calculate programs from their GTA from inside the Coq proof assistant. Second we aim at providing some automation inside Coq to ease the definition of applications, with the formal verification that they actually fullfill the requirements of the GTA framework. Third we aim at providing the way to extract automatically actual parallel functional programs and MapReduce programs from these Coq developments. This talk will present the current status of this work-in-progress. This is a joint work with Kento Emoto, Julien Tesson, and Frederic Dabrowski.
[6]
Frédéric Loulergue. Towards a Framework for Systematically Developing Correct Parallel and Cloud Programs. NII - National Institute of Informatics, Tokyo, October 2013.
Our general goal is to ease the development of correct and verifiable parallel programs with predictable performances using theories and tools to allow a user to develop an efficient application byimplementing simple programs satisfying conditions easily, or ideally automatically, proved. To attain this goal, a framework should be based on (1) high-level algebraic theories of parallel programs, (2) modelling of these theories inside interactive theorem provers (also named proof assistants) such as Coq, to be able to write and reason on programs, (3) axiomatisation of lower level parallel programming primitives and their use to implement the high-level primitives in order to extract actual parallel code from the developments make inside proof assistants, (4) verified compilers to ensure that the compiled code actually preserves the semantics (and yet the correctness) of the extracted source code. This first lecture presents the big picture, an overview of the other lectures and the many open questions related to this goal.
[7]
Frédéric Loulergue. Program Verification with the Coq Proof Assistant. NII - National Institute of Informatics, Tokyo, November 2013. [ .pdf ]
Coq is a proof assistant based on the Curry-Howard correspondence relating terms of a typed Lambda calculus with proof trees of a logical system in natural deduction form. The calculus behind Coq is the calculus of (co)-inductive constructions, an extension of the initial Calculus of Constructions. The main usages of Coq are: (1) program verification, (2) modelling and proof of properties programming languages semantics, (3) formalised mathematical theories. This lecture is a short introduction to Coq for program verification.
[8]
Frédéric Loulergue. Writing and Reasoning about Parallel Programs -- Part 1. NII - National Institute of Informatics, Tokyo, November 2013.
Bulk Synchronous Parallel ML (BSML) is a structured parallel functional programming language based on the Bulk Synchronous Parallelism (BSP) which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism. BSML extends a functional programming language of the MLfamily with a polymorphic data structure and a very small set of primitives. In this lecture we describe a library for reasoning about BSML programs using the Coq interactive theorem prover.
[9]
Frédéric Loulergue. Writing and Reasoning about Parallel Programs -- Part 2. NII - National Institute of Informatics, Tokyo, November 2013.
Bulk Synchronous Parallel ML (BSML) is a structured parallel functional programming language based on the Bulk Synchronous Parallelism (BSP) which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism. BSML extends a functional programming language of the MLfamily with a polymorphic data structure and a very small set of primitives. In this lecture we describe a framework for extracting actual parallel programs from proofs of BSML programs in Coq. This framework is illustrated through several example applications.
[10]
Frédéric Loulergue. Constructive Algorithms in Coq. NII - National Institute of Informatics, Tokyo, November 2013.
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 lecture that Coq provides a cheap way to implement a powerful system to support program calculation. 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 mainly based on the theory of lists.
[11]
Frédéric Loulergue. Bulk Synchronous Parallel Homomorphisms. NII - National Institute of Informatics, Tokyo, November 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 lecture, the BH theory is presented, as well as its formalisation in Coq. An implementation of a BH skeleton is implemented in BSML and verified in Coq. In practice a BH skeleton for the C++ Orléans Skeleton Library C++ could also be used. The framework is illustrated through various applications including sparse matrix vector multiplication and the all nearest smaller values problem.
[12]
Frédéric Loulergue. Generate-Test-Aggregate for Cloud Computing in Coq. NII - National Institute of Informatics, Tokyo, November 2013.
Emoto, Fisher and Hu have integrated the generate-and-test programing(GTA) paradigm and semirings for aggregation of results, to propose a novel parallel programming framework for MapReduce, and to demonstrate how the framework can be efficiently implemented as a library to support parallel programming on Hadoop. In this lecture, we first present the modelling the algebraic structures used in the GTA framework and prove the lemma used to calculate programs with the Coq proof assistant. Second we show how to provide some automation inside Coq to ease the definition of applications, with the formal verification that they actually fulfill the requirements of the GTA framework. Third we provide the way to extract automatically actual parallel functional programs and MapReduce programs from these Coq developments.
[13]
Frédéric Loulergue. Towards a Verified GTA Library. Second Workshop on Frameworks for the Development of Correct (parallel) Programs (FraDeCoPP-2), November 2012.
The goal of this work is threefold. First we aim at modelling the algebraic structures used in the GTA framework and prove the lemma used to calculate programs from their GTA from inside the Coq proof assistant. Second we aim at providing some automation inside Coq to ease the definition of applications, with the formal verification that they actually fullfill the requirements of the GTA framework. Third we aim at providing the way to extract automatically actual parallel functional programs and MapReduce programs from these Coq developments. This talk will present the current status of this work-in-progress. This is a joint work with Kento Emoto, Julien Tesson, and Frederic Dabrowski.
[14]
Frédéric Loulergue. Une bibliothèque vérifiée de squelettes algorithmiques sur tableaux équitablement répartis. Journés Nationales du GDR Génie de la Programmation et du Logiciel, Juin 2012.
Les squelettes algorithmiques sont des motifs abstraits qui apparaissent souvent dans la programmation parallèle. Issus de la programmation fonctionnelle, ce sont des fonctions d'ordre supérieur implantées en parallèle et fournies au programmeur. De manière classique, ils offrent une interface simple à l'utilisateur sans les détails du parallélisme. Nous proposons dans cet article une série de squelettes algorithmiques implantés avec le langage fonctionnel parallèle BSML (Bulk Synchrounous Parallel ML). Ces squelettes permettent de manipuler une structure de données répartie, des tableaux équitablement répartis. La spécification de ces squelettes est données par un type de module de l'assistant de preuve Coq. Une implantation de ce type de module, et donc correcte par rapport à la spécification des squelettes, est réalisée à l'aide de la partie fonctionnelle de Coq augmentée d'une axiomatisation des primitives de BSML. L'extraction de cette implantation en Coq donne du code BSML prouvé correct. Ces squelettes parallèles peuvent alors être compilés par le compilateur BSML et enfin exécutés sur une grande variété de machines parallèles. Nous prouvons également correctes des applications en utilisant la spécification des squelettes et extrayons leurs implantations en BSML.
[15]
Frédéric Loulergue. Vers des environnements infonuagiques vérifiés. Première Journée Informatique en Nuage à Orléans (JINO-1), Juillet 2012.
As the usage of the 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. This software stack ranges from applications to the hypervisor. We argue that most of the layers could be practically formally verified, even if the work to verify all levels is huge.
[16]
Frédéric Loulergue. Modélisation en théorie des types. Application au développement de programmes parallèles corrects. Journée CaSciModOT, Orléans, Décembre 2011.
[17]
Frédéric Loulergue. Functional Parallel Programming with Revised Bulk Synchronous Parallel ML. PDAA Workshop, Hiroshima, November 2010.
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.
[18]
Frédéric Loulergue. Systematic Development of Correct Bulk Synchronous Parallel Programs. PDCAT Conference, Wuhan, China, Deember 2010.
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.
[19]
Frédéric Loulergue. Revised Bulk Synchronous Parallel ML. TOPS Seminar, Tokyo, November 2010.
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. In this talk, Revised BSML is presented and its expressiveness and performance are illustrated through an application examples. We also designed a formal semantics and proved its properties using the Coq proof assistant.
[20]
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.
[21]
F Loulergue. Functional Bulk Synchronous Parallelism in ML. The University of Tokyo, July 2007.
[22]
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.
[23]
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.
[24]
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.
[25]
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.
[26]
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.
[27]
Frédéric Loulergue. Functional programming of parallel and meta computing. Talk at the Komet Workshop, November 2004.
[28]
Frédéric Loulergue. Compositions parallèles et BSML. Seminaire du LIFO, Orléans, march 2003.
[29]
Frédéric Loulergue. Bulk Synchronous Parallel ML: Safety and Expressivity. Talk at The Tokyo Programming Seminar, November 2003.
[30]
Frédéric Loulergue. Distributed Evaluation of Functional BSP Programs. Talk at the International Workshop on High Level Parallel Programming, Orléans, march 2001.
[31]
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.
[32]
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.
[33]
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.
[34]
Frédéric Loulergue. Un langages fonctionnel pur d'ordre supérieur explicitement parallèle. Exposé aux Journées GDR, Rennes, 1997.