The advent of VLSI technology has made the implementation of systems of parallel processors for solving complicated problems in real time feasible. Systolic and wavefront processing systems are popular architectures (implementable in VLSI technology) that utilize many simple processors linked by regular communication geometry. Many researchers have shown implementation of various algorithms using suitable systolic architectures. Very few papers, however, provide a mechanism of formally specifying such systems and prove the correctness of their implementation. The paper under review tries to address these issues of concurrent system specification and implementation, and fills the void in this subject.

First, this paper introduces a language based on Milner’s Calculus of Communicating Systems (CCS) language [1] that can be used to describe processes that communicate values via channels. The values could be integers, Booleans, sequences, etc. A set of fixed number of operators is defined to allow one to recursively define processes. The introduction of the language is informal and several examples are used to clarify the concepts.

Next, the concepts of specification (a rather high-level general description of the intended behavior of a process as seen by a user), implementation (a more detailed description of how the process actually works), and correctness (that is, a given implementation is the correct one for the given specification) are introduced. Two systolic systems--namely, a palindrome recognizer and a sorting machine for WEAVESORT--are introduced in detail. The specifications and at least one possible implementation are described in the language introduced in the paper. Detailed proofs of correctness are developed. These are based upon the idea of transformations and a form of induction called Fixpoint Induction. The proof technique cannot easily be mechanized since there are many obstacles. The proofs use a considerable amount of information about the data-domain over which the systems compute.

The author observes: “Although the examples considered are nontrivial, they are still less complex than realistic systems of practical importance.” I concur wholeheartedly with that. Applying the technique developed in the paper to such practical systems could be very difficult. Perhaps some simpler technique that can be mechanized on a computer will be a welcome addition.