---
# System prepended metadata

title: Handling more than single loops
tags: [equiv-check]

---

###### tags: `equiv-check`

# Handling more than single loops

* One-to-many loops:
    * loop iterations are split, and the operations done are the same
        * e.g., source has a loop with N+M iterations, target has two loops with N and M iterations each, while the operations done in both are same as those in source loop
            *  leaving the complexities of having different kind of variables aside, assume that source loop and both target loops have the same set of variables
            *  check to see if # iterations in source equals sum of # iterations in both (or more) loops in target. 
            *  if passed, then we can split the source loop accordingly, while having the same body in both loops. 
            *  Then, last step is to handle individual loop equivalences 
    * the operations are split into two or more, while the number of iterations remain the same
        * e.g., loop unswitching
            * assume that the source is in unswitched situation, and target is in switched situation
            * check if # iterations in source are the same as # iterations in both loops in target
            * 
* Many-to-many loops:
    * We can use a similar algorithm for many-to-many loops case
        * start with comparing the first two loops and checking their number of iterations
        * if same, move to next loops in both programs
        * otherwise, take the loop with more iterations and split it. Split should be such that the first half of the split has same iterations as the first loop in other system. 
        * Proceed to next loop and compare again to repeat step 2
        * The source and target should be comparable, if last pair of loops should have same # of iterations so we have perfect mappings from source to target

y = 0
prog1: N iterations
for (int i = 0; i < N; i++) {

}

y = 0
-> for (i = 0; i < A, i++) {
    y
}


-> for (i = 0; i < B, i++) {

}

prog2: M+K iterations
for (int j = 0; j < M; j++) {

}

for (int j = 0; j < K; j++) {

}

For equivalence: 
pre: N=M+K, N > 0, M > 0, K > 0
post: N=M+K, 