研究上の成果
本年度の研究では、(1) モードづけできないプログラムの解析手法、(2) モー ド体系の拡張、(3)モード解析の最適化への応用、に関してそれぞれ成果が得 られた。以下、順に紹介する。
モードづけできないプログラムの解析
これまで、モードづけ可能(well-moded)なプログラムについては、効率的な解 析アルゴリズムが確立していたが、モードづけできない(ill-moded)プログラ ムに対して、モード誤りの原因を効率良く特定する方法は確立していなかった。 モードづけできないとは、モード制約の論理積が全体として矛盾するというこ とであるが、そのことを指摘しただけでは、大きなプログラムのデバッグには ほとんど役に立たない。
そこで、全体として矛盾している制約集合の中から、矛盾する極小の部分集合 を効率よく見つけ出すアルゴリズムを開発し、それに基づき、矛盾する制約を を課したプログラム中の記号(または記号出現)を提示する方式を開発した。こ れによって、誤りの可能性のある箇所をかなり絞り込んで提示することが可能 になった。極小集合は、プログラムの大きさと極小集合の大きさとにほぼ比例 する手間で探索できる。
さらに、互いに共通部分を持たない複数の極小部分集合を見つけ出すことで、 複数の誤りが一回の解析で検出できることもわかった。
実験によれば、極小集合の大きさは、プログラムの大きさによらない小さな定 数で抑えることができる。したがって、プログラム解析は、プログラムの大き さと誤りの数とに比例する手間で実行できる。大規模なプログラムの場合には、 プログラムの層化構造にしたがった解析により、探索空間を狭めることができ、 また、より直観的な説明を得ることができる。
モード体系の拡張---モード多相の導入
上で述べたプログラムの層化が、モード多相(mode polymorphism)の導入にも 基本的な役割を果たすことが判明した。
ストリーム併合器をはじめとする汎用性の高い述語は、一つのプログラムの中 で、いろいろなモードで使われうる。本研究におけるモード多相の基本的な考 え方は、プログラム中の述語を、呼出し関係にしたがって層化し、上の層のプ ログラムが下の層のプログラムを呼び出す場合に、呼出し箇所ごとに異なるモー ドで使うことを許すというものである。
この拡張によって、モード体系の実用性は大幅に高まるものと期待できる。特 に、モード体系の下でのプログラムライブラリ構築にとっては、本質的に重要 な拡張と言える。
モード解析の最適化への応用
KLICシステムのジェネリックオブジェクトは、処理系の実装や拡張を容易にす ることに貢献しているが、一方で、間接語を用いることによる空間的オーバー ヘッドや、演算のたびにメソッド表引きを行なうことによる時間的オーバーヘッ ドが問題となることがある。
そこで、ジェネリックオブジェクトの一種であるデータオブジェクトを対象と して、オーバーヘッド除去のためにはどのような解析が必要かを検討し、それ に基づく最適化実験を行なった。実験は、浮動小数点型およびベクタ型のデー タオブジェクトを対象とした。
モード、型、参照数の3種類の基本情報を制約ベースの解析で得たのち、それ らの情報に基づいて具体化状態に関する解析を行なうことにより、ジェネリッ クオブジェクト実装のオーバーヘッドをほぼ除去できることが判明した。
解析系および最適化コンパイラは完成していないが、ハンドコンパイルによる 実験の結果、典型的な浮動小数点演算については現行KLIC処理系の13倍以上、 ベクタの更新演算については、in-place updateが可能なことが参照数解析に よってわかる場合、現行の3.5倍以上の性能向上が得られることがわかった。
ソフトウェアとしての成果
静的解析ツールklint第1版は、KL1プログラムのモード解析を行なって、その 結果を出力する。すべてKL1で記述されている。Flat GHCにないKL1特有の機能 のうち、モジュール化やマクロ展開などには対応しているが、研究の内容で述べたすべての機能には、 まだ対応していない。
klintシステムは、大きく分けて、モード制約生成系およびモード制約充足系 からなる。
モード制約生成系は、次の4サブモジュールからなる。制約生成は、1.→ 2.→ 3.→ 4. の順に流れ作業的に進む。
モード制約充足系は、大きく分けて次の4つの機能からなっている。
このモード制約充足系の最大の特徴は、モードグラフの単一化問題として定式 化されたモード制約充足問題を、プロセス構造の単一化として実現した点であ り、それ自身が、モード体系下でのKL1による動的プロセス構造の記述能力の 検証に役立っている。
klintシステムの機能は、すでに、モード制約充足系自身(190個の節からなり、 2464個のモード制約を課する)の解析に適用可能なレベルに達している。
unaryまたはbinaryなモード制約は、単一化問題として解くことができるが、 そうでないモード制約は、直接的に効率良く解くことはできない。そこで、そ れらの制約の評価を遅延させ、他の制約から得られる情報を用いて簡約化する 機能を実装した。
モード制約充足系自身の解析例では、42個のbinaryでないモード制約はすべて、 他の制約によって、binaryまたはunaryの制約に簡約化され、遅延方式が実用 上十分強力であることが判明した。
また、モード解析系の自己適用によって、大きなプログラムのモードグラフの 形状の特徴をつかむことができ、今後のklintシステムの効率改善のための指 針を得ることができた。
残された課題
本年度は、klintのモード解析機能、およびモードづけできないプログラムの 解析機能の基本的枠組を確立することを最優先に行なってきた。これによって、 KL1プログラムのうち、KL1のベースとなっているFlat GHCの文法に本質的にし たがっているプログラムについては、ほぼ問題なく解析ができるようになった。
だが、KL1がFlat GHCから拡張した機能に個別に対応することは、今後の課題 として残されている。この対応作業の多くは、klintに対するアドホックな拡 張作業となることが予想され、必要性の高いものから着手してゆくのが現実的 である。また、モードづけできないプログラムに対して、その原因をより綿密 に解析する機能も重要であり、その方式の確立と実装も今後の課題である。
上記２つの成果についての自己評価
理論面においては、モードづけできないプログラムに対して、誤りの箇所を効 率よく診断できるアルゴリズムが確立し、その実用化への見通しが立てられた ことが、静的デバッガ実用化の上で大きな成果であったと言える。
また実践面では、作成したモード解析プログラム自身を含む、かなり大きなプ ログラムの解析に成功し、モードから見たプログラムの性質が分析できるよう になったことも、重要な成果といえる。
さらに、モード解析のKLIC処理系の最適化への応用を検討する中で、ジェネリッ クオブジェクトの効率改善のためにどのような種類の解析が必要であるかがわ かり、どの程度の効率改善効果があるかを定量的に示せたことも、意義があっ たと考える。