2025Activity report‌Project-TeamWHISPER

3.1 System​​​‌ performance

Our work on‌ system performance focuses on‌​‌ scheduling, virtualization, synchronization, and​​ the interactions between them.​​​‌ A task scheduler decides‌ which runnable task should‌​‌ be able to execute​​ on a CPU, and,​​​‌ in a multicore setting,‌ on which core that‌​‌ execution should take place.​​ As the task scheduler​​​‌ determines how much CPU‌ time the tasks of‌​‌ an application receive, as​​ well as whether the​​​‌ chosen CPU has effcient‌ access to needed hardware‌​‌ resources (network, accelerators, caches,​​ etc.), it has a​​​‌ large impact on application‌ performance. In a general-purpose‌​‌ programming setting, the task​​ scheduler is typically located​​​‌ in the operating system‌ kernel, and is expected‌​‌ to serve the needs​​ of all applications. It​​​‌ has no knowledge of‌ future application behavior. Such‌​‌ a setting raises many​​ challenges. We are currently​​​‌ focusing on four main‌ issues: scheduling and virtualization,‌​‌ making locks aware of​​ scheduler preemptions, control over​​​‌ scheduling from the user‌ level, and task scheduling‌​‌ for heterogeneous architectures.

Virtualization​​ decomposes the system support​​​‌ into one or more‌ standard operating systems, known‌​‌ as guest OSes, that​​ in turn run on​​​‌ a minimalistic operating system,‌ known as a hypervisor,‌​‌ which provides isolation between​​ the guest OSes and​​​‌ provides access to the‌ hardware. A guest OS‌​‌ schedules application tasks based​​ on its view of​​​‌ the set of available‌ CPUs, but these CPUs‌​‌ are actually just tasks​​ that are in turn​​​‌ scheduled by the hypervisor‌ on the physical CPUs‌​‌ of the machine. This​​ dual level of scheduling​​​‌ introduces the risk of‌ contradictory scheduling strategies. We‌​‌ are investigating the impact​​​‌ of this dual level​ of scheduling on the​‌ performance of applications in​​ a highly multicore setting.​​​‌

Effcient lock algorithms are​ key to ensuring application​‌ scalability on multi-core architectures​​ 25, 28,​​​‌ 7. Two families​ of lock algorithms exist:​‌ (1) with blocking locks,​​ tasks sleep in a​​​‌ wait list until the​ lock is free, whereas​‌ (2) with spin locks,​​ tasks busy-wait on the​​​‌ value of an atomic​ boolean variable that records​‌ whether or not the​​ lock is free. While​​​‌ blocking locks consume less​ CPU, they are also​‌ less reactive, as acquiring​​ the lock requires waking​​​‌ up the acquiring task,​ which entails a context​‌ switch. Spin locks, on​​ the other hand, are​​​‌ very reactive, as the​ lock is acquired by​‌ a busy-waiting task as​​ soon as the lock​​​‌ is released. But spinlocks​ may perform very poorly​‌ in overloaded scenarios, because​​ spinning tasks can preempt​​​‌ the lock-holding task, preventing​ any progress on the​‌ critical path. We would​​ like to turn spin​​​‌ locks into blocking locks​ in an overloaded scenario,​‌ relying on BPF to​​ safely inject code into​​​‌ the kernel to detect​ when the Linux kernel​‌ scheduler preempts the lock​​ holder.

Recently, several frameworks​​​‌ have been developed (notably,​ ghOSt from Google 30​‌ and sched-ext from Meta​​ 23) that allow​​​‌ the user level to​ inject new schedulers into​‌ the Linux kernel. We​​ would like to investigate​​​‌ how such a framework​ can be used to​‌ improve performance, using scheduling-decision-making​​ processes that are not​​​‌ feasible in the kernel.​ For example, machine learning​‌ could be beneficial for​​ inferring task properties and​​​‌ guiding scheduling accordingly, but​ is not practical in​‌ the kernel, due to​​ the latency involved, memory​​​‌ constraints, and the lack​ of kernel support for​‌ floating point numbers. Our​​ goal would be to​​​‌ provide a proof-of-concept, as​ it is not our​‌ focus to develop new​​ machine-learning algorithms. We will​​​‌ also consider whether it​ can be useful to​‌ export other kinds of​​ operating system services to​​​‌ user level, such as​ memory management. Finally, we​‌ will consider whether it​​ is possible to design​​​‌ a generic kernel interface​ for exporting to the​‌ user level performance-critical operating-system​​ services. This work is​​​‌ in collaboration with Alain​ Tchana and Renaud Lachaize​‌ of the Erods team​​ at LIG, as part​​​‌ of the Inria Défi​ OS.

The heuristics for​‌ scheduling employed by the​​ Linux kernel have evolved​​​‌ over time, primarily in​ a homogeneous setting, where​‌ all cores have similar​​ properties. Today, heterogeneous computing​​​‌ is becoming more prevalent,​ combining powerful processors for​‌ compute-intensive tasks with slower,​​ more energy-efficient, processors for​​​‌ lighter weight tasks. Such​ an architecture is found​‌ in the big.LITTLE processors​​ from Arm, typically used​​​‌ in mobile environments, and​ is now moving to​‌ desktop computing, with the​​ Alder Lake architecture from​​​‌ Intel. We will assess​ the degree to which​‌ the Linux kernel task​​ scheduler is able to​​​‌ effectively support such architectures​ and propose improvements, in​‌ terms of both meeting​​ application performance requirements and​​ saving energy. This work​​​‌ is in collaboration with‌ David Bromberg and Djob‌​‌ Mvondo of the WIDE​​ team at Inria-Rennes, as​​​‌ part of the Inria‌ Défi OS.

