An alternative to fault detection and isolation is an improved driver development process that guarantees correctness by construction. One way to achieve this is to synthesise device drivers automatically from a device specification, thus reducing the impact of human error on driver reliability and potentially cutting down on development costs. We have implemented a tool called Termite that does exactly that. Termite combines two formal specifications: one describing the device’s registers and behaviour, and one describing the interface between the driver and the OS, to synthesise a complete driver implementation in C. With Termite, the problem of writing a correct driver is reduced to one of obtaining or developing correct specifications.

Separating device description from OS-related details is a key aspect of our approach. It allows the people with the most appropriate skills and knowledge to develop specifications: device interface specifications can be developed by device manufacturers, and OS interface specifications by the OS developers who have intimate knowledge of the OS and the driver support it provides. In a hand-written device driver, interactions with the device and with the OS are intermingled, leading to drivers that are harder to write and harder to maintain. Termite specifications each deal with a single concern, and thus can be simpler to understand and debug than a full-blown driver.

Device interface specifications are independent of any OS, so drivers for different OSes can be synthesised from a single specification developed by a device manufacturer, thus avoiding penalizing less popular OSes with poor-quality drivers. A further benefit of device and OS separation is that any change in the OS need only be expressed in the OS-interface specification in order to re-generate all drivers for that OS. This is particularly interesting for Linux, which frequently changes its device driver interfaces from release to release.

Generating code from formal specifications reduces the incidence of programming errors in drivers. Assuming that the synthesis tool is correct, synthesised code will be free of many types of programming errors, including memory management and synchronisation bugs, missing return value checks, etc. A bug in a driver can occur only as a result of an error in the specification.

The likelihood of errors due to incorrect OS interface specifications is reduced because these specifications are shared by many drivers and are therefore subject to extensive testing. Errors in device specifications can be reduced by using model checking techniques to establish formal correspondence between the actual device behaviour, as defined in its register-transfer-level description, and the Termite specification. However, this capability is not yet supported in Termite.

While the above discussion is concerned with the technical implications of automatic driver synthesis, the real-world success of this approach depends on device manufacturers and OS developers adopting it.

For device manufacturers, our approach has the potential to reduce driver development effort while increasing driver quality. Furthermore, once developed, a driver specification will allow drivers to be synthesised for any supported OS, thus increasing the OS support for the device.