The goal of this PhD is to design safe and efficient Linux kernel schedulers.
The PhD topic is both in the domains of programming languages and systems. First, we aim at looking both to program proving and abstraction interpretation for improving safety of schedulers. Second, we are looking to improving the performance of schedulers by improving the latency of scheduling events in a multicore setting. The challenge here is to come up with optimization that are both safe and proved.
The PhD will be conducted in the Inria Whisper team as part of the ANR VeriAmos project.
We are looking for students motivated by both operating systems and program analysis or proving. An experience in one of this domains is mandatory.
Applications will be reviewed as soon they are received.