3.2 System‌​‌ re-engineering

In the area​​ of system re-engineering, we​​​‌ are interested in improving‌ the quality of infrastructure‌​‌ software as well as​​ in automating the transformations​​​‌ required to make it‌ possible to use such‌​‌ software in new settings.​​ Our work builds on​​​‌ our previous work on‌ Coccinelle 4, a‌​‌ program transformation system for​​ C code that has​​​‌ been extensively used on‌ the Linux kernel and‌​‌ other C infrastructure software.​​

We are extending Coccinelle​​​‌ to C++ and to‌ Rust. The extension to‌​‌ C++ reuses the existing​​ Coccinelle implementation, simply adding​​​‌ the C++-specific constructs. The‌ goal of this work,‌​‌ in collaboration with Michele​​ Martone of the Leibniz​​​‌ Supercomputing Center, is to‌ consider how Coccinelle can‌​‌ be used to adapt​​ existing HPC software for​​​‌ use on GPUs, by‌ introducing the use of‌​‌ calls to relevant libraries.​​ The extension to Rust,​​​‌ on the other hand,‌ is a complete re-implementation‌​‌ of Coccinelle, to benefit​​ from tools being developed​​​‌ by the Rust community‌ for parsing and pretty‌​‌ printing (Rust Analyzer and​​ rustfmt) Rust code. The​​​‌ reuse of these tools‌ has made it possible‌​‌ to quickly develop a​​ preliminary implementation for the​​​‌ full Rust language. In‌ the future, we may‌​‌ consider how to generalize​​ this process to other​​​‌ languages, addressing the challenge‌ that generic parsing tools‌​‌ may not present information​​ in a way that​​​‌ is suitable for program‌ transformation, for example in‌​‌ the choice of non-terminals.​​

We are considering how​​​‌ Coccinelle can be used‌ to facilitate long-term software‌​‌ maintenance. Many software projects​​ are obliged to maintain​​​‌ multiple variants, e.g.,‌ to meet the demands‌​‌ of users who rely​​ on the properties of​​​‌ old variants. An essential‌ part of software maintenance‌​‌ is thus to apply​​ new bug fixes to​​​‌ these old variants. Intervening‌ changes in the software,‌​‌ however, may imply that​​ fixes can not be​​​‌ applied to older versions‌ directly. We are looking‌​‌ into how Coccinelle can​​ be used to collect​​​‌ and exploit information about‌ recent code changes, to‌​‌ adapt new bug fixes​​ to older source code.​​​‌

Today, there are numerous‌ tools for scanning infrastructure‌​‌ software for common types​​ of vulnerabilities, such as​​​‌ NULL pointer dereferences and‌ buffer overflows. Avoiding such‌​‌ issues, however, is not​​ sufficient to ensure that​​​‌ the code behaves correctly;‌ the code must also‌​‌ implement the intended algorithm.​​ Checking algorithmic properties, however,​​​‌ is much more challenging,‌ because each service implements‌​‌ its own algorithm. Formal​​ verification tools such as​​​‌ Frama-C 24 can make‌ it possible to express‌​‌ and verify such properties,​​ but remain challenging to​​​‌ use, particularly for developers‌ without experience in formal‌​‌ verification. The challenge is​​ compounded by the fact​​​‌ that the code may‌ evolve frequently, making any‌​‌ proofs quickly out of​​ date. We are investigating​​​‌ how to design tools‌ that can facilitate proofs‌​‌ about Linux kernel code,​​​‌ both in how to​ extract relevant parts of​‌ the code base, to​​ reduce the amount of​​​‌ code that has to​ be considered by the​‌ proving process, and in​​ how proofs can be​​​‌ evolved in response to​ changes in the code​‌ base, analogous to the​​ adaptation of bug fixes​​​‌ over multiple versions.

4.1 Linux​‌

Linux is an open-source​​ operating system that is​​​‌ used in settings ranging​ from embedded systems to​‌ supercomputers. Linux kernel v6.1,​​ released in December 2022,​​​‌ comprises over 23 million​ lines of code, and​‌ supports 23 different families​​ of CPU architectures, around​​​‌ 50 file systems, and​ thousands of device drivers.​‌ Linux is also in​​ a rapid stage of​​​‌ development, with new versions​ being released roughly every​‌ 2.5 months. Recent versions​​ have each incorporated around​​​‌ 13,500 commits, from around​ 1500 developers. These developers​‌ have a wide range​​ of expertise, with some​​​‌ providing hundreds of patches​ per release, while others​‌ have contributed only one.​​ Overall, the Linux kernel​​​‌ is critical software, but​ software in which the​‌ quality of the developed​​ source code is highly​​​‌ variable. These features, combined​ with the fact that​‌ the Linux community is​​ open to contributions and​​​‌ to the use of​ tools, make the Linux​‌ kernel an attractive target​​ for software researchers. Tools​​​‌ that result from research​ can be directly integrated​‌ into the development of​​ real software, where it​​​‌ can have a high,​ visible impact.

