My research puts a particular emphasis on experimentation methodologies for distributed applications and algorithms. To this end, I use several approaches, such as direct execution on Experimental Facilities, Emulation, Simulation, and Formal Methods. I also bridge these approaches where possible.
Performance assessment through simulation with SimGrid
Simulation is an appealing methodology to assess the performance of distributed applications, that are particularly challenging to test on real platforms. SimGrid is a scientific instrument enabling the evaluation of distributed algorithms or of unmodified MPI applications. This tool strives toward realism (careful calibration can yield accurate simulations), once the simulation is and performance (simulating up to millions of entities [QRT12]). I am one of the main authors of this framework since 2005.
I work on the efficient simulation of distributed applications since two decades. [DLM+17] presents our approach to the simulation of unmodified MPI applications, enabling the study of their performance in the comfort of the simulator. [CGL+25] summarizes 20 years of work to improve the extensibility and usability of the tool, without sacrificing the precision and versatility at high performance that have been its strengths for over 20 years. SimGrid v4 aims for a better-architected, more stable, maintainable, and well-documented codebase.
Beyond the simulation core, I work on modeling Fog/Cloud/HPC systems. I modeled the electrical consumption of these infrastructures with Anne-Cécile Orgerie (CNRS at IRISA) during the theses of L. Guegan and A. Gougeon [GAO+19, CDOQ18, ROQ+18, OLH+17, ROQ17]. During the thesis of C. Courageux-Sudan, we modeled Wi-Fi networks [CGOQ22, COQ23, COQ24], and we proposed an initial approach to derive a digital twin from the logs of a microservices-based application [COQ21]. We also worked on coupling different simulators by combining PandaPower, SimGrid, and ns-3 to study both the electrical grid and the IT infrastructure controlling it [COQ18].
Formal assessment of distributed applications
Mc SimGrid is a software model checker. It exhaustively explores the tree of possible outcomes for programs launched in SimGrid. It leverages formal techniques to detect symmetries in execution histories (such as ODPOR and UDPOR), to reduce the state space while exploring all possible behaviors.
I co-advised the thesis of Cristian Rosa (defended in 2011) with S. Merz on the introduction of a software model checker in the SimGrid framework. [MQR11] shows how modeling half a dozen of core calls is sufficient to verify programs leveraging hundreds of MPI primitives. The thesis of Marion Guthmuller (defended in 2015) extended this work to the verification of liveness properties on MPI programs. [GCQ18] details how we leveraged system-level introspection mechanisms to make it possible. I co-advised the thesis of The Anh Pham (defended in 2019) with T. Jéron on state space reduction to optimize the formal verification of MPI programs. [PJQ19] details our formalization of the SimGrid computation model, and the adaptation of the UDPOR algorithm to this model.
Together with M. Laurent E. Saillard, I proposed a benchmark to evaluate tools for bug detection in MPI codes [LSQ21].
Current students
- Mathieu Laurent (since 2023): PhD on software model checking
See this page for the past students.
Open positions
Virtualization of distributed applications
In [DLM+17], we detail our complete reimplementation of the MPI standard on top of SimGrid to enable the simulation of unmodified MPI applications. During the postdoctoral work of M. Poquet, we proposed in 2019 the remote simgrid tool to simplify the virtualization of arbitrary applications. [CQ20] introduces a reimplementation of the pthread standard to enable the simulation of multi-threaded applications. The thesis of Léo Cosseron, which I am co-supervising with L. Rilling, focuses on interconnecting virtual machines such as QEMU, KVM, or Xen through a simulated network in SimGrid to enable the study of malicious code that only activates if the study environment is undetectable [CRSQ24].
Current students
- Léo Cosseron (since 2022): PhD on the interconnection of VMs through a simulated network (TANSIV project).
See this page for the past students.