グリッドコンピューティング環境上のプルーフチェッカを用いた超並列演算器の設計検証

本年度(〜平成17年3月31日)の研究実施概要(1)「多ソート代数モデル」による並列演算器の計算モデルを作成した。高速演算性を実現するためのキャリー先見回路やモニタ回路が必要だが、ここでは自然数Nのオーダで計算モデルを作成し、プルーフチェッカで証明可能とした。一方、並列性実現のため「パイプライン機構」を説明する計算モデルとして、ペトリネット表現モデルを導入した。結果、ペトリネットによって分割・合成されたネットワーク・オートマタによりノードあたり証明問題サイズの縮小を図ることに成功した。(2)プルーフチェッカを、グリッドコンピューティング環境上へ実装した。グリッドネットワークとしてはGlobus、並列化ライブラリとしてMPICH-G2を使用した。高速なノード間接続のために、高速ネットワークを使用し、現有設備のノードPCに追加する形で、新規にXeon2.4GHz(dual)×6台を導入し計算クラスタとして構成した。並列・協調動作させるためのマスタサーバ用プロセッサをクラスタ上位に接続配置した(別途予算による)。システム全体として、証明の分割・合成を行うためのシステム構築ならびに並列化ライブラリを利用したプログラム開発を行った。(3)形式検証系に関する海外共同研究者(Canada, France)との合同調査研究を実施した。実施体制としては、(a)申請者:並列化システム構築とプログラム開発(b)Canada研究者:ネットワーク・オートマタによる問題分割の理論検討(c)France研究者:検証対象(超並列演算器)のLOTOS仕様モデル作成という構成をとった。

本年度(〜平成17年3月31日)の研究実施概要(1)「多ソート代数モデル」による並列演算器の計算モデルを作成した。高速演算性を実現するためのキャリー先見回路やモニタ回路が必要だが、ここでは自然数Nのオーダで計算モデルを作成し、プルーフチェッカで証明可能とした。一方、並列性実現のため「パイプライン機構」を説明する計算モデルとして、ペトリネット表現モデルを導入した。結果、ペトリネットによって分割・合成されたネットワーク・オートマタによりノードあたり証明問題サイズの縮小を図ることに成功した。(2)プルーフチェッカを、グリッドコンピューティング環境上へ実装した。グリッドネットワークとしてはGlobus、並列化ライブラリとしてMPICH-G2を使用した。高速なノード間接続のために、高速ネットワークを使用し、現有設備のノードPCに追加する形で、新規にXeon2.4GHz(dual)×6台を導入し計算クラスタとして構成した。並列・協調動作させるためのマスタサーバ用プロセッサをクラスタ上位に接続配置した(別途予算による)。システム全体として、証明の分割・合成を行うためのシステム構築ならびに並列化ライブラリを利用したプログラム開発を行った。(3)形式検証系に関する海外共同研究者(Canada, France)との合同調査研究を実施した。実施体制としては、(a)申請者:並列化システム構築とプログラム開発(b)Canada研究者:ネットワーク・オートマタによる問題分割の理論検討(c)France研究者:検証対象(超並列演算器)のLOTOS仕様モデル作成という構成をとった。