Compositional, dependency-aware C++ concurrency

组合的、依赖感知的 C 并发

基本信息

批准号：
EP/R020566/1
负责人：
Mark Batty
金额：
$ 12.59万
依托单位：
University of Kent
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2018
资助国家：
英国
起止时间：
2018 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FR020566%2F1
关键词：
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.

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