7.1.1 TRAHRHE

• Name:
  Trahrhe expressions and applications in loop optimization
• Keywords:
  Polyhedral compilation, Code optimisation, Source-to-source compiler
• Functional Description:
  This software includes a mathematic kernel for computing Trahthe expressions related to iteration domains, as well as extensions implementing source-to-source transformations of loops for applying optimizations based on Trahrhe expressions.
• News of the Year:
  Two extensions have been implemented, that are new alternatives for the runtime computation of trahrhe expressions values, and that may significantly improve the time performance when using the generated C header files: (1) when activated, adds a precision correction mechanism. Useful when the complexity of the trahrhe expressions yields annoying precision issues. Moreover, it makes the use of MPC useless and thus yields significantly better time performance than when using MPC. (2) when activated, avoids the computation of the trahrhe expressions by solving polynomial equations, and uses instead a dichotomic search mechanism to get the current integer values of the trahrhe expression, through invocations to the ranking polynomials. Another improved dichotomic search may also be activated, that uses the history of previous invocations to accelerate even more the search.
• URL:
  https://­webpages.­gitlabpages.­inria.­fr/­trahrhe
• Contact:
  Philippe Clauss

7.1.2 CFML

• Name:
  Interactive program verification using characteristic formulae
• Keywords:
  Coq, Software Verification, Deductive program verification, Separation Logic
• Functional Description:
  The CFML tool supports the verification of OCaml programs through interactive Coq proofs. CFML proofs establish the full functional correctness of the code with respect to a specification. They may also be used to formally establish bounds on the asymptotic complexity of the code. The tool is made of two parts: on the one hand, a characteristic formula generator implemented as an OCaml program that parses OCaml code and produces Coq formulae, and, on the other hand, a Coq library that provides notations and tactics for manipulating characteristic formulae interactively in Coq.
• News of the Year:
  Addition of lemmas and tactics for proving characteristic formulae sound with respest to the semantics in a foundational way.
• URL:
  http://­www.­chargueraud.­org/­softs/­cfml/
• Contact:
  Arthur Charguéraud
• Participants:
  Arthur Charguéraud, Armaël Guéneau, François Pottier

7.1.3 openCARP

• Name:
  Cardiac Electrophysiology Simulator
• Keyword:
  Cardiac Electrophysiology
• Functional Description:
  openCARP is an open cardiac electrophysiology simulator for in-silico experiments. Its source code is public and the software is freely available for academic purposes. openCARP is easy to use and offers single cell as well as multiscale simulations from ion channel to organ level. Additionally, openCARP includes a wide variety of functions for pre- and post-processing of data as well as visualization.
• URL:
  https://­opencarp.­org/
• Contact:
  Vincent Loechner
• Participants:
  Arun Thangamani, Stephane Genaud, Bérenger Bramas, Tiago Trevisan Jost, Raphael Colin
• Partner:
  Karlsruhe Institute of Technology

7.1.4 SPECX

• Name:
  SPEculative eXecution task-based runtime system
• Keywords:
  HPC, Parallelization, Task-based algorithm
• Functional Description:
  Specx (previously SPETABARU) is a task-based runtime system for multi-core architectures that includes speculative execution models. It is a pure C++11 product without external dependency. It uses advanced meta-programming and allows for an easy customization of the scheduler. It is also capable to generate execution traces in SVG to better understand the behavior of the applications.
• News of the Year:
  During 2022, Specx has been improved to support heterogeneous and distributed computing nodes. It is now possible to create CPU/GPU tasks and Specx will manage the data transfers between the host and devices. In distributed memory, the communications are now part of the task graph. All of these novelties make Specx a good candidate to develop modern HPC applications in C++.
• URL:
  https://­gitlab.­inria.­fr/­bramas/­specx
• Contact:
  Bérenger Bramas

8.1.1 Improvements of the C programming language

Participants: Jens Gustedt.

For the upcoming version of the C standard, C23, we contributed with a large number of proposals that are now integrated in the draft that has been presented by ISO JTC1/SC22 to the national bodies (NB). The final adjustment of the content according to more than 300 NB comments will be made end of Jan, 2023.

This year's contributions that were integrated to C23 are as follows: 192223242526303133343536373842. Over all, out of the about 50 points that are listed in the change history of C23 (Annex M) as major additions, our contributions include:

• adding new keywords such as bool, static_assert, true, false, thread_local and others, and allowed implementations to provide macros for the older spelling with a leading underscore followed by a capital letter as well as defining old and new keywords as macros to enable transition of programs easily;
• removing integer width constraints and obsolete sign representations (so-called “1’s complement” and “sign-magnitude”);
• removing support for function definitions with identifier lists;
• harmonization with ISO/IEC 9945 (POSIX):
  • integration of functions: gmtime_r, localtime_r;
• adding version test macros to library headers that contained changes to aid in upgrading and portability to be used alongside the __STDC_VERSION__ macro;
• including the attributes:
  • [[reproducible]], for marking function types for which inputs may always produce predictable output if given the same input (e.g., cached data) but for which the order of such calls still matter;
  • [[unsequenced]], for marking function types which always produce predictable output and have no dependencies upon other data (and other relevant caveats);
