Equality saturation: a new approach to optimization

Abstract

共通の中間表現に等式情報(equivalences) を追加していき, 飽和されると入力の最適表現が含まれている
そこからグローバルなヒューリスティック(スコア関数のこと) で最適な表現を選択できる.

Introduction

Term Rewriting と違って, 非破壊的に解析できる
- 等式情報を追加するだけなので
(Optimization order does not matter): 等式追加に順序性はない
(Global profitability heuristics):
- 既存の最適化パスはパスごとに評価関数を計算して最適化を行っていた
  - E-Graph はグローバルな評価関数を持てるので, 変換を施した後, 全体を見て評価できる
(Translation validation):
- Circuit Validation にも使える

Contributions

時間的にも空間的にも既存のコンパイラ最適化より有用
単純な最適化と複雑な最適化の両方を発見するのに有効
現行のoptのvalidationをするのに有用
- Sootという最適化ツールの2%のルールにバグが見つかった

Overview

アプローチは入力プログラムの複数のバージョンを表す表現に等式情報(equiv) を伝搬させるという考えに基づいている.
等式推論を効率的にするためには

等式公理のような単純なルールから分岐やループまでをサポートする必要がある.
- PEG を設計した
  - Gated SSA representation と同じく, 参照透過的で副作用がない
  - PEGはそれ自体で完結していて CFG のようなものが’必要ない
課題: 等式情報が追加される度に最悪指数関数的に表現が増加してしまう
- 解決策: PEG に等価表現を統合する -> E-PEG
- 詳しい話は Related Work で

1.1 Program Expression Graphs

loop-induction-variable strength reduction を実例として説明する
- ループ内の代入が全てincrement(i [+-]= k) なら, 加算する量をスケールしてあげれば i * const は i に置き換えられる

PEG

node: 四則演算や条件分岐, ループを表現する演算子
edge: データフロー(演算子と引数をつなぐ)
からなるグラフ,

use(x) は変数が使われることを示す

(a) は i * 5 を表している, edgeは実線で表す

2: $θ$ はループ内でのみ生きる変数, 左辺は初期値, 右辺が前の値からの計算
- なのでサイクルを持つ
- 3: $ϕ$ ノード, 制御 $δ$ を取り, その値によって真偽の処理を選ぶ

こんな感じで純粋な関数として表される.

ヒープへのi/oを伴う操作はヒープを引数にとり, 変更されたヒープを返すことで純粋性を保つ -> なんかモナドみたい

課題: PEG から CFG に戻すときに線形型付けの規律に従わなければいけないので, 線形化する必要がある
- 簡単な方法は見つけたが完全ではない todo
- Javaに対してPEGのからの変換をする際に問題になる

1.2 Encoding equalities using E-PEGs

先程の PEG から生成される E-PEG .

点線は等価性
等値性解析は
- 対象の式パターンであるトリガ
- パターンがE-PEG内で見つかったときに呼ばれるコールバック (ex. a * 0)
  - コールバックが適切な等値関係を追加する (ex. a * 0 = 0)

loop-induction-variable strength reduction では

を必要とする.

分配法則と定数畳み込み等式解析を適用した結果, E-PEG は飽和して,

になる. (書いて確認する todo )

fig (b) は7つの等式関係を持っているので $2^{7} = 128$ 通りの表現を持っていると言える.

fig (c) は 1, 6, 8, 10, 12 を選択すると構築できる.

Peggy では疑似booleanソルバでノードを選択した
- 整数線形計画法ソルバの変数がboolean版
  - 8 3 Global profitabillity heuristic で詳細に説明する.

1.3 Benefits of our approach

Introduction の繰り返し

2. Reasoning about Loops

2.1 Single loop

を考える,

毎回2ずつ増えて, 15回ループする
- $θ$ ノードは [0, 2, 4, ...] を生成する
- eval(s, n): 列 s: int[] の n: PassNode | ??? 番目を返す
  - ループ後の値を表す
- pass(s): 列 s: bool[] の最初にtrueなものを返す
  - ex. この例では 15, $i \geq 29$ がtrueになるのが15番目
前の例では, eval, pass を簡単のために(for clarity)省いていた
ループ内で変動する変数1つ毎に $θ$ はある
- pass はループ内に1つしかない
  - 3 3 Loop peeling や 8 4 Eval and Pass で詳しく話す

2.2 Nested Loops

内側のループでは sum_inner, 外側では sum_outer と区別している
eval_1 が最終的な値
構造は変わらない

2.3 Inter-loop strength reduction

intricate: 複雑

複雑なループを最適化するアプローチを紹介

