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.
|