• allowing compound literals to may also include storage-class specifiers as part of the type to change their lifetime (and possibly turn it into a constant expression);
• adding the constexpr specifier for object definitions and improved what is recognized as a constant expression in conjunction with the constexpr storage-class specifier;
• adding a nullptr constant and a nullptr_t type with a well-defined underlying representation identical to a pointer to void;
• allowing Unicode identifiers in syntax following Unicode Standard Annex, UAX #31;
• allowing certain type definitions (i.e., exact-width integer types such as int128_t), bit-precise integer types, and extended integer types may exceed the normal boundaries of intmax_t and uintmax_t for signed and unsigned integer types, respectively;
• mandating support for call_once;
• enhancing the auto type specifier for single object definitions using type inference;
• adding support for additional time bases, as well as timespec_getres, in <time.h>;
• adding an unreachable feature which has undefined behavior if reached during program execution.

Additionally, the following proposals have been applied that change aspects that are less visible to the end-user of the language:

• Disambiguating the storage class of some compound literals;
• Types and sizes;
• Indeterminate Values and Trap Representations;
• Removing ATOMIC_VAR_INIT;
• Properly defining blocks as part of the grammar.

Other proposals have been discused have been seen favorable for integration into a future version of the standard: 29272841, see also 28323940.

In addition to the C standard we continued our work for the new technical specification TS 6010 18 for a sound and verifiable memory model that is based on provenance, that is on the unique attribution of a storage instance to any valid pointer value.

8.1.2 Ionic Models Code Generation for Heterogeneous Architectures

Participants: Arun Thangamani, Tiago Trevisan Jost, Raphaël Colin, Vincent Loechner, Bérenger Bramas, Stéphane Genaud.

We participate in the research and development of a cardiac electrophysiology simulator in the context of the MICROCARD European project. The CAMUS team provides their optimizing compiler expertise to build a bridge from a high-level language convenient for ionic model experts (called EasyML) to a code that will run on future exascale supercomputers. We aim to generate multiple parallel versions of the ionic simulation to exploit the various parallel computing units that are available in the target architecture nodes (SIMD, multicore, GPU, etc.).

The frontend that we contributed to in 2022 is based on the MLIR extensible compiler. We developed a Python script generating MLIR code from an EasyML ionic model description and integrated it in the openCARP project (7.1.3). We have achieved the automatic vectorization of the ionic code and this work is to be published and presented early next year at the CGO '23 conference. The follow-up work concerns the generation of code for GPUs and for multiple heterogeneous architectures, in coordination with the developments carried out by the STORM team (Inria Bordeaux) on the runtime distributed environment (StarPU).

8.1.3 A Polyhedral Programmable Scheduler

Participants: Tom Hammer, Vincent Loechner.

Scheduling is the central operation in the polyhedral compilation chain: finding the best execution order of loop iterations for optimizing the resulting code. Scheduling algorithms rely on the fundamental Farkas lemma to iteratively compute the schedule matrices associated to each statement of the input code.

The goal of this work is to allow polyhedral compilation experts to produce highly customizable scheduling algorithms in an efficient manner, without having to develop from scratch a new Farkas lemma-based solver and the whole polyhedral compilation toolchain. It will be included in the PeriScop suite (OpenScop, CLooG, PIPLib, etc.). We started to design a specific mini-language (DSL) that allows the user to specify and prioritize its objectives.

This is Tom Hammer's internship main work, in connection with the MICROCARD project that will benefit from the existence of such a scheduling algorithm generator. We wrote a first paper that will be presented to the community during the IMPACT '23 workshop collocated with the HiPEAC '23 conference.

8.1.4 Superloop Scheduling

Participants: Vincent Loechner, Alain Ketterlin, Cedric Bastoul.

This work predates Cédric Bastoul's leave (he is currently detached from the team and working at Qualcomm).

In polyhedral compilation, discovering the best polyhedral schedules remains a grand challenge reinforced by the need to build affine functions. Automatic techniques based on solving systems of affine constraints and/or composing affine scheduling primitives are limited, either by the affine modeling or by their primitive set.

We propose a radically new approach to affine scheduling construction called superloop scheduling. The main idea is to leverage basic-block-level instruction reordering compilation techniques, and then to agglomerate statement instances into "super" loops offered by modern trace analysis tools. We will present this work at the IMPACT '23 workshop.

8.1.5 Automatic Task-Based Parallelization using Source to Source Transformations

Participants: Garip Kusoglu, Bérenger Bramas, Stéphane Genaud.

We worked on a new approach to automatically parallelize any application written in an object-oriented language. The main idea is to parallelize a code as an HPC expert would do it using the task-based method. To do so, we created a new source-to-source compiler on top of Clang-LLVM called APAC. APAC is able to insert tasks in a source-code by evaluating data access and generating the correct dependencies. In 2021, we improved our compiler with a new method to automatically build performance models able to predict the execution time of the tasks. Early results  50 have allowed the activation of only those tasks with sufficient granularity. This work has been however put on stand-by early 2022 after the resignation of the first year student who worked on it. A summer internship has explored the opportunity to transition the transformation framework used from Clang to OptiTrust (developed in the team) and a PostDoc will resume the work in 2023.

8.1.6 Parallel kinetic scheme in complex toroidal geometry

