Taming Concurrency

众所周知，计算机程序很难完善（每个人都经历过“bug”带来的某种形式的不便），即使这种情况开始得到控制，也要付出巨大的代价。软件开发成本高的一个原因是，在系统设计早期所犯的错误可能在系统被测试之前无法被发现——或者更糟的是，被客户使用。在这么晚的阶段纠正错误是非常昂贵的，因为有这么多的工作要重复。所谓的“形式化方法”最初部署在安全关键型软件上，但由于在整个设计过程中使用这些方法可以大大减少由于后期发现设计错误而导致的“报废和返工”，因此它们正变得越来越具有成本效益。形式化方法使这成为可能，因为它们使用形式化符号来指定应该构建什么，从而为每个设计步骤提供正确性的概念。验证设计决策成为一个证明过程，可以通过适当的定理证明软件来帮助。不幸的是，正当真正的进步正在取得时（包括通用工程实践和正式方法的应用），单独的商业开发正在极大地增加挑战。新困难的大方向是“并行”。并发程序必须在干扰其进程的上下文中运行。并发性可能来自对更好性能的渴望，来自将嵌入式程序与物理设备（如汽车和飞机）结合使用，或者来自使用由许多处理器构建的最新硬件设计。传统的工程方法，甚至许多用于检测软件错误的现代自动工具，都不能满足大规模并发的世界，因为当进程相互干扰时，执行路径的数量是天文数字。幸运的是，有研究（英国研究人员处于前沿）可以推理出哪些地方没有干扰和/或受到限制。然而，这些研究途径需要整合在一起，并且在工程师使用它们之前必须实现工具支持。这些是“驯服并发性”的预期输出。

Computer programs are notoriously difficult to perfect (everyone has experienced some form of inconvenience from "bugs") and even if this situation is beginning to come under control, it is at enormous cost. One reason for the high development cost of software is that errors made early in the design of a system can lay undetected until that system is tested - or even worse, used by customers. Correcting errors at such late stages is extremely expensive because so much work has to be repeated. So-called "formal methods" were first deployed on safety-critical software but are becoming more and more cost-effective because their use throughout design can drastically reduce the "scrap and rework" that comes from late detection of design mistakes. Formal methods make this possible because they use formal notations for specifying what should be built and thus offer a notion of correctness for each design step. Verifying design decisions becomes a proof process that can be helped by appropriate theorem proving software. Unfortunately, just as real progress is being made (both with general engineering practices and with the application of formal methods), separate commercial developments are increasing the challenges enormously. The general direction of new difficulties is "concurrency". Programs that are concurrent have to run in contexts which interfere with their progress. Concurrency can come from a desire for better performance, from use of embedded programs in conjunction with physical devices such as cars and planes, or from the use of the latest hardware designs that are built from many processors. Traditional engineering approaches, and even many modern automatic tools for detecting errors in software, are not going to suffice for the world of massive concurrency because the number of execution paths is astronomically large when processes can interfere with each other. Fortunately, there is research (in which UK researchers are at the forefront) for reasoning both about where interference is absent and/or constrained. These research avenues, however, need to be brought together and tool support must be implemented before they are usable by engineers. These are the expected outputs of "Taming Concurrency".