Thursday, December 12th, 2024
- Share
- Share on Facebook
- Share on X
- Share on LinkedIn
Relaxed Concurrency, Proven Concurrency
This habilitation presents several contributions in the field of operating systems, with a particular focus on bug detection in concurrent environments and performance optimization on modern infrastructures.
Manuscript Summary:
"This habilitation presents several contributions in the field of operating systems, with a particular focus on bug detection in concurrent environments and performance optimization on modern infrastructures.
The first part introduces a novel approach to infer concurrent interactions in lock-free multithreaded programs. I developed an innovative heuristic based on memory barrier matching to identify potentially concurrent functions in contexts devoid of explicit locks. Applying this method to the Linux kernel, I uncovered 12 critical bugs threatening system stability and data integrity. Fixes for these bugs have been integrated since version 5.15.
The second part explores the limitations of Key-Value (KV) stores on modern NVMe SSD storage systems. We designed KVell, a new KV store that fully leverages the capabilities of these disks, eliminating CPU bottlenecks affecting existing KV stores. KVell, based on a shared-nothing architecture, achieves significantly faster read and write performance, surpassing state-of-the-art solutions with 2× faster reads and 5× faster writes.
Finally, my work on Linux task scheduling revealed major inefficiencies in multicore architectures, where some cores were consistently underutilized. I addressed these issues, leading to significant improvements in performance and energy efficiency, integrated into the Linux kernel since version 5.5. Additionally, I proposed a new domain-specific language (DSL) for scheduling, complemented by formal proof techniques ensuring the absence of certain types of bugs in scheduling algorithms.
This manuscript concludes with my research project aiming to design and certify systems capable of efficiently leveraging modern and future servers. Current systems increasingly rely on unsafe concurrent memory accesses to maximize hardware performance. However, this approach introduces significant complexity due to the growing diversity of hardware (heterogeneous cores, persistent memory, NUMA architectures, accelerators). My objective is to overcome these challenges by designing applications that efficiently utilize such infrastructures while ensuring correctness through formal methods."
Date and place
Thursday, December 12th, at 2:30 PM
Building H of Ensimag
- Share
- Share on Facebook
- Share on X
- Share on LinkedIn