Dingo: taming device drivers

Device drivers are notorious for being a major source of failure in operating systems. In analysing a sample of real defects in Linux drivers, we found that a large proportion (39%) of bugs are due to two key shortcomings in the device-driver architecture enforced by current operating systems: poorly-defined communication protocols between drivers and the OS, which confuse developers and lead to protocol violations, and a multithreaded model of computation that leads to numerous race conditions and deadlocks. We claim that a better device driver architecture can help reduce the occurrence of these faults, and present our Dingo framework as constructive proof. Dingo provides a formal, state-machine based, language for describing driver protocols, which avoids confusion and ambiguity, and helps driver writers implement correct behaviour. It also enforces an event-driven model of computation, which eliminates most concurrency-relatedfaults. Our implementation of the Dingo architecture i...

• Type: Conference
• Year: 2009
• Where: EUROSYS
• Authors: Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Gernot Heiser
• Keywords: Device Driver Architecture, EUROSYS 2009, Native Linux Drivers, Reliable Device Drivers, System Software