compiler
Isabelle

コンパイラの理論における Dominators に関する定理の証明

More than 1 year has passed since last update.

コンパイラの理論で dominators という概念が出てきます.日本語だと支配節でしょうか.ソースプログラムから生成した基本ブロックをノードとするフローグラフに関する概念です.

初期ノード 0 からあるノード n に至るすべてのパスがノード d を通るならば,ノード d は n の dominator であるといいます.

例えば下図のようなフローグラフを考えると,ノード 5 の dominator は 0, 1, 2, 5 です.5 自身も dominator と考えます.

3 や 4 は 5 の dominator ではありません.それらを通らずに 5 にたどり着くパスがあるからです.

flowgraph.png

この概念はデータフロー解析やループ最適化,SSA (Static Single Assignment) への変換などで役に立ちます.

コンパイラのテキスト Modern Compiler Implementation in ML では,この dominators および関連するノードとノードの集合を計算するために,定義を"再帰化"あるいは"差分化"したという感じの式が出てきます.これらを Isabelle を使って形式的に証明してみました.

証明した主要な定理は次の2つです:

  • Dominators D[n] を計算する際に使用する定理 (テキスト p.407)
D[s_0] = \{s_0\}, \quad
D[n] = \{n\} \cup \left( \bigcap_{p \in \mathrm{pred}[n]} D[p] \right) \quad \mathrm{for}\  n \ne s_0
  • Dominance Frontier DF[n] を計算する際に使用する定理 (テキスト p.434)
\mathit{DF}[n] = \mathit{DF}_\mathrm{local}[n] \cup
 \bigcup_{c \in \mathrm{children}[n]} \mathit{DF}_\mathrm{up}[c]