EPSRC logo

Details of Grant 

EPSRC Reference: EP/M027317/1
Title: C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence
Principal Investigator: Nagarajan, Dr V
Other Investigators:
Topham, Professor N Jackson, Dr PB Sarkar, Dr S
Researcher Co-Investigators:
Project Partners:
Intel Corporation Ltd
Department: Sch of Informatics
Organisation: University of Edinburgh
Scheme: Standard Research
Starts: 09 November 2015 Ends: 30 April 2019 Value (£): 668,897
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
05 Mar 2015 EPSRC ICT Prioritisation Panel - Mar 2015 Announced
Summary on Grant Application Form
Shared-memory multi-core processors are ubiquitous, but programming them

remains challenging. The programming model exposed by such multi-core

processors depends crucially on a "memory consistency model" (MCM), a contract

between the hardware and the programmer, which essentially specifies what

value a read can return. On the hardware side, one key mechanism to implement

the memory consistency model is the "cache-coherence protocol" (CCP), which

essentially communicates memory operations between processors. However, the

connection between the CCP and the MCM remains unclear. This is especially

true for modern CCPs and MCMs, in which CCP design has been divorced from the

requirements of the MCM. We argue that this has negatively impacted the

scalability and the verifiability of CCPs.

On the scalability front, there are serious question marks about sustaining

cache coherence as the number of cores continue to scale. On the verification

front, the application of existing verification techniques, which do not

verify the CCP against the MCM, are arguably broken.

In the C3 proposal, we propose a family of CCPs that are "aware" of, and

verified against the MCM. Our approach is motivated by the fact that both

hardware and programming languages are converging to various relaxed MCMs for

performance oriented reasons. We use such relaxed MCMs as inspiration to

research CCPs that can take advantage of them. Specifically, we will research

"lazy" CCPs where memory operations are batched, and the cost of communicating

a memory operation can be amortised. We will also, for the first time,

formally verify the relationship between the hardware CCPs and the

programmer-oriented MCM they provide. We will investigate rigorously the

gains to be had from such lazy CCPs. We will do this by creating a multi-core

silicon prototype of our proposed CCP, leveraging our experience in the design

of industrial-strength micro-architectures and their implementations.

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.ed.ac.uk