EPSRC logo

Details of Grant 

EPSRC Reference: EP/K040561/1
Title: Relaxed Memory Model Design for Theory and Practice
Principal Investigator: Owens, Dr SA
Other Investigators:
Researcher Co-Investigators:
Project Partners:
INRIA Paris - Rocquencourt University of Cambridge
Department: Sch of Computing
Organisation: University of Kent
Scheme: First Grant - Revised 2009
Starts: 07 January 2014 Ends: 06 January 2016 Value (£): 98,538
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
11 Apr 2013 EPSRC ICT Responsive Mode - Apr 2013 Deferred
05 Jun 2013 EPSRC ICT Responsive Mode - Jun 2013 Announced
Summary on Grant Application Form
In the past few years, computer processors have reached a speed limit imposed

by semiconductor physics. Before, increased performance came from running a

single program faster, but now it comes from running more programs

concurrently, on multiple "cores". Multi-core processors also support

low-power applications, and are becoming popular on mobile devices, such as

smart phones, where several slow cores use less battery power than a single

fast core. To write software for multi-core processors, programmers must

decompose tasks into cooperating programs, ideally one per core. However, even

experts cannot write these programs without tremendous effort, and the

programs often have subtle bugs. Programmers have not been given the

intellectual tools necessary for managing the complexity of multi-core


This project focuses on a critical challenge posed by multi-core processors:

their relaxed memory models. Conceptually, the processor's cores are connected

to a single memory, and programs running on different cores communicate by

writing data to the memory for others to read. In reality, the processor

achieves good performance by not giving the programmer a globally consistent

picture of the memory: at any point in time the cores can appear to disagree

on its contents. The processor does make some guarantees about the memory, so

that the programmer can write working programs, but it carefully avoids making

others. A relaxed memory model specifies which guarantees are made and which

are not. Our objectives are to improve the theory of relaxed memory models,

and to apply this theory to a new model that is easier to understand in


Most of the time, programming in a high-level language should have advantages

over programming in the processor's low-level assembly language: advantages

in, for example, reliability, security, and cost of development. However, this

is not the case with relaxed memory models: the high-level language is more

complicated because it has to account for the variety of significantly

different processors that the high-level language can be compiled to, and it

has to account for the compiler's optimisations too. The primary tension is

between usability/security (for example, that sensitive data will not be

leaked by a malicious program forging pointers to the data) and efficiency,

with the latter driving existing designs. The Java Memory Model attempts to

give basic security guarantees, but several underlying flaws have been

discovered. On the other extreme, the new C and C++ models make no attempt to

provide security guarantees. The design space for relaxed memory models has

not been thoroughly explored.

In this project, we will design a relaxed memory model for a high level

language that gives stronger guarantees to programmers, making it easier to

write, reason about, and verify concurrent programs. Our approach to the

design combines a focus on real-world concurrent algorithms, to ensure that it

is practical, with mathematical rigor, to ensure that it supports robust

reasoning principles that will ultimately help programmers to understand it

and to write high quality concurrent software systems.
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.kent.ac.uk