# Loop invariant


意思是，當我們看一個 assignment instruction `x = v_1 op v_2`，只要兩個 operands `v_1` 和 `v_2` 皆各自滿足下面三點其中一點：

1. ==`v_1` / `v_2` 是常數==

ex:

for (i = 0; i < n; i++) {
    x = 3 * 5;
}

> $\rightarrow$ `v_1 = 3`，`v_2 = 5` 都是常數，在 for loop 裡不會變

2. ==會影響這個 assignment 中 `v_1` / `v_2` 的值的定義都在迴圈外==
> 代表迴圈裡沒有任何 instruction 會改變這 `v_1` / `v_2` 的值，所以每次進入迴圈 `v_1` / `v_2` 的值都是固定的

ex:

a = 10;
b = 20;

for (i = 0; i < n; i++) {
    x = a + b;
}

> $\rightarrow$ `a` 和 `b` 的值都在 for loop 外定義，所以不管 `i` 是多少，`x = a + b` 算起來都一樣，因此我們就說 `x = a + b` 是 invariant

3. ==只有一個定義會影響這個 assignment instruction，而這個定義也是 loop invariant==

意思是我們++允許 `v_1` / `v_2` 在迴圈裡定義++，但是只有一個定義會決定這個 assignment 的 operands 的值（決定 assignment 的結果） ，且這個定義本身也是 loop invariant。

這樣講還是有點不清楚，看個例子：

a = 10;
b = 20;

for (i = 0; i < n; i++) {
    t = a + b;
    x = t * 2;
}

- 第五行的 `t` 的兩個 operands `a` 和 `b` 都在 for loop 外定義，所以滿足第二點，因此 `t = a + b` 這個 assignment 是 loop invariant。
- 第六行的 `x` 第二個 operand 是常數，滿足第一點，第一個 operand `t` 的值只會由前一行的 `t = a + b` 決定，且這個 `t = a + b` 我們剛證明了它也是 loop invariant，所以 `x = t * 2` 是 loop invariant。

什麼情況會是有不只一個定義 reaches this assignment 呢？我們可以看一個例子：

for (i = 0; i < n; i++) {
    if (cond) {
        t = 10;
    } else {
        t = 20;
    }
    x = t * 2;
}

我們可以看到第七行的 `x = t * 2`，假如我們要判斷這個 assignment 是否 loop invariant，我們看他的 operands，第二個 operand `2` 是常數所以滿足第一點，第一個 operand `t` 卻有可能是 if condition 的 `t = 10`，也有可能是 else condition 的 `t = 20`，所以並非只有一個 definition reaches the assignment。

# Hoisting


<font color = "blue">Hoisting</font> 就是把 loop invariant 的 instructions 搬到迴圈外。

但是其實並不是一個 assignment 是 loop invariant 就一定能 hoist（搬到迴圈外），有時後會影響語意，例如下面的例子：

## Invalid hoisting


