3.1.1 Expected Impact

The impact of this research direction is both the usability of our representation for static analyses and optimizations performed in Sections 3.2 and 3.3, and the usability of its semantics to prove the correctness of these analyses.

3.1.2 Scientific Program

3.2.1 Expected impact

The impact of this work is the significantly widened applicability of various tools/compilers related to parallelization: allow optimizations for a larger class of programs, and allow low-cost analysis that scale to very large programs.

We target both analysis for optimization and analysis to detect, or prove the absence of bugs.

3.2.2 Scientific Program

3.3.1 Expected impact

In general, splitting a program into simpler processes simplifies the problem. This observation leads to the following points:

• By abstracting away irregular parts in processes, we expect to structure the long-term problem of handling irregular applications in the polyhedral model. The long-term impact is to widen the applicability of the polyhedral model to irregular kernels.
• Splitting a program into processes reduces the problem size. Hence, it becomes possible to scale traditionally expensive polyhedral analysis such as scheduling or tiling to quote a few.

As for the third research direction, the short term impact is the possibility to combine efficiently classical dataflow programming with compiler polyhedral-based optimizations. We will first propose ad-hoc solutions coming from our HPC application expertise, but supported by strong theoretical results that prove their correctness and their applicability in practice. In the longer term, our work will allow specifying, designing, analyzing, and compiling HPC dataflow applications in a unified way. We target semi-automatic approaches where pertinent feedback is given to the developer during the development process.

3.3.2 Scientific Program

3.4.1 Expected Impact

The short term impact is the possibility to improve simulation speed with a reasonable additional programming effort. The amount of additional programming effort will thus be evaluated in the short term.

In the longer term, our work will allow scaling up simulations both in terms of models and execution platforms. Models are needed not only for individual Systems on a Chip, but also for sets of systems communicating together (e.g., the full model for a car which comprises several systems communicating together), and/or heterogeneous models. In terms of execution platform, we are studying both parallel and distributed simulations.

3.4.2 Scientific Program

6.1.1 DCC

• Name:
  DPN C Compiler
• Keywords:
  Polyhedral compilation, Automatic parallelization, High-level synthesis
• Functional Description:
  Dcc (Data-aware process network C Compiler) compiles a regular C kernel to a data-aware process network (DPN), a dataflow intermediate representation suitable for high-level synthesis in the context of high-performance computing. Dcc has been registered at the APP ("Agence de protection des programmes") and transferred to the XtremLogic start-up under an Inria license.
• News of the Year:
  This year, Dcc was enhanced with an automated scheduler. Specifically, we have implemented an affine loop tiling algorithm and the related affine scheduler optimized for pipelined datapath. We also pursue the debugging of symbolic parallelization.
• Publication:
  hal-03143777
• Contact:
  Christophe Alias
• Participants:
  Christophe Alias, Alexandru Plesco

6.1.2 PoCo

• Name:
  Polyhedral Compilation Library
• Keywords:
  Polyhedral compilation, Automatic parallelization
• Functional Description:
  PoCo (Polyhedral Compilation Library) is framework to develop program analysis and optimizations in the polyhedral model. PoCo features polyhedral building blocks as well as state-of-the-art polyhedral program analysis. PoCo has been registered at the APP (“agence de protection des programmes”) and transferred to the XtremLogic start-up under an Inria licence.
• Release Contributions:
  v4.2: - Piece affine array contraction (extension of the successive minima algorithm) - Fast projection heuristics
• News of the Year:
  This year, Christophe implemented significant features in PoCo. First, a piecewise affine extension of the successive minima array contraction algorithm was added. Also, a set of heuristics for faster polyhedron projection were implemented.
• Contact:
  Christophe Alias
• Participant:
  Christophe Alias

6.1.3 MPPcodegen

• Name:
  Source-to-source loop tiling based on MPP
• Keywords:
  Source-to-source compiler, Polyhedral compilation
• Functional Description:
  MPPcodegen applies a monoparametric tiling to a C program enriched with pragmas specifying the tiling and the scheduling function. The tiling can be generated by any convex polyhedron and translation functions, it is not necessarily a partition. The result is a C program depending on a scaling factor (the parameter). MPPcodegen relies on the MPP mathematical library to tile the iteration sets.
• URL:
  http://­foobar.­ens-lyon.­fr/­mppcodegen/
• Publication:
  hal-02493164
• Authors:
  Christophe Alias, Guillaume Iooss, Sanjay Rajopadhye
• Contact:
  Christophe Alias
• Partner:
  Colorado State University

6.1.4 Encore with dataflow explicit futures

• Keywords:
  Language, Optimizing compiler, Source-to-source compiler, Compilers
• Functional Description:
  Fork of the Encore language compiler, with a new "Flow" construct implementing data-flow explicit futures.
• URL:
  https://­gitlab.­inria.­fr/­lhenrio/­encorewithdatafuts
• Contact:
  Ludovic Henrio

6.1.5 mppcheck

• Keywords:
  Polyhedral compilation, Program verification
• Functional Description:
  mppcheck features a pragma language to specify a polyhedral program transformation directly in the code and a verification algorithm able to check the correctness of the specified transformation. Our language is general enough to specify a loop tiling by an arbitrary polyhedral tile shape (e.g., hexagons, diamonds, trapezoids), and whose size may depend on a scaling parameter (monoparametric tiling). Our verification algorithm checks the legality of the proposed transformation, and provides counterexamples of unsatisfied dependences when it is incorrect. In addition, out tool infers the domain of scaling parameters where the tiling is not legal.
• URL:
  http://­foobar.­ens-lyon.­fr/­mppcheck/
