Compositional, dependency-aware C++ concurrency

We address a difficult technical problem that is drawn from outside of the strict bounds of academic research: we seek a solution to fundamental problems found in the standards of the C and C++ programming languages. C and C++ code is not just prevalent -- it is used to form the lowest and most trusted levels of our systems. The kernel of every mainstream operating system uses some combination of the two, including Windows, MacOS, iOS, Android, Linux and Unix, as do the swathe of embedded controllers with essential functions like engine management. Having a good specification of the language is the first step in verifying the correctness of these vital system components.

-- Combatting software failure --

This work is part of a larger effort to combat software failure by developing techniques to verify the correctness of software. Currently, developers of computer systems rely predominantly on testing to ensure that systems behave as they should. The system is run for some time over various inputs and monitored for failure. The hope is that this will expose enough of the flaws in the system to have it behave reliably once it is deployed. But it is increasingly expensive to achieve good coverage: systems like cars experience varied inputs, and a fleet of a particular model runs collectively for far longer than the time its computer systems are tested. Worse still, modern systems are concurrent -- using multiple communicating processors to complete a task. The delicate interplay between the concurrent processors makes the output of the system dependent on the timing of communication, so that some behaviours occur only a handfull of times in billions of runs, leaving testing little hope of finding associated bugs.

There is evidence that this approach is breaking down and some bugs are evading discovery even in critical systems: for example a concurrency bug caused some of Toyota's cars to suddenly and relentlessly accelerate, killing 83 over 10 years. The wider economic cost of software failure was estimated by the U.S. National Institute of Standards and Technology to cost USD 60bn each year. Improving our approach to software failure would have substantial economic and societal impact.

Verification offers an alternative to testing: one defines desirable properties of the system -- it will not crash, fuel metering will be proportional to accelerator input, and so on -- and mathematically proves that the code satisfies them. In the ideal of verification, there is no space for bugs to creep in and the mathematical proof of correctness is absolute. Unfortunately, verification techniques are invariably built above an idealised model of the computer system, e.g. the assumption that memory accesses take place in a global sequential order, so called sequential consistency (SC). The distance between the ideal and the reality leaves ample space for bugs to persist. In fact the status quo is much worse because we do not have a characterisation of the reality of the system's behaviour: our best models of programming-language behaviour are known to be broken, e.g. in C, C++ and Java.

In this broad context, our project will develop a description of concurrency in the C and C++ languages that matches the reality, permitting the sorts of concurrent behaviour exhibited by compiler optimisations and the underlying concurrent processors. At the same time, we will support components written under the idealised SC assumption, enabling for the first time the use of the most powerful automatic verification techniques in a setting that correctly models the subtle concurrency behaviour of modern languages, dovetailing these previously disparate views of the system. Our work will make verification of concurrent systems more viable, helping to address the economic and social costs of software failure.

The concurrency that lies at the heart of our computer systems is not understood. This lack of a sound foundation makes it impossible to be sure of the security and robustness of our systems. This project will produce a mathematical description of currently ill-defined concurrency in C and C++, and provide an ability to consider programs as an aggregate of components, matching programming practice. We strive for industrial adoption of our approach, targeting the International Standards Organisation and others with tailored impact-driven dissemination.

The problems in C and C++ that we seek to solve are fundamental, and analogous problems are found in the specifications of the Linux concurrency macros, Java, OpenCL, CUDA, LLVM IR and every other programming language that provides efficient low-level access to memory and an optimising compiler.

This project has the potential for broad impact in both academia and industry. We will construct a new scheme for specifying concurrent memory that solves the problems in the state-of-the-art. This new approach to concurrency will produce 3 kinds of impact: it will fix problems in current industrial specifications, it will enable formal verification of compiler optimisations, and it will provide a sound footing for cutting-edge SC verification techniques. We expand on each below.

1. A concrete basis for language concurrency.

Throughout the development of our models we will endeavour to match the style of the existing C++ model and minimise differences. We intend our model to serve as the cleanest and most straightforward replacement for the current flawed model, maximising the potential for impact on future revisions of the C++ specification. Our new concurrency model will be mathematically defined, with a simulator that experts can use to run the model, and test their intuitions. In this way, we will produce a superior alternative to current concurrency specifications, and it is our intent that these should replace the status quo.

The prior experience and contacts of the PI, Batty, place him in a unique position to press for impact across many languages: he has key contacts concerned with the definitions of the Linux concurrency macros, Java and CUDA. Moreover, Batty has been particularly involved in the definition of the C and C++ languages, where developments are keenly watched by other language specifiers, and often adopted more or less verbatim (as in OpenCL and LLVM IR).

This context suggests the following strategy for industrial impact: Batty will present the model defined by this project to the specifiers of C++ and disseminate it to key players in the definition of the Linux concurrency macros, Java, and CUDA.


2. Optimisation validation.

Key processor vendors have engaged with recent research on relaxed memory and sought to limit the introduction of new behaviours, while releasing increasingly detailed and accurate micro-architectural specifications. Compiler writers have not engaged in the same way, but the development of a dependency-aware model of language concurrency will provide all that is needed begin a new line of academic/industrial collaboration. As part of the project, we will validate optimisations using our simulation tools: we hope that these tools might be exported to industry in the future.


3. Supporting SC verification.

A central goal of the project is to provide a sound basis for mature SC verification techniques over a relaxed-memory language, and this has the potential for major impact. It would unify two currently disparate strands of research and would pave the way for verification of industrially-relevant bodies of code that use relaxed concurrency, like the Linux kernel. Future work would leverage this ability and showcase its value to industry.