Starting from​‌ the work of Engler​​ et al. 27,​​​‌ numerous research tools have​ been applied to the​‌ Linux kernel, typically for​​ finding bugs 26,​​​‌ 33, 36,​ 40 or for computing​‌ software metrics 31,​​ 46. In our​​​‌ work, we have studied​ generic C bugs in​‌ Linux code 12,​​ bugs in function protocol​​​‌ usage 34, 35​, issues related to​‌ the processing of bug​​ reports 44 and crash​​​‌ dumps 29, and​ the problem of backporting​‌ 41, 45,​​ illustrating the variety of​​​‌ issues that can be​ explored on this code​‌ base. Unique among research​​ groups working in this​​​‌ area, we have furthermore​ developed numerous contacts in​‌ the Linux developer community.​​ These contacts provide insights​​​‌ into the problems actually​ faced by developers and​‌ serve as a means​​ of validating the practical​​​‌ relevance of our work.​

4.2 Device Drivers

Device​‌ drivers are essential to​​ modern computing, to provide​​​‌ applications with access, via​ the operating system, to​‌ physical devices such as​​ keyboards, disks, networks, and​​​‌ cameras. Development of new​ computing paradigms, such as​‌ the internet of things,​​ is hampered because device​​​‌ driver development is challenging​ and error-prone, requiring a​‌ high level of expertise​​ in both the targeted​​​‌ OS and the specific​ device. Furthermore, implementing just​‌ one driver is often​​ not sufficient; today's computing​​​‌ landscape is characterized by​ a number of OSes,​‌ e.g., Linux, Windows,​​ MacOS, BSD and many​​​‌ real time OSes, and​ each is found in​‌ a wide range of​​ variants and versions. All​​ of these factors make​​​‌ the development, porting, backporting,‌ and maintenance of device‌​‌ drivers a critical problem​​ for device manufacturers, industry​​​‌ that requires specific devices,‌ and even for ordinary‌​‌ users.

The last twenty​​ years have seen a​​​‌ number of approaches directed‌ towards easing device driver‌​‌ development. Réveillère et al.​​ propose Devil 39,​​​‌ a domain-specific language for‌ describing the low-level interface‌​‌ of a device. Chipounov​​ et al. propose RevNic,​​​‌ 22 a template-based approach‌ for porting device drivers‌​‌ from one OS to​​ another. Ryzhyk et al.​​​‌ propose Termite, 42,‌ 43 an approach for‌​‌ synthesizing device driver code​​ from a specification of​​​‌ an OS and a‌ device. Currently, these approaches‌​‌ have been successfully applied​​ to only a small​​​‌ number of toy drivers.‌ Indeed, Kadav and Swift‌​‌ 32 observe that these​​ approaches make assumptions that​​​‌ are not satisfied by‌ many drivers; for example,‌​‌ the assumption that a​​ driver involves little computation​​​‌ other than the direct‌ interaction between the OS‌​‌ and the device. At​​ the same time, a​​​‌ number of tools have‌ been developed for finding‌​‌ bugs in driver code.​​ These tools include SDV​​​‌ 21, Coverity 27‌, CP-Miner, 37 PR-Miner‌​‌ 38, and Coccinelle​​ 11. These approaches,​​​‌ however, focus on analyzing‌ existing code, and do‌​‌ not provide guidelines on​​ structuring drivers.

In summary,​​​‌ there is still a‌ need for a methodology‌​‌ that first helps the​​ developer understand the software​​​‌ architecture of drivers for‌ commonly used operating systems,‌​‌ and then provides tools​​ for the maintenance of​​​‌ existing drivers.

4.3 Multicore‌ computing

Today, multicore computing‌​‌ is fundamental across a​​ wide variety of industries.​​​‌ Applications such as machines‌ learning, scientific computing, image‌​‌ processing, etc., run large​​ numbers of threads on​​​‌ highly multicore processors. Such‌ applications must furthermore contend‌​‌ with a variety of​​ hardware architectures, with different​​​‌ CPU and memory topologies,‌ CPU capacities, access to‌​‌ external resources such as​​ storage, networking and accellerators,​​​‌ etc. Virtualization facilitates hardware‌ sharing, but complicates access‌​‌ to and reasoning about​​ hardware resources. Our work​​​‌ on system performance targets‌ helping multicore applications run‌​‌ more efficiently, and helping​​ developers understand their application​​​‌ performance, to enable them‌ to find appropriate solutions.‌​‌

5.1 Footprint of​​​‌ research activities

Most of‌ our resource-intensive research activities‌​‌ are carried out on​​ Grid 5000, which is​​​‌ a shared national infrastructure,‌ saving the cost of‌​‌ building, transporting, and continuously​​ running a variety of​​​‌ dedicated machines.

6.1 Latest software​​ developments

6.2​​​‌ Open data

• The artifact​ associated with the paper​‌ "FlexGuard: Fast Mutual Exclusion​​ Independent of Subscription", published​​​‌ at SOSP 2025 15​, is available at​‌ https://gitlab.inria.fr/flexguard.
• The artifact​​ associated with the paper​​​‌ "Tapestry: Revealing Wait-For Dependencies​ Between Application Threads", published​‌ at PLOS2025 14,​​ is available at https://gitlab.inria.fr/tapestry​​​‌.
• The artifact associated​ with the paper "Understanding​‌ Linux Kernel Code through​​ Formal Verification: A Case​​​‌ Study of the Task-Scheduler​ Function select_idle_core", published at​‌ OlivierFest 2025 16,​​ is available at https://zenodo.org/records/16842821​​​‌.

7.1 FlexGuard: Fast Mutual​ Exclusion Independent of Subscription​‌

Participants: Victor Laforet [Whisper]​​, Sanidhya Kashyap [EPFL]​​​‌, Călin Iorgulescu [Oracle​ Labs], Julia Lawall​‌ [Whisper], Jean-Pierre Lozi​​ [Whisper].

