PhD CASE Studentship on ARM architectural semantics
Applications are invited for a fully funded EPSRC CASE PhD studentship at
the University of Cambridge Computer Laboratory, with industrial
sponsorship from ARM Ltd. The academic supervisor will be Prof. Peter
Sewell, and the studentship will build on work by Sarkar, Sewell, and
others on mathematically rigorous specifications of the ARM
multiprocessor architecture, as described at
http://www.cl.cam.ac.uk/~pes20/weakmemory.
You should have a strong background in Computer Science, ideally in
both logic and semantics and in computer architecture, and a keen
desire to apply rigorous techniques to the problems of real
multiprocessors. Possible PhD topics include, for example:
- development of a random test methodology for processors being
designed, linking a rigorous architectural model to an RTL simulation
environment;
- verification of multiprocessor interconnects with respect to
an architectural model; and
- development of daemonic software emulators from architectural
models.
The industrial contact is Richard Grisenthwaite, ARM Lead Architect;
the studentship would involve regular meetings with ARM staff and
perhaps
summer internship employment at ARM Cambridge.
For a home student or `eligible' EU student (who has spent at least 3
years working or studying in the UK), the award would provide
maintenance, tuition fees, and an industrial top-up (we would expect
to apply to another source to fund college fees, of ~2.5k p.a.). For
an exceptional non-eligible EU student, the same may be possible,
otherwise the maintenance component would not be funded.
Unfortunately the award does not fund non-EU international student
fees.
Possible start dates are 10 April 2014 or 1 October 2014.
Informal enquiries, including a CV and a brief description of your interests
and relevant background, should be made by email to Peter Sewell.