University of Minnesota
Software Engineering Center

You are here

Model Checking as a Tool Used by Parallelizing Compilers

Date of Publication: 
April 1997
Associated Research Groups: 
Publication Files: 
In this paper we describe the usage of temporal logic and model checking in a parallelizing compiler to analyze the structure of a source program and locate opportunities for optimization and parallelization. The source program is represented as a {\em process graph} in which the nodes are sequential processes and the edges are control and data dependence relationships between the computations at the nodes. By labeling the nodes and edges 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 of the process graph where particular optimizations can be made. To discover opportunities for new optimizations or modify existing ones in this parallelizing compiler, we need only specify their conditions as temporal logic formulas. We do not need to add or modify the code of the compiler. This greatly simplifies the process of locating optimization and parallelization opportunities in the source program and makes it easier to experiment with complex optimizations. Hence, this methodology provides a convenient, concise, and formal framework to carry out program optimizations by compilers.
In Proc. of the 2nd Formal Methods for Parallel Processing: Theory and Applications workshop held at the 11th International Parallel Processing Symposium in Geneva Switzerland, April 1-5, 1997.
@inproceedings{Eric97a, author = "Rus, Teodor and Van Wyk, Eric", title = "Model checking tools for parallelizing compilers", booktitle = "Second International Workshop on Formal Methods for Parallel Programming: Theory and Applications, Proceedings", year = 1997, month = "April" }