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

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

• 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) were working on improving the trustworthiness of synthesised drivers by validating them using automatic verification techniques.

People

Publications

		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
		Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk SAT-based strategy extraction in reachability games AAAI, Austin, TX, USA, January, 2015
		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
		Adam Christopher Walker and Leonid Ryzhyk Predicate abstraction for reactive synthesis Conference on Formal Methods in Computer-Aided Design, Lausanne, Switzerland, October, 2014
		Adam Christopher Walker and Leonid Ryzhyk Predicate abstraction for reactive synthesis Technical Report NRL-8281, NICTA, August, 2014
		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
		Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk Interpolants in two-player games Abstract, iPRA workshop, July, 2014.
		Alexander Legg, Nina Narodytska and Leonid Ryzhyk Practical CNF interpolants via BDDs Abstract, iPRA workshop, July, 2014.
		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
		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
		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
		Leonid Ryzhyk On the construction of reliable device drivers PhD Thesis, UNSW, Sydney, Australia, January, 2010
		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