DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

Capturing OS Expertise in an Event Type System: the Bossa Experience

Julia Lawall
DIKU

Thursday, May 8th, 15:15-16:00
DIKU, Universitetsparken 1, room N037

Abstract:

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.

Scientific host: Andrzej Filinski. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, IT-C and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org