IMADA - Department of Mathematics and Computer Science |
Operating system extensibility is essential to provide adequate service for demanding applications and execution environments. In this context, safety, correctness, and efficiency are all essential. Recently, verification approaches have been developed that are both lightweight and precise enough to find bugs in actual OS kernel code. Nevertheless, these approaches have not been directed to proving that systems code provides specific basic functionalities. We examine the problem of ensuring the correctness of operating system extensions from a domain-specific viewpoint, focusing on the extension of an operating system with new CPU scheduling policies. We have developed a domain-specific language Bossa that makes it easy to implement new policies in an existing operating system kernel. This language is instantiated with a set of event types, specific to the target operating system, that describe relevant information about the target system and the corresponding required behavior of the policy. We illustrate this approach in the context of the Linux operating system. Host: Joan Boyar
SDU HOME | IMADA HOME | Previous Page Last modified: September 23, 2003. Joan Boyar (joan@imada.sdu.dk) |