• Publication:
  hal-03106070
• Contact:
  Christophe Alias
• Participants:
  Christophe Alias, Guillaume Iooss, Sanjay Rajopadhye
• Partner:
  Colorado State University

6.1.6 fkcc

• Name:
  The Farkas Calculator
• Keywords:
  DSL, Farkas Lemma, Polyhedral compilation
• Scientific Description:
  fkcc is a scripting tool to prototype program analyses and transformations exploiting the affine form of Farkas lemma. Our language is general enough to prototype in a few lines sophisticated termination and scheduling algorithms. The tool is freely available and may be tried online via a web interface. We believe that fkcc is the missing chain to accelerate the development of program analyses and transformations exploiting the affine form of Farkas lemma.
• Functional Description:
  fkcc is a scripting tool to prototype program analyses and transformations exploiting the affine form of Farkas lemma. Our language is general enough to prototype in a few lines sophisticated termination and scheduling algorithms. The tool is freely available and may be tried online via a web interface. We believe that fkcc is the missing chain to accelerate the development of program analyses and transformations exploiting the affine form of Farkas lemma.
• Release Contributions:
  - Script language - Polyhedral constructors - Farkas summation solver
• News of the Year:
  This year, Christophe improved the projection algorithm invoked by the 'keep' keyword by combining a Gaussian elimination with a Fourier-Motzkin elimination. Compared to Chernikova algorithm, the performances are greatly improved.
• URL:
  http://­foobar.­ens-lyon.­fr/­fkcc/
• Publication:
  hal-03106000
• Contact:
  Christophe Alias
• Participant:
  Christophe Alias

6.1.7 Vellvm

• Keywords:
  Coq, Semantic, Compilation, Proof assistant, Proof
• Scientific Description:
  A modern formalization in the Coq proof assistant of the sequential fragment of LLVM IR. The semantics, based on the Interaction Trees library, presents several rare properties for mechanized development of this scale: it is compositional, modular, and extracts to a certified executable interpreter. A rich equational theory of the language is provided, and several verified tools based on this semantics are in development.
• Functional Description:
  Formalization in the Coq proof assistant of a subset of the LLVM compilation infrastructure.
• URL:
  https://­github.­com/­vellvm/­vellvm
• Contact:
  Yannick Zakowski
• Participants:
  Yannick Zakowski, Steve Zdancewic, Calvin Beck, Irene Yoon
• Partner:
  University of Pennsylvania

6.1.8 vaphor

• Name:
  Verification of Programs with Horn Clauses
• Keyword:
  Program verification
• Functional Description:
  Program to horn clauses horn clauses with arrays abstraction
• Contact:
  Laure Gonnord
• Partner:
  Vérimag

6.1.9 Data Abstraction

• Name:
  Data Abstraction
• Keywords:
  Static analysis, Program verification, Propositional logic
• Functional Description:

  The tool is an element of a static program (or other) verification process which is done in three steps:

  1. Transform the verification problem into Horn clauses, perhaps using MiniJavaConverter or SeaHorn 2. Simplify the Horn clauses using data abstraction (this tool). 3. Solve the Horn clauses using a Horn solver such as Z3

• Contact:
  Laure Gonnord
• Partner:
  Vérimag

6.1.10 S4BXI

• Keywords:
  Simulation, HPC, Network simulator
• Functional Description:
  S4BXI is a simulator of the Portals4 network API. It is written using SimGrid's S4U interface, which provides a fast flow-model. More specifically, this simulator is tuned to model as best as possible Bull's hardware implementation of portals (BXI interconnect)
• URL:
  https://­s4bxi.­julien-emmanuel.­com/­docs/
• Contact:
  Julien Emmanuel
• Partner:
  Bull - Atos Technologies

6.1.11 llvm-pass

• Name:
  LLVM Pass analyzer
• Keyword:
  Compilation
• Functional Description:
  tool suite to work on llvm passes
• URL:
  https://­github.­com/­llvmpass/­llvm-passes
• Contact:
  Laure Gonnord

6.1.12 kut

• Keywords:
  Polyhedral compilation, Task scheduling
• Scientific Description:
  Task-level parallelism is usually exploited by a runtime scheduler, after tasks are mapped to processing units by a compiler. Kut is the compiler part of a compilation-centric runtime scheduling strategy. With kut, the tasks are partitioned so as to guide the runtime scheduling. Kut inputs an HPC kernel written in C and outputs a C with predicates helping the dynamic decision of the scheduler.
• Functional Description:
  Task-level parallelism is usually exploited by a runtime scheduler, after tasks are mapped to processing units by a compiler. Kut is the compiler part of a compilation-centric runtime scheduling strategy. With kut, the tasks are partitioned so as to guide the runtime scheduling. Kut inputs an HPC kernel written in C and outputs a C with predicates helping the dynamic decision of the scheduler.
• News of the Year:
  2019: version 1
• Publication:
  hal-02421327
• Contact:
  Christophe Alias
• Participants:
  Christophe Alias, Samuel Thibault, Laure Gonnord

6.1.13 ribbit

• Keywords:
  Compilation, Pattern matching, Algebraic Data Types
• Functional Description:
  Ribbit is a compiler for pattern languages with algebraic data types which is parameterized by the memory representation of types. Given a memory representation, it generates efficient and correct code for pattern matching clauses.
• URL:
  https://­gitlab.­inria.­fr/­cash/­ribbit
• Contact:
  Gabriel Radanne

6.1.14 calv

• Name:
  AVL calculator
• Keywords:
  Data structures, OpenMP
