Trustworthy Systems

Dingo: Taming device drivers

Authors

Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser

NICTA

UNSW

Open Kernel Labs

Abstract

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.

BibTeX Entry

  @inproceedings{Ryzhyk_CKH_09,
    address          = {Nuremberg, DE},
    author           = {Ryzhyk, Leonid and Chubb, Peter and Kuz, Ihor and Heiser, Gernot},
    booktitle        = {EuroSys Conference},
    keywords         = {operating systems, device drivers, reliability},
    month            = apr,
    pages            = {275--288},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/1527.pdf},
    title            = {Dingo: Taming Device Drivers},
    year             = {2009}
  }

Download