The University of New South Wales Intel Google

Termite: Automatic Synthesis of Device Drivers

Overview

In this project we explore a radically new approach to driver development. We believe that the conventional manual driver development methodology is redundant since all the knowledge required to control the device from software is created during the design of the device and hence a driver for the device can be derived automatically from hardware design artifacts.

Following this vision, we are implementing a driver synthesis tool called Termite that takes a high-level model of the I/O device written in one of standard hardware modelling languages (SystemC, SystemVerilog, or DML) and a formal specification of the interface between the driver and the operating system and generates a driver implementation in C.

Technical research challenges

  • The state explosion problem. In driver synthesis we are dealing with complex device specifications that contain a large number of state variables. Existing game theoretic algorithms do no scale to systems of such complexity. We are developing techniques to eliminate this barrier, including abstraction and symbolic state space representation.
  • Partial information. In controlling an I/O device, the driver does not have complete visibility of its internal state. Synthesis under partial information involves an additional exponential blow-up in complexity in the worst case. In practice, this blow-up can often be avoided using compositional reasoning and abstraction.
  • Practical driver synthesis. The synthesis tool will necessarily impose certain constraints on how device models are written. The goal is to make these constraints easy to understand for hardware engineers and to make sure that existing device models can be reused for synthesis with minimal changes.

Our partners

  • Our approach to driver synthesis will not work without cooperation from hardware vendors. Therefore we are pursuing this research in collaboration with the OS Research Group at Intel Labs.
  • We are a proud recipient of a Google Research Award. This award will enable us to put more manpower on the project and purchase equipment in 2010.

People

Publications

plain text PDF Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk
The road to trustworthy systems
Proceedings of the 5th ACM Workshop on Scalable Trusted Computing (ACMSTC), Chicago, IL, USA, October, 2010
Invited paper
plain text PDF Leonid Ryzhyk
On the construction of reliable device drivers, PhD Thesis, School of Computer Science and Engineering, Sydney, Australia, 2010
plain text PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009