6.1.1 Heptagon

• Keywords: Compilers, Synchronous Language, Controller synthesis
• Functional Description:

  Heptagon is an experimental language for the implementation of embedded real-time reactive systems. It is developed inside the Synchronics large-scale initiative, in collaboration with Inria Rhones-Alpes. It is essentially a subset of Lucid Synchrone, without type inference, type polymorphism and higher-order. It is thus a Lustre-like language extended with hierchical automata in a form very close to SCADE 6. The intention for making this new language and compiler is to develop new aggressive optimization techniques for sequential C code and compilation methods for generating parallel code for different platforms. This explains much of the simplifications we have made in order to ease the development of compilation techniques.

  The current version of the compiler includes the following features: - Inclusion of discrete controller synthesis within the compilation: the language is equipped with a behavioral contract mechanisms, where assumptions can be described, as well as an "enforce" property part. The semantics of this latter is that the property should be enforced by controlling the behaviour of the node equipped with the contract. This property will be enforced by an automatically built controller, which will act on free controllable variables given by the programmer. This extension has been named BZR in previous works. - Expression and compilation of array values with modular memory optimization. The language allows the expression and operations on arrays (access, modification, iterators). With the use of location annotations, the programmer can avoid unnecessary array copies.

• URL: http://heptagon.gforge.inria.fr
• Contacts: Marc Pouzet, Adrien Guatto, Gwenaël Delaval
• Participants: Adrien Guatto, Brice Gelineau, Cédric Pasteur, Eric Rutten, Gwenaël Delaval, Léonard Gérard, Marc Pouzet
• Partners: UGA, ENS Paris, Inria, LIG

6.1.2 SundialsML

• Name: Sundials/ML
• Keywords: Simulation, Mathematics, Numerical simulations
• Scientific Description:

  Sundials/ML is a comprehensive OCaml interface to the Sundials suite of numerical solvers (CVODE, CVODES, IDA, IDAS, KINSOL). Its structure mostly follows that of the Sundials library, both for ease of reading the existing documentation and for adapting existing source code, but several changes have been made for programming convenience and to increase safety, namely:

  solver sessions are mostly configured via algebraic data types rather than multiple function calls,

  errors are signalled by exceptions not return codes (also from user-supplied callback routines),

  user data is shared between callback routines via closures (partial applications of functions),

  vectors are checked for compatibility (using a combination of static and dynamic checks), and

  explicit free commands are not necessary since OCaml is a garbage-collected language.

• Functional Description: Sundials/ML is a comprehensive OCaml interface to the Sundials suite of numerical solvers (CVODE, CVODES, IDA, IDAS, KINSOL, ARKODE).
• Release Contributions:

  Adds support for v4.x of the Sundials Suite of numerical solvers.

  Notably this release adds support for nonlinear solvers, improves the interface to linear solvers, adds support for new vector array operations, and subdivides the ARKode interface into three submodules (ARKStep, ERKStep, and MRIStep).

• URL: http://inria-parkas.github.io/sundialsml/
• Publications: hal-01408230v1, hal-01967659v1
• Authors: Jun Inoue, Timothy Bourke, Marc Pouzet
• Contacts: Marc Pouzet, Timothy Bourke
• Participants: Jun Inoue, Marc Pouzet, Timothy Bourke

6.1.3 Zelus