Participants: Bérenger Bramas.

Bérenger Bramas collaborated with the TONUS team on a solver for the conservative transport equation with variable coefficients in complex toroidal geometries. He applied several optimizations at algorithm or implementation level to obtain high performance 45.

8.1.7 Automatic vectorization of static computational kernels

Participants: Hayfa Tayeb, Bérenger Bramas.

Compilers can automatically vectorize codes if there are zero to few data transformations to perform. However, when memory accesses are not contiguous, non linear or even chaotic, compilers usually fail. This is why we proposed a new method where we transform the dependency graph into a graph made of vectorial instructions. Our different layers aim at minimizing the number of instructions, especially data transformation instructions, that are needed to get a vectorized code. To do so we have developed the Autovesk compiler, which converts scalar C++ code into a vectorized C++ equivalent. We tested the performance of our approach by vectorizing different types of kernels, and we showed that we outperform the GNU C++ compiler by a speedup factor of 4 on average and up to 11. This work is described in a preprint 44.

8.1.8 Algebraic Loop Tiling

Participants: Clément Rossetti, Philippe Clauss.

We are currently developing a new approach for loop tiling, where tiles are no longer characterized by the sizes of their edges, but by their volumes, i.e., the number of embedded iterations. Algebraic tiling is particularly dedicated to parallel loops, where load balancing among the parallel threads is crucial for reaching high runtime performance.

Rectangular tiles of quasi-equal volumes, but of different shapes, are obtained thanks to mathematical computations based on the inversion of Ehrhart polynomials. The Trahrhe software (see Section 7.1.1) is dedicated to such computations, and to the automatic generation of header files in C, that can be used for the runtime computation of the algebraic tile bounds.

Clément Rossetti has started his related PhD work in October 2022. Integration of algebraic loop tiling into the source-to-source polyhedral compiler Pluto has been initiated by Clément. Any Pluto user will get access to automatic algebraic tiling thanks to the new Pluto flag -atiling.

A paper presenting for the first time the algebraic loop tiling technique will be presented at IMPACT 2023 12.

8.2.1 An efficient particle tracking algorithm for large-scale parallel pseudo-spectral simulations of turbulence

Participants: Bérenger Bramas.

The statistical studies of particles moving in a fluid is a widely used technic to study turbulences. We used this method to perform direct numerical simulations (DNS) of homogeneous isotropic turbulence and investigated the dynamics of different particle shapes at different scales in turbulence using a filtering approach. Bérenger Bramas collaborated on this project to design a particle interaction system able to work efficiently on large supercomputers 10. The work is implemented in a software called TurTLE.

8.2.2 Multi-GPU parallelization of the Lattice Boltzmann Method

Participants: Clément Flint, Philippe Helluy, Bérenger Bramas, Stéphane Genaud.

In the context of the ITI IRMIA++, we work on the parallelization of the Lattice Boltzmann Methodology (LBM), a general framework for constructing efficient numerical fluid simulations. This method is well-suited to GPU computations. However, a number of GPU implementations are limited in the simulation scale because the data size that has to be handled is constrained by the GPU memory. We have proposed a parallelization based on the division of the lattice structure into multiple subsets that can be executed individually on corresponding data sets. Our implementation enables the distribution of the computations on multiple CPUs and GPUs using StarPU, hence relaxing the constraint on GPU memory. This work has been published in 15.

8.3.1 Ordered Read-Write Locks for applications

Participants: Jens Gustedt.

In the context of a project with ICube's Mécaflu team we use our implementation of Ordered Read-Write Locks (ORWL) 4 to integrate parallelism into an already existing Fortran application that computes floods in the geographical region that is subject to the study. That parallelization has been achieved by using ORWL on a process level. It connects several executables that run the legacy code in separate processes and is able to launch such a stiched execution in shared memory and distributed contexts. One of the steps to this goal has been to design a specific decomposition of geological data 9.

8.3.2 Scheduling multiple task-based applications on distributed heterogeneous computing nodes

Participants: Jean Etienne Ndamlabin, Bérenger Bramas.

The size, complexity and cost of supercomputers continue to grow making any waste more critical than in the past. Consequently, we need methods to reduce the waste coming from the users' choices, badly optimized applications or heterogeneous workloads during executions. In this context, we started activities on the scheduling of several task-based applications on given hardware resources. Specifically, we created load balancing heuristics to distribute the task-graph over the processing units. We are creating a new scheduler in StarPU to validate our approach. We will perform performance evaluation in the next stage, first using a simulator (SimdGrid) and then on real hardware.

8.3.3 Multreeprio: a scheduler for task-based applications on heterogeneous hardware

Participants: Hayfa Tayeb, Bérenger Bramas.

In the context of the TEXTAROSSA project, we investigated how the Heteroprio scheduler can be improved. We created a new scheduler called Multreeprio where the tasks can have multiple priorities, instead of having priorities for each type of tasks. We created different heuristics to assign priorities based on the workload, the type of processing units or even the locality. Preliminary results have been presented at COMPAS'22 17.

8.3.4 Automatic Configuration of the Heteroprio Scheduler

Participants: Clément Flint, Ludovic Paillat, Bérenger Bramas.

