H. Pompougnac, U. Beaugnon, A. Cohen, D. Potop-Butucaru: Weaving Synchronous Reactions into the Fabric of SSA-form Compilers. ACM Trans. Archit. Code Optim. 19(2): 22:1-22:25 (2022)
K. Didier, D. Potop-Butucaru, G. Iooss, A. Cohen, J. Souyris, P. Baufreton, A. Graillat: Correct-by-Construction Parallelization of Hard Real-Time Avionics Applications on Off-the-Shelf Predictable Hardware. ACM Trans. Archit. Code Optim. 16(3): 24:1-24:27 (2019)
D. Potop-Butucaru: Real-Time Systems Compilation. Habilitation Thesis, 2015
T. Carle, D. Potop-Butucaru, Y. Sorel, D. Lesens: From Dataflow Specification to Multiprocessor Partitioned Time-Triggered Real-Time Implementation. Leibniz Trans. Embed. Syst. 2(2): 01:1-01:30 (2015)
R. Gorcitz, E. Kofman, T. Carle, D. Potop-Butucaru, R. de Simone: On the Scalability of Constraint Solving for Static/Off-Line Real-Time Scheduling. FORMATS 2015: 108-123
D. Potop-Butucaru, S. Edwards, G. Berry: Compiling Esterel. Springer, May 2007. ISBN: 0387706267
D. Potop-Butucaru, B. Caillaud, A. Benveniste: Concurrency in synchronous systems. Formal Methods Syst. Des. 28(2): 111-130 (2006)
Full list available in my CV. For indicators, see my Google Scholar profile.
Fabien Siron (2020-) CIFRE funding (with KronoSafe). Co-supervision with Robert de Simone. Topic: Formal verification methodology for LET real-time applications.
Hugo Pompougnac (2019-2022). Full supervision. Topic: Timing-predictable implementation of neural networks. To defend on Dec 9, 2022.
Keryan Didier (2015-2019). Full supervision. PhD thesis: Contributions to the safe and efficient parallelisation of hard real-time systems. Current position: engineer at OCaMLPro.
Thomas Carle (2011-2014). Full supervision. PhD thesis: Efficient compilation of embedded control specifications with complex functional and non-functional properties. Current position: assistant professor at IRIT, Toulouse, France.
Manel Djemal (2010-2014). Co-supervision with A. Munier. PhD thesis: Reconciling performance and predictability on a NoC-based MPSoC using off-line scheduling techniques.
Lopht is a compiler for real-time embedded systems. It performs the automatic allocation, real-time multiprocessor scheduling, and optimized code generation. It outputs full implementations, including exe- cutable code and platform configuration code, that are functionally correct and respect all the non-functional requirements (including real-time requirements).
mlirlus is a HPC/ML compiler and intermediate representation for Real-Time Embedded (RTE) systems. It allows the joint specification and efficient compilation of both the high-performance data processing operations and reactive control and interaction with the environment. Further description in our 2022 HiPEAC paper.
Full list of software in my CV.
I have dedicated my entire research career to the topic of optimized implementation of real-time embedded systems. The focus has steadily enlarged as time passed:
As a natural further extension to this work, I have dedicated the past 10 years to creating bridges between the real-time embedded (RTE) systems community and the high-performance compilation (HPC) community of which classical compilers (such as gcc and llvm) and ML compilers (such as TVM, Glow or MLIR) are the best-known output. My objective is to use formal methods to reconcile RTE safety and HPC efficiency in the implementation of embedded systems subject to non-functional (e.g. real-time, memory) constraints.
- Efficient sequential compilation of domain-specific embedded specifications during my PhD.
- Synthesizing efficient communication and sychronization protocols for multiprocessor, multi-core and many-core applications during my post-doc years.
- Synthesizing full-fledged multi-/many-core implementations that are both efficient and guaranteed to satisfy non-functional requirements (such as real-time requirements), during the first years at Inria.
I advocate for a real-time systems compilation approach that combines aspects of both real-time/embedded (RTE) systems design and high-performance compilation (HPC).
Like a classical or ML compiler such as GCC or MLIR, a real-time systems compiler should use fast and efficient scheduling and code generation heuristics, to ensure scalability. Similarly, it should provide traceability support under the form of informative error messages enabling an incremental trial-and-error design style, much like that of classical application software. This is more difficult than in a classical compiler, given the complexity of the transformation flow (creation of tasks, allocation, scheduling, synthesis of communication and synchronization code, etc.), and requires a full formal integration along the whole flow, including the crucial issue of correct hardware abstraction.
A real-time systems compiler should perform precise, conservative timing accounting along the whole scheduling and code generation flow, allowing it to produce safe and tight real-time guarantees. More generally, and unlike in classical compilers, the allocation and scheduling algorithms must take into account a variety of non-functional requirements, such as real-time constraints, criticality/partitioning, preemptability, allocation constraints, memory size, etc. When the accent is put on the respect of requirements (as opposed to optimization of a metric, like in classical compilation), resulting scheduling problems are quite different.
On these topics, I have directed 4 PhD theses and have been PI or Inria PI on multiple research projects and direct industry collaborations. I have led the development of Lopht, a tool and method for the automatic parallelization and resource allocation for critical real-time control applications, which has reached TRL4 on large-scale industrial avionics applications. In the past three years, I have led the development of mlir-lus, an extension of the open-source MLIR ML compiler allowing the efficient compilation of reactive ML programs.