These might suit good students interested in compilation (for the first), or in concurrency systems semantics and either SMT-based test generation (for the second) or mechanised proof (for the third). They are probably best suited for an MPhil/Part III project rather than a Part II project, though it might be possible to craft a Part II project in a similar vein on a smaller scale.
Supervisors: Alasdair Armstrong + Peter Sewell
Sail is a language developed in Cambridge for describing instruction set architecture (ISA) specifications, with the Arm-A and Morello ISA specs auto-translated from Arm's internal language to Sail, and the official RISC-V and research CHERI-RISC-V ISA specs hand-written in Sail. It allows descriptions of instructions using arbitrary-width bitvectors and mathematical integers, with a lightweight dependent type system. From Sail one can generate C emulators for validation and software testing, and theorem-prover definitions for proof. However, arbitrary-width bitvectors and mathematical integers, while convenient for specification and formal reasoning, cause issues for efficient emulation - which is important when running large suites of compliance tests on the architecture model.
This project would involve integrating Sail into an existing (or custom) JIT framework to optimise the runtime performance. There are many options available in this space, e.g. libgccjit, LLVM, GraalVM, etc., so there is a lot of flexibility in this project depending on interest. There is is also space for similar but related projects, e.g. on profile-guided optimisation or additional up-front optimisations. A student for this project would ideally have a strong interest in compilers, and some OCaml programming experience.
Links: https://github.com/rems-project/sail
Supervisors: Thibaut Pérami + Ben Simner + Peter Sewell
The Arm-A architecture (like most others) has a "relaxed memory model", a concurrency semantics that allows hardware optimisations such as out-of-order execution to be observable in a program's concurrency behaviour - as described in the "Multicore Semantics and Programming" course.
Those semantics have been formalized by various models, some of which are executable - i.e., for which there is a software tool that takes as input a test case and possible hardware behavior and decides whether it is allowed or not by the architecture. This is essential when developing new formal models of the architecture or extending previous versions, both for comparing models against experimentally observed hardware behaviour (to validate the model and/or to discover hardware bugs) and for comparing one model against another. Such comparisons also rely critically on having a good suite of interesting tests, hand-written and/or automatically generated. Several tools for generating interesting tests have been developed, including diy (https://diy.inria.fr/) and memalloy (https://johnwickerson.github.io/memalloy/), and related work uses SMT solvers to compare models, MemSynth (https://homes.cs.washington.edu/~emina/doc/memsynth.pldi17.pdf).
Recent and ongoing research is extending the scope of relaxed-memory semantics to cover systems features, including virtual memory, instruction fetch, and exceptions:
We have a substantial corpus of hand-written tests, symbolic evaluation tooling to compute whether a test is allowed in an arbitrary model (isla, https://www.cl.cam.ac.uk/~pes20/isla/isla-cav2021-extended.pdf), and some tooling for executing tests experimentally on hardware. We now think that it would be best to explore clean-slate automatic test generation to cover these new features. The particular aim of this project is to implement a tool similar to diy that focuses on tests and models for the virtual memory architecture of Arm processors. There is scope for creating use of SMT solvers to produce interesting tests, e.g. tests that discriminate between specific candidate models.
The student should:
Supervisors: Christopher Pulte + Thibaut Pérami + Ben Simner + Peter Sewell
The Arm-A architecture (like most others) has a "relaxed memory model", a concurrency semantics that allows hardware optimisations such as out-of-order execution to be observable in a program's concurrency behaviour - as described in the "Multicore Semantics and Programming" course.
To precisely define and document the semantics for hardware and software implementors and to support testing and verification, different formalisations have been developed for Armv8-A: (1) an operational semantics, expressing the concurrency behaviour using mechanisms resembling micro-architecture, and (2) an axiomatic model, capturing the concurrency behaviour abstractly using relations on memory events and axioms over them.
A detailed paper proof shows these two models to be equivalent (http://www.cl.cam.ac.uk/~pes20/armv8-mca/armv8-mca-draft.pdf, https://www.repository.cam.ac.uk/handle/1810/292229), but so far there is no mechanised proof of this - so the paper proof might contain errors, and in any case is hard to maintain as the models evolve. The goal of this project is a mechanised equivalence proof between versions of the axiomatic and operational models, cut down or simplified enough to make this viable within the project scope. This would involve formalising model definitions and mechanising the existing paper proof in a proof assistant such as Coq or Isabelle. Some initial infrastructure for these definitions will be available in Coq.
Students interested in this project should have some experience in working with a mechanised proof assistant.