Since the parallel structure of the original program is preserved, the transformations also provide a basis for syntax-directed proofs of total correctness under the fairness assumption. These proofs make use of infinite ordinals. Computing Reviews Brent T. Hailpern Fairness constraints require that every component of a parallel program that is enabled sufficiently often will eventually progress. It is well known that seemingly correct parallel programs fail under adverse schedulers. This paper discusses the relationship between parallelism, fairness, and nondeterminism.
Transformations reduce new concepts to known concepts.
For example, in order to analyze a parallel program P that assumes certain fairness constraints, the authors transform the original program P into a new program P . The program P will have no fairness assumptions, but will include an explicit scheduler that implements the required fairness policies. The paper is well written, but does require the reading and understanding of many formal definitions and theorems. It describes which transformations can be done and which are impossible. Most of the paper is dedicated to applications of transformations in order to achieve program correctness.