Concurrency without toil: A systematic method for parallel program design (Q685624)

The paper presents a systematic method for the development of concurrent systems. The method is an extension of the classical invariant method of Dijkstra for sequential programming. It consists in a sequence of refinement steps that transform a coarse-grained version of a concurrent system into a finer-grained one. The material is organized in six chapters as follows: The first chapter contains a short introduction. The second chapter introduces a programming notation and a proof system. The formal concurrent system (FCS) is a transition system. FCS uses the notion of process but a special operation for parallel composition of processes is not provided. The lack of parallel composition is from ``without toil'' view point adopted. The third chapter contains a detailed description of the stepwise refinement method for the design of a concurrent system. The method is illustrated in the next two chapters; an abstract algorithm for the mutual exclusion problem is developed step by step into a network of communicating sequential processes. The last chapter, chapter 6, contains the conclusion. The main idea is that most program refinement can be performed using formal manipulation, although the formal development might be rather long. The article is not completely self contained but it is easy to read. Its style is mathematically rigorous and comprehensive.