• Keywords: Numerical simulations, Compilers, Embedded systems, Hybrid systems
• Scientific Description: The Zélus implementation has two main parts: a compiler that transforms Zélus programs into OCaml programs and a runtime library that orchestrates compiled programs and numeric solvers. The runtime can use the Sundials numeric solver, or custom implementations of well-known algorithms for numerically approximating continuous dynamics.
• Functional Description: Zélus is a new programming language for hybrid system modeling. It is based on a synchronous language but extends it with Ordinary Differential Equations (ODEs) to model continuous-time behaviors. It allows for combining arbitrarily data-flow equations, hierarchical automata and ODEs. The language keeps all the fundamental features of synchronous languages: the compiler statically ensure the absence of deadlocks and critical races, it is able to generate statically scheduled code running in bounded time and space and a type-system is used to distinguish discrete and logical-time signals from continuous-time ones. The ability to combines those features with ODEs made the language usable both for programming discrete controllers and their physical environment.
• URL: https://zelus.di.ens.fr
• Publications: hal-03051954v1, hal-02333603v1, hal-02426533v1, inria-00554271v1, hal-01242732v1, hal-00654113v1, hal-00909029v1, hal-01575621v4, hal-01575631v1, hal-00766726v1, hal-00938891v1, hal-00654112v1, hal-01879026v1, hal-01549183v2, hal-00938866v1
• Authors: Marc Pouzet, Timothy Bourke
• Contacts: Marc Pouzet, Timothy Bourke, Guillaume Baudart
• Participants: Marc Pouzet, Timothy Bourke
• Partner: ENS Paris

6.1.4 Vélus

• Name: Verified Lustre Compiler
• Keywords: Synchronous Language, Compilation, Software Verification, Coq, Ocaml
• Functional Description: Vélus is a prototype compiler from a subset of Lustre to assembly code. It is written in a mix of Coq and OCaml and incorporates the CompCert verified C compiler. The compiler includes formal specifications of the semantics and type systems of Lustre, as well as the semantics of intermediate languages, and a proof of correctness that relates the high-level dataflow model to the values produced by iterating the generated assembly code.
• Release Contributions: First source-code release. Treatment of primitive reset construct. Clocks allowed for node arguments.
• URL: https://velus.inria.fr
• Contacts: Timothy Bourke, Lelio Brun, Marc Pouzet

6.1.5 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
• Contacts: Christophe Alias, Guillaume Iooss, Sanjay Rajopadhye
• Partner: Colorado State University

6.1.6 MPP

• Name: MonoParametric Partitionning transformation
• Keywords: Compilation, Polyhedral compilation
• Functional Description: This library applies a monoparametric partitioning transformation to polyhedra and affine functions. This transformation is a subset of the parametric sized tiling transformation, specialized for the case where shapes depend only on a single parameter. Unlike in the general case, the resulting sets and functions remain in the polyhedral model.
• URL: https://github.com/guillaumeiooss/MPP
• Contacts: Guillaume Iooss, Christophe Alias, Sanjay Rajopadhye

6.1.7 ProbZelus

• Keywords: Synchorous language, Probability
• Functional Description: ProbZelus is a synchronous probabilistic programming language built on top of Zelus a dataflow language à la Scade/Lustre. ProZelus offers several streaming inference techniques including a semi-symbolic inference algorithm based on delayed sampling.
• URL: https://github.com/IBM/probzelus
• Authors: Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, Michael Carbin
• Contact: Guillaume Baudart
• Partners: CSAIL, MIT, IBM

Specifying and compiling the modular reset construct in Coq.

In the original Lustre language, the only way to reset the internal state of an instantiated function is to propagate and test explicit reset signals. Later languages, like Lucid Synchrone and Scade, provide a construct for resetting an instance modularly (it works for any function) and efficiently (testing occurs only at the point of instantiation). L. Brun's thesis work focused on formalizing and compiling this construct in Coq with end-to-end correctness proofs. He introduced a novel semantic rule for adding the reset construct to an existing language, a new intermediate language that allows sequenced manipulations of shared state, and a proof based on making explicit intermediate memory manipulations. This work was presented in January at the 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020) in New Orleans 12. After an initial cancellation due to the first lockdown, L. Brun defined his thesis in July 20.

Adding enumerated types

