回路変換、ループフージョン、そして数学的帰納法による証明

サミュエル・カワード氏との共著：データパス回路の変換は、実質的にコンパイラ最適化とみなせるのか？

コルネル大学の訪問中に、サムは算術演算子を融合（フュージョン）するための一連のハードウェア最適化法則について提示した。コンパイラ分野のバックグラウンドを持つネイトからは、「これらをより伝統的なコンパイラの変換として捉えることはできるだろうか？」という問いが投げかけられた。

要約（TL;DR）： 答えは「イエス」ですが、その過程はかなり複雑で難しい側面があります。このブログ記事では、具体的な事例を通じてこの問いに対する答えを示します。具体例としては、ループ融合（コンパイラ最適化）の技術を用いて、キャリーセーブ加算（ハードウェア最適化）を発見することです。

キャリーセーブ加算について（サムによる解説）

3 つの n ビットのビットベクトルを合計する問題（$x + y + z$）を考えてください。2 つのビットベクトルの加法が可能なと仮定すると、最も単純な解決策は $x$ と $y$ を足してから、その結果に $z$ を足し算することです。ただし、2 つのビットベクトルを加算するたびに、不整合（キャリー）を最低位から最高位まで伝搬させる必要があります。不幸にも、この計算にかかる時間は、ビットベクトルの幅に対して少なくとも対数関数的に比例します。ハードウェアでは、はるかに高速に処理でき、$(x+y)$ の計算時間と同様の時間で $(x+y+z)$ を算出できます。さらにわずかな定数のオーバーヘッドさえ追加すればよいだけです。これを達成するためには、3 つの同価値の個々のビット（$x[i], y[i], z[i]$）を入力とし、2 ビット $s$ と $c$ を出力する全加算器（full-adder）を使用します。ここで $s$ と $c$ は以下の関係にあります： $$2c + s = x[i] + y[i] + z[i]$$

ゲートレベルでの定義は以下の通りです：

• $c = \text{MAJ}(x[i], y[i], z[i])$ $= (x[i] \land y[i]) \oplus (x[i] \land z[i]) \oplus (y[i] \land z[i])$ （※ MAJ は多数決演算子）
• $s = x[i] \oplus y[i] \oplus z[i]$

この全加算器を $n$ 個用意し、同価値のビットに対して並列に動作させることで、3 つの入力値を 2 つに統合（リダクション）できます。以下がその例です：

1010 (x)  = 10
1011 (y)  = 11
+0011 (z) = 3
----------
0010      = 2   （ここでキャリーが発生）
+10110    = 22  （残りの加算結果）
----------
11000     = 24  （最終結果）

まず、局所的な情報のみを確認するため定数時間で 3 つの値を 2 つに減少させる処理を行います。これは完全な加法全体を実行するよりもはるかに高速です。もちろん、2 つのビットベクトルを一度だけ加算するための時間コストを支払う必要がありますが、これを逐次的に 2 回行うことよりはるかに効率的です。この技術は「キャリーセーブ加算」と呼ばれ、任意数の被加数へと一般化できます。

ループ融合について（ネイトによる解説）

ここでは、後ほどキャリーセーブ加算を「再発見」するために利用するコンパイラ概念であるループ融合（loop fusion）について簡単に説明します。以下の例には 2 つのループが含まれています：

# ループ 1: 各要素を二乗
for i in range(n):
    a[i] = a[i] * a[i]

# ループ 2: 各要素に 1 を足す
for i in range(n):
    a[i] = a[i] + 1

コンパイラにおける古典的な最適化の一つが、これら 2 つのループを融合させることです。これにより、配列 $a$ を 1 回しか反復処理しなくても済みます：

for i in range(n):
    a[i] = a[i] * a[i] + 1

これは効率的であり、プログラム内でループの実行回数を減らすだけでなく、操作を融合させることでロード／ストア命令の削減も実現できます。ネイトの問いは、「ループ融合というレンズを通してキャリーセーブ加算を発見できるだろうか？」というものでした。

課題（The Challenge）

