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.