Cs6241 Hw3
Tony Hannan
14 Oct 2003
In order for an invariant definition to be moved before the loop, it must dominate all its uses in the loop, ie. be the only definition for all uses in the loop. However, an invariant definition that shares a loop use with one or more definitions outside of the loop, does dominate the use once it is executed the first time, because the other definitions are outside the loop and will never get re-executed. So, we can move these kind of invariant definitions outside the loop by splitting the loop in two. The first loop executes a copy of the loop until the invariant is executed. That block then continues in the second loop which is a copy of the loop without the invariant. These two loops are equivalent to the original because once the invariant is executed it always holds and therefore does not have to be in the second loop. Again this only holds for non-dominating invariants whose other definitions are outside the loop. Below is an example:
Original loopEquivalent loops with invariant (x := 2) removed
Notice, in both loops, that once the invariant, x := 2, is executed, x will always equal 2 for the rest of the loop, because it is the only definition of x inside the loop.
Below is the algorithm for transforming a single loop with a single non-dominating invariant definition into an equivalent two-part loop with the invariant removed (like above). The gist of it is to copy the loop, remove the invariant from the second loop, and have the outgoing edges of the invariant block in the first loop point to the corresponding destination blocks in the second loop.
procedure TransformLoopWithoutInvariant (LoopHeader, Invariant)
LoopHeader: in Node
Invariant: in Statement
|| assumes Invariant is sole definition of variable in Loop. Make copy of loop and
|| attach to existing loop by having outpointers of Invariant block point to corresponding
|| blocks in new loop. Also remove Invariant from new loop.
begin
NewLoop, InvariantBlock, NewInvariantBlock: Node
NewLoop := CopyLoop (LoopHeader)
|| NewLoop will have no entry but the same exits
InvariantBlock := BlockOf (Invariant)
NewInvariantBlock := CopyOfIn (InvariantBlock, NewLoop)
|| CopyOfIn will return the corresonding block in NewLoop
RemoveStatementIn (Invariant, NewInvariantBlock)
for each e in SuccessorEdges (InvariantBlock)
with each f in SuccessorEdges (NewInvariantBlock) do
|| iterate over each old edge with corresponding new edge
ChangeHeadOfToHeadOf (e, f)
|| change head of old edge to point to the head of new edge
od
end
This algorithm will produce an equivalent program with the invariant removed from the loop as long as the invariant definition is the only definition of its variable in the loop. By “only definition” we allow the same invariant definition to appear multiple times in the loop. In other words “x := 2” can appear multiple times in the loop above, since once one of them is executed, x will equal 2 for the remainder of the loop. To handle these cases I would extend the above algorithm as follows:
procedure TransformLoopWithoutInvariants (LoopHeader, Invariants)
|| assume all Invariants have the same definition
LoopHeader: in Node
Invariant: in set of Statement
begin
NewLoop, InvariantBlock, NewInvariantBlock: Node
NewLoop := CopyLoop (LoopHeader)
for each Invariant in Invariants do
InvariantBlock := BlockOf (Invariant)
NewInvariantBlock := CopyOfIn (InvariantBlock, NewLoop)
RemoveStatementIn (Invariant, NewInvariantBlock)
for each e in SuccessorEdges (InvariantBlock)
with each f in SuccessorEdges (NewInvariantBlock) do
ChangeHeadOfToHeadOf (e, f)
od
od
end
The above algorithms will work for both dominating invariants and non-dominating invariants, and for single uses or multiple uses in the loop. Other definitions can reach from outside the loop, but only the same definition can be inside the loop.
If multiple different definitions for the same variable exist inside the loop, the loop can not be transformed to move any definition outside the loop. This is because any iteration could change the variable by going through one or the other definition.