Dingo: Taming Device Drivers

Select |




Print


Ryzhyk, Leonid; Chubb, Peter; Kuz, Ihor; Heiser, Gernot

Ryzhyk, Leonid; Chubb, Peter; Kuz, Ihor; Heiser, Gernot


2009-04-01


Conference Material


Eurosys 2009


Nuremberg, DE


275-288


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, and a multithreaded model of computation. The former results in drivers that violate expected protocols between the device and operating system, while the latter leads to concurrency-related faults such as deadlocks and race conditions. 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 protocols. It also enforces an event-driven model of computation, which eliminates most concurrency-related faults. Our implementation of the Dingo architecture in Linux avoids most concurrency errors and reduces the likelihood of protocol errors in Dingo drivers, while introducing negligible performance overhead. It allows Dingo and native Linux drivers to coexist, offering a gradual migration path to more reliable device drivers.


Operating Systems, Device Drivers, Reliability


http://eurosys2009.informatik.uni-erlangen.de/


nicta:1527


Ryzhyk, Leonid; Chubb, Peter; Kuz, Ihor; Heiser, Gernot. Dingo: Taming Device Drivers. In: Eurosys 2009; Nuremberg, DE. 2009-04-01. 275-288.



Loading citation data...

Citation counts
(Requires subscription to view)