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

共享内存多核处理器无处不在，但编程它们仍然具有挑战性。这种多核处理器暴露的编程模型主要依赖于“内存一致性模型”（MCM），这是硬件和程序员之间的一种契约，本质上规定了读取可以返回的值。在硬件方面，实现内存一致性模型的一个关键机制是“缓存一致性协议”（CCP），它本质上是处理器之间的内存操作通信。然而，中国共产党和MCM之间的联系仍然不清楚。对于现代CCP和MCM来说尤其如此，CCP的设计已经脱离了MCM的要求。我们认为这对ccp的可扩展性和可验证性产生了负面影响。在可扩展性方面，随着核心数量的不断增加，保持缓存一致性存在严重的问题。在验证方面，现有的验证技术的应用，不针对MCM验证CCP，可以说是失败的。在C3提案中，我们提出了一系列“意识到”并根据MCM进行验证的ccp。我们的方法源于这样一个事实，即硬件和编程语言都出于性能导向的原因而向各种宽松的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.