Towards Proving Optimistic Multicore Schedulers

Operating systems have been shown to waste machine resources by leaving cores idle while work is ready to be scheduled. This results in suboptimal performance for user applications, and wasted power. Recent progress in formal verification methods have led to operating systems being proven safe, but operating systems have yet to be proven free of performance bottlenecks. In this paper we instigate the first effort in proving performance properties of operating systems by designing a multicore scheduler that is proven to be work-conserving.


Published in:
HotOS
Year:
2017
Keywords:
Laboratories:




 Record created 2017-05-02, last modified 2018-09-13

Postprint:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)