These pages describe the original REMS project, principally supported by the eponymous EPSRC Programme Grant from 2013-2019. We also use "REMS" informally as a research group name, and the continuation of much of the original REMS project work is described under the topics of my home page.

The mainstream computing infrastructure on which we all rely works well enough to support much of modern society, but it is neither robust nor secure — as demonstrated over the years by untold numbers of system failures and successful malicious attacks. Fundamentally, this is because the engineering methods by which computer systems are built are not up to the task. Normal practice is based on a test-and-debug engineering process, with triumvirates of code, manually curated tests, and prose specification documents; it relies also on the division of labour that is enabled by common interfaces, allowing systems to be composed of subsystems built by different groups. But prose specification documents do not provide an oracle that one can test a system against, leaving code, tests, and specifications only weakly related; they are inherently ambigous, lacking mathematical precision; and the existing specifications of many key interfaces leave much to be desired. Moreover, some of the legacy interfaces that we still rely on, such as the C programming language, were simply not designed to protect against the accidental errors and malicious attacks that are now so common.

REMS (Rigorous Engineering for Mainstream Systems), is an EPSRC-funded Programme Grant (2013-2020, £5.6M, Cambridge, Imperial, and Edinburgh) to explore how we can use rigorous mathematics to improve engineering practice for mainstream computer systems, to make them more robust and secure: broadly, to “create the intellectual and software tools to apply semantics and verification at the heart of mainstream system engineering”. Addressing this problem needs close interaction between the normally disjoint cultures of systems and semantics research, and REMS brings together an unusual combination of researchers in both to achieve this: in architecture, operating systems, security, and networks, and in programming languages, automated reasoning, and verification. Building on many years of research worldwide on mathematical semantics and verification, we are finally in a position to scale up, to apply mathematically rigorous semantics to mainstream systems:

The project is focussed on lightweight rigorous methods: precise specification (post hoc and during design) and testing against specifications, with full verification only in some cases. It thus provides a relatively smooth adoption path from conventional engineering, and the project emphasises building useful (and reusable) semantics and tools. We are building accurate full-scale mathematical models of some of the key computational abstractions (processor architectures, programming languages, concurrent OS interfaces, and network protocols), studying how this can be done, and investigating how such models can be used for new verification research and in new systems and programming language research. Supporting all this, we are also working on new specification tools and their foundations.

REMS is organised into five interlinked tasks, shown on the front page. Three tasks are focussed on the three key abstractions: Task 2 on multicore processor architectures, Task 3 on programming languages, and Task 4a on concurrent systems software interfaces. In each of these, some subtasks build models and specifications of key parts of today’s mainstream interfaces or of major research proposals, while other subtasks go on to apply, extend, and relate those models. For all three, good semantic tools, built in Task 1, are needed to work with the large mathematical definitions of our models. Task 4b addresses higher-level abstractions and the theory of how we can reason about these concurrent systems (Task 4 of the original proposal has been split into Task 4a and Task 4b for clarity).

Much of this needs collaboration not just between systems and semantics researchers within the project, but also with academic partners elsewhere and with industry vendors and groups. We have substantial interactions with Arm, IBM, the ISO C and C++ standards committees (WG14 and WG21), the RISC-V Foundation Memory Model and ISA Formal Task Groups, the IETF, the ECMAScript committee, and the WebAssembly Committee. We have also engaged with Amazon, POSIX, the FreeBSD development community, the Linux concurrency development community, Qualcomm, Apple, and Nvidia. Also very important are close working links with other major academic projects, especially:

Academic collaborators include colleagues at St Andrews, Kent, Leicester, INRIA Paris, Chalmers, NICTA Australia, and the DeepSpec NSF Expedition in Computing in the USA.