HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Provable Multicore Schedulers with Ipanema: Application to Work Conservation

Abstract : 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 sched-ulers 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [57 references]  Display  Hide  Download

Contributor : Gilles Muller Connect in order to contact the contributor
Submitted on : Saturday, April 25, 2020 - 4:09:34 PM
Last modification on : Wednesday, March 16, 2022 - 3:44:12 AM


Files produced by the author(s)



Baptiste Lepers, Redha Gouicem, Damien Carver, Jean-Pierre Lozi, Nicolas Palix, et al.. Provable Multicore Schedulers with Ipanema: Application to Work Conservation. Eurosys 2020 - European Conference on Computer Systems, Apr 2020, Heraklion / Virtual, Greece. ⟨10.1145/3342195.3387544⟩. ⟨hal-02554342⟩



Record views


Files downloads