< Retour au sommaire

Provable Multicore Schedulers with Ipanema

Julia Lawall le

Lieu: TBA

An OS-kernel thread scheduler decides which thread runs at a given moment on a given core. A scheduler is thus a key OS service since any bad decision that it makes may lead to cores wasting cycles and may increase application response times. Validating the good behavior of a multicore scheduler calls for proofs, but today’s production schedulers reach tens of thousands of lines of C code, making proofs of the scheduling policy impractical. In this work, we propose the use of a domain-specific language to raise the level of abstraction, reduce the code size, and guide proofs, taking the property of work conservation (no core is idle if any core is overloaded) as an example.

To appear at Eurosys 2020. Joint work with B. Lepers, R. Gouicem, D. Carver, J. Lozi, N. Palix, V. Aponte, W. Zwaenepoel, J. Sopena, and G. Muller.