Heteroprio is a scheduler designed for heterogeneous machines that was implemented in StarPU, a task-based execution engine on heterogeneous multicore architectures. To use this scheduler, the users must tune it by providing priorities for the different types of tasks that exist in their applications. This requires a significant programming effort and the given configuration might be inefficient because of possible incorrect intuition from the users or because a single application might have different execution scenarios that would execute better with different priorities. Clément Flint and Bérenger Bramas created and evaluated several heuristics to configure Heteroprio automatically. These heuristics are simple and can be evaluated without analyzing the complete graph of tasks. The results have been published 8.

8.4.1 Survey of Separation Logic for Sequential Programs

Participants: Arthur Charguéraud.

Arthur Charguéraud has written the manuscript for his Habilitation (HDR), titled A Modern Eye on Separation Logic for Sequential Programs, to be defended in Febuary 2023. This manuscript provides a survey of Separation Logic for sequential programs, in the line of the tutorial article published at ICFP'20  48. It also gives a complete introduction of the working of the CFML tool (7.1.2), as well as its extensions for reasoning about time bounds (PhD thesis of Armaël Guéneau) and reasoning about space bounds (PhD thesis of Alexandre Moine).

8.4.2 Formal Verification of a Transient Data Structure

Participants: Arthur Charguéraud.

Prior to his PhD co-advised by Arthur Charguéraud and François Pottier (Inria Paris, team Cambium), Alexandre Moine worked during his M2 internship on the specification and verification of the functional correctness and time complexity of a transient stack, using CFML (7.1.2). A transient data structure is a package of an ephemeral data structure, a persistent data structure, and fast conversions between them. The transient stack studied is a scaled-down version of Sek, a general-purpose sequence data structure implemented in OCaml. Internally, it relies on fixed-capacity arrays, or chunks, which can be shared between several ephemeral and persistent stacks. Dynamic tests are used to determine whether a chunk can be updated in place or must be copied: a chunk can be updated if it is uniquely owned or if the update is monotonic. There are very few examples of verified transient data structures in the literature, let alone examples of transient data structures whose correctness and time complexity are verified. This result has been published at the conference CPP'22 11 and has received one of the three Distinguished Paper Awards.

8.4.3 Formal Proof of Space Bounds for Garbage-Collected Programs

Participants: Arthur Charguéraud.

Alexandre Moine, co-advised by Arthur Charguéraud and François Pottier, has presented a novel, high-level program logic for establishing space bounds in Separation Logic, for programs that execute with a garbage collector. A key challenge is to design sound, modular, lightweight mechanisms for establishing the unreachability of a block. In the setting of a high-level, ML-style language, a key problem is to identify and reason about the memory locations that the garbage collector considers as roots. We demonstrate the expressiveness and tractability of the proposed program logic via a range of examples, including recursive functions on linked lists, objects implemented using closures and mutable internal state, recursive functions in continuation-passing style, and three stack implementations that exhibit different space bounds. These last three examples illustrate reasoning about the reachability of the items stored in a container as well as amortized reasoning about space. All the results are proved in Coq on top of Iris. This work has been accepted for publication at POPL'23 43.

8.4.4 Omnisemantics: Operational Semantics for Nondeterministic Languages

Participants: Arthur Charguéraud.

Arthur Charguéraud worked with collegues from MIT (Adam Chlipala and two of his students, Andres Erbsen and Samuel Gruetter) on a paper describing the technique of omni-semantics, a style for describing operational semantics particularly well-suited for nondeterministic languages. This technique introduces judgments that relate starting states to sets of outcomes, rather than to individual outcomes. Thus, a single derivation of these semantics for a particular starting state and program describes all possible nondeterministic executions, whereas in traditional small-step and big-step semantics, each derivation only talks about one single execution. We demonstrate how this restructuring allows for straightforward modeling of languages featuring both nondeterminism and undefined behavior. Specifically, omni-semantics inherently assert safety, i.e., they guarantee that none of the execution branches gets stuck, while traditional semantics need either a separate judgment or additional error markers to specify safety in the presence of nondeterminism. Applications presented include proofs of type soundness for lambda calculi, mechanical derivation of reasoning rules for program verification, and a forward proof of compiler correctness for terminating but potentially nondeterministic programs. All results are formalized in Coq. This work has been accepted for publication in the journal ACM Transactions on Programming Languages and Systems (TOPLAS) 21.

8.4.5 OptiTrust: Producing Trustworthy High-Performance Code via Source-to-Source Transformations

Participants: Arthur Charguéraud, Begatim Bytyqi, Guillaume Bertholon.

In 2022, we pursued the development of the OptiTrust prototype framework for producing high-performance code via source-to-source transformations. We completed a major case study: a high-performance parallel implementation of a particle-in-cell algorithm used for plasma simulations. The naive implementation of the simulation consists of about 250 lines of C code. The optimization script consists of about 150 lines of OCaml code. The execution of that script produces a highly optimized code, essentially equivalent to the one that had been implemented by hand a few years ago  46. A draft paper describing the main features of the framework and the case study is available 20.

The work on OptiTrust from Sept. 2019 to Sept. 2022 has been funded by an Inria “exploratory action”. This line of research will continue for 4 years as part of an ANR grant, starting in Oct. 2022, with Arthur Charguéraud as PI. Thomas Koehler has been hired to work as a postdoc on this project, starting in Jan. 2023, to contribute to the implementation of transformations and of static analyses to justify correctness.

