For OS developers, the quality and reputation of their OS depends greatly on the quality of its device drivers: major OS vendors suffer serious financial and image damage because of faulty drivers [10]. Driver quality can be improved by providing and encouraging the use of tools for automatic driver synthesis as part of driver development toolkits. Since Termite drivers can co-exist with conventional hand-written drivers, migration to automaticallygenerated drivers can be implemented gradually.

Another concern for OS developers is that acceptance and success of their OS depends largely on compatibility with a wide range of devices. Since device interface specifications are OS independent, providing support for driver synthesis allows the reuse of all existing Termite device interface specifications, leading to potential increases in an operating system’s base of compatible devices.

In this paper we make the following contributions. First, we present an approach to driver synthesis based on separate specifications of device and OS interfaces. Second, we define a formal language for specifying such interfaces. Third, we describe an algorithm based on game theory to generate drivers from the specifications. Finally, we evaluate the proposed approach based on our experience synthesising Linux and FreeBSD drivers for two real devices: a Secure Digital (SD) card host controller, and a USB-to-Ethernet adapter.

The rest of this paper is structured as follows. We start with a high-level overview of the synthesis methodology in Section 2. Section 3 describes the specification language of Termite, while Section 4 presents a sample driver specification illustrating how real device and OS interfaces are defined in this language. Section 5 outlines our driver synthesis algorithm, followed by a qualitative and quantitative evaluation of the Termite approach and the resulting drivers in Section 6. Section 7 discusses the limitations of the current Termite implementation. Finally, we survey related work in Section 8 and draw conclusions in Section 9.

2. OVERVIEW OF DRIVER SYNTHESIS

Termite generates an implementation of a driver based on a formal specification of its device and OS interfaces. The device interface specification describes the programming model of the device, including its software-visible states and behaviours. The OS interface specification defines services that the driver must provide to the rest of the system, as well as OS services available to the driver. Given these specifications, Termite produces a driver implementation that translates any valid sequence of OS requests into a sequence of device commands.