変数の生存区間解析のためのSATソルバを用いた型推論アルゴリズム Export

@inproceedings{citeulike:4275276, abstract = {コード最適化問題の一つであるレジスタ割付け問題において最適な割付けを実現するためには，レジスタを変数そのものに割付けるのではなく，変数が生きている（live である）範囲に対して割付ける必要がある．変数の生存区間の概念は，この目的のために提案された抽象的な概念であり，直感的には，変数の定義集合の特定の部分集合が有効であるプログラムポイントの集合に対応する．しかし従来の枠組みでは，生存期間の概念は，プログラムのフローグラフから生存区間を計算するグラフ論的な手続きの記述として定義されている．このため，生存区間解析の性質等がやや見通しの悪いものとなっている． 本論文では，生存区間解析のより宣言的な方式の確立を目指し，まず，変数の生存区間を表現する静的な型システムを定義する．この型システムでは，変数の型は，プログラム中の変数定義の部分集合であり，型推論規則は，変数の定義の到達可能性に関する推論規則を表現する．次に，プログラムが型をもつ制約条件を推論するアルゴリズムを構築する．各変数の生存区間は，制約を満たす最小解に対応する．型推論で計算する制約は論理式の制約で表現され，その最小解は，SAT の最適化問題であるMIN-ONE を解くOptSAT アルゴリズムを用いて解かれる．本論文で提案した方式は，実装済である．}, author = {山本, 雅洋 and 大堀}, citeulike-article-id = {4275276}, keywords = {sat}, posted-at = {2009-07-29 03:23:24}, priority = {2}, title = {変数の生存区間解析のためのSATソルバを用いた型推論アルゴリズム} }

TY - CONF ID - citeulike:4275276 L3 - citeulike-article-id:4275276 N2 - コード最適化問題の一つであるレジスタ割付け問題において最適な割付けを実現するためには，レジスタを変数そのものに割付けるのではなく，変数が生きている（live である）範囲に対して割付ける必要がある．変数の生存区間の概念は，この目的のために提案された抽象的な概念であり，直感的には，変数の定義集合の特定の部分集合が有効であるプログラムポイントの集合に対応する．しかし従来の枠組みでは，生存期間の概念は，プログラムのフローグラフから生存区間を計算するグラフ論的な手続きの記述として定義されている．このため，生存区間解析の性質等がやや見通しの悪いものとなっている． 本論文では，生存区間解析のより宣言的な方式の確立を目指し，まず，変数の生存区間を表現する静的な型システムを定義する．この型システムでは，変数の型は，プログラム中の変数定義の部分集合であり，型推論規則は，変数の定義の到達可能性に関する推論規則を表現する．次に，プログラムが型をもつ制約条件を推論するアルゴリズムを構築する．各変数の生存区間は，制約を満たす最小解に対応する．型推論で計算する制約は論理式の制約で表現され，その最小解は，SAT の最適化問題であるMIN-ONE を解くOptSAT アルゴリズムを用いて解かれる．本論文で提案した方式は，実装済である． TI - 変数の生存区間解析のためのSATソルバを用いた型推論アルゴリズム KW - sat AU - 山本, 雅洋 AU - 大堀 ER -