The PhD topic of Guillaume Bertholon, starting in Sept 2022, consists of developing a framework for representing Separation Logic derivations and applying proof-preserving, source-to-source transformations onto those derivations. His preliminary work has been presented at the JFLA workshop 14.

9.1.1 H2020 projects

9.2.1 ANR OptiTrust

Participants: Arthur Charguéraud, Guillaume Bertholon, Jens Gustedt, Alain Ketterlin.

Turning a high-level, unoptimized algorithm into a high-performance code can take weeks, if not months, for an expert programmer. The challenge is to take full advantage of vectorized instructions, of all the cores and all the servers available, as well as to optimize the data layout, maximize data locality, and avoid saturating the memory bandwidth. In general, annotating the code with "pragmas" is insufficient, and domain-specific languages are too restrictive. Thus, in most cases, the programmer needs to write, by hand, a low-level code that combines dozens of optimizations. This approach is not only tedious and time-consuming, it also degrades code readibility, harms code maintenance, and can result in the introduction of bugs. A promising approach consists of deriving an HPC code via a series of source-to-source transformations guided by the programmer. This approach has been successfully applied in niche domains, such as image processing and machine learning. We aim to generalize this approach to optimize arbitrary code. Furthermore, the OptiTrust project aims at obtaining formal guarantees on the output code. A number of these transformations are correct only under specific hypotheses. We will formalize these hypotheses, and investigate which of them can be verified by means of static analysis. To handle the more complex hypotheses, we will transform not just code but also formal invariants attached to the code. Doing so will allow exploiting invariants expressed on the original code for justifying transformations performed at the n-th step of the transformation chain.

• Funding: ANR
• Start: October 2022
• End: September 2026
• Coordinator: Arthur Charguéraud (Inria)
• Partners: Inria team Camus (Strasbourg), Inria team TONUS (Strasbourg), Inria team Cambium (Paris), Inria team CASH (Lyon), CEA team LIST

9.2.2 ANR AUTOSPEC

Participants: Bérenger Bramas, Philippe Clauss, Stéphane Genaud, Garip Kusoglu, Michel Tching.

The AUTOSPEC project aims to create methods for automatic task-based parallelization and to improve this paradigm by increasing the degree of parallelism using speculative execution. The project will focus on source-to-source transformations for automatic parallelization, speculative execution models, DAG scheduling, and the activation mechanisms for speculative execution. With this aim, the project will rely on a source-to-source compiler that targets the C++ language, a runtime system with speculative execution capabilities, and an editor (IDE) to enable compiler-guided development. The outcomes from the project will be open-source with the objective of developing a user community. The benefits will be of great interest both for developers who want to use an automatic parallelization method, but also for high-performance programming experts who will benefit from improvements of the task-based programming. The results of this project will be validated in various applications such as a protein complexes simulation software, and widely used open-source software. The aim will be to cover a wide range of applications to demonstrate the potential of the methods derived from this project while trying to establish their limitations to open up new research perspectives.

• Funding: ANR (JCJC)
• Start: October 2021
• End: September 2025
• Coordinator: Bérenger Bramas

Member of the conference program committees

• Arthur Charguéraud was a PC member for the Symposium on Principles of Programming Languages (POPL 2022)and for the Internation Workshop on Advances in Separation Logic (ASL 2022).
• Philippe Clauss was a PC member for IMPACT 2022 (12th International Workshop on Polyhedral Compilation Techniques) and for IPDRM’2022 (Fifth Annual Workshop on Emerging Parallel and Distributed Runtime Systems and Middleware).

Reviewer

• Bérenger Bramas was a reviewer for Supercomputing (Poster), Compas, and the Conference on Mathematical Foundations of Computer Science (MFCS).
• Vincent Loechner and Philippe Clauss were reviewers for PPoPP '23 (27th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming).

10.1.1 Journal

10.1.2 Scientific expertise

• Jens Gustedt is a member of the ISO/IEC working groups ISO/IEC PL1/SC22/WG14 and WG21 for the standardization of the C and C++ programming languages, respectively.

10.1.3 Research administration

• Jens Gustedt is the head of the ICPS team for the ICube lab.
• Jens Gustedt is a member of the executive board of directors of the ICubelab, responsible for the IT and CS policy and for the coordination between the lab and the Inria center. In that function he also represents ICube in the board of the INRIA Nancy - Grand Est research center.
• Jens Gustedt is member of the steering committee of the interdisciplanary institute IRMIA++ of Strasbourg University.

10.2.1 Teaching

