Software Engineering and Formal Methods: 10th

Book Preface

There is much research activity around formal support for concurrency. The reasons for this ought be clear. For non-critical applications, good (semi-formal) engineeringmethods are sometimes adequate for sequential programs. Such methods borrow much from past formal research and, even here, organisations such as Praxis report that adding formalmethods to the development process can bring about a return on investment because of the tighter control and reduction in the late discovery of errors that are expensive to fix because they result from decisions made much earlier in the design process.

Once one moves to the design of concurrent systems, the enormous increase in the number of execution paths brought about by thread interaction makes it effectively impossible to have any confidence in correctness without some form of formal proof.

One might ask why designers should be so rash as to venture into such dangerous territory. Unfortunately, there is no choice — the pressures to face concurrency become ever greater. First, the (economic) limits for the extrapolation of “Moore’s law” mean that hardware performance can only be increased by moving from “multi-core” to “many-core” hardware (i.e. numbers of threads likely to measured in hundreds). Secondly, embedded systems often run in parallel with physical phenomena that are varying continuously; control software linked to the physical world by sensors and actuators cannot ignore these state changes. Thirdly, a class of application has to be implemented by physically distributed sets of processors.

The combination of a realisation that concurrency cannot be avoided with the acknowledgement that its mastery requires formal tools has generated many research strands. Notable activity in the areas of rely/guarantee thinking, separation logic, atomicity refinement and linearisability is addressed in the body of this paper (citations to relevant papers are given below). To apply some of these research ideas to the paper itself, the attempt here is to look for constructive interaction between several threads of research. In particular, this paper looks to tease out the key concepts from the various methods and indicate a path to one or more methods that achieve real synergy from what are currently rather distinct approaches. This is a much deeper exercise than just seeking combinations of notations.