A Typed Interrupt Calculus

  • Jens Palsberg
  • Di Ma
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


Most real-time systems require responsive interrupt handling. Programming of interrupt handlers is challenging: in order to ensure responsiveness, it is often necessary to have interrupt processing enabled in the body of lower priority handlers. It would be a programming error to allow the interrupt handlers to interrupt each other in a cyclic fashion; it could lead to an unbounded stack. Until now, static checking for such errors could only be done using model checking. However, the needed form of model checking requires a whole-program analysis that cannot check program fragments. In this paper, we present a calculus that contains essential constructs for programming interrupt-driven systems. The calculus has a static type system that guarantees stack boundedness and enables modular type checking. A number of common programming idioms have been type checked using our prototype implementation.


  1. 1.
    Martín Abadi and Luca Cardelli. A Theory of Objects. Springer-Verlag, 1996.Google Scholar
  2. 2.
    Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1981.zbMATHGoogle Scholar
  3. 3.
    Dennis Brylow, Niels Damgaard, and Jens Palsberg. Static checking of interrupt-driven software. In Proceedings of ICSE’01, 23rd International Conference on Software Engineering, pages 47–56, Toronto, May 2001.Google Scholar
  4. 4.
    Luca Cardelli and Andrew D. Gordon. Mobile ambients. In M. Nivat, editor, Proceedings of Foundations of Software Science and Computation Structures, pages 140–155. Springer-Verlag (LNCS 1378), 1998.CrossRefGoogle Scholar
  5. 5.
    M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and lambda-calculus semantics. In J. Seldin and J. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 535–560. Academic Press, 1980.Google Scholar
  6. 6.
    J. Roger Hindley. Types with intersection: An introduction. Formal Aspects of Computing, 4:470–486, 1991.CrossRefGoogle Scholar
  7. 7.
    R. Milner. A Calculus of Communicating Systems. Springer-Verlag (LNCS 92), 1980.zbMATHGoogle Scholar
  8. 8.
    Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, part I/II. Information and Compuation, 100(1):1–77, September 1992.Google Scholar
  9. 9.
    Mayur Naik and Jens Palsberg. Compiling with code-size constraints. In LCTES’02, Languages, Compilers, and Tools for Embedded Systems joint with SCOPES’02, Software and Compilers for Embedded Systems, June 2002.Google Scholar
  10. 10.
    Jens Palsberg. Type-based analysis and applications. In Proceedings of PASTE’01, ACM Workshop on Program Analysis for Software Tools, pages 20–27, June 2001.Google Scholar
  11. 11.
    Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. Journal of Functional Programming, 11(3):263–317, May 2001.Google Scholar
  12. 12.
    Jens Palsberg and Matthew Wallace. Reverse engineering of real-time assembly code. Manuscript, 2002.Google Scholar
  13. 13.
    Andreas Podelski. Model checking as constraint solving. In Proceedings of SAS’00, International Static Analysis Symposium, pages 22–37. Springer-Verlag (LNCS 1824), 2000.Google Scholar
  14. 14.
    Wayne Wolf. Computers as Components, Principles of Embedded Computing System Design. Morgan Kaufman Publishers, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Jens Palsberg
    • 1
  • Di Ma
    • 1
  1. 1.Department of Computer SciencePurdue UniversityW. Lafayette

Personalised recommendations