Model Checking Tools for Parallelizing Compilers

In this paper we apply temporal logic and model checking to analyze the structure of a source program represented as a process graph. The nodes of this graph are sequential processes whose computations are specified as transition systems; the edges are dependence (flow and control) relations between the computations at the nodes. This process graph is used as an intermediate source program representation by a parallelizing compiler. By labeling the nodes and the edges of the process graph with descriptive atomic propositions and by specifying the conditions necessary for optimizations and parallelizations as temporal logic formulas, we can use a model checker to locate nodes and sub-graphs of the process graph where particular optimizations can be made. We illustrate this technique by showing how a parallelizing compiler can determine if the iterations of an enumerated loop can be executed concurrently. To add or modify optimizations in this parallelizing compiler, we need only specify..