Untangling device drivers
Device drivers are hard to write. Moreover, they tend to receive less
scrutiny (the `many eyes look deep') than core parts of the Linux
kernel. This means that bugs are far more likely in device drivers
than in any other part of the kernel code.
The situation is exacerbated because the rules for writing device
drivers are arcane, complex, and change fairly often --- and that's
talking only about the kernel interfaces. In addition there is no
isolation between a driver's operation and the rest of the kernel,
which means that driver bugs can (and sometimes do) cause the entire
machine to freeze, crash, or otherwise misbehave.
We've been trying to work out how to improve the situation.
First, one can simplify drivers by removing all possibility of concurrency
in the driver. A state-machine driver model can be made just as
efficient as the current driver model, and has the advantage of being
easier to specify and implement than current drivers.
Secondly, we define the interface between a driver and the rest of the
system, and specify it semi-formally in a checkable language that can
generate appropriate header files. This approach keeps Linux's
traditional ability to change the driver/kernel interface, and
offers a way to document changes in a clear and rigorous way.
We've implemented a prototype device driver (for a USB NIC). In the
talk we'll describe the framework, and also the prototype, and discuss
the issues. We'll also reveal the statistical study we've made of
Linux driver bugs, and show how many could have been avoided by our
The main work for this was done by Leonid Ryzhyk. Peter Chubb implemented part of the prototype framework. The presentation will be shared between Peter and Leonid.
Peter started using Unix in 1979, and was programming for the Edition 7 kernel by 1982. He started using Linux with the Manchester Computer Centre distribution (Linux kernel verson 0.91).
He helped to found Slug, the Sydney Linux Users' Group, in 1993, and has been active in the Linux community ever since. He currently manages Gelato@UNSW, a group working on Linux scalability and performance.