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

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.

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.