Concurrency without toil: A systematic method for parallel program design
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.
- A structured approach for developing concurrent programs in Java
- Simplification of boolean verification conditions
- scientific article; zbMATH DE number 3856387 (Why is no real title available?)
- An example of stepwise refinement of distributed programs: quiescence detection
- scientific article; zbMATH DE number 7441269 (Why is no real title available?)
This page was built for publication: Concurrency without toil: A systematic method for parallel program design
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685624)