為什麼會發生這樣的問題是因為，loop invariant 只保證每一輪迴圈算出來的結果相同，但沒辦法確保所有的 use 看到的值和原本的 code 相同。
> "use" 和下面會用到的 "live" 定義可參考另一篇筆記 [Liveness](https://hackmd.io/0qVOS9wxQ564sfFQMsPYwg#use--live)

## Safe hoist 條件


上圖的意思是，如果一個 loop invariant assignment 再進一步滿足這三個條件，我們才能確保他能 safe hoist：

1. ==在 loop 結束後會用到 `x` 的地方，在原程式裡一定會經過 `d`==

因為當我們 hoist `d: x = v1 op v2`，即把 `d` 這個 assignment 搬到迴圈外，那麼 `x` 就會變成在 loop 前就被定義。

所以如果原 code 裡在迴圈結束之後有一個 instruction 會用到 `x`，但是本來不會經過 `d`，那麼他原本應該要用的 `x` 值就不會是 `d` assign 的值，而我們卻把 `d: x = v1 op v2` 搬到迴圈外，使得這個 instruction 也用到 `d` 定義的 `x`，語意就改變了。

2. ==迴圈裡只有一個對 `x` 的定義==

例如一個 for loop 裡如果有 `if...else...`，在不同的 condition 對 `x` 有不同的定義，因為我們不能保證到底會執行到 if 還是 else，所以不能 hoist。

3. ==在進入迴圈前的入口 `x` 不是 live 的==
> (Definition dominates all of its uses.)

假如 `x` 在 preheader 是 live 的，意思是存在某條 path 從 preheader 到某個會用到 `x` 的點，且　preheader 設的 `x` 到用到的地方中間沒有其他定義（loop 裡不一定會改到 `x`）

在這樣的情況下，原本應該要用進迴圈前定義的 `x`，如果我們 hoist，就會變成把 `x` 的定義搬到 loop 外，變成這個 assignment 必定執行，hoist 無條件重設 `x`，破壞原本語意。

除此之外，其實還有一點：

4. ==不能在原本不會發生 exception 的地方產生新的 exception==
> (No new exceptions: Cannot introduce exceptions on paths where they didn't exist)

關於這一點，看下方例子比較清楚：

### 例子

出自 jserv 老師 [ACD 期中題目詳解](https://gist.github.com/jserv/6651856532ffcc29106d222924666a30)




簡單來說，如果一開始 $n \leq 0$，那麼 $i < n$ 永遠不會成立，因此我們直接走 False exit，在這個情形下，我們永遠不會執行到 `B2` 的 `t=a/b`。

假如我們在這個情況下 hoist，代表我們把 `t=a/b` 搬到 loop 之前（一定會執行到），那就有可能在這條 path 上產生原本根本不會發生的 exception。

比較值得注意的是我們不試選 F 選項的 A, B 條件皆成立，因為單單強制執行 `t=a/b` 就隱含了 `b` 有可能是零的可能性（原本沒有可能），所以我們不用再加一個條件 `b == 0` 一定要發生。
> 邏輯上是這樣，可以多想幾次。

另外還有單單只有條件 A 並不會使 hoisting illegal，假如 `b == 0`，因為我們說只有條件 A，所以 `n > 0`，因此迴圈至少跑一次。在這樣的情況下，原本的 code `B1` 條件成立，會執行到 `B2`，所以會有 exception；如果我們 hoist，把 `t=a/b` 搬到 loop 之前，因為變成一定會執行，所以一樣也會產生 exception，我們並沒有 introduce new exception。

# Stength Reduction

先定義一些會用到的 terms：

## Induction variables

### Linear Induction Variable

直接看例子：


在這個 loop 裡，`i` 的值每個 iterate 固定加一，直到 `i == n` 時跳出迴圈跳到 `L2`。


我們可以看到迴圈裡的兩個變數 `j` 和 `k` 可以用 `i` 的 linear function 表示，並且係數都是常數（`j` 的 $(4, 0)$ 和 `k` 的 $4$）或 loop invariant 的變數（`k` 的 `a`，因為迴圈裡沒有去改 `a` 的值）

$\rightarrow$ 透過這樣的關係式，我們也可以看到，當 `i` 的值增加 $c$ 時，`j` 和 `k` 都會各加 $4c$

在這樣的情況下，我們說 `i` 是一個 <font color = "blue">linear induction variable</font>。

### Basic Induction Variable


我們說迴圈裡的變數 `i` 是一個 <font color = "blue">basic induction variable</font>，如果他在迴圈裡定義的方式是 `i = i + c` 或 `i = i - c`，其中 `c` 是 loop invariant，也就是說 `c` 要嘛是常數，要嘛是在迴圈外定義的，要嘛是在迴圈內定義，但只有一個定義，且這個定義也是 loop invariant。

### Derived Induction Variable


我們說迴圈裡的變數 `k` 是一個 <font color = "blue">derived induction variable</font>，如果他是一個 induction variable `j` 乘上 / 加上某個 loop invariant `c`。

如果 `j` 也是一個 <font color = "blue">induction variable in the family of `i`</font>，也就是說，`j` 可以寫成：

j = ai + b        // 其中 a, b: loop invariant

那麼我們還需要確保：

1. 唯一會決定 `k` 的 `j` 是在 loop 裡的這個
2. 在 loop 裡，定義 `j` 的地方和定義 `k` 的地方之間沒有改變 `i` 的定義

#### ex: legal

for (i = 0; i < N; i++) {
    j = 2*i + 1;   
    k = j + 5;     
}

#### ex: illegal

for (i = 0; i < N; i++) {
    j = 2*i + 1;
    i = i + 1;     
    k = j + 5;
}

在 `j` 和 `k` 的定義之間改變了 `i` 的定義。

## Strength Reduction


每個 loop variable 的 linear expression 都會新增一個 auxiliary variable，初值設為 linear function 的常數，新變數每輪增加一次項係數的值。