Details

Autor(en) / Beteiligte

• Wang, Bingyao
• Noorafshan, Sepehr
• Achermann, Reto
• Seltzer, Margo

Titel

Synthesizing Device Drivers with Ghost Writer

Ist Teil von

• Proceedings of the 12th Workshop on Programming Languages and Operating Systems, 2023, p.10-17

Ort / Verlag

New York, NY, USA: ACM

Erscheinungsjahr

2023

Quelle

ACM Digital Library

Beschreibungen/Notizen

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