Reasoning with Relaxed Memory Models
Lead Research Organisation:
University of Cambridge
Department Name: Computer Science and Technology
Abstract
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.
Publications
Alglave J
(2011)
Tools and Algorithms for the Construction and Analysis of Systems
Alglave J
(2012)
Fences in weak memory models (extended version)
in Formal Methods in System Design
Sarkar S
(2012)
Synchronising C/C++ and POWER
Sarkar S
(2011)
Understanding POWER multiprocessors
Sarkar S
(2011)
Understanding POWER multiprocessors
in ACM SIGPLAN Notices
Ševcík J
(2013)
CompCertTSO A Verified Compiler for Relaxed-Memory Concurrency
in Journal of the ACM
Description | Clarification of the concurrency behaviour of multiprocessors and programming languages |
First Year Of Impact | 2011 |
Sector | Digital/Communication/Information Technologies (including Software) |
Impact Types | Economic |