On a method of multiprogramming. Foreword by David Gries
The book presents a method for the formal development of parallel programs. It is based on the theory of Owicky and Gries well-established in proving the correctness of multiprograms a posteriori. The authors now turn the tables and show how to use Owicky/Gries theory to formally derive multiprograms from a specification. The book consists of 32 (more or less short) chapters that are divided into two parts: Chapter 1 through 11 set out the basic techniques, whereas each chapter of the second part presents an example applying the technique. Chapter 12, called the Yellow pages, summarizes the notations and the rules developed in the first part. The first chapter shows that parallel execution of sequential programs may result in unforeseeable effects even if the sequential programs are extremely simple. The next five chapters introduce the Owicky/Gries theory step by step. Chapter 7 presents the formalism at work. The remaining chapters of the first part are concerned with synchronization issues. In the second part, the authors discuss the well-known concepts how to synchronize parallel processes, e.g., mutual exclusion, non-blocking write protocol, synchronous communication, deriving correct implementations using their method. Then, they apply the method to some algorithms, e.g., distributed computation of a spanning tree and the alternating bit protocol. These chapters are of very different length (6-20 pages). It is not clear who the intended reader of this book should be. The authors call it a research monograph; the structure of the book and the level of detail in presenting proofs, however, lead to the impression that the book can be used as a textbook, although only on a postgraduate level. In each case, a chapter title like ``Three theorems and two examples is too vague.
- A formal methodology using attributed grammars for multiprocessing-system software development. II. Validation
- Formalizing and implementing Gries' program development method in dynamic logic
- Language hierarchies and interfaces. International summer school, Marktoberdorf, Germany, 1975
- Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations
- Invariant-based reasoning about parameterized security protocols
- Streamlining progress-based derivations of concurrent programs
- scientific article; zbMATH DE number 1639446 (Why is no real title available?)
- Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
- Deriving Real-Time Action Systems Controllers from Multiscale System Specifications
- scientific article; zbMATH DE number 4133478 (Why is no real title available?)
- Program development with control abstractions.
- Structured programming in symbolic multiprocessing
- scientific article; zbMATH DE number 4052998 (Why is no real title available?)
- scientific article; zbMATH DE number 193739 (Why is no real title available?)
- scientific article; zbMATH DE number 400580 (Why is no real title available?)
- On a method for the formal design of multiprograms
- scientific article; zbMATH DE number 1878568 (Why is no real title available?)
- Using ontologies and algebra of algorithms for formalized development of parallel programs
- Formalization of parallelism forms in IPCL
- An algebraic approach to refinement with fair choice
- A verified durable transactional mutex lock for persistent x86-TSO
- Formal derivation of an algorithm for distributed phase synchronization
- Concurrency without toil: A systematic method for parallel program design
- A formal model of data structures and abstract algorithms for multiprocessor computer systems
This page was built for publication: On a method of multiprogramming. Foreword by David Gries
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4258224)