Automatic Device Driver Synthesis

Device drivers are tedious to write and they are notoriously unreli-able. Automatic device driver synthesis is a radical approach to creatingdrivers faster and with fewer defects by generating them automaticallyfrom operating system and hardware device specifications. This the-sis addresses the two fundamental challenges in driver synthesis: (1)usability and (2) scalability.The usability challenge is to enable developers to create driversthrough a well-defined, predictable sequence of steps. It falls into thefollowing three design objectives: (1) ease of developing specificationsfor driver synthesis, (2) ease of debugging synthesis errors due to incor-rect specifications, and (3) enabling the benefits of automation withoutsacrificing the flexibility of conventional driver development. In thisthesis I develop a new driver synthesis methodology that addressesthe first objective through a modular high-level specification languagewhose syntax and semantics are close to those of familiar imperativeprogramming languages like C. I address the second objective by devel-oping powerful debugging techniques that help the developer identifyand fix specification defects through a well-defined process. Finally,the proposed methodology strikes the balance between automation andflexibility by generating driver code in a user-guided fashion, wherethe user can interactively alter or amend automatically generated code,while the synthesis tool verifies user changes.The scalability challenge is to create a synthesis algorithm that iscapable of handling real-world device specifications. I address this chal-lenge with a new scalable synthesis engine based on predicate-basedabstraction refinement. Solutions are developed to the three key prob-lems involved in the implementation of efficient predicate abstraction,which have not been addressed previously in a synthesis setting: (1)keeping abstractions concise, (2) solving abstract games efficiently, (3)and computing abstractions symbolically.The proposed techniques are implemented in a new tool calledTermite-2 and evaluated by synthesising drivers for a number of I/Odevices representative of a typical embedded platform. Termite-2 is thefirst tool to combine the power of automation with the flexibility of con-ventional development. It is also the first practical synthesis tool basedon abstraction refinement. Finally, it is the first synthesis tool to supportautomated debugging of input specifications