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