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

共享内存多核处理器无处不在，但对其进行编程仍然具有挑战性。这种多核处理器的编程模型主要依赖于“内存一致性模型”（MCM），这是硬件和程序员之间的一种契约，它基本上指定了读取可以返回什么值。在硬件方面，实现内存一致性模型的一个关键机制是“缓存一致性协议”（CCP），它本质上是处理器之间的内存操作通信。然而，CCP和MCM之间的联系仍然不清楚。尤其是对于现代CCP和MCM，CCP设计已经脱离MCM的要求。我们认为，这对CCP的可扩展性和可验证性产生了负面影响。在可扩展性方面，随着内核数量的不断增加，保持缓存一致性存在严重的问题。在验证方面，现有的验证技术的应用，不验证CCP对MCM，可以说是打破。在C3提案中，我们提出了一系列CCP，这些CCP“知道”MCM并根据MCM进行验证。我们的方法是出于这样一个事实，即硬件和编程语言都收敛到各种宽松的MCM性能为导向的原因。我们使用这种放松的MCM作为灵感来研究可以利用它们的CCP。具体来说，我们将研究“懒惰”CCP，其中内存操作是分批的，并且可以摊销内存操作的通信成本。我们还将首次正式验证硬件CCP和它们提供的面向程序员的MCM之间的关系。我们将严格调查从这些懒惰的CCP身上获得的收益。我们将通过创建我们提出的CCP的多核原型来实现这一点，利用我们在工业强度微架构及其实现的设计方面的经验。

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.