Hostname: page-component-745bb68f8f-b6zl4 Total loading time: 0 Render date: 2025-01-26T10:10:12.220Z Has data issue: false hasContentIssue false
  • English
  • Français

What is the meaning of these constant interruptions?

Published online by Cambridge University Press:  01 November 2007

GRAHAM HUTTON  and
JOEL WRIGHT
GRAHAM HUTTON
Affiliation:
School of Computer Science and IT, University of Nottingham, UK
JOEL WRIGHT
Affiliation:
School of Computer Science and IT, University of Nottingham, UK
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Asynchronous exceptions, or interrupts, are important for writing robust, modular programs, but are traditionally viewed as being difficult from a semantic perspective. In this article, we present a simple, formally justified, semantics for interrupts. Our approach is to show how a high-level semantics for interrupts can be justified with respect to a low-level implementation, by means of a compiler and its correctness theorem. In this manner we obtain two different perspectives on the problem, formally shown to be equivalent, which gives greater confidence in the correctness of our semantics.

Type
Article
Information
Journal of Functional Programming , Volume 17 , Issue 6 , November 2007 , pp. 777 - 792
Copyright
Copyright © Cambridge University Press 2007

References

Ager, M. S.Biernacki, D.Danvy, O. & Midtgaard, J. (2003) From Interpreter to Compiler and Virtual Machine: a Functional Derivation. Technical Report RS-03-14. BRICS, Aarhus, Denmark.CrossRefGoogle Scholar
Aiken, A., Wimmers, E. L. & Williams, J. H. (1990) Program Transformation in the Presence of Errors. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, pp. 210–217.Google Scholar
Allison, L. (1989) Direct semantics and exceptions define jumps and coroutines. Information Processing Letters, 31, 327–330.CrossRefGoogle Scholar
Ancona, D., Lagorio, G. & Zucca, E. (2001) A core calculus for Java exceptions. SIGPLAN Notices, 36 (11), 16–30.Google Scholar
Appel, A. (1992) Compiling With Continuations. Cambridge University Press.Google Scholar
Auwaerter, J. F. (1976) American National Standard – Programming Language PL/I. ANSI X3.53-l976. New York: American National Standards Institute.Google Scholar
Backhouse, R. (2003) Program Construction: Calculating Implementations From Specifications. New York: John Wiley.Google Scholar
Borger, E. & Schulte, W. (2000) A practical method for specification and analysis of exception handling: A Java/JVM case study. IEEE Trans. Software Eng. 26 (9), 872–887.Google Scholar
Chase, D. (1994a) Implemention of exception handling, Part I. J. C Language Trans. 5 (4), 229–240.Google Scholar
Chase, D. (1994b) Implemention of exception handling, Part II. J. C Language Trans. 6 (1), 20–32.Google Scholar
Claessen, K. & Hughes, J. (2000) QuickCheck: A lightweight tool for random testing of Haskell programs. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming. ACM Press.Google Scholar
Cleaveland, R., Luttgen, G. & Natarajan, V. (2001) Priority in process algebra. In: Handbook of Process Algebra, Bergstra, J. A.Ponse, A. & Smolka, S. A. (eds), Elsevier, pp. 711–765.CrossRefGoogle Scholar
Cristian, F. (1989) Exception handling. Anderson, T. (ed), Dependability of Resilient Computers. Blackwell Scientific Publications, pp. 68–97.Google Scholar
Drew, S., Gouph, K. J. & Ledermann, J. (1995) Implementing Zero Overhead Exception Handling. Tech. Rept. 95-12. Faculty of Information Technology, Queensland University of Technology.Google Scholar
Drew, S. J. & Gough, K. J. (1994) Exception Handling: Expecting The Unexpected. Comp. languages. 20 (2), 69–87.CrossRefGoogle Scholar
Drossopoulou, S. & Valkevych, T. (2000) Java Exceptions Throw No Surprises. Technical report. Department of Computing, Imperial College of Science, Technology and Medicine.Google Scholar
Dybvig, R. K. & Hieb, R. (1989) Engines from continuations. J. Comput. languages, 14 (2), 109–123.Google Scholar
Goodenough, J. B. (1975) Exception handling: Issues and a proposed notation. Commun. ACM, 18 (12), 683–696.Google Scholar
Gordon, A. (1995) Bisimilarity as a Theory of Functional Programming. BRICS Notes Series NS-95-3. Aarhus University.Google Scholar
Haynes, C. T. & Friedman, D. P. (1984) Engines build Process Abstractions. In: Proceedings of the 1984 ACM Symposium on Lisp and Functional Programming. ACM Press, pp. 18–24.Google Scholar
Hinze, R. & Löh, A. (2006) The lhs2TeX System for Typesetting Haskell. Available at: http://www.cs.uu.nl/~andres/lhs2tex/.Google Scholar
Hoare, C. A. R. (1985) Communicating Sequential Processes. Prentice-Hall.Google Scholar
Hutton, G. (2007) Programming in Haskell. Cambridge University Press.CrossRefGoogle Scholar
Hutton, G. & Wright, J. (2004) Compiling exceptions correctly. In: Proceedings of the 7th International Conference on Mathematics of Program Construction. Lecture Notes in Computer Science, vol. 3125. Stirling, Scotland: Springer.Google Scholar
Hutton, G. & Wright, J. (2006) Calculating an exceptional machine. Loidl, Hans-Wolfgang (ed), Trends in Functional Programming volume 5. Selected papers from the Fifth Symposium on Trends in Functional Programming, Munich, November 2004. Bristol: Intellect.CrossRefGoogle Scholar
Jacobs, B. & Poll, E. (2003) Java Program Verification at Nijmegen: Developments and Perspective. Technical Report NIII-R0318. Nijmegen Institute for Computing and Information Sciences.CrossRefGoogle Scholar
Jacobs, B. (2001) A formalisation of Java's exception mechanism. In: ESOP 2001: Proceedings of the 10th European Symposium on Programming Languages and Systems. Springer-Verlag, pp. 284–301.Google Scholar
Klein, G. & Nipkow, T. (2006) A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Program. Languages Syst. 28 (4): 619–695.Google Scholar
Laird, J. (2001) A fully abstract game semantics of local exceptions. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society.Google Scholar
Laird, J. (2002) Exceptions, Continuations and Macro-expressiveness. In: Proceedings of the 11th European Symposium on Programming Languages and Systems. Springer Verlag.Google Scholar
Leino, K., Rustan, M. & Snepscheut, van de, Jan, L. A. (1994) Semantics of exceptions. In: Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi. North-Holland, pp. 447–466.Google Scholar
Lillibridge, M. (1999) Unchecked exceptions can be strictly more powerful than Call/CC. Higher-Order Symbolic Comput. 12 (1), 75–104.Google Scholar
Marlow, S., PeytonJones, S. Jones, S.Moran, A. & Reppy, J. (2001) Asynchronous exceptions in Haskell. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press.Google Scholar
McBride, C., McKinna, J. & Altenkirch, T. (2006) The epigram system. Available at: http://www.e-pig.org/.Google Scholar
McKinna, J. & Wright, J. (2006, July) Towards type-correct, provably correct, compilers: A case study in epigram. J. Funct. Program.Google Scholar
Milner, R. (1989) Communication and Concurrency. Prentice Hall.Google Scholar
Milner, R. (1999) Communicating and Mobile Systems: The π-Calculus. Cambridge University Press.Google Scholar
Milner, R., Tofte, M., Harper, R. & MacQueen, D. (1997) The Definition of Standard ML (Revised). MIT Press.Google Scholar
Moran, A., Lassen, S. B. & Jones, S. L. P. (1999) Imprecise exceptions, co-inductively. Electron. Notes Theor. Comp. Sci. 26.Google Scholar
Nipkow, T. (2004) Compiling exceptions correctly. Archive of Formal Proofs. Available at: http://afp.sourceforge.net/.Google Scholar
Palsberg, J. & Ma, D. (2002) A typed interrupt calculus. In: Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer-Verlag, pp. 291–310.Google Scholar
Pessaux, F. & Leroy, X. (2000) Type-based analysis of uncaught exceptions. ACM Trans. Program. Languages Syst. 22 (2), 340–377.Google Scholar
PeytonJones, S. Jones, S. (2001) Tackling the awkward squad: Monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In: Engineering Theories of Software Construction Hoare, T.Broy, M. & Steinbruggen, R. (eds), IOS Press. Presented at the 2000 Marktoberdorf Summer School.Google Scholar
PeytonJones, S. Jones, S.Reid, A.Hoare, T.Marlow, S. & Henderson, F. (1999) A semantics for imprecise exceptions. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press.Google Scholar
Ramsey, N. & Jones, S. P. (2000) A Single Intermediate Language That Supports Multiple Implementations Of Exceptions. In: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation. ACM Press, pp. 285–298.CrossRefGoogle Scholar
Reynolds, J. C. (1972) Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM Annual Conference. ACM Press, pp. 717–740.Google Scholar
Riecke, J. G. & Thielecke, H. (1999) Typed exceptions and continuations cannot macro-express each other. In: Proceedings of the 26th International Colloquium on Automata, Languages and Programming. Springer Verlag.Google Scholar
Sebesta, R. W. (2006) Concepts of Programming Languages, 7th ed. Pearson Addison Wesley.Google Scholar
Spivey, M. (1990) A functional theory of exceptions. Sci. Comput. Program. 14 (1), 25–43.Google Scholar
Thielecke, H. (2000) On exceptions versus continuations in the presence of state. In: Proceedings of the 9th European Symposium on Programming Languages and Systems. Springer Verlag.Google Scholar
Troelstra, A. S. & van Dalen, D. (1988) Constructivism in Mathematics: An Introduction. Vol. 1. Elsevier.Google Scholar
Wand, M. (1995) Compiler correctness for parallel languages. In: Proceedings of the 7th International Conference on Functional Programming and Computer Architecture. ACM Press.Google Scholar
Wright, A. K. & Felleisen, M. (1994) A syntactic approach to type soundness. Inform. Comput. 115 (1), 38–94.Google Scholar
Yi, K. & Ryu, S. (2002) A cost-effective estimation of uncaught exceptions in standard ML programs. Theor. Comput. Sci. 277 (1–2), 185–217.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.