Automatic device driver synthesis with termite

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Automatic device driver synthesis with termite

Full text

Pdf (548 KB)

Source

ACM Symposium on Operating Systems Principles archive
Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles table of contents

Big Sky, Montana, USA

SESSION: Device drivers table of contents

Pages 73-86

Year of Publication: 2009

ISBN:978-1-60558-752-3

Authors

Leonid Ryzhyk	NICTA, UNSW, Sydney, Australia
Peter Chubb	NICTA, UNSW, Sydney, Australia
Ihor Kuz	NICTA, UNSW, Sydney, Australia
Etienne Le Sueur	NICTA, UNSW, Sydney, Australia
Gernot Heiser	NICTA, UNSW, Open Kernel Labs, Sydney, Australia

Sponsors

ACM: Association for Computing Machinery
SIGOPS: ACM Special Interest Group on Operating Systems

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 62, Downloads (12 Months): 62, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1629575.1629583 What is a DOI?

ABSTRACT

Faulty device drivers cause significant damage through down time and data loss. The problem can be mitigated by an improved driver development process that guarantees correctness by construction. We achieve this by synthesising drivers automatically from formal specifications of device interfaces, thus reducing the impact of human error on driver reliability and potentially cutting down on development costs.

We present a concrete driver synthesis approach and tool called Termite. We discuss the methodology, the technical and practical limitations of driver synthesis, and provide an evaluation of non-trivial drivers for Linux, generated using our tool. We show that the performance of the generated drivers is on par with the equivalent manually developed drivers. Furthermore, we demonstrate that device specifications can be reused across different operating systems by generating a driver for FreeBSD from the same specification as used for Linux.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S.K. Rajamani, and A. Ustuner. Thorough static analysis of device drivers. In 1st EuroSys Conf., pages 73--85, Leuven, Belgium, Apr 2006.
	2	V. Chipounov and G. Candea. Reverse-engineering drivers for safety and portability. In 4th HotDep, San Diego, CA, USA, Dec 2008.
	3	A. Chou, B. Fulton, and S. Hallem. Linux kernel security report, 2005.
	4	M. Condict, D. Bolinger, D. Mitchell, and E. McManus. Microkernel modularity with integrated kernel performance. Technical report, OSF Research Institute, Jun 1994.
	5	C.L. Conway and S.A. Edwards. NDL: a domain-specific language for device drivers. In LCTES'04, pages 30--36, Washington, DC, USA, Jun 2004.
	6	J. Corbet, A. Rubini, and G. Kroah-Hartman. Linux Device Drivers. O'Reilly & Associates, Inc, 3rd edition, 2005.
	7	A. Edvardsson. SD card mass storage controller. http://www.opencores.org.
	8	D.R. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In 4th OSDI, pages 1--16, San Diego, CA, Oct 2000.
	9	U. Erlingsson, M. Abadi, M. Vrable, M. Budiu, and G.C. Necula. XFI: software guards for system address spaces. In 7th OSDI, pages 75--88, Seattle, Washington, Nov 2006.
	10	A. Ganapathi, V. Ganapathi, and D. Patterson. Windows XP kernel crash analysis. In 20th LISA, pages 101--111, Washington, DC, USA, 2006.
	11	T. Henzinger, R. Jhala, and R. Majumdar. Counterexample-guided control. In 30th ICALP, pages 886--902, Jul 2003.
	12	J.N. Herder, H. Bos, B. Gras, P. Homburg, and A.S. Tanenbaum. MINIX 3: A highly reliable, self-repairing operating system. Operat. Syst. Rev., 40(3):80--89, Jul 2006.
	13	IEEE 802.3 Ethernet working group. http://grouper.ieee.org/groups/802/3/.
	14	LOTOS -- a formal description technique based on the temporal ordering of observational behavior, 1989. ISO Standard 8807.
	15	B. Leslie, P. Chubb, N. Fitzroy-Dale, S. Götz, C. Gray, L. Macpherson, D. Potts, Y. R. Shen, K. Elphinstone, and G. Heiser. User-level device drivers: Achieved performance. Journal of Computer Science and Technology, 20(5):654--664, Sep 2005.
	16	J. Liedtke, U. Bartling, U. Beyer, D. Heinrichs, R. Ruland, and G. Szalay. Two years of experience with a μ-kernel based OS. Operat. Syst. Rev., 25(2):51--62, Apr 1991.
	17	F. Mérillon, L. Réveillère, C. Consel, R. Marlet, and G. Muller. Devil: An IDL for hardware programming. In 4th OSDI, pages 17--30, San Diego, CA, USA, Oct 2000.
	18	M. O'Nils, J. Öberg, and A. Jantsch. Grammar based modelling and synthesis of device drivers and bus interfaces. In 24th Euromicro Conf., Washington, DC, USA, 1998.
	19	Realtek Corp. Single-chip multifunction 10/100mbps Ethernet controller with power management. datasheet., 2005.
	20	L. Ryzhyk, P. Chubb, I. Kuz, and G. Heiser. Dingo: Taming device drivers. In 4th EuroSys Conf., Nuremberg, Germany, Apr 2009.
	21	SD Card Association. SD specifications part 1: Physical layer simplified specification, version 2.00, 2006.
	22	SD Card Association. SD specifications part a2: SD host controller simplified specification, version 2.00, 2007.
	23	J. Sun, W. Yuan, M. Kallahalla, and N. Islam. HAIL: a language for easy and correct device access. In 5th EMSOFT, pages 1--9, Jersey City, NJ, USA, Sep 2005.
	24	M.M. Swift, B.N. Bershad, and H.M. Levy. Improving the reliability of commodity operating systems. In 19th SOSP, Bolton Landing (Lake George), New York, USA, Oct 2003.
	25	W. Thomas. On the synthesis of strategies in infinite games. In 12th STACS, pages 1--13, 1995.
	26	E. Walkup and G. Borriello. Automatic synthesis of device drivers for hardware/software co-design. Technical Report 94-06-04, University of Washington, Aug 1994.
	27	S. Wang, S. Malik, and R.A. Bergamaschi. Modeling and integration of peripheral devices in embedded systems. In 40th DATE, 2003.
	28	F. Zhou, J. Condit, Z. Anderson, I. Bagrak, R. Ennals, M. Harren, G. Necula, and E. Brewer. SafeDrive: Safe and recoverable extensions using language-based techniques. In 7th OSDI, pages 45--60, Seattle, WA, USA, Nov 2006.