On a Method of Multiprogramming

by D. Gries (Foreword), W.H.J. Feijen, A.J.M. van Gasteren

Here, the authors propose a method for the formal development of parallel programs - or multiprograms as they prefer to call them. They accomplish this with a minimum of formal gear, i.e. with the predicate calculus and the well- established theory of Owicki and Gries. They show that the Owicki/Gries theory can be effectively put to work for the formal development of multiprograms, regardless of whether these algorithms are distributed or not.

390 pages, Hardcover

First published June 11, 1999

Reviews

[Max Lybbert · Rating 4 out of 5]

The book is very interesting, although I'm not entirely certain how useful it is. Feijen and Gasteren develop a set of rules to use when proving the correctness of multithreaded programs, and then prove several solutions to multithreaded problems. The issue is that their rules are based on very limited primitives (atomic set, atomic add, and "wait for condition variable," notably *NOT* "atomic add and return the old or new value"). Those primitives may be useful in lock free code, but they would need to be expanded for "normal" locking code.

However, the proofs for Dekker's algorithm, the non-blocking writer protocol (similar to what the Linux kernel calls seqlocks ( http://en.wikipedia.org/wiki/Seqlock )), and more general synchronization problems are worth what I paid for the book.

Additionally, if I ever wish to implement a message passing/CSP system ( http://swtch.com/~rsc/thread/ ) efficiently, I'll turn to the chapter on mutual inclusion. And "multi-programming" includes more than just multithreaded programming. It also includes programming with multiple processes. The algorithms in this book would be very helpful in implementing a system of multiple processes communicating through shared memory without system-wide mutexes.

[Angelo · Rating 3 out of 5]

Software engineering is hard enough as it is, but creating communicating programs is exponentially harder. This book has the Feijen-style of building up an argument based on pure logic, with a "touch of smartness" along the way.

Furthermore, I was one of the last students to actually have been taught this course by Mr. Feijen. I intended to sit in on the class one year, and then really take the course the next, but alas, a retirement got in my way...