Modern dataflow languages, like Lucid Synchrone and Scade, allow users to declare enumerated types and use them in constructions for sampling and conditional activation. This feature is not only useful in itself, but also provides a target for the compilation of advanced features like state machines  28. This year, T. Bourke and L. Brun added enumerated types to the Vélus compiler. This involved generalizing the syntax and semantics of the if, merge, and when operators; adapting passes for optimizing and initializing sequential code; and adapting the interface with CompCert. We replaced the hard-coded bool type with a pre-declared enumerated type of two elements. This simplifies the semantics and compilation passes, but requires extra work to treat standard operators like not, and, and or, which are inefficient if implemented by branching statements rather than machine operations. This work provides a solid basis for the thesis work of B. Pesin and will eventually appear in the publicly available compiler.

Non-normalized Lustre.

Much of our previous work has focused on a subset of “normalized” programs where the form of expressions and equations is constrained to facilitate compilation. Last year, during P. Jeanmaire's M2 internship, we generalized the definitions of syntax and semantics in our prototype compiler to accept non-normalized programs, and added a compilation pass called transcription to convert a normalized program in this richer syntax into the syntax used by downstream passes. This year, during B. Pesin's M2 internship, we implemented the passes to normalize programs in the richer syntax. Our implementation operates in two phases. The first simplifies the abstract syntax tree by unnesting delay operators and function instances, and distributing other operators over lists. The second replaces initialization expressions in delay operators by constant terms, introducing extra registers per clock rate to determine when initialization should occur. The correctness proofs involved showing that static clock annotations corresponded with the semantics of the program, and also that a certain notion of variable dependency is preserved by compilation passes. A report on this work was accepted to appear in the 32nd edition of the Journées Francophones des Langages Applicatifs (JFLA 2021).

Harmonic clocks

We studied the extension of a synchronous language with periodic harmonic clocks based on the work of Mandel et al. 26, 35, 27, 33, 34 on n-synchrony and the extension proposed by Forget et al. 30

Mandel et al. considered a language with periodic clocks expressed as ultimately periodic binary sequences. The decision procedures (equality, inclusion, precedence) for such an expressive language can be very costly. It is thus sometimes useful to apply an envelope-based abstraction, that is, one where sets of clocks are represented by a rational slope and an interval. Forget considered simpler “harmonic” clocks. His decision procedures conincide with those for the envelope-based abstraction but without any loss of information. During his M2 internship, B. Pauget continued this line of work by extending the input language of the Vélus Lustre compiler with harmonic clocks. This work was the starting point for the proposal of a new intermediate language for a synchronous compiler that is capable of exploiting clock information to apply agressive optimizations and generate parallel code.

New Intermediate Language MObc (Multi Object Code)

This intermediate language is reminiscent of the intermediate Obc language used in the Vélus and Heptagon compiler, but with some important differences and new features. MObc permits a synchronous function to be represented as a set of named state variables and possibly nested blocks with a partial ordering which express the way blocks can and must be called. In comparison, Obc represents a synchronous function as a set of state variables and a transition function that is itself written in a sequential language. Each block comprises a set of equations in Single Static Assignment (SSA) form, that is, exactly one equation per variable, so as to simplify the implementation of a number of classic optimizations (for example, constant propagation, inlining, common sub-expression elimination, code specialisation). Then, every block is translated into a step function (e.g., a C function). This intermediate language has been designed to facilitate the generation of code for a real-time OS and a multi-core target. This work exploits two older results: the article of Caspi et al. 25 that introduces an object representation for synchronous nodes and a “scheduling policy” that specifies how their methods may be called, and; the work of Pouzet et al. 36 on the calculation of input/output relations to merge calculations. We are preparing and article on this subject.

Scheduling and code generation for periodic streams

In this approach, the top-level node of a Lustre program is distinguished from inner nodes. It may contain special annotations to specify the triggering and other details of node instances from which separate “tasks” are to be generated. Special operators are introduced to describe the buffering between top-level instances. Notably, different forms of the when and current operators are provided. Some of the operators are under-specified and a constraint solver is used to determine their exact meaning, that is, whether the signal is delayed by zero, one, or more cycles of the receiving clock, which depends on the scheduling of the source and destination nodes. Scheduling is formalized as a constraint solving problem based on latency constraints between some pairs of input/outputs that are specified by the designer.

