User-Guided Device Driver Synthesis
Leonid Ryzhyk, University of Toronto, NICTA, and University of New South Wales; Adam Walker, NICTA and University of New South Wales; John Keys, Intel Corporation; Alexander Legg, NICTA and University of New South Wales; Arun Raghunath, Intel Corporation; Michael Stumm, University of Toronto; Mona Vij, Intel Corporation
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 a new driver synthesis toolkit, called Termite-2. Termite-2 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 Termite-2 by synthesizing drivers for a number of I/O devices representative of a typical embedded platform.
Open Access Media
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.
author = {Leonid Ryzhyk and Adam Walker and John Keys and Alexander Legg and Arun Raghunath and Michael Stumm and Mona Vij},
title = {{User-Guided} Device Driver Synthesis},
booktitle = {11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)},
year = {2014},
isbn = { 978-1-931971-16-4},
address = {Broomfield, CO},
pages = {661--676},
url = {https://www.usenix.org/conference/osdi14/technical-sessions/presentation/ryzhyk},
publisher = {USENIX Association},
month = oct
}
connect with us