• Functional Description:
  calv is a calculator which is used to run different implementations of AVL trees, and compare their relative performances.
• URL:
  https://­gitlab.­inria.­fr/­paiannet/­calv
• Contact:
  Paul Iannetta

6.1.15 adtr

• Name:
  ADT Rewriting language
• Keywords:
  Compilation, Static typing, Algebraic Data Types, Term Rewriting Systems
• Functional Description:

  ADTs are generally represented by nested pointers, for each constructors of the algebraic data type. Furthermore, they are generally manipulated persistently, by allocating new constructors.

  ADTr allow representing ADTs in a flat way while compiling a pattern match-like construction as a rewrite on the memory representation. The goal is to then use this representation to optimize the rewriting and exploit parallelism.

• URL:
  https://­github.­com/­Drup/­adtr
• Publication:
  hal-03355377
• Contact:
  Gabriel Radanne
• Participants:
  Gabriel Radanne, Paul Iannetta, Laure Gonnord

6.1.16 dowsing

• Keywords:
  Static typing, Ocaml
• Functional Description:

  Dowsing is a tool to search function by types. Given a simple OCaml type, it will quickly find all functions whose types are compatible.

  Dowsing works by building a database containing all the specified libraries. New libraries can be added to the database. It then builds an index which allow to quickly answer to requests.

• URL:
  https://­github.­com/­Drup/­dowsing/
• Publication:
  hal-03355381
• Contact:
  Gabriel Radanne
• Participants:
  Gabriel Radanne, Laure Gonnord

6.1.17 odoc

• Keyword:
  Ocaml
• Functional Description:
  OCaml is a statically typed programming language with wide-spread use in both academia and industry. Odoc is a tool to generate documentation of OCaml libraries, either as HTML websites for online distribution or to create PDF manuals and man pages.
• News of the Year:
  This year, Gabriel Radanne rewrote a significant portion of odoc to provide improved HTML output, make it possible to produce other document formats, and introduce the ability to produce man pages. Florian Angeletti then implemented PDF output and integrated the usage of odoc in the official OCaml distribution. Concurrently, Jon Ludlam and Leo White rewrote the resolution mechanism of odoc. This all led to a joint presentation at the OCaml workshop and an upcoming new major release.
• URL:
  https://­github.­com/­ocaml/­odoc/
• Contact:
  Gabriel Radanne
• Participants:
  Jon Ludlam, Gabriel Radanne, Florian Angeletti, Leo White

7.1.1 Flexible Synchronization for Parallel Computations.

Participants: Ludovic Henrio, Matthieu Moy, Amaury Maillé.

Parallel applications make use of parallelism where work is shared between tasks; often, tasks need to exchange data stored in arrays and synchronize depending on the availability of these data. Fine-grained synchronizations, e.g. one synchronization for each element in the array, may lead to too many synchronizations while coarse-grained synchronizations, e.g. a single synchronization for the whole array, may prevent parallelism. Last year we proposed PromisePlus, a synchronization tool allowing tasks to synchronize on chunks of arrays with a granularity configurable by the programmer. We presented these results at the FSEN 2021 conference 14.

This year, we worked on a parametrisation of FIFO queues that are used to stream information between processes. We proposed an extension of classical FIFO queues where the granularity of synchronization can vary at runtime. Preliminary results are promising but additional work is necessary before publishing them.

7.1.2 An Optimised Flow for Futures: From Theory to Practice.

Participants: Nicolas Chappe, Ludovic Henrio, Amaury Maillé, Matthieu Moy, Hadrien Renaud.

A future is an entity representing the result of an ongoing computation. A synchronisation with a "get" operation blocks the caller until the computation is over, to return the corresponding value. When a computation in charge of fulfilling a future delegates part of its processing to another task, mainstream languages return nested futures, and several "get" operations are needed to retrieve the computed value (we call such futures "control-flow futures"). Several approaches were proposed to tackle this issues: the "forward" construct, that allows the programmer to make delegation explicit and avoid nested futures, and "data-flow explicit futures" which natively collapse nested futures into plain futures. This paper supports the claim that data-flow explicit futures form a powerful set of language primitives, on top of which other approaches can be built. We prove the equivalence, in the context of data-flow explicit futures, between the "forward" construct and classical "return" from functions. The proof relies on a branching bisimulation between a program using "forward" and its "return" counterpart. This result allows language designers to consider "forward" as an optimisation directive rather than as a language primitive. Following the principles of the Godot system, we provide a library implementation of control-flow futures, based on data-flow explicit futures implemented in the compiler. This small library supports the claim that the implementation of classical futures based on data-flow ones is easier than the opposite. Our benchmarks show the viability of the approach from a performance point of view.

The idea of Data-Flow Explicit Future is not new: it has been proposed by Ludovic Henrio in  46, and a partial implementation and theoretical study was done in  42. An implementation of data-flow explicit futures in the Encore language was made but not published during the M2 internship of Amaury Maillé. We performed performance analysis and compared several implementation during the internship of Hadrien Renaud, and proposed an optimization together with its proof of correctness during the internship of Nicolas Chappe. These three internships were concluded by a journal publication 7.

7.1.3 Locally abstract globally concrete semantics

Participants: Ludovic Henrio, Reiner Hähnle, Einar Broch Johnsen, Crystal Chang Din, Lizeth Tapia Tarifa.

This is a joint with Reiner Hähnle (TU Darmstadt), Einar Broch Johnsen, Crystal Chang Din, Lizeth Tapia Tarifa (Univ Oslo), Ka I Pun (Univ Oslo and Univ of applied science).

7.1.4 PNets: Parametrized networks of automata

