On a method of multiprogramming. Foreword by David Gries

From MaRDI portal





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.




Cited in
(24)








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)