[talks] R Dockins preFPO

[Melissa M. Lawson]

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.