A framework for on-line partial evaluation

Abstract

The term partial evaluation describes a class of program transformation techniques. The heart of these techniques is to transform programs by incorporating portions of known runtime data into the program. The resulting program has been "partially" evaluated - some of the actions of the programs can be performed at compile-time due to the known data. There are two general classes of known data that can be used by such a process. The first class is composed of data that is implicit in the production of the program; examples include textual constants, macro expanded values, type tag values, method dispatch tables, etc. Some amount of such data occurs frequently in high-level programs. The second category is composed of data that is explicitly provided at compile time. Such data can be used to create customized versions of very general programs such as ray-tracing and numerical modeling systems.

In this thesis we propose a formal framework for an on-line partial evaluation system. The underlying model for values in the partial evaluator is not restricted to finite-height lattices; the termination of the evaluator depends on the convergence of operations, rather than on a restricted model for values in the system. The proposed framework clearly separates the partial evaluation algorithm from the abstract domains used for representing information during the evaluation, allowing a wide variety of evaluations to be effected by the same core algorithm. The partial evaluation algorithm that is proposed as part of the framework is a polyvarient on-line algorithm that makes effective use of the static information present in program source while preserving soundness and termination. The thesis presents careful proofs of termination and soundness based on characterizations of behaviour under the natural semantics. The key to the algorithm is recognizing when exact analysis is safe with regards to termination and when a more conservative approximation is needed.

The actual on-line algorithm depends only on the properties of the abstract domains, not on particular choices of abstraction. The abstract domains allow the partial evaluation algorithm to take advantage of safe computations whenever possible. The overall algorithm we propose compares favourably to other partial evaluation systems in its ability to capture information present in the program, and the ability of the system to execute without any human intervention other than an indication of how much the system is permitted to increase the size of resulting program. The ability of a general system to generate reasonable results without human intervention is a key advantage that is a prerequisite for having this type of technology applied in real systems.