Participants: Ludovic Henrio, Quentin Corradi, Eric Madelaine, Rabéa Ameur Boulifa.

• A refinement theory for open pNets. This work is realized with Eric Madelaine (INRIA Sophia-Antipolis), Rabéa Ameur Boulifa (Telecom ParisTech) and Quentin Corradi who did part of his internship in the Cash team.

An article that follows the internship of Quentin Corradi is being written.

7.1.5 A Survey on Verified Reconfiguration

Participants: Ludovic Henrio, Helene Coullon, Frederic Loulergue, Simon Robillard.

7.1.6 A Survey on Parallelism and Determinacy

Participants: Ludovic Henrio, Laure Gonnord, Lionel Morel, Gabriel Radanne.

7.1.7 Verified Compilation Infrastructure for Concurrent Programs

Participants: Nicolas Chappe, Ludovic Henrio, Matthieu Moy, Ambre Suhamy, Yannick Zakowski.

The objective of this research direction is to provide semantic and reasoning tools for the formalization of concurrent programs and the verification of compilers for concurrent languages. In particular, we want to apply these results to the design of verified optimizing compilers for parallel high-level languages. We wish to proceed in the spirit of the approach advocated in Vellvm 9: compositional, modular, executable monadic interpreters based on Interaction Trees  67 are used to specify the semantics of the language, in contrast with more traditional transition systems. Proving correct optimizations for such concurrent languages naturally requires new proof techniques that we need to design as well. This research direction is at its early stages, but we have promising early results. This year we have the following new achievements:

• During the internship of Ambre Suhamy, we have designed a concurrent semantics, based on an extension of interaction trees, for CCS (Calculus of communicating systems). We proved preliminary results over this semantics.
• Based on this first investigation, we have started the design of a major extension of interaction trees (dubbed "ctrees") for internal non-determinism — allowing in praticular to encode concurrency. The formalisation and ground theory has been designed, leading to the definition of notions of bisimulations over these constructions. We will investigate its application to a couple of use cases in 2022. This line of work is a collaboration with Steve Zdancewic and Paul He from University of Pennsylvania.
• Nicolas Chappe has started his PhD thesis under the supervision of Yannick Zakowski, Matthieu Moy, and Ludovic Henrio. The PhD is entitled “Toward a verified compilation infrastructure for concurrent programs: Non-sequential paradigms in Vellvm”. The first investigations conducted during the PhD has been dedicated to the design of semantics (based on ctrees) for concurrent programs supporting weak memory models.

7.2.1 Data Abstraction: A General Framework to Handle Program Verification of Data Structures

Participants: Julien Braine, Laure Gonnord, David Monniaux.

