The simple examples the authors begin with immediately convince us that multiprogramming is highly difficult. Even if each individual program is proven correct, we have to show that their concurrent execution will not induce total deadlock, nor will any individual starvation prevent a component from completing its job. Using mutual exclusion to ensure that each component is not affected by others is not a solution, it is refusing the advantages of multiprogramming. There is a strong need for new and efficient tools to guarantee at least partial correctness in multiprogramming. Programming notations and assertions are presented in the first two chapters. The Owicki-Gries theory is the foundation of any correctness proof in multiprogramming. Ways of controlling complexity are given. Problems of synchronization, deadlock, and individual progress are discussed, and many examples and exercises are provided.

In sequential programming, proving the correctness of a program is far more difficult than building a program from the elements of its proof: a preassertion (the initial state of the data) being given and a postcondition (the desired final state) being assigned, intermediate assertions are not too difficult to discover, and statements between them are easy to write. The same thing is true in multiprogramming, as David Gries says in his preface: “It is far easier to develop the proof and program hand in hand, with the proof ideas leading the way.”

The constructive part of the book begins in chapter 12, with many exercises of various kinds (some are concerned only with proofs, others with program development) and various orders of difficulty. Chapter 13 is the first place in which derivation of an algorithm is presented, but, curiously enough, it begins with three a posteriori proofs, perhaps because the authors wish to exhibit the simplicity of program derivation in comparison. In subsequent chapters, mutual exclusion, phase synchronization, and communication protocols are revisited, as are Dijkstra’s semaphores. The derivation of three important algorithms ends the book: distributed computation of a spanning tree, Safra’s termination detection algorithm, and the alternating bit protocol.

The book’s structure is coherent: you cannot derive a program from the elements of its proof if you have not mastered these elements, so methods of proving program correctness necessarily come first. Readers should resist the temptation to skip the first part of the book and go directly to program derivation. The simple examples given in the first chapters show that you cannot rely on pure intuition when concurrency between programs is involved. Aphorisms by the authors, such as “In multiprogramming, never lean on intuition of any kind, but on rigorous proof instead” and “Careful calculation, rather than ‘intelligent guessing,’ will be responsible for the art of constructing multiprograms” remind me of Henry Ledgard’s famous programming proverbs.

Because the correctness of programs running concurrently on a computer has to be proven, formal methods cannot be avoided. The authors keep the core theory simple. The last aphorism of the book is, “Simplicity is a major scientific concern.” In my own experience, and likely that of many programmers, simplicity is not achieved on the first try: a lot of work has to be done to obtain a simple, clear program. I can imagine the impressive work done by the authors to produce such a simple presentation of multiprogramming methods. Several strategies are described for moving from given preassertions to desired postassertions. Maintaining the symmetry of assertions between similar components is a good heuristic.

Recent events have shown that programming practices are poor. Although programming has been made into a science, which should lead to solid program construction, many programs remain empirical objects, unable to cope with situations that should have been thought of. Tools exist that allow the development of good, solid programs. This book exhibits such tools for multiprogramming. It is an excellent book, which can be read easily and must be read carefully by any programmer concerned with multiprogramming, and by any student of computer science.