• Licence: Vincent Loechner, Algorithmics and programmation, 82h, L1, Université de Strasbourg, France
• Licence: Vincent Loechner, System administration, 40h, Licence Pro, Université de Strasbourg, France
• Licence: Vincent Loechner, System programming, 20h, L2, Université de Strasbourg, France
• Licence: Vincent Loechner, Parallel programming, 32h, L3, Université de Strasbourg, France
• Licence: Vincent Loechner, System administration, 40h, Licence Pro, Université de Strasbourg, France
• Master: Vincent Loechner, Real-time systems, 12h, M1, Université de Strasbourg, France
• Eng. School: Vincent Loechner, Parallel programming, 20h, Telecom Physique Strasbourg - 3rd year, Université de Strasbourg, France
• Master: Bérenger Bramas, Compilation and Performance, 24h, M2, Université de Strasbourg, France
• Master: Bérenger Bramas, Compilation, 24h, M1, Université de Strasbourg, France
• Licence: Philippe Clauss, Computer architecture, 18h, L2, Université de Strasbourg, France
• Licence: Philippe Clauss, Bases of computer architecture, 22h, L1, Université de Strasbourg, France
• Master: Philippe Clauss, Compilation, 84h, M1, Université de Strasbourg, France
• Master: Philippe Clauss, Real-time programming and system, 37h, M1, Université de Strasbourg, France
• Master: Philippe Clauss, Code optimization and transformation, 31h, M1, Université de Strasbourg, France
• Licence: Alain Ketterlin, Architecture des systèmes d'exploitation, L3 Math-Info, 38h, Université de Strasbourg, France
• Licence: Alain Ketterlin, Programmation système, L2 Math-Info, 60h, Université de Strasbourg, France
• Master: Alain Ketterlin, Preuves assistées par ordinateur, 18h, Université de Strasbourg, France
• Master: Alain Ketterlin, Compilation, 84h, Université de Strasbourg, France
• Licence: Stéphane Genaud, Algorithmics and programmation, 82h, L1, Université de Strasbourg, France
• Licence: Stéphane Genaud, Parallel programming, 30h, L3, Université de Strasbourg, France
• Master: Stéphane Genaud, Cloud and Virtualization, 12h, M1, Université de Strasbourg, France
• Master: Stéphane Genaud, Large-Scale Data Processing, 15h, M1, Université de Strasbourg, France
• Master: Stéphane Genaud, Distributed Storage and Processing, 15h, M2, Université de Strasbourg, France
• Eng. School: Stéphane Genaud, Introduction to Operating Systems, 16h, Telecom Physique Strasbourg - 1st year, Université de Strasbourg, France
• Eng. School: Stéphane Genaud, Object-Oriented Programming, 60h, Telecom Physique Strasbourg - 1st year, Université de Strasbourg, France

10.2.2 Supervision

• PhD in progress: Clément Flint, Efficient data compression for high-performance PDE solvers., advised by Philippe Helluy (TONUS), Stéphane Genaud, and Bérenger Bramas, since Nov 2020.
• PhD in progress: Arun Thangamani, Code generation for heterogeneous architectures, advised by Stéphane Genaud and Vincent Loechner, since Sept 2021.
• PhD from Oct 2022 to : Garip Kusoglu, Automatic task-based parallelization by source-to-source transformations, advised by Stéphane Genaud and Bérenger Bramas, since Oct 2021.
• PhD in progress: Alexandre Moine, Formal Verification of Space Bounds, advised by Arthur Charguéraud and François Pottier, at Inria Paris, since Oct 2021.
• PhD in progress: Hayfa Tayeb, Efficient scheduling of task-based applications under energy constraints, advised by Abdou Guermouche (HiePACS) and Bérenger Bramas, since Nov 2021.
• PhD in progress: Guillaume Bertholon, Formal Verification of Source-to-Source Transformations, is advised by Arthur Charguéraud and Jens Gustedt, since Sept 2022.
• PhD in progress: Anastasios Souris, Speculative execution in the task-based parallelization, advised by Philippe Clauss and Bérenger Bramas, since July 2022.
• PhD in progress: Clément Rossetti, Algebraic loop transformations, advised by Philippe Clauss, since Oct 2022.

10.2.3 Juries

• Arthur Charguéraud was an examiner for:
  • the PhD thesis of Adam Khayam, defended on Nov. 30, 2022, at the University of Rennes 1.
• Philippe Clauss was a reviewer for:
  • the PhD thesis of Paul Ianetta, defended on May 2, 2022, at ENS Lyon.
  • the PhD thesis of Camille Le Bon, defended on July 5, 2022, at the University of Rennes 1.
• Philippe Clauss was an examiner for:
  • the PhD thesis of Jean-Romain Luttringer, defended on Nov. 28, 2022, at the University of Strasbourg.
• Vincent Loechner was a reviewer for:
  • the PhD thesis of Van Man NGUYEN, defended on Dec. 16, 2022, at the University of Bordeaux.

10.3.1 Castor Informatique Contest

Participants: Arthur Charguéraud.

Arthur Charguéraud is a co-organizer of the Concours Castor informatique. The purpose of the Concours Castor in to introduce pupils, from CM1 to Terminale, to computer sciences. 700,000 teenagers played with the interactive exercises in November and December 2022.

10.3.2 Modern C

Participants: Jens Gustedt.

Jens Gustedt has a blog about efficient programming, in particular about the C programming language.

10.3.3 Interventions

Arthur Charguéraud visited two classes (5ème, age 12) in December, to comment on the Concours Castor Informatique, and to give a brief overview on the development of computer sciences since the introduction of the Internet, as well as on the path to becoming a programmer.

International journals