以下のプログラム断片を考えてください。これは、3 つのブール値からなる配列 $x$, $y$, および $z$ を受け取り、ブール値からなる配列 $s$（$= x + y + z$）を出力します：

# (x+y) を実行し、結果を w に保存
a[0] = 0
for i in range(n):
    w[i], a[i+1] = FullAdd(x[i], y[i], a[i])

# (w+z) を実行し、結果を s に保存
b[0] = 0
for i in range(n):
    s[i], b[i+1] = FullAdd(w[i], z[i], b[i])

このプログラムは、2 つの独立した加法を逐次的に実行して、3 つのビットベクトル入力同士を加算していることが容易に分かるでしょう。私たちは、各全加算器（

FullAdd

）がそのキャリーを次の全加算器に渡すシーケンスとしてビットベクトルの加算を実装しています。ここで的问题是：ループ融合を適用すると何が起きるのでしょうか？

a[0] = 0
b[0] = 0
for i in range(n):
    w[i], a[i+1] = FullAdd(x[i], y[i], a[i])
    s[i], b[i+1] = FullAdd(w[i], z[i], b[i])

これにそれほど大きな違いはありません（ただし、逐次的に実行することでメモリ使用量を節約できるかもしれません）。しかし、キャリーセーブのトリックを用いた加算器の融合バージョンを考えてみてください：

c[0] = 0
d[0] = 0
for i in range(n):
    w*[i], c[i+1] = FullAdd(x[i], y[i], z[i])
    s*[i], d[i+1] = FullAdd(w*[i], c[i], d[i])

上記の 2 つのプログラムは少なくとも非常に似ているように見えますね。それらは同じ最終的な出力を生み出すのでしょうか（$s = s*$ か？）です。キャリーセーブのトリックに関する大局的な解析（グローバル分析）から、両者が一致することは分かっていますが、局所的な証明が存在するでしょうか？つまり、ビットベクトルとしての $s$ と $s*$ の実際の意味に依存せずに、単に値を操作することでこれら 2 つのプログラムの同値性を示すことはできるのでしょうか。答えは「イエス」です。以下ではその証明を行います。

証明（興味がない方はスキップしてください）

ビットレベルでの分析を行っていきましょう。すべての解析を $\mathbb{F}_2$（体または有限体）で行います（そのため、XOR が足算、AND が掛算とみなせます）。なお、$\text{MAJ}(x, y, z) = xy + yz + xz$ となります（通常は＋が OR の意味で定義されますが、ここで XOR を使用しても同様に機能します）。

最初のプログラムから： $$s[i] = w[i] + z[i] + b[i]$$ $$= x[i] + y[i] + a[i] + z[i] + b[i]$$

第二のプログラムから： $$s*[i] = w*[i] + c[i] + d[i]$$ $$= x[i] + y[i] + z[i] + c[i] + d[i]$$

したがって、$a[i] + b[i] = c[i] + d[i]$ ならば、これらの $s$ と $s*$ の値は同値であることが分かります。私たちは帰納法によってこれを証明します。基本ケース $a[0] + b[0] = c[0] + d[0]$ は真であり、これは $a[0] = b[0] = c[0] = d[0] = 0$ よりも明らかです。帰納のステップについては $a[i] + b[i] = c[i] + d[i]$ を仮定します。

ステップ 1: $a[i+1] + b[i+1] = c[i+1] + \text{MAJ}(x[i] + y[i] + z[i], a[i], b[i])$ の検証

簡略化のため、索引 $[i]$ を省略して以下のように書きます： $$= \text{MAJ}(x, y, a) + \text{MAJ}(x + y + a, z, b)$$ $$= xy + ya + xa + (x + y + a)z + zb + (x + y + a)b$$ $$= xy + ya + xa + xz + yz + az + zb + xb + yb + ab$$ $$= xy + xz + yz + (x + y + z)a + (x + y + z)b + ab$$ $$= \text{MAJ}(x, y, z) + \text{MAJ}(x + y + z, a, b)$$ $$= c[i+1] + \text{MAJ}(x + y + z, a, b)$$

