Reasoning with Relaxed Memory Models

Computer Science is undergoing a difficult transition. The continual performance improvements of past decades were achieved primarily by speeding up sequential computation. Constraints in device manufacture, especially the problem of power consumption, are driving a shift to ubiquitous concurrent computation, with multicore processors becoming commonplace. Programming these, however, to deliver high-performance and reliable systems, remains very challenging. There are two key difficulties, which we address here. Firstly, the concurrent algorithms that are being developed, such as non-blocking datastructures and implementations of software transactional memory, are very subtle, so informal reasoning cannot give high confidence in their correctness. Secondly, the extensive prior work on software verification for concurrency (including temporal logics, rely-guarantee reasoning, separation logic, and process calculi) neglects what is now a key phenomenon: relaxed memory models. For performance reasons, typical multiprocessors do not provide a sequentially consistent memory model. Instead, memory accesses may be reordered in various constrained ways, making it still harder to reason about executions. In this project we will establish accurate semantics for the behaviour of real-world processors, such as x86, PowerPC, and ARM architectures, covering their memory models and fragments of their instruction sets. We will experimentally validate these, building on our previous experience with realistic large-scale semantics. Above these, we will develop theoretical and practical tools for specifying and proving correctness of modern algorithms, building on our experience with separation logic, mechanized reasoning, and algorithm design. We will thereby lay the groundwork for verified compilation targeting real multicore processors, providing both high performance and high confidence for future applications.