EPSRC logo

Details of Grant 

EPSRC Reference: EP/F036345/1
Title: Reasoning with Relaxed Memory Models
Principal Investigator: Sewell, Professor PM
Other Investigators:
Fraser, Dr KA Parkinson, Dr M
Researcher Co-Investigators:
Project Partners:
INRIA Paris - Rocquencourt
Department: Computer Science and Technology
Organisation: University of Cambridge
Scheme: Standard Research
Starts: 01 December 2008 Ends: 30 November 2012 Value (£): 813,748
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
24 Jan 2008 ICT Prioritisation Panel (Technology) Announced
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.cam.ac.uk