Driver Synthesis is one activity of the Trustworthy Systems group.
Aim: develop a practical methodology for automatic
synthesis of device drivers from existing I/O device specifications.
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
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.
More information can be found on the
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 2010 Google Research Award.