2009 Fiscal Year Annual Research Report
情報爆発に対応する高度にスケーラブルなソフトウェア構成基盤
| Project Area | Cyber Infrastructure for the Information-explosion Era |
|---|
| Project/Area Number |
18049015
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
近山 隆 The University of Tokyo, 大学院・工学系研究科, 教授 (40272380)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
湯淺 太一 京都大学, 情報学研究科, 教授 (60158326)
上田 和紀 早稲田大学, 理工学術院, 教授 (10257206)
|
|---|
| Keywords | 並列分散処理 / クラスターコンピューティング / システム検証 / プロセス計算 / LMNtal / InTrigger |
|---|
| Research Abstract |
前年度までの成果を受けて、設計を確認するための試作を通じた機能と性能の確認を行った。
○並列システム検証の要素技術の確立に向けての技術開発を進めた。
・LMNtal処理系を最適化し、モデル検査器で状態数の多いプログラムを扱えるようにした。また統合開発環境を増強、階層や非連結性を含むグラフに対しても適切な状態可視化機能を提供した。
・検証システムの基礎として、前年度から開発を進めていたクラスタ環境向け並列SATソルバc-satの整備と性能評価を進め、31PE規模のクラスタ上で23倍以上の性能向上が得られることを実証した。
・モデル検査器については、状態空間分割方法、通信頻度、マルチコアCPUでの使用コア数などのチューニングによって、128PEを通常設定で実行した場合と比べて、最大2.4倍の速度向上を得た。
○実時間性の高いごみ集め(GC)アルゴリズムの正当性の検証のために、抽象モデル検査手法を適用、定理証明(支援)系を使用して実モデルと抽象モデルの整合性を厳密に証明した。
○大規模分散処理の記述体系のひとつとして、分散共有メモリインタフェースDMIを設計・実装した。DMIはpthread型のプログラミングスタイルを採用しながら、大規模分散システムでは必須な動的参加・脱退を許す。このためのコンシステンシプロトコルを設計・実装、同期粒度指定を可能にしてかなり大規模な分散環境においてもメッセージパッシング型プログラミングに近い性能を実現した。
○動的で非均質な環境でスケーラブルな分散並列処理のための基礎ツール群の整備を継続して行った。代表的成果のひとつとして、広域大規模分散環境に向いた分散デッドロックフリーなオーバレイネットワークのルーチング方式を最適化設計・実装し、高い性能を検証したことがある。
|
