Project Suggestions in Applied Semantics, 2009-2010
(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 same general area.
Possible supervisors for these include:
A memory model exploration tool
Multiprocessors such as x86, PowerPC, and ARM exhibit
relaxed memory models in which threads have only
approximately consistent views of shared memory, as do concurrent
high-level languages such as Java and C++.
In current research we are investigating the semantics of these models
(see here).
We have a memevents
tool, described briefly in the POPL
2009 and TPHOLs 2009 papers, that takes small test programs
and calculates the set of all executions that are allowed by some of
our memory models. This project is to re-implement a version
of memevents
to do the core of that calculation by
calling out to an external tool such as
an SMT
solver, which would be useful for further exploration of different
models. The project would suit someone with interests in semantics
and in automated reasoning.
An efficient x86-TSO emulator
We have recently proposed a precisely defined semantics for the
behaviour of x86 multiprocessors, x86-TSO (see the TPHOLs 2009 paper
and Technical Report UCAM-CL-TR-745
here) that
captures how different threads can observe each others actions.
This project is to produce a emulator for the model that lets
one test concurrent algorithms against more or less demonic versions
of the semantics. Ideally this would cope with standard x86 binaries
(preferably on Linux) and be efficient enough to use for practical
testing of subtle concurrent algorithms. The project would suit
someone with interests both in semantics and in low-level systems.
Good typechecking for HOL (Ridge, Owens, Sewell?)
Interactive tools for automated reasoning, such as the
HOL4
and
Isabelle
systems (developed by Mike Gordon and Larry Paulson, with many
others),
let one write mathematical definitions, type-check them, and support
various tactics for automated and manual proof.
The core of this project is the production of a high-quality
standalone typechecker for HOL4, that can take a collection of HOL4
source files and quickly do type inference it, with good reporting of
any type errors. The HOL4 type system is broadly similar to that of
ML, with top-level polymorphism.
Possible approaches are here:
SEMINAL: Searching for ML Type-Error Messages
Benjamin Lerner, Dan Grossman and Craig Chambers
The 2006 ACM SIGPLAN Workshop on ML (ML 2006)
Portland, Oregon, 16th September 2006
and here:
Christian Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Sci. Comput. Programming, 50:189-224, 2004.
Probably one should reuse the existing HOL4 lexing and parsing code.
If the project goes well, a possible extension would be to synthesise,
from the typechecked source, Isabelle/HOL or HOL light definitions.
This project would suit a good semantically minded programmer. It
would probably be written in OCaml or ML.
Peter.Sewell@cl.cam.ac.uk