An Algebraic Approach to Parameterised Loop Decomposition

Abstract

Loop scheduling is to explore more possible parallelism by re-organizing the loop body without changing its semantics; it results in more efficient utilization of the underlying hardware. Recently, research has been shifting from well studied instruction level parallelism to thread level parallelism (TLP) in order to follow the trends of CPU design; parts of the COCONUT project are moving in this direction as well. Loops are usually represented in graph-like structures, which, without algebraic properties, can make formal verification very difficult. In this thesis, a new representation of a loop, called an extensible loop specification, is proposed, based on the code graph and loop specification concepts already used in the COCONUT code generator. Extensible loop specifications are intended to be used by TLP loop scheduling algorithms; their algebraic properties derive from those of loop specifications and code graphs. During the process of discovering a new loop representation, we use a relational model to verify some transformations of control flow graphs where transitions are labeled with code graphs.