Performance-oriented applications​​​‌ require efficient locks to​ harness the computing power​‌ of multicore architectures. While​​ fast, spinlock algorithms suffer​​​‌ severe performance degradation when​ thread counts exceed available​‌ hardware capacity, i.e., in​​ oversubscribed scenarios. Existing solutions​​​‌ rely on imprecise heuristics​ for blocking, leading to​‌ suboptimal performance. We present​​ FlexGuard, the first approach​​​‌ that systematically switches from​ busy-waiting to blocking precisely​‌ when a lock-holding thread​​ is preempted. FlexGuard achieves​​​‌ this by communicating with​ the OS scheduler via​‌ eBPF, unlike prior approaches.​​ FlexGuard matches or improves​​​‌ performance in LevelDB, a​ memory-optimized database index, PARSEC's​‌ Dedup, and SPLASH2X's Raytrace​​ and Streamcluster, boosting throughput​​​‌ by 1-6x in nonoversubscribed​ and up to 5x​‌ in oversubscribed scenarios.

This​​ paper was published at​​​‌ SOSP 2025 15.​ It has received badges​‌ for "Artifacts Available", "Artifacts​​ Evaluated and Functional", and​​ "Results Reproduced".

7.2 Scheduler​​​‌ Guided OpenMP Execution in‌ Cloud VMs

Participants: Himadri‌​‌ Chhaya-Shailesh [Whisper].

OpenMP​​ is a widely used​​​‌ framework for parallelizing applications,‌ enabling thread-level parallelism via‌​‌ simple source-code annotations. It​​ follows the fork-join model​​​‌ and relies heavily on‌ barrier synchronization among worker‌​‌ threads. Running OpenMP-enabled applications​​ in the cloud is​​​‌ increasingly popular due to‌ elasticity, fast startup, and‌​‌ pay-as-you-go pricing.

In cloud-based​​ execution, worker threads run​​​‌ inside a virtual machine‌ (VM) and are subject‌​‌ to dual levels of​​ scheduling: threads are placed​​​‌ by the guest scheduler‌ on guest virtual CPUs‌​‌ (vCPUs), and vCPUs are​​ managed as ordinary tasks​​​‌ by the host scheduler‌ on the host's physical‌​‌ CPUs (pCPUs). Because the​​ guest and host schedulers​​​‌ act independently, a semantic‌ gap emerges that can‌​‌ undermine application performance. Barrier​​ synchronization, whose efficiency depends​​​‌ on timely scheduling decisions,‌ is vulnerable to this‌​‌ semantic gap, and remains​​ underexplored.

Host-level preemptions in​​​‌ which guest vCPUs remain‌ queued on busy pCPUs,‌​‌ stall application progress. We​​ show that performance can​​​‌ be substantially improved by‌ (1) dynamically adapting the‌​‌ degree of parallelism (DoP)​​ at the start of​​​‌ each parallel region and‌ (2) dynamically choosing between‌​‌ spinning versus blocking at​​ barriers on a per-thread,​​​‌ per-barrier basis. We propose‌ paravirtualized, scheduler-informed techniques that‌​‌ accurately guide these decisions​​ and demonstrate their effectiveness​​​‌ in realistic deployments.

The‌ main contributions of this‌​‌ thesis are summarized below:​​

1. A novel analysis of​​​‌ how the semantic gap‌ between the guest and‌​‌ the host schedulers influences​​ OpenMP applications, facilitated by​​​‌ our in-house host-guest scheduler‌ tracing and visualization tool,‌​‌ dispel_tracer.
2. Phantom Tracker, an​​ algorithmic solution that leverages​​​‌ paravirtualized task scheduling to‌ detect and quantify Phantom‌​‌ vCPUs accurately.
3. pv-barrier-sync, a​​ dynamic barrier synchronization mechanism​​​‌ driven by the scheduler‌ insights produced by Phantom‌​‌ Tracker.
4. Juunansei, an OpenMP​​ runtime extension that demonstrates​​​‌ the practical utility of‌ Phantom Tracker and pv-barrier-sync‌​‌ with additional optimizations.

This​​ thesis was defended on​​​‌ December 17, 2025.19‌

7.3 Linux as a‌​‌ microkernel: the memory management's​​ case

Participants: Papa Assane​​​‌ Fall [Whisper].

Main‌ memory is a critical‌​‌ resource in data centers,​​ due to its major​​​‌ impact on application performance‌ and server costs. However,‌​‌ Linux's memory management system,​​ designed to be general-purpose,​​​‌ is not always optimal‌ for diverse workload requirements.‌​‌ This thesis 20introduces​​ USM, a framework for​​​‌ the rapid development of‌ memory management policies in‌​‌ Linux. USM adopts a​​ microkernel-inspired design, enabling memory-management​​​‌ policies to run in‌ user space. We demonstrate‌​‌ the flexibility of USM​​ by implementing a variety​​​‌ of memory-menagament policies, and‌ evaluate its performance against‌​‌ state-of-the-art solutions.

This work​​ was carried out as​​​‌ part of the Defi‌ OS. It was supervised‌​‌ by Alain Tchana in​​ Grenoble and Jean-Pierre Lozi​​​‌ in Paris.

7.4 Tapestry:‌ Revealing Wait-For Dependencies Between‌​‌ Application Threads

Participants: Tomáš​​ Faltin [Whisper], Himadri​​​‌ Chhaya-Shailesh [Whisper], Julia‌ Lawall [Whisper], Jean-Pierre‌​‌ Lozi [Whisper].

