Relaxed Memory Model Design for Theory and Practice

在过去的几年里，计算机处理器已经达到了半导体物理施加的速度限制。以前，性能的提高来自于运行单个程序的速度更快，但现在它来自于在多个“核”上同时运行更多的程序。多核处理器还支持低功耗应用，并在移动设备上变得流行起来，比如assmart手机，在这些设备中，几个慢核比单个快核消耗更少的电池电量。要为多核处理器编写软件，程序员必须将任务分解成协作程序，理想情况下每个核一个。然而，即使是专家也无法在不付出巨大努力的情况下编写这些程序，而且这些程序经常有细微的错误。程序员还没有得到管理多核计算复杂性所需的智能工具。这个项目关注的是多核处理器带来的一个关键挑战：他们的宽松内存模型。从概念上讲，处理器的核心连接到单个内存，运行在不同核心上的程序通过将数据写入内存以供其他人读取来进行通信。在现实中，处理器通过不给程序员一个全局一致的内存图像来实现良好的性能：在任何时间点，内核可能看起来在其内容上存在分歧。处理器确实对内存做了一些保证，这样程序员就可以编写工作程序，但它小心地避免了繁琐的事情。一个放松的记忆模型规定了哪些保证得到了保证，哪些没有。我们的目标是改进松弛记忆模型的理论，并将该理论应用于一个在实践中更容易理解的新模型。在大多数情况下，用高级语言编程应该比用处理器的低级汇编语言编程具有优势：例如，在可靠性、安全性和开发成本方面。然而，对于宽松的内存模型，情况并非如此：高级语言更加复杂，因为它必须考虑高级语言可以编译到的各种截然不同的处理器，也必须考虑编译器的优化。主要的紧张关系是可用性/安全性(例如，敏感数据不会被恶意程序伪造指向数据的指针所掩盖)和效率之间的紧张关系，后者推动了现有的设计。Java内存模型试图提供基本的安全保证，但已经发现了几个潜在的缺陷。在另一个极端，新的C和C++模型没有尝试提供安全保证。松弛内存模型的设计空间还没有被彻底开发，在这个项目中，我们将为高级语言设计一个松弛内存模型，为程序员提供更强有力的保证，使编写、推理和验证并发程序变得更容易。我们的设计方法结合了对真实世界并发算法的关注，以确保其实用性和数学严谨性，以确保它支持健壮的推理原则，这最终将帮助程序员理解它并编写高质量的并发软件系统。

In the past few years, computer processors have reached a speed limit imposedby semiconductor physics. Before, increased performance came from running asingle program faster, but now it comes from running more programsconcurrently, on multiple "cores". Multi-core processors also supportlow-power applications, and are becoming popular on mobile devices, such assmart phones, where several slow cores use less battery power than a singlefast core. To write software for multi-core processors, programmers mustdecompose tasks into cooperating programs, ideally one per core. However, evenexperts cannot write these programs without tremendous effort, and theprograms often have subtle bugs. Programmers have not been given theintellectual tools necessary for managing the complexity of multi-corecomputation.This project focuses on a critical challenge posed by multi-core processors:their relaxed memory models. Conceptually, the processor's cores are connectedto a single memory, and programs running on different cores communicate bywriting data to the memory for others to read. In reality, the processorachieves good performance by not giving the programmer a globally consistentpicture of the memory: at any point in time the cores can appear to disagreeon its contents. The processor does make some guarantees about the memory, sothat the programmer can write working programs, but it carefully avoids makingothers. A relaxed memory model specifies which guarantees are made and whichare not. Our objectives are to improve the theory of relaxed memory models,and to apply this theory to a new model that is easier to understand inpractice.Most of the time, programming in a high-level language should have advantagesover programming in the processor's low-level assembly language: advantagesin, for example, reliability, security, and cost of development. However, thisis not the case with relaxed memory models: the high-level language is morecomplicated because it has to account for the variety of significantlydifferent processors that the high-level language can be compiled to, and ithas to account for the compiler's optimisations too. The primary tension isbetween usability/security (for example, that sensitive data will not beleaked by a malicious program forging pointers to the data) and efficiency,with the latter driving existing designs. The Java Memory Model attempts togive basic security guarantees, but several underlying flaws have beendiscovered. On the other extreme, the new C and C++ models make no attempt toprovide security guarantees. The design space for relaxed memory models hasnot been thoroughly explored.In this project, we will design a relaxed memory model for a high levellanguage that gives stronger guarantees to programmers, making it easier towrite, reason about, and verify concurrent programs. Our approach to thedesign combines a focus on real-world concurrent algorithms, to ensure that itis practical, with mathematical rigor, to ensure that it supports robustreasoning principles that will ultimately help programmers to understand itand to write high quality concurrent software systems.