• 7 articleG.Giovanni Agosta, M.Marco Aldinucci, C.Carlos Alvarez, R.Roberto Ammendola, Y.Yasir Arfat, O.Olivier Beaumont, M.Massimo Bernaschi, A.Andrea Biagioni, T.Tommaso Boccali, B.Berenger Bramas, C.Carlo Brandolese, B.Barbara Cantalupo, M.Mauro Carrozzo, D.Daniele Cattaneo, A.Alessandro Celestini, M.Massimo Celino, I.Iacopo Colonnelli, P.Paolo Cretaro, P.Pasqua D’ambra, M.Marco Danelutto, R.Roberto Esposito, L.Lionel Eyraud-Dubois, A.Antonio Filgueras, W.William Fornaciari, O.Ottorino Frezza, A.Andrea Galimberti, F.Francesco Giacomini, B.Brice Goglin, D.Daniele Gregori, A.Abdou Guermouche, F.Francesco Iannone, M.Michal Kulczewski, F.Francesca Lo Cicero, A.Alessandro Lonardo, A.Alberto Martinelli, M.Michele Martinelli, X.Xavier Martorell, G.Giuseppe Massari, S.Simone Montangero, G.Gianluca Mittone, R.Raymond Namyst, A.Ariel Oleksiak, P.Paolo Palazzari, P. S.Pier Stanislao Paolucci, F.Federico Reghenzani, C.Cristian Rossi, S.Sergio Saponara, F.Francesco Simula, F.Federico Terraneo, S.Samuel Thibault, M.Massimo Torquati, M.Matteo Turisini, P.Piero Vicini, M.Miquel Vidal, D.Davide Zoni and G.Giuseppe Zummo. Towards EXtreme scale technologies and accelerators for euROhpc hw/Sw supercomputing applications for exascale: The TEXTAROSSA approach.Microprocessors and Microsystems: Embedded Hardware Design 95November 2022, 104679
  HALDOIback to text
• 8 articleC.Clément Flint, B.Bérenger Bramas and L.Ludovic Paillat. Automated prioritizing heuristics for parallel task graph scheduling in heterogeneous computing.PeerJ Computer ScienceSeptember 2022
  HALback to text
• 9 articleS.Sleimane Hariri, S.Sylvain Weill, J.Jens Gustedt and I.Isabelle Charpentier. A balanced watershed decomposition method for rain-on-grid simulations in HEC-RAS.Journal of Hydroinformatics242January 2022, 315–332
  HALback to text
• 10 articleC.Cristian Lalescu, B.Bérenger Bramas, M.Markus Rampp and M.Michael Wilczek. An efficient particle tracking algorithm for large-scale parallel pseudo-spectral simulations of turbulence.Computer Physics Communications278September 2022, 108406
  HALDOIback to text

International peer-reviewed conferences

• 11 inproceedingsA.Alexandre Moine, A.Arthur Charguéraud and F.François Pottier. Specification and Verification of a Transient Stack.CPP 2022 - 11th ACM SIGPLAN International Conference on Certified Programs and ProofsPhiladelphia, United StatesJanuary 2022
  HALDOIback to text
• 12 inproceedingsC.Clément Rossetti and P.Philippe Clauss. Algebraic Tiling.IMPACT 2023, 13th International Workshop on Polyhedral Compilation TechniquesIMPACT 2023, 13th International Workshop on Polyhedral Compilation TechniquesToulouse, FranceJanuary 2023
  HALback to text
• 13 inproceedingsA.Arun Thangamani, T.Tiago Trevisan, V.Vincent Loechner, S.Stephane Genaud and B.Bérenger Bramas. Lifting Code Generation of Cardiac Physiology Simulation to Novel Compiler Technology.Proceedings of the 21st ACM/IEEE International Symposium on Code Generation and Optimization (CGO ’23)21st ACM/IEEE International Symposium on Code Generation and Optimization (CGO ’23)Montréal Québec, CanadaACMFebruary 2023, 13
  HALDOI

National peer-reviewed Conferences

• 14 inproceedingsG.Guillaume Bertholon and A.Arthur Charguéraud. An AST for Representing Programs with Invariants and Proofs.Journées Francophones des Langages ApplicatifsJFLA 2023 - 34èmes Journées Francophones des Langages ApplicatifsPraz-sur-Arly, FranceJanuary 2023, 43-58
  HALback to text
• 15 inproceedingsC.Clément Flint, B.Berenger Bramas, S.Stephane Genaud and P.Philippe Helluy. Parallelization of the Lattice-Boltzmann schemes using the task-based method.COMPAS 2022 - Conférence francophone d'informatique en Parallélisme, Architecture et SystèmeAmiens, FranceJuly 2022
  HALback to text
• 16 inproceedingsB.Basile Sauvage, S.Stéphane Genaud, A.Arash Habibi, V.Vincent Loechner and P.-O.Pierre-Olivier Simonard. Émergence d'un leadership distribué pour la construction d'un enseignement.AIPU22 - 32ème Congrès de l'Association Internationale de Pédagogie UniversitaireRennes, FranceMay 2022
  HALback to text
• 17 inproceedingsH.Hayfa Tayeb, B.Bérenger Bramas, A.Abdou Guermouche and M.Mathieu Faverge. MulTreePrio: Scheduling task-based applications for heterogeneous computing systems.COMPAS 2022 - Conférence francophone d'informatique en Parallélisme, Architecture et SystèmeAmiens, FranceJuly 2022
  HALback to text

