Partial Evaluation of Concurrent Programs
10am, Wednesday, March 19, 1997
The goal of this dissertation is to develop partial evaluation (program specialization) techniques specific to concurrent programs.
The language chosen for this investigation is a very simple CSP-like language. A standard binding-time analysis for imperative languages is conservatively extended in order to deal with the basic concurrent constructs: synchronous communication and nondeterministic choice. Based on the resulting binding-time annotations, a specialization transformation is formally defined using a labeled transition system with actions. The correctness of the partial evaluation is stated and a proof is included. This result is closely related to (strong) bisimulation, the equivalence relation on transition systems. We name the two directions of the bisimulation equivalence soundness and completeness respectively.
In order to maintain a clear presentation, this simple specialization algorithm addresses only the data transfer component of the communication; a post-specialization analysis for the detection and removal of redundant synchronizations (i.e. synchronizations whose removal does not increase the nondeterminism of a program) is presented separately. This redundant-synchronization analysis is based on the characterization of dependencies in a CSP-like language.
Several pragmatic issues such as improving the binding-time analysis, controlling loop unrolling and the consequences of lifting nondeterminism from run-time to specialization-time are discussed. Two additional binding-time analyses are presented. We call one of them speculative because the specialization transformation based on it is sound but not complete. We call the other one extended because it includes an on-line redundant-synchronization analysis.
The relationship between partial evaluation and different types of fairness is also studied. In order to deal with a wide range of fair run-time systems, ranging from strong to weak, and from process-fair to channel-fair and communication-fair, we use a general operational framework for specifying fairness properties as systematic means of reducing nondeterminism. We then prove the correctness (as bisimulation equivalence) or just the soundness of specialization transformations under various binding-time analyses.
Throughout the dissertation, the power of the newly developed techniques is shown in several examples.