Part II and MPhil Project Suggestions, 2010-2011
(these will be updated from time to time)
The projects below are outline suggestions - feel free to come and
discuss how they could be turned into full proposals, or to suggest others in
the general area of applied semantics, especially
the relaxed-memory concurrency that
real-world multiprocessors exhibit, in verified compilation, or in
programming language semantics.
Possible supervisors for these include:
What is C, again?
C is part of the foundation of most computer systems, and much effort
has been devoted to its standardisation over the years, e.g. with
ANSI C from 1989 and C99. Currently a new revision is underway,
informally known
as C1X, and
the WG14 group
group has produced a working draft
(N1494).
But all these are prose documents, without any mathematical semantics,
so the basic question, of whether a language implementation meets
the standard, is not even precisely defined, let alone testable or
provable.
The goal of this project is to give an operational semantics for a
modest fragment of C, aiming to capture the intent
of the standard. The semantics should be usable as a test oracle:
given a small source program, it should be possible to calculate the
set of all permitted executions. The choice of the fragment to be
covered would be an important early choice: dealing with all of C is
almost certainly impractical, so one would expect to cover only a
small fragment, but we would probably hope to include at
least some of the concurrency aspects. It might be appropriate to
express the semantics directly in a functional programming language
(e.g. OCaml) or perhaps in a proof assistant or using the Ott tool.
Background:
- Michael Norrish gave a semantics for a significant fragment of C in
HOL, in his 1998 Computer Laboratory PhD C
formalised in HOL.
- There is ongoing work here on the C++ concurrency semantics, which is
expected to be adopted (or adapted) for C1X:
Mathematizing C++
Concurrency by Mark Batty, Scott Owens, Susmit Sarkar, Peter
Sewell, and Tjark Weber. This has identified several issues with
the current C++0x draft, and proposed solutions which seem likely to
be adopted.
- Xavier
Leroy's CompCert is a
verified compiler from a C-like language, Clight.
- There is ongoing work here on verified compilation from an
extension of Clight with threads and shared memory: CompCertTSO
by Suresh Jagannathan (Purdue), Peter Sewell (Cambridge), Jaroslav
Sevcik (Cambridge), Viktor Vafeiadis (Cambridge), and Francesco Zappa
Nardelli (INRIA).
This is a challenging project which would suit someone with an
interest in semantics as it can be applied to real systems. It could
well lead in to a PhD in a related area.
Peter.Sewell@cl.cam.ac.uk