Synthesizing Device Drivers with Ghost Writer

Authors

Bingyao Wang, Sepehr Noorafshan, Reto Achermann and Margo Seltzer

Venue

Proceedings of the 12th Workshop on Programming Languages and Operating Systems (PLOS'23)

Links

[ .doi ] [ .pdf ] [ .bib ]

Abstract

Device drivers are components that enable operating systems to interact with devices. Unfortunately, they are the main source of bugs in operating systems, because writing a driver is an intricate and error-prone process that requires extensive knowledge of devices and operating systems. Furthermore, supporting new devices and accommodating kernel revisions require significant development effort. To facilitate the development of device drivers, we present Ghost Writer, an end-to-end toolchain that allows developers to synthesize correct-by-construction device drivers from high-level specifications. Ghost Writer supports control and data plane operations (e.g., handling DMA transactions). It makes synthesis tractable by 1) modeling the device interface as a set of virtual registers that abstract the hardware details and 2) leveraging behavior trees to model operations on virtual registers and synthesize complex operations from simpler ones. Our prototype can synthesize putc for the PL011 UART device and send_packet for the VirtIO network device. We believe that Ghost Writer can be the foundation towards automating the development of correct-by-construction device drivers.

Bibtex

@inproceedings{Wang:2023:SDD,
 author = {Wang, Bingyao and Noorafshan, Sepehr and Achermann, Reto and Seltzer, Margo},
 booktitle = {Proceedings of the 12th Workshop on Programming Languages and Operating Systems},
 doi = {10.1145/3623759.3624545},
 id = {Wang:2023:SDD},
 isbn = {9798400704048},
 location = {Koblenz, Germany},
 pages = {10–17},
 publisher = {Association for Computing Machinery},
 series = {PLOS'23},
 title = {Synthesizing Device Drivers with Ghost Writer},
 url = {https://doi.org/10.1145/3623759.3624545},
 year = {2023}
}

Contact

The University of British Columbia
Department of Computer Science
2366 Main Mall
ICICS Building, Office 341
Vancouver, BC V6T 1Z4
Canada

achreto [at] cs.ubc.ca
+1 604 827 2446