Architecture specifications notionally define the fundamental interface between hardware
and software: the envelope of allowed behaviour for processor implementations, and the …

Despite many years of research, it has proven very difficult to develop a memory model for
concurrent programming languages that adequately balances the conflicting desiderata of …

Modern computer systems consist of a multitude of abstraction layers (eg, OS kernels,
hypervisors, device drivers, network protocols), each of which defines an interface that hides …

Timing side-channels are arguably one of the main sources of vulnerabilities in
cryptographic implementations. One effective mitigation against timing side-channels is to …

In this paper we develop semantics for key aspects of the ARMv8 multiprocessor
architecture: the concurrency model and much of the 64-bit application-level instruction set …

We introduce a strengthening of the release-acquire fragment of the C11 memory model that
(i) forbids dubious behaviors that are not observed in any implementation;(ii) supports fence …

The interfaces between layers of a system are susceptible to bugs if developers of adjacent
layers proceed under subtly different assumptions. Formal verification of two layers against …

C remains central to our computing infrastructure. It is notionally defined by ISO standards,
but in reality the properties of C assumed by systems code and those implemented by …

We show that the weak memory model introduced by the 2011 C and C++ standards does
not permit many common source-to-source program transformations (such as expression …

The CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for
a functional programming language to date. The architecture of the compiler, a sequence of …