2020 Fiscal Year Research-status Report
Fusion of Meta-Scalable Theorem Prover and Parallel Model Checker to Realize Large-Scale Fast Formal Verification
| Project/Area Number |
19K11821
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
和崎 克己 信州大学, 学術研究院工学系, 教授 (70271492)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | 非同期並列システム / ハードウェアコンパイラ / 定理証明器 / モデル検査器 / 形式検証系 / 関数型言語系 / 状態空間生成 / ペトリネット |
|---|
| Outline of Annual Research Achievements |
検証対象とする回路の厳密プロパティ検査を目的とし，論理ゲート素子間の接続をメッセージパッシング型並列計算でモデル化する研究を継続している．定理証明は回路構造と接続の正当性に関するプロパティ検査に専念する．実規模での組合せ回路全体での振る舞い検証は，並列化モデルチェッカを用いて検証することになるが，スケーラブルでかつ繰り返し構造を有するPEの実例として，高速乗算回路の高基数コンプレッサモジュールについて実際に多ソート代数を理論的基盤とする定理証明を記述し，Mizarプルーフチェッカを用いた機械検証を行ったところ，回路合成の構造上の正しさならびに入出力関係の正しさなど所望のプロパティ検証に成功した．
関数型言語系の上のハードウェアコンパイラを機能拡張する目的のため，開発中の Melasy+ ハードウェアコンパイラを，分散環境向けに機能拡張する研究を実施した．具体的には，(a)上位設計としての対象回路の構成情報は，簡易な回路記述に文法を縮約した関数型プログラミング言語系(HDCaml)の上で記述し，系からのコンパイラ出力として，LOTOSコード生成器ならびにモデル検査が処理できる形式の回路構成，入出力関係列（XML中間表現）が自動的に得られるようにしたが，振る舞い解析のためのWhite BoxならびにBlack Box型のLOTOSライブラリ（OpenDill）を制作した．コード生成器によって下位設計（ペトリネットモデル）が得られ，状態空間生成器を用いて初期状態から駆動することで，全状態プロセスグラフを得るが，この解析器のメモリ効率化を図った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
関数型言語系の上のハードウェアコンパイラを機能拡張する目的のため，開発中の Melasy+ ハードウェアコンパイラを，分散環境向けに機能拡張する準備実装は継続しており，この課題に関する研究は順調に進捗している．また，上位設計としての対象回路の構成情報は，簡易な回路記述に文法を縮約した関数型プログラミング言語系の上で記述するが，LOTOSコード生成器は既にフランス INRIA/VASYからCADPツールの提供とライセンスを受けており，モデル検査が実際に実行できるまでの環境の構築は終わっており，この課題に関する研究は順著に進捗している．対象関数型言語系として，Objective Caml を使用し，XML中間表現に基づき，LOTOSコード生成器によって下位設計（ペトリネットモデル）が得られ，状態空間生成器を用いて初期状態から駆動することを試行していたが，LOTOSコード生成器の実装と機能については不充分な状態で，今後の進捗が待たれている．
|
| Strategy for Future Research Activity |
申請書の内容に基づき，プルーフチェッカとモデル検査器を並列化，メニーコア・クラスタ基盤へ実装する準備を進める．これは正当性（プロパティ）検証済の回路ライブラリを基礎とし，プルーフチェッカとモデル検査器を並列化し，メニーコア・クラスタ基盤へ実装するものである．システム統合のため，証明の分割・合成を行うためのシステム構築ならびにintel TBB並列化ライブラリを利用したプログラム開発を行う．具体的には，多数のPE群の動作検証のため，振る舞い状態空間を最適分割することで，メニーコアプロセッサ上での高スケーラブルな検証を，実サイズレベルまで強化する．この目標のため，まずクラスタ基盤管理ベースとして OpenFlow SWを使用する．高速なノード間接続のために，56Gb/s光高速ネットワークバス（InfiniBand）の導入も検討する．現有設備のスレーブノード ×16台を計算クラスタとして構成する．以上で構成されたクラスタ基盤上に，Mizarプルーフチェッカ・定理証明エンジンと，モデル検査器の実行プログラムを並列化コンパイラを用いて実装を進めていく.
ここまでの研究が順調に進捗した前提で，令和4年度は，並列化ライブラリを利用した総合的なプログラム開発に着手する．ここでは形式検証統合システムの並列化部分の性能向上を行う．具体的には，システム統合のため，状態空間の分割・合成を行うためのアルゴリズム開発と，並列化ライブラリを利用した総合的なプログラム開発を行う．性能評価対象は，パイプラインあるいはトーラス接続された超並列演算器（PE）とする．計算を多ソート代数でモデル化し，超並列接続のための制御器のモデルによって多数のPEをネットワーク・オートマタによって論理接続した構成とする．
|
| Causes of Carryover |
新型コロナウイルス感染症の影響により，2020年9月に予定されていた国内会議（情報処理学会FIT）がオンライン開催となり，出張等旅費が執行されなくなったため，次年度使用額がプラスとなった．
令和3年度の新型コロナウイルス感染症の影響は未だ見通せない状況ではあるが，対外発表の機会を捉えつつ，今回発生した次年度使用額は有効に執行を計画していきたい．
|
Research Products
(7 results)
