| EPSRC Reference: |
EP/M027317/1 |
| Title: |
C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence |
| Principal Investigator: |
Nagarajan, Dr V |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| 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: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
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
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| 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 |