The purpose of automatic transformation of sequentially specified programs into concurrent programs is to exploit inherent parallelism. Input to this transformation is a sequential specification of a program along with an independency relation. Output is a concurrent program specification, which can be implemented easily in a language such as OCCAM.

This paper begins with an overview of relevant literature, which makes particular reference to monitor- and message-based concurrent languages. Surprisingly, the authors do not mention Chandy and Misra’s work on Unity.

The main part of the paper focuses on the necessary theory to present the actual transformation and prove it correct under certain sufficient conditions. To specify the behavior of computations, the authors introduce concurrent and possibly-concurrent regular expressions as well as a variant of trace theory (result histories). To find a correct transformation from possibly-concurrent to concurrent expressions, the authors introduce the concept of a synchronization guard. They defer the proof of the main theorem to a dense appendix; the proof is decomposed into eight lemmata, each with a tedious proof.

Next, the authors introduce the specification language Banach, a Pascal-like language extended with keywords to specify independent operations. The programmer need not worry about synchronization: the Banach compiler applies a transformation, introducing the parallel construct and so-called synchronization guards, to guarantee concurrent behavior equivalent to the specified sequential behavior. As an example, the authors specify the dining philosophers problem and show its transformed code. Other examples include copying input to output using buffers, and matrix multiplication. Finally, the authors show how Banach programs can be modeled by the theoretical concepts used in the main part of the paper.

I recommend this interesting paper to any researcher working on concurrent specifications. The notation is unusual, however, and the presentation is rather terse: considerable calculational effort is expected from the wary reader. I found few errors, but two are worth mentioning. At the bottom of page 104, “sequence ad” has to be “history ad,” and in example 3.3 (p. 108), “(a,&Dgr;)” should be “[a,&Dgr;]” because it refers to a tuple, not a regular expression.