Proving properties on programs accessing data structures such as arrays often requires universally quantified invariants, e.g., "all elements below index i are nonzero". In our paper accepted at SAS 2021 11 (long version in 17, we propose a general data abstraction scheme operating on Horn formulas, into which we recast previously published abstractions. We show that our instantiation scheme is relatively complete: the generated purely scalar Horn clauses have a solution (inductive invariants) if and only if the original problem has one expressible by the abstraction.

7.2.2 Search functions by types

Participants: Gabriel Radanne, Laure Gonnord, Clement Allain.

Sometimes, we need a function so deeply that we have to go out and search for it. How do we find it? Sometimes, we have clues: a function which manipulates list is probably in the List module ...but not always! Sometimes, all we have is its functionality: doing the sum of a list of integers. Unfortunately, search by functionality is difficult.

Rittri proposed an approximation: use the type of the function as a key to search through libraries: in our case, int list -> int. To avoid stumbling over details such as the order of arguments, he proposed to use matching modulo type isomorphism – a notion broader than syntactic equality. Unfortunately, algorithms for unification modulo type isomorphisms are extremely costly (at best NP). An exhaustive search would not be usable during programming in practice.

In this research direction, we investigate how to scale search by types. For this purpose, we developed new algorithm technique similar to indexes used in databases, but appropriate for keys following a rich language of types. Early result have been published in ML2021 15 and we have developed a prototype, Dowsing 6.1.16, implementing these ideas.

7.2.3 A new module system for OCaml

Participants: Clement Blaudeau, Didier Remy, Gabriel Radanne.

Modularity is a key tool for building reusable and structured code. While the OCaml module system is known for being expressive and powerful, specifying its behavior and formalizing its properties has proven to be hard. This research direction aims to develop a comprehensive description of a generative subset of the OCaml module system (called the source system), with a focus on the signature avoidance problem. By extending the signature syntax with existential types (inspired by $F_{\omega }$), we describe an alternate system (called canonical) with a simpler set of judgments that both solves the issues of the source description and provides formal guarantees through elaboration into $F_{\omega }$. We show that the canonical system is more expressive than the source one and state at which conditions canonical typing derivations can be translated back into the source typing. As a middle point between the path-based representation of OCaml and the formal description of $F_{\omega }$, the canonical presentation is a framework which we believe could support numerous features (applicative functors, transparent ascription, module aliases, ...) and could serve as a basis for a redefinition of module system of an industry-grade language as OCaml.

7.3.1 Optimizing compiling for tree-like structures

Participants: Paul Ianetta, Laure Gonnord, Gabriel Radanne.

Trees are used everywhere, yet their internal operations are nowhere as optimized as arrays are. This work is in the continuity of the research on cache-oblivious algorithms for trees. It investigate the properties of structural transformations on trees via two directions.

First, we studied how to develop structural low-level operations to efficiently manipulate trees in-place and how to optimized and parallelize such operations 18. This yielded an optimized implementation to manipulate AVL trees 6.1.14.

Following this study, we developed a more general framework that aims to decompose and optimize arbitrary transformation on trees by expressing them as rewrite rules on Algebraic Data Types. In this approach, the traditional semantic of functional programs with pattern matching is reinterpreted as optimized, in-place, imperative loop nests. These results were published in GPCE2021 13 and implemented in a prototype compiler 6.1.15.

7.3.2 Parallel rewriting operations on Trees

Participants: Thaïs Baudon, Carsten Fuhs, Laure Gonnord.

During the M2 internship of Thaïs Baudon, partially funded by the CODAS's ANR project, we studied the problem of scheduling programs with complex data structures with the point of view of term rewriting. As related work, we show that although scheduling operations on efficient data structures apart from arrays should have a great impact on performance, there is nearly no work on this topic. However, some related work from the rewriting community gives us great insights about the link between termination and scheduling. Our contributions as a first step toward full efficient compilation of programs with inductive data structures are 1. first algorithms for this parallel evaluation, 2. a code generation algorithm to generate efficient parallel evaluators, 3. a prototype implementation and first experimental results

Part of this work, namely the proposition of a novel parallel complexity notion was published in the WST workshop 16.

7.3.3 Memory optimizations for Algebraic Data Types

Participants: Thaïs Baudon, Gabriel Radanne, Laure Gonnord.

In the last few decades, Algebraic Data Types (ADT) have emerged as an incredibly effective tool to model and manipulate data for programming. Additionally, ADTs could provide numerous advantages for optimizing compilers, as the rich declarative description could allow them to choose the memory representation of the types.

Initially, ADTs were mostly present in functional programming languages such as OCaml and Haskell. Such GC-managed functional languages generally use uniform memory representation which prohibit agressive optimisations of the representation of ADTs. However, ADTs are now present in many different languages, notably Scala and Rust, which permit such optimizations.

The goal of this research direction is to investigate how to represent terms of Algebraic Data Types and how to compile pattern matching efficiently. We aim to develop a generic compilation framework which accomodate arbitrarely complex memory representation for terms, and to provide news ways to optimize the representation of ADTs. A prototyper compiler has been implemented 6.1.13.

7.3.4 Vellvm: Verified LLVM

Participants: Calvin Beck, Bastien Rousseau, Irene Yoon, Yannick Zakowski, Steve Zdancewic.

We develop, in collaboration with the University of Pennsylvania, a formally verified in Coq compilation infrastructure based on LLVM, dubbed Vellvm 6.1.7. Compared to other existing verified compilation framework, we define the semantics of the languages we consider as monadic interpreters built on top of the Interaction Trees framework. This approach brings us benefits in terms of modularity, compositionality and executability, as well as leads to an equational mode of reasoning to establish refinements. The following major achievements have taken place this year:

• We have published the description of our new infrastructure at ICFP'21 9.
• A major redefinition of the memory model, led by Calvin Beck and accounting for the necessary finite view of the memory imposed by the presence of pointer to integer casts in LLVM IR, has been started. Most of it is finished, we are working on validating the new model by proving optimizations corrects and will submit an article about it during the year 2022.
• Reasoning about the various monadic interpreters involved in such semantics is challenging. A major process of abstraction and generalization of the equational theory expected from these monads, and a zoo of implementations of these theories, has been developed — an effort led by Irene Yoon. These results will be submitted as an article during the year 2022.
• Spiral is a compilation framework for the generalization of efficient low level code for numerical computations. HELIX is a formalization in Coq of part of this framework that Vadim Zaliva has developped during his PhD. We have proved correct a back end of the HELIX compilation chain down to Vellvm. The full chain will be described in a journal paper during the year 2022.
• As part of his internship, Bastien Rousseau has developed a set of verified combinators to build control flow graphs compositionally and anonymously. By providing in this way a DSL to write program transformations over LLVM IR, we obtain for free a set of well-formedness properties over the generated code. Furthermore, each combinator coming with a semantic characterestic equation, we obtain compositional reasoning principles. We plan on complementing this work with its dual: a DSL of patterns to deconstruct a graph into its construction as combinators.

7.3.5 Verified Abstract Interpreters as Monadic Interpreters

Participants: Laure Gonnord, Sébastien Michelland, Yannick Zakowski.

In the realm of verified compilation, one typically wants to verify the static analyzes used by the compiler. In existing works, the analysis is typically written as a fuel-based pure function in Coq and verified against the semantics described as a transition system. The goal of this research is to develop the tools and reasoning principles to transfer these ideas to a context where the semantics of the language is defined as a monadic interpreters built on Interaction Trees.

During his internship, Sébastien Michelland has developed a first promising prototype, establishing a highly modular framework to build and prove correct such analyses. He has instantiated his result on a toy Imp language, and is now aiming at instantiating it on a toy assembly language. We plan on submitting an article describing these first results, before considering the application of the technique to Vellvm.

7.3.6 A Complete Compilation Chain for Polyhedral High-Level Synthesis

Participants: Christophe Alias, Alexandru Plesco.

High-Level Synthesis tools lacks high-level optimizations. This work shows the feasibility of using the polyhedral model to design the HLS tool itself. We propose a complete compilation chain based on data-aware process networks (DPN), a dataflow intermediate representation suitable for HLS in the context of high-performance computing. DPN combines the benefits of a low-level dataflow representation-close to the final circuit-and affine iteration space tiling to explore the parallelization trade-offs (local memory size, communication volume, parallelization degree). We outline our compilation algorithms to map a C program to a DPN (front-end), then to map a DPN to an FPGA configuration (back-end). Finally, we present synthesis results on compute-intensive kernels from the Polybench suite.

This work has been accepted for publication in the CC'21 conference 10. The compiler has been completely implemented 6.1.1, 6.1.2. It is now used in the Xtremlogic startup.

7.3.7 Enhancing the Polyhedral Model with Parametric Tiling

Participants: Guillaume Iooss, Christophe Alias, Sanjay Rajopadhye.

For polyhedral programs, parametric tiling in its full generality is known to be non-linear, breaking the mathematical closure properties of the polyhedral model. Most compilation tools therefore either perform fixed size tiling, or apply parametric tiling in only the final, code generation step. We introduce monoparametric tiling, a restricted parametric tiling transformation. We show that, despite being parametric, it retains the closure properties of the polyhedral model. We first prove that applying monoparametric partitioning (i) to a polyhedron yields a union of polyhedra with modulo conditions, and (ii) to an affine function produces a piecewise-affine function with modulo conditions. We then use these properties to show how to tile an entire polyhedral program. Our monoparametric tiling is general enough to handle tiles with arbitrary tile shapes that can tessellate the iteration space (e.g., hexagonal, trapezoidal, etc). This enables a wide range of polyhedral analyses and transformations to be applied.

This work has been accepted for publication in the international journal of parallel programming 8. We also provide a complete implementation 6.1.3.

7.3.8 Affine Multibanking for High-Level Synthesis

Participants: Christophe Alias, Matthieu Moy.

High-level circuit compilers (high-level synthesis, HLS) are able to translate a C program to an FPGA circuit configuration. Unlike software parallelization, there is no operating system to place the computation and the memory at runtime. All the parallelization decisions must be done at compile time. In this work, we address the compilation of data placement under parallelism and resource constraints. We propose an HLS algorithm able to partition the data across memory banks, so parallel access will target distinct banks to avoid data transfer serialization. Our algorithm is able to minimize the number of banks and the maximal bank size.

The first results are still preliminary, but promising 19. We are working on extending the experimental validation to more general polyhedral kernels.

7.3.9 Towards a Trace-Based Polyhedral Model

Participants: Hugo Thievenaz, Keiji Kimura, Christophe Alias.

This work is funded by the polytrace Inria exploratory action. Our results are still preliminary, but promising 22. We are currently working on the cases which require piece-wise affine mappings.

7.3.10 A Polyhedral Approach for Scalar Promotion

Participants: Alec Sadler, Christophe Alias, Hugo Thievenaz.

Memory accesses are a well known bottleneck whose impact might be mitigated by using properly the memory hierarchy until registers. In this paper, we address array scalarization, a technique to turn temporary arrays into a collection of scalar variables to be allocated to registers. We revisit array scalarization in the light of the recent advances of the polyhedral model, a general framework to design optimizing program transformations. We propose a general algorithm for array scalarization, ready to be plugged in a polyhedral compiler, among other passes. Our scalarization algorithm operates on the polyhedral intermediate representation. In particular, our scalarization algorithm is parametrized by the program schedule possibly computed by a previous compilation pass. We rely on schedule-directed array contraction and we propose a loop tiling algorithm able to reduce the footprint down to the available amount of registers on the target architecture. Experimental results confirm the effectiveness and the efficiency of our approach.

This is a preliminary, but promising work 21. We are working on extending the tiling model to handle more dependence patterns.

7.3.11 A Polyhedral Approach for Auto-Parallelization using a Distributed Virtual Machine

Participants: Damien De Montis, Jean-Baptiste Besnard, Christophe Alias.

As parallel systems have to undergo an unprecedented transition towards more parallelism and hybridization, we propose to discuss the consequences on programming models. In particular, MPI and OpenMP may face some complexity barriers due to the added complexity required by such hardware. We propose to build from the ground up a new way to program a parallel system, relying both on a distributed runtime, unifying multiple nodes in a coherent ensemble, and on advanced tools from the Polyhedral model. We first describe the Distributed Virtual Machine (DVM) runtime establishing a data-flow environment suitable to the polyhedral transformations. We present and identify what we have seen as key components in such a system, transposing loop nests to a distributed set of machines thanks to a pragma notation combined with an automatic tiling approach. Eventually, while presenting results we open the discussion of remaining challenges and some potential mitigation.

This is a preliminary work, which will serve as basis for a collaboration with Paratools 20. An ANR project is under submission around these topics.

7.4.1 Standard-compliant parallel SystemC simulation of loosely-timed transaction level models: From baremetal to Linux-based applications support. Integration

Participants: Matthieu Moy, Gabriel Busnot, Tanguy Sassolas, Nicolas Ventroux.

To face the growing complexity of System-on-Chips (SoCs) and their tight time-to-market constraints, Virtual Prototyping (VP) tools based on SystemC/TLM2.0 must get faster while maintaining accuracy. However, the ASI SystemC reference implementation remains sequential and cannot leverage the multiple cores of modern workstations. In this paper, we present SCale 2.0, a new implementation of a parallel and standard-compliant SystemC kernel, reaching unprecedented simulation speeds. By coupling a parallel SystemC kernel with shared resources access monitoring and process-level rollback, we can preserve SystemC atomic thread evaluation while leveraging the available host cores. We also generate process interaction traces that can be used to replay any simulation deterministically for debug purpose. Evaluation on baremetal applications shows ×15 speedup compared to the ASI SystemC kernel using 33 host cores reaching speeds above 2300 Million simulated Instructions Per Second (MIPS). Challenges related to parallel simulation of full software stack with modern operating systems are also addressed with speedup reaching ×13 during recording run and ×24 during the replay run.

This is a continuation from the earlier conference article  32. We extended the approach to support simulation of Linux-based applications, and published the results in 6.

9.1.1 Inria associate team not involved in an IIL or an international program

9.1.2 Participation in other International Programs

9.2.1 Other International Collaborations

9.2.2 Visits of international scientists

10.1.1 Scientific events: organisation

• Together with Emmanuelle Saillard, Kevin Martin and Frédéric Dubrowski, Laure Gonnord and Ludovic Henrio animate the remote "CLAP" seminar

10.1.2 Journal

10.1.3 Teaching

• Bachelor (“Licence”):
  • Christophe Alias, INSA CVL, 3A STI, "Compilation": 26h ETD (CM+TD).
  • Thaïs Baudon Université Claude Bernard Lyon1, LIFASR4 (Architecture des Ordinateurs), L2 Informatique : 16h TD + 24h TP;
  • Thaïs Baudon Université Claude Bernard Lyon1, LIFAP1 (Algorithmique et programmation en C) L1 Informatique : 27h TP.
  • Paul Iannetta Université Claude Bernard Lyon1, L2 informatique, LIFAP2 : Algorithmique et programmation fonctionnelle: 18h TP
  • Julien Braine Université Claude Bernard Lyon1, Bases de Données avancées, L3 Informatique : 32h TD;
  • Laure Gonnord Université Claude Bernard Lyon1, L3 LIFASR5 Systèmes : 20h
  • Laure Gonnord Esisar engineer school, Valence, 3A, C programming labs TP 30h
  • Matthieu Moy co-responsabilité de la mention informatique de la licence de sciences UCBL.
  • Gabriel Radanne Université Claude Bernard Lyon1, L3, LIFProject (Ecandrement de projets étudiants): 16h.
• Master:
  • Christophe Alias, ENS de Lyon, Préparation à l'agrégation d'informatique, "Compilation": 10h CM.
  • Christophe Alias, INSA CVL, 4A STI, "Optimisation des applications embarquées": 26h ETD (CM+TD).
  • Christophe Alias, Laure Gonnord and Yannick Zakowski: ENSL, M2 IF course (sept-nov 2021) "Advanced static analyses for compilation", CR 14.
  • Damien Pous and Yannick Zakowski: ENSL, M2 IF course (sept-nov 2021) "Program Verification with Coinduction and Proof Assistants", CR 16.
  • Paul Iannetta: Université Claude Bernard Lyon1, M1 informatique, MIF01 : "Gestion de projet et génie logiciel": 12h TP, 3h TD
  • Laure Gonnord: Esisar engineer school, Valence, 4A, "Compilation course" CM+TD 20h
  • Laure Gonnord: Esisar engineer school, Valence, 4A, "Database course" CM+TD 25h
  • Matthieu Moy: Université Claude Bernard Lyon1, M1 informatique, MIF01 : "Gestion de projet et génie logiciel": 12hCM, 12h TP, 3h TD
  • Matthieu Moy: Université Claude Bernard Lyon1, M1 informatique, MIF08 : "Compilation et Traduction de programmes": 7h30CM, 15h TP, 7h30TD
  • Gabriel Radanne, Ludovic Henrio, and Nicolas Chappe: ENSL, M1: "Compilation et Analyse de Programmes" 28h CM, 24h TP.
  • Ludovic Henrio: University of Nice Sophia Antipolis, M2 Ubinet. "an algorithmic approach to distributed systems"3h30 CM+TD

10.1.4 Supervision

• Hugo Thievenaz's PhD thesis is supervised by Christophe Alias and Keiji Kimura (Waseda University, Japan).
• Julien Braine's PhD thesis is supervised by Laure Gonnord and David Monniaux (Verimag, Grenoble)
• Paul Iannetta's PhD thesis is supervised by Laure Gonnord, Gabriel Radanne and Lionel Morel (Insa de Lyon)
• Thaïs Baudon's PhD thesis is supervised by Laure Gonnord and Gabriel Radanne
• Julien Emmanuel's PhD thesis is supervised by Matthieu Moy and Ludovic Henrio
• Amaury Maillé's PhD thesis is supervised by Ludovic Henrio and Matthieu Moy
• Nicolas Chappe's PhD thesis is supervised by Yannick Zakowski, Matthieu Moy and Ludovic Henrio

10.1.5 Juries

• Christophe Alias was a reviewer in the PhD committee of Salwa Kobeissi, University of Strasbourg. Advisor: Philippe Clauss, Title: "Speculative Rewriting of Recursive Programs as Loop Candidates for Efficient Parallelization and Optimization Using an Inspector-Executor Mechanism".
• Yannick Zakowski was an examiner for the practical programming exam of the concours of the ENS.
• Christophe Alias was in the admission committee for the second concours of ENS de Lyon as an examiner.
• Laure Gonnord was in the PhD commitee of TODO
• Matthieu Moy is in the PhD jury of Nicolas Leclaire, TIMA, supervised by Stéphane Mancini. Title: Methodology for Code-Optimization of Memory Data-Layouts for High-Performance-System Architectures with Complex Memory Hierarchies. Report submited in december 2021, defense planned in january 2022.

10.2.1 Internal or external Inria responsibilities

• Laure Gonnord was member of the "Inria Commission d'Evaluation" until sept 2021
• Laure Gonnord is member of the GDR GPL board and in charge of the associated Young researcher school

International journals

• 6 articleG.Gabriel Busnot, T.Tanguy Sassolas, N.Nicolas Ventroux and M.Matthieu Moy. Standard-compliant parallel SystemC simulation of loosely-timed transaction level models: From baremetal to Linux-based applications support.Integration, the VLSI Journal79July 2021, 23-40
  HALDOIback to text
• 7 articleN.Nicolas Chappe, L.Ludovic Henrio, A.Amaury Maillé, M.Matthieu Moy and H.Hadrien Renaud. An Optimised Flow for Futures: From Theory to Practice.The Art, Science, and Engineering of Programming61July 2021, 1-41
  HALDOIback to text
• 8 articleG.Guillaume Iooss, C.Christophe Alias and S.Sanjay Rajopadhye. Monoparametric Tiling of Polyhedral Programs.International Journal of Parallel Programming49March 2021, 376–409
  HALDOIback to text
• 9 articleY.Yannick Zakowski, C.Calvin Beck, I.Irene Yoon, I.Ilia Zaichuk, V.Vadim Zaliva and S.Steve Zdancewic. Modular, compositional, and executable formal semantics for LLVM IR.Proceedings of the ACM on Programming Languages5ICFPAugust 2021, 1-30
  HALDOIback to textback to textback to text

International peer-reviewed conferences

• 10 inproceedingsC.Christophe Alias and A.Alexandru Plesco. Data-Aware Process Networks.CC 2021 - 30th ACM SIGPLAN International Conference on Compiler ConstructionVirtual, South KoreaACMMarch 2021, 1-11
  HALDOIback to textback to text
• 11 inproceedingsJ.Julien Braine, L.Laure Gonnord and D.David Monniaux. Data Abstraction: A General Framework to Handle Program Verification of Data Structures.SAS 2021 - 28th Static Analysis Symposium12913Lecture notes in computer scienceChicago, United StatesOctober 2021, 215-235
  HALDOIback to text
• 12 inproceedingsJ.Julien Emmanuel, M.Matthieu Moy, L.Ludovic Henrio and G.Grégoire Pichon. S4BXI: the MPI-ready Portals 4 Simulator.MASCOTS 2021 - 29th IEEE International Symposium on the Modeling, Analysis, and Simulation of Computer and Telecommunication SystemsHouston, United StatesIEEENovember 2021, 1-8
  HALback to text
• 13 inproceedingsP.Paul Iannetta, L.Laure Gonnord and G.Gabriel Radanne. Compiling pattern matching to in-place modifications.GPCE 2021 - 20th International Conference on Generative Programming: Concepts & ExperiencesChicago & Virtual, United StatesOctober 2021
  HALDOIback to text
• 14 inproceedingsA.Amaury Maillé, L.Ludovic Henrio and M.Matthieu Moy. Promise Plus: Flexible Synchronization for Parallel Computations on Arrays.Lecture Notes in Computer ScienceFSEN 2021 - 9th IPM International Conference on Fundamentals of Software EngineeringTehran, IranMay 2021, 1-7
  HALback to text

Conferences without proceedings

• 15 inproceedingsC.Clément Allain, G.Gabriel Radanne and L.Laure Gonnord. Isomorphisms are back!: Smart indexing for function retrieval by unification modulo type isomorphisms.ML 2021 - ML WorkshopVirtual, FranceAugust 2021, 1-3
  HALback to text
• 16 inproceedingsT.Thaïs Baudon, C.Carsten Fuhs and L.Laure Gonnord. Parallel Complexity of Term Rewriting Systems.WST 2021 - 17th International Workshop on TerminationVirtual, FranceJuly 2021, 1-6
  HALback to text

Reports & preprints

• 17 reportJ.Julien Braine, L.Laure Gonnord and D.David Monniaux. Data Abstraction: A General Framework to Handle Program Verification of Data Structures.RR-9408Inria Grenoble Rhône-Alpes; VERIMAG UMR 5104, Université Grenoble Alpes, France; LIP - Laboratoire de l’Informatique du Parallélisme; Université Lyon 1 - Claude Bernard; ENS LyonMay 2021, 1-29
  HALback to text
• 18 reportP.Paul Iannetta, L.Laure Gonnord and G.Gabriel Radanne. Parallelizing Structural Transformations on Tarbres.RR-9405ENS Lyon, CNRS & INRIAApril 2021, 21
  HALback to text
• 19 reportI.Ilham Lasfar, C.Christophe Alias, M.Matthieu Moy, R.Rémy Neveu and A.Alexis Carré. Affine Multibanking for High-Level Synthesis.RR-9440Inria - Research Centre Grenoble – Rhône-AlpesDecember 2021
  HALback to text
• 20 reportD.Damien de Montis, J.-B.Jean-Baptiste Besnard and C.Christophe Alias. A Polyhedral Approach for Auto-Parallelization using a Distributed Virtual Machine.RR-9432INRIA , LIP - ENS Lyon; ParatoolsOctober 2021, 25
  HALback to text
• 21 reportA.Alec Sadler, C.Christophe Alias and H.Hugo Thievenaz. A Polyhedral Approach for Scalar Promotion.RR-9437Institut National de Recherche en Informatique et en Automatique (INRIA)November 2021, 14
  HALback to text
• 22 reportH.Hugo Thievenaz, K.Keiji Kimura and C.Christophe Alias. Towards Trace-Based Array Contraction.RR-9442Inria; Waseda UniversityDecember 2021, 20
  HALback to text

Softwares

• 23 softwareM.Marouane Belaoucha, C.Christophe Alias, D.Denis Barthou and S.Sid Touati. FADAlib: an open source C++ library for fuzzy array dataflow analysis.November 2021GNU Lesser General Public License v3.0 or later
  HALSoftwage Heritage