Back to overview

Provable Multicore Schedulers with Ipanema: Application to Work Conservation

Type of publication Peer-reviewed
Publikationsform Proceedings (peer-reviewed)
Author Lepers Baptiste, Gouicem Redha, Carver Damien, Lozi Jean-Pierre, Palix Nicolas, Apont Maria-Virginia, Zwaenepoel Willy, Sopena Julien, Lawall Julia, Muller Gilles,
Project Building Flexible Large-Graph Processing Systems on Commodity Hardware
Show all

Proceedings (peer-reviewed)

Title of proceedings EuroSys 2020
DOI 10.1145/3342195.3387544

Open Access

Type of Open Access Repository (Green Open Access)


Recent research and bug reports have shown that work conservation, the property that a core is idle only if no other core is overloaded, is not guaranteed by Linux's CFS or FreeBSD's ULE multicore schedulers. Indeed, multicore schedulers are challenging to specify and verify: they must operate under stringent performance requirements, while handling very large numbers of concurrent operations on threads. As a consequence, the verification of correctness properties of schedulers has not yet been considered. In this paper, we propose an approach, based on a domain-specific language and theorem provers, for developing schedulers with provable properties. We introduce the notion of concurrent work conservation (CWC), a relaxed definition of work conservation that can be achieved in a concurrent system where threads can be created, unblocked and blocked concurrently with other scheduling events. We implement several scheduling policies, inspired by CFS and ULE. We show that our schedulers obtain the same level of performance as production schedulers, while concurrent work conservation is satisfied.