Trustworthy Systems

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:

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

Collaborators

We collaborate with several academic and industry partners on various aspects of driver synthesis and related problems:

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
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