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

There will be immediate research benefits from the proposed research; future benefits to those who develop programs in industry or institutions; and long term benefits to all users of computers. These are considered and justified in turn.

Success in this research would bring together several strands of thought on the most appropriate ways to develop concurrent programs. This is a field where UK researchers are already at the forefront of research but the synergy that would result from a unification of rely/guarantee thinking with separation logic could be another major advance on which we could all build. The same payoff would result from a link between atomicity refinement and linearisability methods. Furthermore, although a top-down approach is to be used as an initial guide, the concepts should also provide useful targets for bottom-up methods and tool support.

More tractable methods for developing complex concurrent programs will have a strong impact on the work of development programmers who are already struggling with concurrency and are bound to have to tackle this difficult area ever more often (at least) because of the move to massively parallel (many-core) hardware. The methods developed in this project will be made easier to adopt in industry by the development of tool support within a work package of the project.

Once the new methods are more widely used, the quality of concurrent software will be higher (i.e. less bugs). Furthermore, performance of future systems will be made better because of the ability of program designers to tackle the design of concurrent systems with greater confidence. This will be beneficial to all users of computers.