研究上の成果
本年度の研究では、(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処理系の最適化への応用を検討する中で、ジェネリッ クオブジェクトの効率改善のためにどのような種類の解析が必要であるかがわか り、どの程度の効率改善効果があるかを定量的に示せたことも、意義があったと 考える。