Application​​ slowdowns that accumulate on​​​‌ the critical path significantly‌ impact performance. Identifying them‌​‌ requires visualizing inter-thread wait-for​​​‌ dependencies, a task neglected​ by existing tools, especially​‌ regarding ad-hoc, busywaiting synchronization.​​ We present Tapestry, which​​​‌ efficiently traces these dependencies​ by dynamically switching between​‌ hardware watchpoints and software​​ breakpoints. Using three use​​​‌ cases, we show that​ Tapestry is able to​‌ reveal NUMA effects and​​ explain performance anomalies in​​​‌ oversubscribed and virtualized environments.​

This work was published​‌ at the 13th Workshop​​ on Programming Languages and​​​‌ Operating Systems (PLOS 2025),​ held with SOSP 2025​‌ 14.

7.5 The​​ Impact of Kernel Asynchronous​​​‌ APIs on the Performance​ of a Kernel VPN​‌

Participants: Cesaire Mounah-Honore [WIDE]​​, Djob Mvondo [WIDE]​​​‌, Julia Lawall [Whisper]​, Yérom-David Bromberg [WIDE]​‌.

Linux kernel VPNs​​ suffer from severe performance​​​‌ degradation under high load​ due to execution order​‌ inversion (EoI), a phenomenon​​ where packet recombination functions​​​‌ preempt earlier pipeline stages.​ This leads to severe​‌ latency spikes and throughput​​ reductions. We investigate kernel​​​‌ threads and workqueues as​ alternative kernel asynchronous APIs​‌ to address these limitations,​​ achieving up to a​​​‌ 4.7x increase in throughput​ while reducing tail latency​‌ by 65%. These results​​ demonstrate the importance of​​​‌ selecting appropriate kernel asynchronous​ APIs for kernel-level network​‌ applications.

This short paper​​ was published at the​​​‌ 2025 ACM International Systems​ and Storage Conference (SYSTOR)​‌ 18

7.6 Understanding Linux​​ Kernel Code through Formal​​​‌ Verification: A Case Study​ of the Task-Scheduler Function​‌ select_idle_core

Participants: Julia Lawall​​ [Whisper], Keisuke Nishimura​​​‌ [Whisper], Jean-Pierre Lozi​ [Whisper].

On the​‌ one hand, the Linux​​ kernel task scheduler is​​​‌ critical to all application​ performance. On the other​‌ hand, it is widely​​ agreed that its code​​​‌ complexity is spiraling out​ of control, and only​‌ a tiny handful of​​ kernel developers understand it.​​​‌ We are exploring the​ opportunities and challenges in​‌ applying formal verification to​​ Linux kernel task-scheduler code.​​​‌ Building on a previous​ work focusing on the​‌ evolution of the function​​ should_we_balance, we here consider​​​‌ a version of the​ key task-placement function select_idle_core​‌ and the evolution of​​ the iterators on which​​​‌ it relies.

This work​ was published at the​‌ OlivierFest 2025 workshop, held​​ with SPLASH 2025 16​​​‌. It received an​ "Artifacts Available" badge.

7.7​‌ Advances in Semantic Patching​​ for HPC-oriented Refactorings with​​​‌ Coccinelle

Participants: Michele Martone​ [LRZ], Julia Lawall​‌ [Whisper].

Currently, the​​ most energy-efficient hardware platforms​​​‌ for large-scale floating point-intensive​ calculations (also known as​‌ High Performance Computing, or​​ HPC) are graphical processing​​​‌ units (GPUs). However, porting​ existing scientific codes to​‌ GPUs can be far​​ from trivial. This article​​​‌ summarizes our recent advances​ in enabling machine-assisted, HPC-oriented​‌ refactorings with reference to​​ existing APIs and programming​​​‌ idioms available in C​ and C++. The tool​‌ we are extending and​​ using for the purpose​​​‌ is called Coccinelle. An​ important workflow we aim​‌ to support is that​​ of writing and maintaining​​​‌ tersely written application code,​ while deferring circumstantial, ad-hoc,​‌ performance-related changes to specific,​​ separate rules called "semantic​​​‌ patches". GPUs currently offer​ very limited debugging facilities.​‌ The approach we are​​ developing aims at preserving​​ intelligibility, longevity, and relatedly,​​​‌ debuggability of existing code‌ on CPUs, while at‌​‌ the same time enabling​​ HPC-oriented code evolutions such​​​‌ as introducing support for‌ GPUs, in a scriptable‌​‌ and possibly parametric manner.​​ This article sketches a​​​‌ number of self-contained use‌ cases, including further HPC-oriented‌​‌ cases which are independent​​ from GPUs.

This work​​​‌ was published at the‌ 30th International Workshop on‌​‌ High-Level Parallel Programming Models​​ and Supportive Environments (HIPS),​​​‌ held with IPDPS 17‌.

9.1 National initiatives

10.1 Promoting‌ scientific activities

10.2 Teaching -​ Supervision - Juries -​‌ Educational and pedagogical outreach​​

10.3 Popularization

• Maxime Derri‌​‌ gave a talk at​​ FOSDEM 2025 on "Performance​​​‌ evaluation of the Linux‌ kernel eBPF verifier".
• Keisuke‌​‌ Nishimura gave a talk​​ at Linux Plumbers on​​​‌ "Applying Program Verification to‌ Linux Kernel Code: Challenges,‌​‌ Practices, and Automation".

11.1 Major publications

