Taming Concurrency

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

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".