COPLAS talk: Julia Lawall: Towards Verification of Linux Kernel Code

Speaker

Julia Lawall is a researcher at Inria Paris. She was on the faculty atDIKU in 2000-2011. Her work is at the intersection of systems, programminglanguages, and software engineering. She has developed the transformationtool Coccinelle that is extensively used on the Linux kernel. Building onthis work, she is currently investigating operating system performanceverification of operating system code. She is a program chair of USENIXATC 2023, DSN 2024, and EuroSys 2025, and an associate editor of thejournal Science of Computer Programming. 

Title

Towards Verification of Linux Kernel Code

Abstract

An operating system controls all of the resources on a computer, and assuch its correctness is essential. There have been several recent effortsto design operating systems in a way that facilitates their verification,but these are not operating systems that are widely used. We targetverification of some core parts of the Linux kernel. In additional to theusual challenges of software verification, we have to additionally addressthe fact that the Linux kernel changes frequently, with a new release every2-3 months. In this talk, we present our first effort, verification of thefunction should_we_balance, which has existed in 11 variants since 2013.We study in particular the impact of the changes in the source code on theverification process and the bugs and the missed optimization opportunitiesthat the process of verifying the code has helped to identify. 

Joint work with Keisuke Nishimura. 

Host

Fritz Henglein (DIKU)

All are welcome. No registration required.  Feel free to forward this invitation. 

The Copenhagen Programming Languages Seminar (COPLAS) is a collaboration between DTU, ITU, Roskilde University and UCPH. To be informed about COPLAS activities and related talks, join this mailing list.