Scientific books

• 18 bookJ.Jens Gustedt, P.Peter Sewell, K.Kayvan Memarian, V. B.Victor B F Gomes and M.Martin Uecker. A Provenance-aware Memory Object Model for C.ISO/IEC TC1/SC22/WG14June 2022, 131
  HALback to text

Reports & preprints

• 19 reportÉ.Étienne Alepins and J.Jens Gustedt. Unsequenced functions.Inria Nancy - Grand EstApril 2022, 11
  HALback to text
• 20 miscA.Arthur Charguéraud, B.Begatim Bytyqi, D.Damien Rouhling and Y. A.Yann A Barsamian. OptiTrust: an Interactive Framework for Source-to-Source Transformations.September 2022
  HALback to text
• 21 miscA.Arthur Charguéraud, A.Adam Chlipala, A.Andres Erbsen and S.Samuel Gruetter. Omnisemantics: Smooth Handling of Nondeterminism.September 2022
  HALback to text
• 22 reportA.Alex Gilding and J.Jens Gustedt. Introduce storage-class specifiers for compound literals.N3038ISO JCT1/SC22/WG14July 2022
  HALback to text
• 23 reportA.Alex Gilding and J.Jens Gustedt. The constexpr specifier for object definitions.N3018ISO JCT1/SC22/WG14June 2022
  HALback to text
• 24 reportA.Alex Gilding and J.Jens Gustedt. Type inference for object definitions.N3007ISO JCT1/SC22/WG14June 2022
  HALback to text
• 25 reportA.Alex Gilding and J.Jens Gustedt. Underspecified object declarations.N3006ISO JCT1/SC22/WG14June 2022
  HALback to text
• 26 reportJ.Jens Gustedt. Add new optional time bases: Proposal for C23.N2957ISO JCT1/SC22/WG14April 2022
  HALback to text
• 27 reportJ.Jens Gustedt. Basic lambdas for C: proposal for C23.N2892ISO JCT1/SC22/WG14January 2022, 52
  HALback to text
• 28 miscJ.Jens Gustedt. Improve type generic programming (slides).February 2022
  HALback to textback to text
• 29 reportJ.Jens Gustedt. Improve type generic programming: proposal for C23.N2890ISO JCT1/SC22/WG14January 2022, 82
  HALback to text
• 30 reportJ.Jens Gustedt. Make false and true first-class language features: proposal for C2x.N2935ISO JTC1/SC22/WG14February 2022
  HALback to text
• 31 reportJ.Jens Gustedt and J.JeanHeyd Meneide. Introduce the nullptr constant.N3042ISO JTC1/SC22/WG14July 2022
  HALback to text
• 32 miscJ.Jens Gustedt. Options for lambdas: (slides).February 2022
  HALback to text
• 33 reportJ.Jens Gustedt. Pointers and integer types.N2889ISO JCT1/SC22/WG14January 2022
  HALback to text
• 34 reportJ.Jens Gustedt. Primary expressions and constant expressions, clarification request.ISO JTC1/SC22/WG14June 2022
  HALback to text
• 35 reportJ.Jens Gustedt. Remove ATOMIC VAR INIT.N2886ISO JTC1/SC22/WG14January 2022
  HALback to text
• 36 reportJ.Jens Gustedt. Require exact-width integer type interfaces.N2888ISO JTC1/SC22/WG14January 2022
  HALback to text
• 37 reportJ.Jens Gustedt. Revise spelling of keywords: proposal for C23.N2934ISO JTC1/SC22/WG14February 2022
  HALback to text
• 38 reportJ.Jens Gustedt. Type inference for variable definitions and function returns: proposal for C23.N2923ISO JCT1/SC22/WG14January 2022, 22
  HALback to text
• 39 miscJ.Jens Gustedt. Type inference for variables and functions (slides).February 2022
  HALback to text
• 40 miscJ.Jens Gustedt. Type-generic lambdas: (slides).February 2022
  HALback to text
• 41 reportJ.Jens Gustedt. Type-generic lambdas: proposal for C23.N2924ISO JCT1/SC22/WG14January 2022, 14
  HALback to text
• 42 reportJ.Jens Gustedt and M.Martin Uecker. Properly define blocks as part of the grammar: proposal for C23.N2937ISO JCT1/SC22/WG14February 2022, 3
  HALback to text
• 43 reportA.Alexandre Moine, A.Arthur Charguéraud and F.François Pottier. A High-Level Separation Logic for Heap Space under Garbage Collection (Extended Version).Inria2022
  HALback to text
• 44 miscH.Hayfa Tayeb, B.Bérenger Bramas and L.Ludovic Paillat. Autovesk: Automatic vectorization of unstructured static kernels by graph transformations.December 2022
  HALback to text

Other scientific publications

• 45 articleM.Matthieu Boileau, B.Bérenger Bramas, E.Emmanuel Franck, R.Romane Hélie, P.Philippe Helluy and L.Laurent Navoret. Parallel kinetic scheme in complex toroidal geometry.SMAI Journal of Computational MathematicsDecember 2022, 249-271
  HALDOIback to text