Trustworthy Systems

User-guided device driver synthesis

Authors

Leonid Ryzhyk, Adam Christopher Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm and Mona Vij

NICTA

Intel Corporation

University of Toronto

Abstract

Automatic device driver synthesis is a radical approach to creating drivers faster and with fewer defects by generating them automatically based on hardware device specifications. We present the design and implementation of the first practical driver synthesis toolkit, called Numbat. Numbat is the first tool to combine the power of automation with the flexibility of conventional development. It is also the first practical synthesis tool based on abstraction refinement. Finally, it is the first synthesis tool to support automated debugging of input specifications. We demonstrate the practicality of Numbat by synthesizing drivers for several I/O devices representative of a typical embedded platform: a webcam, a serial controller, an I2C bus, a real-time clock, and a hard disk controller.

BibTeX Entry

  @inproceedings{Ryzhyk_WKLRSV_14,
    address          = {Broomfield, CO, USA},
    author           = {Ryzhyk, Leonid and Walker, Adam Christopher and Keys, John and Legg, Alexander and Raghunath, Arun
                        and Stumm, Michael and Vij, Mona},
    booktitle        = {USENIX Symposium on Operating Systems Design and Implementation},
    keywords         = {termite, device drivers, abstraction refinement, predicate abstraction},
    month            = oct,
    pages            = {661--676},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8077.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/8077.pdf},
    title            = {User-Guided Device Driver Synthesis},
    year             = {2014}
  }

Download