Dingo

The Dingo project investigates how existing operating systems, such as Linux, can be made more driver-friendly without radically changing their architecture. To this end, we analysed the main factors that complicate driver development and provoke bugs. We used the results of this analysis to define a new device driver architecture that simplifies driver development and helps reduce errors.

Where do bugs come from?

The chart shows a summary of our study of 500 bugs found in Linux device drivers.

In Dingo, we focus on two types of bugs—concurrency bugs, i.e. race conditions and deadlocks resulting from incorrect synchronisation of OS threads inside the driver, and OS protocol violations, i.e. situations when the driver fails to behave the way the OS expects it to. The common property of these types of bugs is that both of them are related to how the driver interacts with the OS. Dingo tackles these bugs by defining a cleaner and more disciplined interface between the driver and the OS, which simplifies driver development and helps avoid errors.

The Dingo architecture can be implemented as a standalone driver framework or as an extension of an existing OS driver framework. Our current implementation of Dingo in Linux consists of runtime adapters that translate Linux driver protocols into Dingo protocols and a compiler for the Tingu protocol specification language, described below. This implementation allows Dingo and Linux drivers to coexist in the same system, thus offering a smooth migration path to more relable device drivers.

Dealing with concurrency bugs

Our study of driver bugs confirmed that driver developers generally fail to correctly handle multithreading inside the driver. This led us to replace the multithreaded model of computation for drivers with a more disciplined event-based model, where a driver is triggered by a sequence of events from the environment, such as I/O requests or device interrupts. Events are delivered atomically, thus reducing the amount of concurrency and non-determinism that the driver must handle. For performance reasons, drivers are not allowed to block inside an event handler.

The Dingo runtime framework serialises all invocatins of the driver, thus taking over the burden of synchronisation from the driver developer. Importantly, such serialisation is implemented without sacrificing the performance: as shown in our Eurosys'09 paper, Dingo drivers achieve I/O throughput, latency, and CPU utilisation very close to those of native Linux drivers.

Dealing with OS protocol violations

Linux (as well as other current OSes) defines many types of events exchanged with the driver along with constraints on the ordering and arguments of these events. While these constraints are not intrinsically complex, they are often left undocumented, which confuses driver developers and provokes bugs. In Dingo, we specify driver protocols using Tingu—a visual language based on state machines, which allows capturing constraints on driver behaviour in a concise and clear manner. For example, the following figure shows a fragment of the Ethernet controller driver protocol.

Given a Tingu specification of driver protocols, the driver developer implements the driver in C, pretty much as he would normally do. The protocol specifications serve as guidelines that explicitly name events that the driver is required to handle or generate in every state.

Since the Tingu language has well-defined formal semantics, Tingu specifications can be used as properties against which a driver implementation can be verified either statically or at runtime. Dingo currently supports runtime verification by compiling driver protocol specifications into a runtime observer that intercepts all communication between the driver and the OS and detects protocol violations committed by either side.

In principle, Tingu specifications could also be used to generate driver templates to be filled by the developer with device-specific details. We currently do not support this in Dingo. Instead, we are working on a more radical approach, which consists of generating a complete driver implementation fully automatically, from a combination of device and OS protocol specifications.

People

Publications

		Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu Automatic verification of active device drivers ACM Operating Systems Review, Volume 48, Number 1, May, 2014
		Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser The case for active device drivers Asia-Pacific Workshop on Systems (APSys), pp. 25–30, New Delhi, India, August, 2010
		Leonid Ryzhyk On the construction of reliable device drivers PhD Thesis, UNSW, Sydney, Australia, January, 2010