G. Iooss prototyped these ideas in the Heptagon compiler. He implemented a code generation scheme based on translating the extended operators into combinations of standard Lustre operators so as to reuse the existing compiler backend. While we learned much from these experiments, they also revealed that the code generated in this way tended to contain very many nested branching structures. This work was described in 22.

Continuing this work, and building on ideas from Prelude  29 and the n-synchronous model  33, T. Bourke began work on a new prototype compiler for a simplified version of the source language. The new source language is based on two main design designs. First, clocks no longer contain a phase component, they simply specify the rate (the inverse of the period). This simplifies the definition of clock equality and the types of sampling operators. Second, explicit buffer operators are no longer required. Rather, the notion “synchronous” flows is relaxed and more emphasis is placed on causality. These two changes lead to a new compilation scheme based on periodically writing and reading shared variables.

This work is funded by a direct industrial contract with Airbus.

Distribution of the language

The language, its compiler and examples (release 2.1) are now on GitHub: https://github.com/INRIA/zelus. It is also available as an OPAM package. All the installation machinery has been greatly simplified.

Set-based simulation of Zelus programs

In collaboration with Francois Bidet (PhD. student under the supervision of Sylvie Putot and Eric Goubault from Ecole polytechnique), we are developing a method to perform set-based simulation of Zelus program. Set-based simulation goes beyond concrete simulation (the default simulation mode of all existing hybrid system modeling languages). Instead of computing one trajectory, it computes a set of trajectories or flowpipes at once, replacing a possibly unbounded number of concrete simulations. It is also able to deal with models with partially known parameters and inputs.

Very little tools currently deal with models expressed modularily (as the parallel and hierarchical composition of subsystems, with function application and the mix between a software model and ODEs, for example). A prototype is under way. Set based simulation is done on the intermediate language generated by Zelus, that is a collection of tarnsition functions acting on a state.

Property Based Testing of Hybrid Programs

Property-based program testing involves checking an executable specification by running many tests. We build on the work of Georgios Fainekos and Alexandre Donzé, and take inspiration from earlier work by Nicolas Halbwachs, to write a Zélus library of synchronous observers with a quantitative semantics that can be used to specify properties of a system under test. We implemented several optimization algorithms for producing test cases, some of which are gradient-based. This year, we have studied the use SUNDIALS CVODEs (sensitivity analysis) to find more falsification examples and faster.

7.6.1 Reactive Probabilistic Programming

Synchronous languages were introduced to design and implement real-time embedded systems with a (justified) enphasis on determinacy. Yet, they interact with a physical environment that is only partially known and are implemented on architectures subject to failures and noise (e.g., channels, variable communication delays or computation time). Dealing with uncertainties is useful for online monitoring, learning, statistical testing or to build simplified models for faster simulation. Actual synchronous and languages provide limited support for modeling the non-deterministic behaviors that are omnipresent in embedded systems.

In collaboration with Louis Mandel (IBM), Erik Atkinson, Michael Carbin and Benjamin Sherman (MIT). We have designed ProbZelus, an extension of Zelus with probabilistic constructs to model uncertainties and perform inference-in-the-loop. The language makes it possible to describe probabilistic models in interaction with an observable environment. At runtime, a set of inference techniques can be used to learn the distributions of model parameters from observed data.

ProbZelus, is the first synchronous probabilistic programming language,combining language constructs for streams (reactivity) with those for probabilistic programming thus enablinginference-in-the-loop. We gave a measure-based co-iterative semantics for ProbZelus that forms the basis of a compiler and demonstrate a semantics-preserving compilation strategy to a first-order functional language: $\mu F$.

