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

点击翻译按钮获取中文摘要

Shared-memory multi-core processors are ubiquitous, but programming themremains challenging. The programming model exposed by such multi-coreprocessors depends crucially on a "memory consistency model" (MCM), a contractbetween the hardware and the programmer, which essentially specifies whatvalue a read can return. On the hardware side, one key mechanism to implementthe memory consistency model is the "cache-coherence protocol" (CCP), whichessentially communicates memory operations between processors. However, theconnection between the CCP and the MCM remains unclear. This is especiallytrue for modern CCPs and MCMs, in which CCP design has been divorced from therequirements of the MCM. We argue that this has negatively impacted thescalability and the verifiability of CCPs. On the scalability front, there are serious question marks about sustainingcache coherence as the number of cores continue to scale. On the verificationfront, the application of existing verification techniques, which do notverify the CCP against the MCM, are arguably broken. In the C3 proposal, we propose a family of CCPs that are "aware" of, andverified against the MCM. Our approach is motivated by the fact that bothhardware and programming languages are converging to various relaxed MCMs forperformance oriented reasons. We use such relaxed MCMs as inspiration toresearch CCPs that can take advantage of them. Specifically, we will research"lazy" CCPs where memory operations are batched, and the cost of communicatinga memory operation can be amortised. We will also, for the first time,formally verify the relationship between the hardware CCPs and theprogrammer-oriented MCM they provide. We will investigate rigorously thegains to be had from such lazy CCPs. We will do this by creating a multi-coresilicon prototype of our proposed CCP, leveraging our experience in the designof industrial-strength micro-architectures and their implementations.