• 1​​​‌ inproceedingsJ.Julien Brunel‌, D.Damien Doligez‌​‌, R. R.René​​ Rydhof Hansen, J.​​​‌ L.Julia L. Lawall‌ and G.Gilles Muller‌​‌. A foundation for​​ flow-based program matching using​​​‌ temporal logic and model‌ checking.POPLSavannah,‌​‌ GA, USAACMJanuary​​ 2009, 114--126back​​​‌ to text
• 2 inproceedings‌J.Julien Brunel,‌​‌ D.Damien Doligez,​​ R. R.René Rydhof​​​‌ Hansen, J. L.‌Julia L. Lawall and‌​‌ G.Gilles Muller.​​ A foundation for flow-based​​​‌ program matching: using temporal‌ logic and model checking‌​‌.The 36th annual​​ ACM SIGPLAN-SIGACT symposium on​​​‌ Principles of programming languages,‌ POPL'09The 36th annual‌​‌ ACM SIGPLAN-SIGACT symposium on​​ Principles of programming languages,​​​‌ POPL'09Savannah, Georgia, United‌ StatesACMJanuary 2009‌​‌, 114-126HALDOI​​
• 3 articleL.Laurent​​​‌ Burgy, L.Laurent‌ Réveillère, J. L.‌​‌Julia L. Lawall and​​ G.Gilles Muller.​​​‌ Zebu: A Language-Based Approach‌ for Network Protocol Message‌​‌ Processing.IEEE Trans.​​ Software Eng.374​​​‌2011, 575-591back‌ to text
• 4 inproceedings‌​‌J.Julia Lawall and​​ G.Gilles Muller.​​​‌ Coccinelle: 10 Years of‌ Automated Evolution in the‌​‌ Linux Kernel.2018​​ USENIX Annual Technical Conference​​​‌Boston, MA, United States‌July 2018HALback‌​‌ to textback to​​ textback to text​​​‌
• 5 inproceedingsJ.Julia‌ Lawall, D.Derek‌​‌ Palinski, L.Lukas​​ Gnirke and G.Gilles​​​‌ Muller. Fast and‌ Precise Retrieval of Forward‌​‌ and Back Porting Information​​ for Linux Device Drivers​​​‌.2017 USENIX Annual‌ Technical ConferenceSanta Clara,‌​‌ CA, United StatesJuly​​ 2017, 12HAL​​​‌back to text
• 6‌ inproceedingsB.Baptiste Lepers‌​‌, R.Redha Gouicem​​, D.Damien Carver​​​‌, J.-P.Jean-Pierre Lozi‌, N.Nicolas Palix‌​‌, M.-V.Maria-Virginia Aponte​​, W.Willy Zwaenepoel​​​‌, J.Julien Sopena‌, J.Julia Lawall‌​‌ and G.Gilles Muller​​. Provable Multicore Schedulers​​​‌ with Ipanema: Application to‌ Work Conservation.Eurosys‌​‌ 2020 - European Conference​​ on Computer SystemsHeraklion​​​‌ / Virtual, GreeceApril‌ 2020HALDOIback‌​‌ to text
• 7 inproceedings​​J.-P.Jean-Pierre Lozi,​​​‌ F.Florian David,‌ G.Gaël Thomas,‌​‌ J. L.Julia L.​​​‌ Lawall and G.Gilles​ Muller. Remote Core​‌ Locking: Migrating Critical-Section Execution​​ to Improve the Performance​​​‌ of Multithreaded Applications.​Proceedings of the 2012​‌ USENIX Annual Technical Conference​​ (USENIX ATC '12)2012​​​‌ USENIX Annual Technical Conference​ (USENIX ATC '12)Boston,​‌ MA, United StatesACM​​2012HALDOIback​​​‌ to text
• 8 inproceedings​F.Fabrice Mérillon,​‌ L.Laurent Réveillère,​​ C.Charles Consel,​​​‌ R.Renaud Marlet and​ G.Gilles Muller.​‌ Devil: An IDL for​​ hardware programming.Proceedings​​​‌ of the Fourth Symposium​ on Operating Systems Design​‌ and Implementation (OSDI)San​​ Diego, CaliforniaUSENIX Association​​​‌October 2000, 17--30​back to text
• 9​‌ inproceedingsG.Gilles Muller​​, C.Charles Consel​​​‌, R.Renaud Marlet​, L. P.Luciano​‌ P. Barreto, F.​​Fabrice Mérillon and L.​​​‌Laurent Réveillère. Towards​ Robust OSes for Appliances:​‌ A New Approach Based​​ on Domain-specific Languages.​​​‌Proceedings of the 9th​ Workshop on ACM SIGOPS​‌ European Workshop: Beyond the​​ PC: New Challenges for​​​‌ the Operating SystemKolding,​ Denmark2000, 19--24​‌back to text
• 10​​ inproceedingsG.Gilles Muller​​​‌, J. L.Julia​ L. Lawall and H.​‌Hervé Duchesne. A​​ Framework for Simplifying the​​​‌ Development of Kernel Schedulers:​ Design and Performance Evaluation​‌.HASE - High​​ Assurance Systems Engineering Conference​​​‌Heidelberg, GermanyIEEEOctober​ 2005, 56--65back​‌ to text
• 11 inproceedings​​Y.Yoann Padioleau,​​​‌ J. L.Julia L.​ Lawall, R. R.​‌René Rydhof Hansen and​​ G.Gilles Muller.​​​‌ Documenting and Automating Collateral​ Evolutions in Linux Device​‌ Drivers.EuroSysGlasgow,​​ ScotlandMarch 2008,​​​‌ 247--260back to text​
• 12 articleN.Nicolas​‌ Palix, G.Gaël​​ Thomas, S.Suman​​​‌ Saha, C.Christophe​ Calvès, J. L.​‌Julia L. Lawall and​​ G.Gilles Muller.​​​‌ Faults in Linux 2.6​.ACM Transactions on​‌ Computer Systems322​​June 2014, 4:1--4:40​​​‌back to text
• 13​ inproceedingsL.Lucas Serrano​‌, V.-A.Van-Anh Nguyen​​, F.Ferdian Thung​​​‌, L.Lingxiao Jiang​, D.David Lo​‌, J.Julia Lawall​​ and G.Gilles Muller​​​‌. SPINFER: Inferring Semantic​ Patches for the Linux​‌ Kernel.USENIX Annual​​ Technical ConferenceBoston /​​​‌ Virtual, United StatesJuly​ 2020HALback to​‌ text