を考える, (a) は

と等価

トップレベルの + ノードには　eval や pass が含まれている.

(A) 和の分配 $i + θ_{2} (0, 1 + j) = θ_{2} (i + 0, i + (1 + j))$
(B) $i + 0 = i$
(C) 結合則と可換 $i + (1 + j) = 1 + (i + j)$
(D) 0から $n$ incすると $n$
(E) $ecal_{2} (j, k) + i = eval_{2} (j + i, k)$
(F) $j + i = i + j$

3. Local changes have non-local effects

単純な公理の組み合わせがどのように大きな変更になるのか, 例を示す
- PEGで未だに検討されていないループ最適化に関する課題を説明する

3.1 Loop-based code motion

(b) - (c): * の分配法則
(c) - (d): loop-induction-variable strength reduction

3.2 Resturcturing the CFG

3.3 Loop peeling

Loop peeling: ループ内の最初のイテレーションをループ前に配置する

(b) - (c): $pass_{1} (C) = ϕ (eval_{1} (C, Z), Z, S (pass_{1} (peel_{1} (C))))$
- $Z$ : 0-itのカウント値
- $S$ : カウントを増加させる関数 (i.e. S = \x.x+ 1)
- peel: pop_front する
(c) - (d):
- op(φ(A, B, C), D) = φ(A, op(B, D), op(C, D))
(d) - (e):
- eval(op(a_i...), Z) = op(eval(a_1, Z), ...)
- eval(θ(A, B), Z) = A
- eval(C, Z) = C, where C: const

お気持ち: 最初はindexアクセスの効率化だけ考えてループ, 分岐考慮しなくて良い?

3.4 Branch Hoisting

Branch Hoisting: 条件分岐をループの中から外に移動させる

cond がループ不変のときに使える
- 適用範囲狭そうなのでskip

3.5 Limitations of PEGs

高度なループ最適化については, Equality Saturation で処理できると考えられているが, まだ検討されていない

異なる入れ子レベルのループを1つのループに融合させる

は理想的には1重のループに出来る.

解決策
- ビルトインの公理を追加する
- ループアンローリング
  - PEGにいくつかルールを追加することでループアンローリングされた

Loop interchange

Loop interchange: for i in R1, for j in R2 -> for j in R2, for i in R1

これらの最適化には新しいopを追加しなければならず, 注意深く形式化する必要がある

現在のコストモデルではループの境界を考慮しないので正確な最適化が出来ない, これらはfuture work

4. Formalization of our approach

最適化の流れ

Saturation Engine

等価解析の集合 $A$ , $ir_{1} \to a ir_{2}$ : $a$ 等を使って, $ir_{2}$ に変換できる, 決定的である必要はない.

IRに半順序を定める

(ir_{1} \to a ir_{2}) \Rightarrow ir_{1} ⊑ ir_{2}

ir_{1} \to ir_{2} \Leftrightarrow^{\exists} \in A, (ir_{1} \to a ir_{2} \land ir_{1} \neq = ir_{2})

再帰的に無限に適用出来る公理
- A = (A + 1) - 1 は実行回数に制限をつけて停止性を保証

5. PEGs and E-PEGs

5.1 formalization of PEGs

$⟨ N, L, C ⟩$ , $N$ ノード, $L : N \to F$ ノードから semantic function の集合への semantic function

semantic function

5.3 Built-in Axioms

todo

6. Representing imperative code as PEGs

6.1 The SIMPLE programming language

6.2 Translating SIMPLE Programs to PEGs

6.3 Type-directed translation

6.4 Preservation of Semantics

7. Reverting a PEG to imperative code

7.1 CFG-like PEGs

7.2 Overview

7.3 Translating Loops

7.4 Translating Branches

7.5 Sequencing Operations and Statements

7.6 Loop Fusion

7.7 Branch Fusion

7.8 Hoisting Redundancies from Branches

7.9 Loop-invariant code motion

8. The peggy instantiation

8.1 Intermediate representation

8.2 Saturation Engine

8.3 Global profitabillity heuristic

nodeを使うかどうかを0-1で持っておく
s.t. 選択されたnodeが CFG-like PEG になるか

8.4 Eval and Pass

9. Evaluation

9.1 Time and space overhead

9.2 implementaing optimizations

9.3 translation validation

10. Related work

11. Conclusion and future work

Appendix A: Axioms

A.1 General-purpose axioms

Built-in E-PEG ops

$θ$ nodeに関する公理

$^{\exists} T = θ_{i} (A, T) \Leftrightarrow T = A$

Quartz 5

Explorer

Equality saturation a new approach to optimization