|
本研究では、百台規模のクラスタシステム上での実行に適した並列分散型の形式的設計検証アルゴリズムの研究を行い、以下の成果を得た。
1.二分決定グラフ(BDD)の並列処理:論理関数処理を進めていく過程で、動的に真理値を固定する変数を選択していくことによりBDDを分割して並列処理を行うアルゴリズムを提案し、このアルゴリズムにより並列度以上の高速化(スーパーリニア効果)が達成できることを示した。また、クラスタシステム上でこのアルゴリズムを実行することにより、1台の計算機上での逐次アルゴリズムではメモリ不足のために解くことが出来ないような問題でも、並列化により解くことが可能になった。
2.探索処理の並列アルゴリズム:設計検証で用いられる探索問題に対して、探索処理中に動的に部分問題に分割し、分割した部分問題を各マシンに動的に割り当てて並列に探索を行うアルゴリズムを提案し、最適順序付け問題でスーパーリニア効果を達成できることを示した。
3.並列システムの設計検証:多数の並行プロセスからなるシステムの検証に適した記号モデル検査アルゴリズムとデッドロックフリー性の検証手法を提案し、従来手法に比べて100倍以上高速化できることを示した。
4.並列ソーティングアルゴリズム:クラスタシステムで並列バイトニックソートの有効性を検証した。複数のスイッチングハブを用いたイーサーネットワークを使用したクラスタシステムでは、予想通りスイッチングハブ間の通信がボトルネックになることが判明した。一方で、VIA方式によるcLANのフルバンド幅構成のネットワークを採用することにより、このようなボトルネックを解消できることを示した。
|
