Rob Dockins will present his preFPO on Tuesday November 29 at 10AM in Room 402. The members of his committee are: Andrew Appel, advisor; David Walker and Xavier Leroy (INRIA), readers; David August and Mark Braverman, nonreaders. Everyone is invited to attend his talk. His abstract follows below. ---------------------- Title ========== Behavioral Refinement Abstract ======================== What does it mean for a compiler to be correct? This question is of central importance for anyone attempting to prove a compiler correct, or for users of a compiler to understand what they should expect the compiler to do. Surprisingly, no real consensus has emerged as to the best answer to this question. As a result, it can be rather difficult to understand what a particular compiler correctness proof actually proves, and it is especially difficult to understand the relationship between various different compiler verification efforts. In this thesis, I will propose a specific approach to the question of compiler correctness which is simple and easy to understand, but is also capable of expressing the correctness statement for the majority of compiler correctness projects that currently exist. In other words, I will develop a single parametrized theory of correctness which can be instantiated multiple ways to achieve a theory specific to a particular language and compiler. To accomplish this, I borrow the idea of bisimulations from the concurrency calculus community and adjust it somewhat to fulfill our needs. The main strength of bisimulations is that they easily handle nondeterministic computation. Although popular programming languages rarely feature explicitly nondeterministic features, nondeterminism is nonetheless frequently introduced through interaction with the environment and/or via concurrency primitives. Thus, it is important to smoothly handle nondeterminism in our theory of program semantics. However, the bisimulations developed for concurrency calculi lack a feature we will find very important in our compiler correctness setting: they cannot reason about programs which may go wrong, or exhibit undefined behavior. In situations where undefined behavior occurs, the compiler writer wishes to have freedom to replace the undefined behavior with arbitrary behavior. Bisimulations to not allow us to express this sort of transformation. Thus, we develop a notion of program refinement, which weakens the notion of bisimulation just enough to allow the proper handling of undefined behavior. This notion of refinement provides exactly what we need to answer our motivating question: "A correct compiler is one which outputs a program which is a refinement of the input program." I defend the notion of refinement by relating to an axiomatic semantics based on a variant of Hennessy-Milner logic. The formulae of Hennessy-Milner logic allow one to express specifications of the observable behavior of a program. We show that refinement is precisely the same as preserving all observable specifications in the logic. I will also develop a theory of safe programs. Safe programs are those which will never exhibit undefined behavior. We show that for the safe programs, our notion of refinement collapses back into the more traditional notion of bisimulation. In addition, we demonstrate an interesting and unexpected result: program safety is intimately related to the axiom of the excluded middle (EM) in the logic of observable specifications. Safe programs enjoy EM, whereas unsafe programs do not. In this thesis, I will examine three different variations of bisimulation of increasing complexity (strong, branching and environmental), and show how they can all be relaxed into refinements. For each, we will give a logical characterization which will precisely capture the properties preserved by refinement, and for each we will develop the theory of safe programs. I intend to show that environmental refinement provides an excellent theory for reasoning about realistic languages and execution contexts. In particular, I shall argue that it provides just the right abstraction for discussing the correctness of the verified C compiler CompCert.