Relaxed Memory Model Design for Theory and Practice

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

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.