Compositional, dependency-aware C++ concurrency

我们解决了学术研究严格界限之外的一个难题：我们寻求C和C++编程语言标准中发现的基本问题的解决方案。C和C++代码不仅仅是流行的--它被用来形成我们系统的最低和最受信任的级别。每个主流操作系统的内核都使用了这两种操作系统的某种组合，包括Windows、MacOS、iOS、Android、Linux和Unix，以及一系列具有引擎管理等基本功能的嵌入式控制器。拥有良好的语言规范是验证这些重要系统组件的正确性的第一步。--对抗软件故障--这项工作是通过开发技术来验证软件的正确性来对抗软件故障的更大努力的一部分。目前，计算机系统的开发人员主要依靠测试来确保系统按其应有的方式运行。系统在各种输入上运行一段时间，并监控故障。人们希望，这将暴露出足够多的系统缺陷，使其在部署后能够可靠地运行。但要实现良好的覆盖成本越来越高：像汽车这样的系统经历了不同的输入，特定车型的车队集体运行的时间远远长于其计算机系统的测试时间。更糟糕的是，现代系统是并发的--使用多个通信处理器来完成任务。并发处理器之间微妙的相互作用使系统的输出依赖于通信的时间，因此一些行为在数十亿次运行中只出现了几次，使得测试几乎没有希望找到相关的错误。有证据表明，这种方法正在崩溃，一些错误正在逃避发现，甚至在关键系统中也是如此：例如，一个并发错误导致丰田的一些汽车突然无情地加速，导致83人在10年内死亡。美国国家标准与技术研究所估计，软件故障造成的更广泛的经济损失每年要花费600亿美元。改进我们处理软件故障的方法将产生重大的经济和社会影响。验证提供了测试的另一种选择：一种定义系统的期望属性--它不会崩溃，燃料计量将与加速器输入成正比，等等--并从数学上证明代码满足它们。在验证的理想中，没有错误潜入的空间，正确性的数学证明是绝对的。不幸的是，验证技术总是建立在计算机系统的理想化模型之上，例如，假设存储器访问以全局顺序发生，即所谓的顺序一致性(SC)。理想和现实之间的距离给虫子留下了足够的生存空间。事实上，现状要糟糕得多，因为我们没有系统行为的真实特征：我们最好的编程语言行为模型已知被打破，例如在C、C++和Java中。在这种广泛的背景下，我们的项目将开发一种符合现实的C和C++语言中的并发性描述，允许编译器优化和底层并发处理器所表现出的并发行为类型。同时，我们将支持在理想化的SC假设下编写的组件，首次能够在正确模拟现代语言的微妙并发行为的环境中使用最强大的自动验证技术，与这些以前不同的系统视图相吻合。我们的工作将使并发系统的验证更加可行，有助于解决软件故障的经济和社会成本。

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.