What is the meaning of these constant interruptions?

cJFP 17 (6): 777–792, 2007. 2007 Cambridge University Press 777doi:10.1017/S0956796807006363 First published online 25 April 2007 Printed in the United KingdomWhat is the meaning of these constantinterruptions?GRAHAM HUTTON and JOEL WRIGHTSchool of Computer Science and IT, University of Nottingham, UKAbstractAsynchronous exceptions, or interrupts, are important for writing robust, modular programs,but are traditionally viewed as being difficult from a semantic perspective. In this article, wepresent a simple, formally justified, semantics for interrupts. Our approach is to show how ahigh-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 differentperspectives on the problem, formally shown to be equivalent, which gives greater confidencein the correctness of our semantics.1 IntroductionExceptions are an important feature of modern programming languages, supportingthe development of modular programs that are robust to various kinds of unexpectedevents. There are two basic kinds of exceptions: those that arise from within a pro-gram itself, such as a division by 0, and those that arise from its external environment,such as a timeout. The former are termed synchronous exceptions, because they canarise only at specific points, while the latter are termed asynchronous exceptions,because they can potentially arise at any point. For simplicity ...