We defined the semantics of multiple inference algorithms on $\mu F$ including particle filtering and delayed sampling: a semi-symbolic inference scheme. We then introduced a novel streaming delayed sampling implementation which enables partial exact inference over infinite streams in bounded memory for a large class of models.

ProbZelus is implemented on top of Zelus and available on Github9. The main article Reactive Probabilistic Programming was presented the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020) 1 and a short introduction to ProbZelus was presented at the Journées Francophones des Langages Applicatifs (JFLA 2020) 18.

7.6.2 Compiling Stan to Generative Probabilistic Languages

Stan is a probabilistic programming language that is popular in the statistics community, with a high-level syntax for expressing probabilistic models. Stan differs by nature from generative probabilistic programming languages like Church,Anglican, or Pyro. We proposed a comprehensive compilation scheme to compile any Stan model to a generative language and proved its correctness. We use our compilation scheme to build two new backends for the Stanc3 compiler targeting Pyro and NumPyro. Experimental results show that the NumPyro backend yields significant speedup compared to Stan on existing benchmarks.

Our compiler leverages the rich set of Pyro and Numpyro features for Stan users. Building on Pyro we thus extended Stan with support for explicit variational inference guides and deep probabilistic models, i.e., probabilistic models involving neural networks. The compiler is available on GitHub10 and an article is currently under submission.

Collaboration with Airbus

Our work on multi-clock Lustre programs is funded by a contract with Airbus.

9.1.1 FP7 & H2020 Projects

9.2.1 ANR

The ANR JCJC project “FidelR” led by T. Bourke began in 2020 and continues for four years.

9.2.2 FUI: Fonds unique interministériel

9.2.3 Programme d'Investissements d'Avenir (PIA)

9.2.4 Others

10.1.1 Scientific events: organisation

10.1.2 Scientific events: selection

10.1.3 Journal

10.2.1 Teaching

• Marc Pouzet is Director of Studies for the CS department, at ENS.
• Licence : M. Pouzet & T. Bourke: “Operating Systems” (L3), Lectures and TDs, ENS, France.
• Master : M. Pouzet, G. Baudart, & T. Bourke, “Models and Languages for Reactive Systems” (M1), Lectures and TDs, ENS, France.
• Master: M. Pouzet & T. Bourke & G. Baudart: “Synchronous Systems” (M2), Lectures and TDs, MPRI, France
• Master: M. Pouzet: “Synchronous Reactive Languages” (M2), Lectures, Master COMASIC (École Polytechnique) and FIL (Université Paris-Sud, Saclay), France
• Master: T. Bourke: “A Programmer’s introduction to Computer Architectures and Operating Systems" (M1), 32h, École Polytechnique, France
• Master: G. Baudart: “Synchronous Programming” (M2), TDs, Université de Paris, France
• Bachelor: T. Bourke: “A Programmer’s introduction to Computer Architectures and Operating Systems" (L2), 32h, École Polytechnique, France
• Internships T. Bourke participated in reviewing the L3 and M1 internships of students at the ENS, France.

10.2.2 Supervision

• PhD: Lélio Brun, under review, supervised by T. Bourke and M. Pouzet, defended in June 2020.
• PhD in progress: Ismail Lakhim-Bennani, 2nd year, supervised by M. Pouzet, G. Frehse, and T. Bourke.
• PhD in progress: Paul Jeanmaire, 1st year, supervised by T. Bourke and M. Pouzet.
• PhD in progress: Baptiste Pauget, 1st year, supervised by M. Pouzet. CIFRE (ANSYS Toulouse and INRIA PARKAS).
• PhD in progress: Basile Pesin, 1st year, supervised by T. Bourke and M. Pouzet.

International journals

• 12 articleTimothyT. Bourke, LélioL. Brun and MarcM. Pouzet. Mechanized semantics and verified compilation for a dataflow synchronous language with resetProceedings of the ACM on Programming Languages4POPLJanuary 2020, 1-29
  HALDOIback to text
