Contact the School of Informatics, Computing, and Cyber Systems
Analysis and Certification of Parallel Programs
Principal Investigator
Frédéric Loulergue
Collaborators
Allan Blanchard (CEA LIST, France), Wadoud Bousdira (LIFO, Université d’Orléans, France), Frédéric Dabrowski (LIFO, Université d’Orléans, France), Gaétan Hains (DPSL-DAL, Huawei Technologies, France), Kento Emoto (Kyushu Institute of Technology, Japan), Arvid Jakobsson (DPSL-DAL, Huawei Technologies, France), Nikolai Kosmatov (CEA LIST, France), Mathieu Lemerre (CEA LIST France), Kiminori Matsuzaki (Kochi University of Technology, Japan), Thomas Pinsard (LIFO, Université d’Orléans, France), Wijnand Suijlen (DPSL-DAL, Huawei Technologies, France), Thibaut Tachon (DPSL-DAL, Huawei Technologies, France), Julien Tesson (Université Paris-Est Créteil France)
Overview
Software is becoming more and more pervasive. Very high assurance software is therefore becoming a necessity. 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.
A program could be either verified to satisfy some specific properties (for example no runtime error, no deadlock, etc.), or to be correct with respect to a functional specification. Both top-down approaches, where the programs are correct by construction, or bottom-up approaches, where programs are first written, then formally certified can be used to obtain correct programs. We are investigating and developing methods and systems for analyzing and certifying parallel programs.
The SYDPACC system relies on 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 provides a systematic way of developing such parallelism from specifications for practically nontrivial examples. Program calculation is a kind of program transformation based on the theory of constructive algorithms. 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. The SYDPACC system is a set of libraries for the proof assistant Coq that allows to write naive (i.e. inefficient) functional programs then to transform them into efficient 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.
Frama-C is an extensible modular framework for the static and dynamic analysis, as well as deductive verification of C programs that offers different analyzers as plugins. Currently, Frama-C does not support the proof of functional properties for concurrent code. Conc2Seq is a new tool, realized as a Frama-C plugin, dedicated to the deductive verification of concurrent C programs. Assuming the program under verification respects an interleaving semantics, Conc2Seq performs automatic transformation of 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 resulting annotated code can then be processed by the deductive verification plugin WP. The proposed code transformation technique can also allow the user to reason about a concurrent program through the interleaving semantics using other existing Frama-C analyzers.
Bulk synchronous parallelism offers an abstract and simple model of parallelism yet allowing to take realistically into account the communication costs of parallel algorithms. It has been used in many application domains. BSPlib and its extensions are programming libraries for the C language that support the BSP style. There exist high-level approaches to BSP that are particularly suited to the partly automated generation of correct-by-construction programs from specifications using a proof assistant. However, they cannot yet attain the same performances than imperative BSP programs. Formal verification of imperative BSP programs based on formal semantics, even using automatic provers, still require a huge development effort. The goal of the joint effort with Huawei Technologies France is a tradeoff: instead of aiming at the full functional verification of programs, we will address the fully automatic verification of some interesting properties in BSP imperative programs using static analysis techniques. We are also investigating the generation of BSPlib C programs for high-level descriptions such as BSP automata.
Analyzing and formally certifying programs, in particular parallel or concurrent ones, is a difficult task. All the systems above work on the source code of programs. However to provide a higher assurance about these programs, one should ensure that no bugs are introduced by the compilation. Therefore we are also working on verified compilation phases and compilers for parallel languages, in particular an imperative language featuring nested atomic sections with thread escape.
Funding
- Huawei Technologies (2016-2019)
- CEA and DGA: PhD Grant (2013-2016)
- Japan Science and Technology Agency (JST): project 10102704 (2011-2014)
- French National Research Agency (ANR): ANR-2010-INTB-0205-02 (2011-2014)
- French Ministry of Research: Phd Grants (2007-2012)
- Université d’Orléans and The University of Tokyo: SDPP project (2008-2008)
- Japanese Society for the Promotion of Science: Invitation Fellowship for Research Program (2007)
Related Publications
- 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). CEUR Workshop Proceedings, 2016
- 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
- Loulergue Frédéric, Wadoud Bousdira, and Julien Tesson. Calculating Parallel Programs in Coq using List Homomorphisms. In “International Journal of Parallel Programming”, 2016
- Frédéric Loulergue. Development of correct-by-construction functional parallel programs (tutorial). In ACM Symposium on Applied Computing (SAC). ACM, 2016
- Loulergue Frédéric, Wadoud Bousdira, and Julien Tesson. Calcul de programmes parallèles avec Coq. In Nicolas Ollinger, editor, École des Jeunes Chercheurs en Informatique Mathématique, collection Alpha. CNRS Éditions, 2015
- Sylvain Dailler, Extension paramétrée de compilateur certifié pour la programmation parallèle, PhD Thesis, LIFO, University of Orléans, December 2015