Implementing reliable Linux device drivers in ATS

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 , Dawson Engler, An empirical study of operating systems errors, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 2: Manuel Fähndrich , Mark Aiken , Chris Hawblitzel , Orion Hodson , Galen Hunt , James R. Larus , Steven Levi, Language support for fast and reliable message-based communication in singularity OS, Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, April 18-21, 2006, Leuven, Belgium
• 3: Thomas Hallgren , Mark P. Jones , Rebekah Leslie , Andrew Tolmach, A principled approach to operating system construction in Haskell, ACM SIGPLAN Notices, v.40 n.9, September 2005
• 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 , Henry M. Levy, Improving the reliability of commodity operating systems, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 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.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability

General Terms:
Languages

Keywords:
ATS, applied type system, device driver programming