The old saw, “If you think it’s easy, [then you’ve proved that] you don’t understand the problem,” was directed at me a long time ago, but only once or twice (I claim). It has been myfirsthand, abiding experience that no computing challenge is more severely underestimated than the design of concurrent or distributed systems. As is true in number theory, a problem and its statement can be ultra-simple, while its solution or proof shockingly difficult, if not apparently impossible. The author illustrates this early in the book by showing how the interleaved execution of statements belonging to different concurrent processes destroys correctness in the simplest of cases, if correctness-preserving constructs are not rigorously designed into the system.

This second edition of Ben-Ari’s book, which follows the first edition by 16 years, is outstanding in its concurrent explication of the problem, and of the various principles, techniques, and implementations of its solution. On the preface’s very first page, the author states a truism that should berepeated daily, so that our conceit in having mastered, say, the latest programming language features will not go to our heads: “[B]asic concepts like interleaving, mutual exclusion, safety and liveness remain with us ... as have semaphores, monitors, channels and messages [over the past 16 years].” In other words, real fundamentals don’t change. However, a strong impetus for the revised edition is the “truly new development in concurrency ... [:] the widespread use of model checkers for verifying concurrent and distributed programs.” This edition thus addresses the use of state diagrams in verifying correctness at the outset.

The book is written for “advanced undergraduate[s] and beginning graduate students, as well as practicing software engineers interested in obtaining a scientific background in this field.” And a scientific background is what this excellent book provides, at just the right depth and breadth. The topics, if not exact titles, of the book’s 13 chapters are: what concurrent programming is; the concurrent programming abstraction; critical sections; verification of concurrent programs; advanced critical-section algorithms; semaphores; monitors; channels; spaces (the Linda model); distributed algorithms; global properties; consensus, as in the Byzantine generals problem; and real-time systems. The appendices cover the pseudocode notation used in the book, mathematical logic, a concurrency problem set, software tools, and further reading.

The pseudocode notation is clear and appealing, and leaves no confusion regarding what is global, what is local, and what is atomic. Regarding the logic appendix, I am really grateful to the author for seeing fit to point out, in such a short space, a cognitive problem with material implication that I dare say rears its head at the most inopportune moments, and generates doubts regarding a proof under consideration. The author points out that Wason selection tasks, of which an example is in the appendix, help psychologists investigate difficulties in reasoning with material implication. This is typical of the author’s attention to careful pedagogy, which pervades the entire book.

Though the book is excellent and instructive stand-alone reading, it is fair to consider it as being also strongly coupled to Web sites that carry model-checking and simulation software (and also references to classic and contemporary books and papers). Among these ancillary tools for learning concurrency are: the author’s Ben-Ari concurrent interpreter (BACI) concurrency simulator; the Spin model-checker, whose language is Promela; and distributed algorithms in Java (DAJ), a distributed algorithm scenario-generating tool. The author has “made a point of using Spin to verify all the algorithms in the book, and [has] found this to be extremely effective in increasing [his] understanding of the algorithms.” Examples are displayed in state diagrams, pseudocode, and in a choice of Promela, Java, and Ada, all in a coherent, intelligible fashion.

The book includes a well-placed section on advanced concepts of (linear) temporal logic in its chapter on verification, and gives clear definitions of the necessary conditions for critical-section correctness: mutual exclusion; lack of deadlock (also known as “livelock,” as the author points out); and lack of starvation. Verification is done using invariant assertions, deductive proofs with temporal logic, and (Spin) model checking. The proof of mutual exclusion via induction on the states of computation is highly instructive. Regarding Spin/Promela, if this is your first encounter with the nondeterminism of guarded commands, you would do well to slow your reading of this part.

The four jobs I’ve had (in series) over the last 30 years have concerned event-driven, hard real-time systems (in aerospace, factory automation, and rapid transit). Chapter 13, “Real-Time Systems,” presents and elucidates the issues very well indeed, and accords perfectly with my colleagues’ and my experiences.

Near the end of this outstanding book, the author says: “We have become tolerant of unreliable desktop software that crashes frequently. This attitude is simply unacceptable for ... systems that control critical tasks, especially for systems that cannot be debugged.” Hear, hear!