skip to main content
10.1145/1292597.1292605acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article

Implementing reliable Linux device drivers in ATS

Published: 02 October 2007 Publication History

Abstract

Contemporary software systems often provide mechanisms forextending functionalities, which imposes great safety concerns on the well-being of critical infrastructures. ATS is a recently developed language with its type system rooted in Applied Type System framework which combines linear and dependent type theories for enforcing safe use of resources at low-level. In this paper, we describe a framework for constructing reliable Linux device drivers in ATS. Specifically, drivers are written and type checked in ATS, then compiled and linked to kernel with safety guarantee. Our preliminary experience shows that this approach can effectively enhance the reliability of device drivers and save the testing/debugging time.

References

[1]
Andy Chou, Junfeng Yang, Benjamin Chelf, Seth Hallem, and Dawson R. Engler. An empirical study of operating system errors. In Symposium on Operating Systems Principles, pages 73-88, 2001.
[2]
Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi. Language support for fast and reliable message-based communication in singularity os. In EuroSys '06: Proceedings of the 2006 EuroSys conference, pages 177-190, New York, NY, USA, 2006. ACM Press. ISBN 1-59593-322-0.
[3]
Thomas Hallgren, Mark P. Jones, Rebekah Leslie, and Andrew Tolmach. A principled approach to operating system construction in haskell. SIGPLAN Not., 40(9):116-128, 2005. ISSN 0362-1340.
[4]
Simon Peyton Jones et al. Haskell 98 - A non-strict, purely functional language. Available at http://www.haskell.org/onlinereport/, February 1999.
[5]
Alessandro Rubini, Jonathan Corbet, and Greg Kroah-Hartman. Linux Device Drivers, Third Edition. Oreilly and Associates Inc, 2005. ISBN 978-0596-00590-0.
[6]
Michael M. Swift, Brian N. Bershad, and Henry M. Levy. Improving the reliability of commodity operating systems. In SOSP '03: Proceedings of the nineteenth ACM symposium on Operating systems principles, pages 207-222, New York, NY, USA, 2003. ACM Press.
[7]
Hongwei Xi. Applied Type System (extended abstract). In post-workshop Proceedings of TYPES 2003, pages 394-408. Springer-Verlag LNCS 3085, 2004.
[8]
Dengping Zhu and Hongwei Xi. Safe Programming with Pointers through Stateful Views. In Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages , Long Beach, CA, January 2005. Springer-Verlag LNCS, 3350.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification
October 2007
76 pages
ISBN:9781595936776
DOI:10.1145/1292597
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 October 2007

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. ATS
  2. applied type system
  3. device driver programming

Qualifiers

  • Article

Conference

ICFP07
Sponsor:

Acceptance Rates

PLPV '07 Paper Acceptance Rate 6 of 8 submissions, 75%;
Overall Acceptance Rate 18 of 25 submissions, 72%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)3
  • Downloads (Last 6 weeks)0
Reflects downloads up to 14 Feb 2025

Other Metrics

Citations

Cited By

View all

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media