Skip to main content

Automatic Device Driver Synthesis

Termite: Automatic Synthesis of Device Drivers

Overview

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. The key idea behind this approach is that the driver synthesis problem can be formalised as a two-player game between the driver and its environments, consisting of the hardware device and the OS. A correct driver implementation can then be obtained from a winning strategy in this game.

The goal of the Termite project is to turn this vision into a practical device driver synthesis tool. To this end, we must address two fundamental research challenges:

  • How do we efficiently solve games with over 2^1000 states? Such games, which routinely arise in driver synthesis, cannot be solved with existing game theoretic techniques. To address this challenge, we have developed an efficient game solving algorithm based on abstraction and symbolic computation.
  • How do we build a practical software development workflow around game-based synthesis? While in theory synthesis can work as a “push-button” technology that generates a specification-compliant implementation without any user involvement, in practice this seldom leads to satisfactory results. We believe that a practical synthesis tool must combine the power of automation with the flexibility of manual development. To this end, we have developed the user-guided synthesis method where the user and the tool interact to produce a driver implementation. The user has full control over the synthesis process, while the tool acts as an assistant that suggests, but does not enforce, implementation options and ensures correctness of the resulting code.

Getting started

The best way to start learning about Termite is by reading our OSDI'14 paper. For an in-depth look into the Termite core synthesis engine, please refer to the FMCAD'14 paper or the extended technical report. If you would like to take Termite for a test drive, you can download it through github. Follow the Getting Started tutorial in the documentation directory for a walk through the synthesis process using a simple example. Finally, you can find more realistic specifications and synthesised drivers in the specs directory.

Download

Termite can be downloaded from the github repository under the BSD license.

Termite is an experimental tool designed as a research vehicle for new synthesis algorithms and methodologies. It is still under development and as such is not yet as feature-complete and user-friendly as we would like it to be. Therefore, if you are considering using Termite in your project, we recommend that you contact Leonid or Adam to help you with evaluation.

Screenshots

User-guided code generation GUI

User-guided code generation GUI

Debugging using a counterexample strategy

Debugging using a counterexample strategy

External funding

  • Intel. In 2013, an international team consisting of researchers from NICTA, University of Toronto, University of Colorado Boulder, and Imperial College London received a generous gift of US$1.1M from Intel Corporation to carry out a research project titled Automatic Synthesis of High Assurance Device Drivers. The project is scheduled to run for three years. See project description and overview slides for more details.
  • Google. 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.

Collaborators

We collaborate with several academic and industry partners on various aspects of driver synthesis and related problems:
  • Intel Labs. 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.
  • Pavol Cerny (CU Boulder), Thomas Henzinger, Roopsha Samanta, Arjun Radhakrishna and Thorsten Tarrach (IST Austria) are looking into automatically transforming sequential drivers synthesised by Termite to work correctly in the multithreaded OS kernel environment. They have obtained some interesting preliminary results published in CAV'13 and CAV'14.
  • Alastair Donaldson, Ethel Bradsley, and Pantazis Deligiannis (Imperial College London) are working on improving the trustworthiness of synthesised drivers by validating them using automatic verification techniques.

People

Past

Publications

Abstract
Slides
PDF Pavol Cerny, Edmund Clarke, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach
From non-preemptive to preemptive scheduling using synchronization synthesis
International Conference on Computer Aided Verification, San Francisco, USA, July, 2015
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
SAT-based strategy extraction in reachability games
AAAI, Austin, TX, USA, January, 2015
Abstract
Slides
PDF Leonid Ryzhyk, Adam Christopher Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm and Mona Vij
User-guided device driver synthesis
USENIX Symposium on Operating Systems Design and Implementation, pp. 661-676, Broomfield, CO, USA, October, 2014
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Conference on Formal Methods in Computer-Aided Design, Lausanne, Switzerland, October, 2014
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Technical Report NRL-8281, NICTA, August, 2014
Abstract PDF Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach
Regression-free synthesis for concurrency
International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Interpolants in two-player games
Abstract, iPRA workshop, July, 2014.
Abstract PDF Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Practical CNF interpolants via BDDs
Abstract, iPRA workshop, July, 2014.
Abstract PDF Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Christopher Walker
Solving games without controllable predecessor
International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
Abstract PDF Mona Vij, John Keys, Arun Raghunath, Scott Hahn, Vincent Zimmer, Leonid Ryzhyk, Adam Christopher Walker and Alexander Legg
Device driver synthesis
Intel Technology Journal, Volume 17, Number 2, pp. 136-157, December, 2013
Abstract PDF Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach
Efficient synthesis for concurrency by semantics-preserving transformations
25th International Conference on Computer Aided Verification, pp. 1–16, Saint Petersburg, Russia, July, 2013
Abstract PDF Leonid Ryzhyk
On the construction of reliable device drivers
PhD Thesis, UNSW, Sydney, Australia, January, 2010
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
ACM Symposium on Operating Systems Principles, pp. 73-86, Big Sky, MT, US, October, 2009