2008 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)
|
|---|
| Keywords | 並列分散処理 / クラスターコンピューティング / システム検証 / プロセス計算 / LMNtal / InTrigger |
|---|
| Research Abstract |
情報爆発を支える情報処理基盤は, かつてない規模で広くかつ大量に分散した情報資源を統合, 高度で適応的な協調処理と柔軟な資源の共有により, さまざまな状況に対応できる弾力性の高いものが必要になる. この実現には, 高度で複雑な機能を提供するソフトウェアを, 百万台以上の計算ノードやペタバイト以上の分散したデータ, それらを結合するネットワーク上に実現する必要があるが, 既存のソフトウェア構成技術にはこのためには不十分な点が多い. 本研究では, 新しい環境に適したソフトウェアの効率的構成のための新たなモデル, モデルを体現するプログラム言語などの記述体系や実装技術, それらの利用を容易化するツール群からなる, 高度にスケーラブルな情報基盤のためのソフトウェア基盤の基礎技術を確立する.
前年度までにシステムを構成する各モジュールの持つべき機能とインタフェースを明らかにする機能設計を中心に研究を進めてきたが、研究計画の第3年度にあたる平成20年度はさらにその設計を詳細化し、部分的には試作も進めた。
1 並列システム検証の要素技術の確立に向けて
充足可能性問題およびLTLモデル検査の並列実行方式の検討を継続した。充足可能性問題(SAT)ソルバについては並列SATソルバC-SATの開発と、既存のマルチスレッドSATソルバMiraXTの改良を行った。また、分散並列LTLモデル検査ツールDiVinEに対し、通信オーバーヘッドの増大を抑制する方式を提案・実装し、最大15\%弱の実行時間の削減を確認した。
2 スケーラブルな計算モデルとその検証への展開に向けて
従来から進めてきたLMNtalの高速軽量な処理系に対し整備改良を進めるとともに、ソフトウェア開発の上流から下流までを統一的に扱える高信頼ソフトウェアのための統合開発検証環境の構築を目指して、LMNtal統合開発環境LMNtalEditorを実装して公開した。また、型なしラムダ計算からLMNtalへの細粒度で非決定的なエンコーディング法を提案し、その理論的性質の検討を行った。
3 大規模分散システムを開発するための新たなプログラミング言語の設計
並行プロセス間の複雑なインタラクションを簡潔に記述し、かっモバイルコードの安全性を確保するため、プロセス計算をベースモデルに採用する一方で、実用的な分散システムの開発に用いる事ができるよう、プログラム記述のしやすさを考慮した高レベルの言語機能を備える言語を設計した。
4 動的で非均質な環境でスケーラブルな分散並列処理を行なうために必要な諸機能
基礎となるツール群を整備を継続して行った。具体的には、広域計算環境用のスケーラブルな高性能通信ライブラリ、ネットワークトポロジーを考慮した効率的なバンド幅推定手法、複雑なグリッド環境で柔軟なプログラミングを実現するフレームワークなどが主要な成果である。
|
