Relaxed Memory Model Design for Theory and Practice

In the past few years, computer processors have reached a speed limit imposed
by semiconductor physics. Before, increased performance came from running a
single program faster, but now it comes from running more programs
concurrently, on multiple "cores". Multi-core processors also support
low-power applications, and are becoming popular on mobile devices, such as
smart phones, where several slow cores use less battery power than a single
fast core. To write software for multi-core processors, programmers must
decompose tasks into cooperating programs, ideally one per core. However, even
experts cannot write these programs without tremendous effort, and the
programs often have subtle bugs. Programmers have not been given the
intellectual tools necessary for managing the complexity of multi-core
computation.

This project focuses on a critical challenge posed by multi-core processors:
their relaxed memory models. Conceptually, the processor's cores are connected
to a single memory, and programs running on different cores communicate by
writing data to the memory for others to read. In reality, the processor
achieves good performance by not giving the programmer a globally consistent
picture of the memory: at any point in time the cores can appear to disagree
on its contents. The processor does make some guarantees about the memory, so
that the programmer can write working programs, but it carefully avoids making
others. A relaxed memory model specifies which guarantees are made and which
are 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 in
practice.

Most of the time, programming in a high-level language should have advantages
over programming in the processor's low-level assembly language: advantages
in, for example, reliability, security, and cost of development. However, this
is not the case with relaxed memory models: the high-level language is more
complicated because it has to account for the variety of significantly
different processors that the high-level language can be compiled to, and it
has to account for the compiler's optimisations too. The primary tension is
between usability/security (for example, that sensitive data will not be
leaked by a malicious program forging pointers to the data) and efficiency,
with the latter driving existing designs. The Java Memory Model attempts to
give basic security guarantees, but several underlying flaws have been
discovered. On the other extreme, the new C and C++ models make no attempt to
provide security guarantees. The design space for relaxed memory models has
not been thoroughly explored.

In this project, we will design a relaxed memory model for a high level
language that gives stronger guarantees to programmers, making it easier to
write, reason about, and verify concurrent programs. Our approach to the
design combines a focus on real-world concurrent algorithms, to ensure that it
is practical, with mathematical rigor, to ensure that it supports robust
reasoning principles that will ultimately help programmers to understand it
and to write high quality concurrent software systems.

The primary impact of this project will be on the programmers who develop
low-level, concurrent, systems software. Currently, only a small community of
specialised programmers work on this kind of software, because it is
extraordinarily difficult to develop; a significant part of the challenge is
to understand and use the relaxed memory models supported by multi-core
processors and the programming languages that compile to them. Nevertheless,
the software that they develop directly affects all of society. It runs at the
heart of all servers, desktops, laptops, tablets, and smart phones, and its
quality has a direct impact on the stability, security, and performance of
these systems. The research proposed here will make it easier to write
efficient and robust low-level concurrent software by providing a more
intuitive relaxed memory model along with tools to understand it. This will
both enlarge the community who can write such software, and lead to better
quality software running of all of our devices.

The project will also help programming language designers and hardware
designers, both in academia and in industry, by building a richer
understanding of the trade-offs between elegance/understandability and
performance in relaxed memory model design. Language memory models influence
hardware design, and vice versa; for example, the C11/C++11 'consume' feature
lets programmers take advantage of some PowerPC or ARM specific guarantees,
while the ARM architecture has recently added special load and store
instructions designed to support C11/C++11 sequentially consistent atomic
operations. The ideas we develop to build our relaxed memory model in this
project will help produce further synergy.

Finally, we are also aiming for educational impact by making relaxed memory
programming accessible at the undergraduate level. Currently, we can teach
basic concurrent programming above a sequentially consistent memory model, but
we cannot also deal with the detailed pragmatics of relaxed memory. For
example, Herlihy and Shavit's textbook 'The Art of Multiprocessor Programming'
limits the topic of relaxed memory to a brief description in an appendix; and a
module on the basics of real-world relaxed memory is a challenging part of the
CS Master's degree programme at the University of Cambridge. The problem is
that existing models are simply too complex to understand, and simple
rule-of-thumb design patterns lead to inefficient programs. Because our model
will be more amenable to intuitive understanding, and especially because of our
focus (Task 2) on interactive software tools that can demonstrate how the model
works, and that can test algorithms, it should be accessible to students.