• 13 article AlbertA. Cohen and JieJ. Zhao. Flextended Tiles: a Flexible Extension of Overlapped Tiles for Polyhedral Compilation ACM Transactions on Architecture and Code Optimization January 2020
  HAL DOI

International peer-reviewed conferences

• 14 inproceedings GuillaumeG. Baudart, LouisL. Mandel, EricE. Atkinson, BenjaminB. Sherman, MarcM. Pouzet and MichaelM. Carbin. Reactive probabilistic programming PLDI 2020 - 41th ACM SIGPLAN International Conference in Programming Language Design and Implementation London / Virtual, United Kingdom June 2020
  HAL DOI
• 15 inproceedings Best paper AlanA. Cha, ErikE. Wittern, GuillaumeG. Baudart, James C.J. Davis, LouisL. Mandel and Jim A.J. Laredo. A Principled Approach to GraphQL Query Cost Analysis ESEC/FSE 2020 - 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering Sacramento / Virtual, United States https://2020.esec-fse.org/ November 2020
  HAL DOI back to text
• 16 inproceedings LorenzoL. Chelini, AndiA. Drebes, OleksandrO. Zinenko, AlbertA. Cohen, NicolasN. Vasilache, TobiasT. Grosser and HenkH. Corporaal. Progressive Raising in Multi-level IR CGO 2021 : International Symposium on Code Generation and Optimization International Conference on Code Generation and Optimization (CGO) Seoul / Virtual, South Korea February 2021
  HAL back to text
• 17 inproceedings LenaL. Grimm, StevenS. Smyth, AlexanderA. Schulz-Rosengarten, ReinhardR. von Hanxleden and MarcM. Pouzet. From Lustre to Graphical Models and SCCharts FDL 2020 - Forum for Specification and Design Languages 2020 Forum for Specification and Design Languages (FDL) Kiel, Germany http://fdl-conference.org/ November 2020
  HAL DOI

Conferences without proceedings

• 18 inproceedings GuillaumeG. Baudart, LouisL. Mandel, MarcM. Pouzet, EricE. Atkinson, BenjaminB. Sherman and MichaelM. Carbin. Programmation d'Applications Réactives Probabilistes JLFA 2020 - Journées Francophones des Langages Applicatifs Gruissan, France http://jfla.inria.fr/jfla2020.html January 2020
  HAL back to text
• 19 inproceedings Nuno MiguelN. Nobre, AndiA. Drebes, GrahamG. Riley and AntoniuA. Pop. Bounded Stream Scheduling in Polyhedral OpenStream IMPACT 2020 - 10th International Workshop on Polyhedral Compilation Techniques Bologna, Italy January 2020
  HAL

Doctoral dissertations and habilitation theses

• 20 thesis LélioL. Brun. Mechanized semantics and verified compilation for a dataflow synchronous language with reset Université Paris sciences et lettres July 2020
  HAL back to text

Reports & preprints

• 21 misc GuillaumeG. Baudart, JavierJ. Burroni, MartinM. Hirzel, LouisL. Mandel and AvrahamA. Shinnar. Extending Stan for Deep Probabilistic Programming January 2021
  HAL
• 22 misc GuillaumeG. Iooss, MarcM. Pouzet, AlbertA. Cohen, DumitruD. Potop-Butucaru, JeanJ. Souyris, VincentV. Bregeon and PhilippeP. Baufreton. 1-Synchronous Programming of Large Scale, Multi-Periodic Real-Time Applications with Functional Degrees of Freedom March 2020
  HAL back to text

Other scientific publications

• 23 misc AndiA. Drebes, LorenzoL. Chelini, OleksandrO. Zinenko, AlbertA. Cohen, HenkH. Corporaal, TobiasT. Grosser, KanishkanK. Vadivel and NicolasN. Vasilache. TC-CIM: Empowering Tensor Comprehensions for Computing-In-Memory Bologna, Italy January 2020
  HAL