There are four interlinked Tasks:

Task 1: Semantic tools

The mathematical models of mainstream-system abstractions that we need have to be expressed in well-defined formal languages, for the sake of mathematical precision; and those languages need good software tool support, to let us handle large and complex definitions. In this task we address the foundational question of what formal languages are suitable for this purpose; the pragmatic question of what facilities good tool support should provide; and the engineering question of actually building these tools to a sufficient quality to be usable by other researchers and by industry staff. In REMS we are developing and using :

These are used in much of the rest of the project. We also continue to maintain the Ott tool for programming language semantic definition (supporting user-defined syntax and inductive relations over it, and compiling to LaTeX, Coq, HOL4, and Isabelle/HOL), and to study the foundations needed for future semantic tools, focussed on Nominal Type Theory.

[Task 1 papers] [Task 1 bib]

Task 2: Architectural Multiprocessor Semantics

Our first key interface is the architectural one between hardware and software, specifying the multiprocessor behaviours that processor implementations guarantee and that systems code relies on. Normal industrial practice is to specify this interface in informal-prose architecture reference manuals, but these prose descriptions cannot be used directly to test either the hardware below the interface or software above it, or to build verification tools, let alone as a basis for proof. Compounding the problem, architectures must be nondeterministic loose specifications, to accommodate microarchitectural variation, so one cannot simply characterise them with reference implementations. We are pursuing several directions here: [Task 2 papers] [Task 2 bib]

Task 3: Systems Programming Languages

The next key interface is the programming language. Systems programming is almost entirely carried out using low-level languages such as C/C++. These are efficient and relatively easy to interface with hardware, but they are difficult to use, even more difficult to use correctly, and incredibly difficult to reason about, especially in the concurrent setting. This has led, directly or indirectly, to the vast majority of bugs and vulnerabilities observed in modern operating systems. [Task 3 papers] [Task 3 bib]

Task 4: Concurrent Software Interfaces and Verification

Our final task develops reasoning methods and examines some particular higher-level software interfaces.

Task 4a: Concurrency Reasoning

Task 4b: OS APIs and Network Protocols

[Task 4 papers] [Task 4 bib]