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 metadatas

Cited literature [57 references]  Display  Hide  Download

https://hal.inria.fr/hal-02554342
Contributor : Gilles Muller <>
Submitted on : Saturday, April 25, 2020 - 4:09:34 PM
Last modification on : Thursday, September 3, 2020 - 3:56:28 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

124

Files downloads

377