|
The essence of compiling exceptions.
Graham Hutton and Joel Wright. To be submitted for publication, 2003.
Given the importance of exceptions, it is perhaps surprising that in textbooks and research articles on compilation, exceptions are often not considered at all, or one finds rather
brief mention of concepts such as "marking the stack" and
"unwinding the stack". In this article we make such ideas
precise, by presenting a compiler for a small language with
exceptions, together with a proof of its correctness with respect to a formal semantics for the language. To the best
of our knowledge, this is the first time that a compiler for
exceptions has been proved to be correct, but we
would welcome any pointers to other work in this area.
A nice, and rather short, paper.
The first two sections (sections 2 and 3), which show a basic compiler for arithmetic expressions and prove its correctness, are well worth reading for their elegance, even if you are not interested in the discussion of compiling exceptions.
It should be noted that the exception mechanism discussed is less expressive than what you would find in languages such as Ada or C++, and the implementation discussed is a bit naive.
EOPL2 devotes section 7.4 to exceptions, but these are implemented using continutations, in the context of a CPS interpreter, so efficient compilation of exceptions isn't covered.
The paper uses Haskell as an executable notation. Interestingly, the authors mention they used QuickCheck while developing the code in the paper and before proving it is correct.
Posted to implementation by Ehud Lamm on 2/18/03; 1:09:18 PM
|
The essence of compiling exceptions