ここで、$d[i+1] = \text{MAJ}(x[i] + y[i] + z[i], a[i], b[i])$ であることを示す必要があります。これは、帰納法によって $a[i]b[i] = c[i]d[i]$ を証明することで容易に示されます（帰納の仮説を強化する）。

ステップ 2: $ab=cd$ を仮定し、$d[i+1] = \text{MAJ}(x + y + z, a, b)$ が成り立つことを示す： $$\text{MAJ}(x + y + z, a, b) = (x + y + z)a + ab + (x + y + z)b$$ $$= (x + y + z)(a + b) + ab$$ $$= (x + y + z)(c + d) + cd$$ $$= (x + y + z)c + (x + y + z)d + cd$$ $$= \text{MAJ}(x + y + z, c, d)$$ $$= \text{MAJ}(w*, c, d)$$ $$= d[i+1]$$

最後に、$a[i]b[i] = c[i]d[i]$ を帰納法によって証明します。基本ケースは自明です。しかし、帰納のステップは少し複雑になります（面倒な作業が必要）。

ステップ 3: $ab=cd$ を仮定し、$a[i+1]b[i+1] = c[i+1]d[i+1]$ が成り立つことを示す $$a[i+1]b[i+1] = \text{MAJ}(x, y, a)\text{MAJ}(w, z, b)$$ $$= (xy + ya + xa)(wz + zb + wb)$$ $$= xyzw + xyzb + xywb + yzwa + yzab + ywab + xzwa + xzab + xwab$$

ここで $w$ をすべての項に展開する必要があり、項数は多くなります。これを簡略化するために、式において $w$ が出現する各用語では、その成分 ${x, y, a}$ のうちちょうど 2 つが同時に現れることに注目してください（例：$xyzw = xyzx + xyzy + xyza$）。この中で既に現れている成分を用いる 2 つの項は等価であり（$xx=x$, $yy=y$ より）、相互に相殺（キャンセル）されます。つまり、実質的に $w$ は、その式の中にすでに出現していない成分の一つに置換されるだけです： $$= xyza + xyzb + xyab + xyza + yzab + xyab + xyza + xzab + xyab$$ $$= xyzb + yzab + xyab + xyza + xzab$$ $$= xyz(a + b) + ab(xy + yz + xz)$$ $$= xyz(c + d) + cd(xy + yz + xz)$$

これは比較的シンプルに見えます。次に $c[i+1]d[i+1]$ に関心を持ちましょう： $$c[i+1]d[i+1] = \text{MAJ}(x, y, z)\text{MAJ}(x + y + z, c, d)$$ $$= (xy + yz + xz)(xc + yc + zc + cd + xd + yd + zd)$$ $$= (xyzc + xycd + xyzd) + (xyzc + yzcd + xyzd) + (xyzc + xzcd + xyzd)$$ このステップでは、個々の部分表現内で即時に相殺されるものを省略しましたが、それらの間にもさらに相殺可能な項があります： $$= xyzc + xyzd + xycd + yzcd + xzcd$$ $$= xyz(c + d) + cd(xy + yz + xz) = a[i+1]b[i+1]$$

この証明は少々複雑（gnarly）ですが、少なくとも原理的には私たちが示そうとしたことを意味します：ループ融合を実行し、さらにこの種の帰納的論理に基づいてループ本体を書き換えることのできるコンパイラは、自動的にキャリーセーブ加算器を発見できるのです。

結論

明らかに、キャリーセーブのトリックを再発見する必要はありません。なぜなら、私たちはそれを知っているからです。むしろ、他の同様のトリックも同様に発見できると期待されています。ハードウェアの世界では、オペレーターレベルの最適化ライブラリを構築したり、アンロールされた回路向けのビットレベルの最適化ライブラリを構築したりするのは簡単です。一方、コンパイラの最適化は中間領域（ミドル）で動作しており、プログラムに内在する規則性（レギュラリティ）を活用することで、アンロールせずに局所的な変換からグローバルな最適化を構築しなければなりません。ハードウェアにも規則性は存在し、私たちはこれを利用すべきでしょう。そうすれば、2 つの最適化選択肢（完全なハードウェア設計か、完全にアンロールされた回路か）で困ることはなくなるはずです。