11.2 Publications of​​ the year

11.3‌​‌ Cited publications

• 21 inproceedings​​T.Thomas Ball,​​​‌ E.Ella Bounimova,‌ B.Byron Cook,‌​‌ V.Vladimir Levin,​​ J.Jakob Lichtenberg,​​​‌ C.Con McGarvey,‌ B.Bohus Ondrusek,‌​‌ S. K.Sriram K.​​ Rajamani and A.Abdullah​​​‌ Ustuner. Thorough Static‌ Analysis of Device Drivers‌​‌.EuroSys2006,​​ 73--85back to text​​​‌
• 22 inproceedingsV.Vitaly‌ Chipounov and G.George‌​‌ Candea. Reverse Engineering​​ of Binary Device Drivers​​​‌ with RevNIC.EuroSys‌2010, 167--180back‌​‌ to text
• 23 article​​J.Jonathan Corbet.​​​‌ The extensible scheduler class‌.Linux Weekly News‌​‌February 2023, URL:​​ https://lwn.net/Articles/922405/back to text​​​‌
• 24 inproceedingsP.Pascal‌ Cuoq, F.Florent‌​‌ Kirchner, N.Nikola\"i​​ Kosmatov, V.Virgile​​​‌ Prevosto, J.Julien‌ Signoles and B.Boris‌​‌ Yakobowski. Frama-C: A​​ Software Analysis Perspective.​​​‌Software Engineering and Formal‌ Methods - 10th International‌​‌ Conference (SEFM)Thessaloniki, Greece​​October 2012, URL:​​​‌ http://pathcrawler-online.com/pubs/final_sefm12.pdfback to text‌
• 25 inproceedingsT.Tudor‌​‌ David, R.Rachid​​ Guerraoui and V.Vasileios​​​‌ Trigonakis. Everything you‌ always wanted to know‌​‌ about synchronization but were​​ afraid to ask.​​​‌Symposium on Operating Systems‌ Principles (SOSP)2013,‌​‌ 33-48back to text​​
• 26 inproceedingsI.Isil​​​‌ Dillig, T.Thomas‌ Dillig and A.Alex‌​‌ Aiken. Sound, complete​​ and scalable path-sensitive analysis​​​‌.PLDIJune 2008‌, 270--280back to‌​‌ text
• 27 inproceedingsD.​​​‌ R.Dawson R. Engler​, B.Benjamin Chelf​‌, A.Andy Chou​​ and S.Seth Hallem​​​‌. Checking System Rules​ Using System-Specific, Programmer-Written Compiler​‌ Extensions.OSDI2000​​, 1--16back to​​​‌ textback to text​
• 28 inproceedingsH.Hugo​‌ Guiroux, R.Renaud​​ Lachaize and V.Vivien​​​‌ Quéma. Multicore Locks:​ The Case Is Not​‌ Closed Yet.2016​​ USENIX Annual Technical Conference,​​​‌ USENIX ATC 2016, Denver,​ CO, USA, June 22-24,​‌ 2016USENIX Association2016​​, 649--662back to​​​‌ text
• 29 inproceedingsL.​Lisong Guo, J.​‌Julia Lawall and G.​​Gilles Muller. Oops!​​​‌ Where Did That Code​ Snippet Come From?MSR​‌ 2014 - 11th Working​​ Conference on Mining Software​​​‌ RepositoriesHyderabad, IndiaACM​May 2014, 52-61​‌HALDOIback to​​ text
• 30 inproceedingsJ.​​​‌ T.Jack Tigar Humphries​, N.Neel Natu​‌, A.Ashwin Chaugule​​, O.Ofir Weisse​​​‌, B.Barret Rhoden​, J.Josh Don​‌, L.Luigi Rizzo​​, O.Oleg Rombakh​​​‌, P.Paul Turner​ and C.Christos Kozyrakis​‌. GhOSt: Fast &​​ Flexible User-Space Delegation of​​​‌ Linux Scheduling.Symposium​ on Operating Systems Principles​‌Association for Computing Machinery​​2021, 588--604back​​​‌ to text
• 31 article​A.Ayelet Israeli and​‌ D. G.Dror G.​​ Feitelson. The Linux​​​‌ kernel as a case​ study in software evolution​‌.Journal of Systems​​ and Software833​​​‌2010, 485--501back​ to text
• 32 inproceedings​‌A.Asim Kadav and​​ M. M.Michael M.​​​‌ Swift. Understanding modern​ device drivers.ASPLOS​‌2012, 87--98back​​ to text
• 33 inproceedings​​​‌J.Jakob Koschel,​ P.Pietro Borrello,​‌ D. C.Daniele Cono​​ D\textquoterightElia, H.Herbert​​​‌ Bos and C.Cristiano​ Giuffrida. Uncontained: Uncovering​‌ Container Confusion in the​​ Linux Kernel.32nd​​​‌ USENIX Security Symposium (USENIX​ Security 23)Anaheim, CA​‌USENIX AssociationAugust 2023​​, 5055--5072URL: https://www.usenix.org/conference/usenixsecurity23/presentation/koschel​​​‌back to text
• 34​ articleJ.Julia Lawall​‌, J.Julien Brunel​​, N.Nicolas Palix​​​‌, R. R.René​ Rydhof Hansen, H.​‌Henrik Stuart and G.​​Gilles Muller. WYSIWIB:​​​‌ exploiting fine-grained program structure​ in a scriptable API-usage​‌ protocol-finding process.Software:​​ Practice and Experience43​​​‌1January 2013,​ 67-92HALDOIback​‌ to text
• 35 inproceedings​​J.Julia Lawall,​​​‌ B.Ben Laurie,​ R. R.René Rydhof​‌ Hansen, N.Nicolas​​ Palix and G.Gilles​​​‌ Muller. Finding Error​ Handling Bugs in OpenSSL​‌ Using Coccinelle.European​​ Dependable Computing ConferenceValencia,​​​‌ SpainApril 2010,​ 191-196HALDOIback​‌ to text
• 36 inproceedings​​T.Tuo Li,​​​‌ J.-J.Jia-Ju Bai,​ Y.Yulei Sui and​‌ S.-M.Shi-Min Hu.​​ Path-sensitive and alias-aware typestate​​​‌ analysis for detecting OS​ bugs.ASPLOSACM​‌2022, 859--872back​​ to text
• 37 inproceedings​​​‌Z.Zhenmin Li,​ S.Shan Lu,​‌ S.Suvda Myagmar and​​ Y.Yuanyuan Zhou.​​​‌ CP-Miner: A Tool for​ Finding Copy-paste and Related​‌ Bugs in Operating System​​ Code.OSDI2004​​, 289--302back to​​​‌ text
• 38 inproceedingsZ.‌Zhenmin Li and Y.‌​‌Yuanyuan Zhou. PR-Miner:​​ automatically extracting implicit programming​​​‌ rules and detecting violations‌ in large software code‌​‌.Proceedings of the​​ 10th European Software Engineering​​​‌ Conference2005, 306--315‌back to text
• 39‌​‌ inproceedingsF.Fabrice Mérillon​​, L.Laurent Réveillère​​​‌, C.Charles Consel‌, R.Renaud Marlet‌​‌ and G.Gilles Muller​​. Devil: An IDL​​​‌ for Hardware Programming.‌4th Symposium on Operating‌​‌ System Design and Implementation​​ (OSDI)2000, 17--30​​​‌back to text
• 40‌ inproceedingsJ.Jeho Oh‌​‌, N. F.Necip​​ Fazil Yildiran, J.​​​‌Julian Braha and P.‌Paul Gazzillo. Finding‌​‌ broken Linux configuration specifications​​ by statically analyzing the​​​‌ Kconfig language.ESEC/FSE‌ACM2021, 893--905‌​‌back to text
• 41​​ inproceedingsL. R.Luis​​​‌ R. Rodriguez and J.‌ L.Julia L. Lawall‌​‌. Increasing Automation in​​ the Backporting of Linux​​​‌ Drivers Using Coccinelle.‌11th European Dependable Computing‌​‌ Conference - Dependability in​​ Practice11th European Dependable​​​‌ Computing Conference - Dependability‌ in PracticeParis, France‌​‌November 2015HALback​​ to text
• 42 inproceedings​​​‌L.Leonid Ryzhyk,‌ P.Peter Chubb,‌​‌ I.Ihor Kuz,​​ E.Etienne Le Sueur​​​‌ and G.Gernot Heiser‌. Automatic device driver‌​‌ synthesis with Termite.​​SOSP2009, 73--86​​​‌back to text
• 43‌ inproceedingsL.Leonid Ryzhyk‌​‌, A.Adam Walker​​, J.John Keys​​​‌, A.Alexander Legg‌, A.Arun Raghunath‌​‌, M.Michael Stumm​​ and M.Mona Vij​​​‌. User-Guided Device Driver‌ Synthesis.OSDI2014‌​‌, 661--676back to​​ text
• 44 inproceedingsR.​​​‌ K.Ripon K. Saha‌, J. L.Julia‌​‌ L. Lawall, S.​​Sarfraz Khurshid and D.​​​‌ E.Dewayne E Perry‌. On the Effectiveness‌​‌ of Information Retrieval Based​​ Bug Localization for C​​​‌ Programs.ICSME 2014‌ - 30th International Conference‌​‌ on Software Maintenance and​​ EvolutionIEEEVictoria, Canada​​​‌September 2014, 161-170‌HALDOIback to‌​‌ text
• 45 inproceedingsF.​​Ferdian Thung, D.​​​‌ X.Dinh Xuan Bach‌ Le, D.David‌​‌ Lo and J. L.​​Julia L. Lawall.​​​‌ Recommending Code Changes for‌ Automatic Backporting of Linux‌​‌ Device Drivers.32nd​​ IEEE International Conference on​​​‌ Software Maintenance and Evolution‌ (ICSME)IEEERaleigh, North‌​‌ Carolina, United StatesOctober​​ 2016HALback to​​​‌ text
• 46 inproceedingsW.‌Wei Wang and M.‌​‌M.W. Godfrey. A​​ Study of Cloning in​​​‌ the Linux SCSI Drivers‌.Source Code Analysis‌​‌ and Manipulation (SCAM)IEEE​​2011back to text​​​‌