Capturing OS expertise in an event type system
Julia Lawall, Gilles Muller, Luciano Porto Barreto · 2002
Emerging applications have increasingly specialized scheduling requirements. Changing the scheduling policy of an existing OS is, however, often difficult because scheduling code is typically deeply intertwined with the rest of the kernel. We have recently introduced the Bossa framework to facilitate the implementation and integration of new scheduling policies. While the use of Bossa simplifes the problem of implementing a new scheduler, knowledge of the control and data flow through the scheduling actions of the kernel is still needed to ensure that the behavior of the provided scheduling policy matches kernel expectations. In this paper, we propose a modular type system that provides a high-level characterization of the aspects of kernel behavior that affect the correctness of a scheduling policy. These types guide policy development and are linked with the compiler to enable static verification of correctness properties.