C3: Scalable & Verified Shared Memory via Consistency-directed Cache Coherence

Lead Research Organisation: University of Edinburgh
Department Name: Sch of Informatics

Abstract

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.

Planned Impact

This project will potentially have major impact, primarily on processor
architecture companies, and thereby on UK economy and indeed society.

The potential industrial impact is massive. UK and international companies
such as Intel, ARM, Synopsys and IBM are all directly engaged in scaling up
heterogeneous many-core shared memory systems. Our project is potentially a
key enabler in this direction, and this is reflected in the various supporting
letters from our industrial partners. We have several key industrial contacts,
and a track record of transferring technologies from academia to the
commercial sphere. Also note that verification is a key concern in all
semiconductor companies, and cache coherence is recognised to be a
particularly hard target. Our techniques, if successful, will open a new and
potentially far cheaper avenue of verification of the hard problems in this
area.

Processor companies such as the above are by themselves a significant sector
of the UK economy. However, since our techniques take full account of the
needs of the programmer, and in fact are designed to bolster such
important-to-programmer models as C11/C++11 and OpenCL, the potential
beneficiaries extend to compiler companies, and indeed concurrent and system
software companies. These mechanisms can potentially transmit the gains we
obtain, in verifiability, in performance, and in reliability, to all of
society.
 
Description The cache coherence protocol is a mechanism to ensure that values updated in one processor core are visible to others. The consistency model is the specification (exposed to programmers) that defines how a memory system should behave. We have discovered that, if the coherence protocol is made aware and designed against the specifications of the memory consistency model, then the protocol can be made to scale to larger number of processors. We have demonstrated this by developing a scalable coherence protocol that is designed targeting the x86TSO memory consistency model (supported by today's Intel, AMD and Sparc processors). We have also developed a novel technique to verify the coherence protocol against the memory consistency model.
Exploitation Route The protocols and verification techniques developed as part of the project makes multicore processors more scalable and reliable. Processor manufacturers can use the protocols developed to develop more scalable multicore processors. The verification techniques developed can be used to ensure that the coherence protocols to not suffer from costly bugs.
Sectors Digital/Communication/Information Technologies (including Software),Electronics

 
Description ARM Studentship
Amount £63,584 (GBP)
Organisation ARM Holdings 
Sector Private
Country United Kingdom of Great Britain & Northern Ireland (UK)
Start 09/2016 
End 08/2020
 
Description ARM Research Summit (2016) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Dr. Vijay Nagarajan was an invited speaker at the ARM Research Summit which attracted in excess of 100 delegates. The talk sparked questions and discussions and led to an ARM studentship in a related area.
Year(s) Of Engagement Activity 2016
URL https://developer.arm.com/research/summit/previous-summits/2016
 
Description HP visit (Palo Alto) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact About 15 HP Labs employees attended the research talk. The talk lead to the start of a collaboration.
Year(s) Of Engagement Activity 2016
 
Description HPCA 2017(Austin) 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact We presented two papers at HPCA 2017 (co-located with CGO and PPoPP), a top-tier conference in computer architecture attend by around 500 people.
Year(s) Of Engagement Activity 2017
URL https://hpca2017.org/
 
Description Micro 2016 conference (Taiwan) 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Cheng-Chieh Huang presented our paper at this top-tier architecture conference, attended by around 250 delegates. This led to eventually Cheng-Chieh landing a job at Mentor Graphics.
Year(s) Of Engagement Activity 2016
URL https://www.microarch.org/micro49/
 
Description School Visit (Princeton) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Dr. Vijay Nagarajan delivered an invited presentation at Princeton university. About 20 academic staff and post-graduate students attended this talk, the talk sparked questions and discussions which lead to the exchange of papers and ideas between the research groups involved.
Year(s) Of Engagement Activity 2016
 
Description School visit (Michigan) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact 20 post-graduate students and faculty attended for a research visit to University of Michigan which sparked questions and discussion afterwards.
Year(s) Of Engagement Activity 2016
 
Description School visit (Rutgers) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact 25 students and faculty attended the research visit to University of Rutgers, which sparked questions and discussions afterwards.
Year(s) Of Engagement Activity 2016
 
Description School visit (U Penn) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Dr. Vijay Nagarajan delivered an invited lectuer at U Penn. This talk sparked questions and discussion with academic staff and post-graduate students afterwards.
Year(s) Of Engagement Activity 2016