学部3年生研究室説明会向け
研究テーマ紹介（和崎）

概要

1. 非同期並列システムのモデルと検証

2. 定理証明系による検証系の補強

3. 上位記述とハードウェアコンパイラ

4. MPI/PCクラスタによる各種アプリケーションの実装

指導方針

参考資料・リンク集

■質問・相談はこちらへどうぞ

2009年12月17日 12:02 更新

●概要

情報システムにおける「セキュリティ（security）」に関しては、暗号化通信・ファイルシステムに代表される「安全性（safety）」とともに、システムの信頼性・堅牢性（Reliability）の確保が大変重要である。非同期に動作する通信プロトコルやハードウェアなど、並列システムの設計とその動作検証は一般に難しく、モデル化・設計・検証の能力を向上させる必要がある。

私が指導可能な分野は「数理情報工学」であり、私は、特に、並列システムモデル（concurrent system models）とそのモデル化手法（ネット指向設計、プロセス代数仕様設計、等）、ならびにその形式検証系（定理証明系、モデル検査系）、更にMPI/PCクラスタ型計算機を用いた各種アプリケーション開発などに興味があり、現在の研究活動範囲としている。

現在のところ実施中ならびに今後指導を予定しているテーマとしては、大別して以下の４つが挙げられる。

[A] 非同期並列システムのモデルと検証
[B] 定理証明系による検証系の補強
[C] 上位記述とハードウェアコンパイラ
[D] MPI/PCクラスタによる各種アプリケーションの実装

●非同期並列システムのモデルと検証

非同期チャネルで相互に結合され、並行動作するプロセスを、仕様に基づいて記述し、その動作検証を行うことは重要である。
プロセスのモデルには、以下のような手法がある。

(1) セルオートマトン（cellular automaton, network automata）
(2) ペトリネット（Petri net）
(3) プロセス代数仕様（BLA : Basic-LOTOS oriented Algebra, CCS, CSP）

(1) セルオートマトン

セルオートマトンとは、一つの（有限）状態遷移機械（automata）を「セル（cell）」とし、それをn個定義したものである。次に、n個のcell_i(i=1,...,n)を協調・同期動作させるための、同期化ラベル積（Synchronized product）を定義する。通常のautomataについての相互関係を拡張するだけなので、classicな同期型順序回路から出発したボトムアップ設計で使われてきたモデル化手法である。ハードウェア上への並列プロセッサ要素(PE)の、繰り返し構造を有するような実装は容易（図1,図2）であるが、設計時の同期化ラベル積の扱いは難しく、記述性が低い。
→もっと詳しく


図1 セル型FIFOモデルの各FSM	図2 セル型FIFOモデルの1次元順次接続図

(2) ペトリネット

ペトリネットは、並行動作する離散事象システムのモデル化手法の一つである。システム資源を表す「プレース」、システムの生成する事象を表す「トランジション」、資源と事象との間の関係を結ぶ「アーク」、ならびにシステム内のデータフローを表現し駆動するための「マーク」から構成される数学モデルである。簡単なネット構造のため、構造的あるいは動的な、様々な性質について解析性が高い。また、各要素を結んだネット図は、視覚的にもシステムの「振る舞い」を理解するための助けになる（図3）。
→もっと詳しく

自動販売機のペトリネットモデル

図3 自動販売機のモデル（FC-PNクラス：在庫数=4）

しかしながら階層型ネット構造はシステム内のインスタンス（実体）が増加すると記述性が低下する。また、data typing（データ型）に関する概念や操作がない。時間付き階層型ペトリネットを設計・解析・シミュレーション実行するための環境として、HiPSと呼ぶ統合環境を開発している（図4）。開発言語はC#を使用している。時間付きマーキングの機能を、論理ゲート素子の遅延要素として適用し、新たなゲートの振る舞いモデルを定義し、階層化することで複雑な組み合わせ論理回路を構成した。

図4 ペトリネット統合設計・解析・シミュレーション環境：HiPS

(3) プロセス代数による合成手法

プロセス代数手法は、システムをプロセス（process）の群としてとらえ、相互のメッセージ通信を用いて同期化して全体を構成する方法がある。プロセスとは、動作（action）の列のことである。動作によって、メッセージを送ったり、受け取ったりする。各プロセスの定義は、プロセス代数仕様（Basic-LOTOS oriented Algebra(BLA)）を用いる。BLAにACT-ONEと呼ぶ抽象データ型（abstract data typing）の拡張を行ったものが、(Full-)LOTOSである。LOTOSの言語仕様は、ISO8807として国際標準となっている（図5）。LOTOSの process algebraic part は、
・CCS : Milner's Calculus of Communicating Systems
・CSP : Hoare's Communicating Sequential Processes
に基づいている。並列抽象機械、メッセージ通信によるプロセス定義、についての詳しい知識を欲する場合、これをぜひ読んでおこう。
→もっと詳しく

図5 LOTOSにおけるプロセス定義と並列合成の記述例
（Bolognesi,T. and Brinksma,E.,"Introduction to the ISO Specification Language LOTOS", Jan.1987より転載）

プロセス代数でモデル化したシステムは、その振る舞い（behaviour）をトレースしたグラフ、つまりLTS（Labelled Transition System）を生成する。このLTSについて種々の性質の検証を行う。この手法のことをモデルチェッキング（model checking）と呼ぶ。先述のセルオートマトンを出発点とし、そのトレースグラフを Kripke構造＜状態値、遷移関数、atomic propositionの組＞によって生成する場合もある。プロセス代数設計を出発点とした場合、LTS構造＜状態値、アーク、ラベル付きトランジションの組＞によって生成される。検証したい諸性質（例えば、BUS arbiterの場合で、同時に2つ以上のノードにバス獲得権をアサートしない、など）は、modalな時相論理系（μ-calculas、CTL（computational tree logic）、ACTLなど）で記述する。ターゲットとなるLTSの状態空間について、性質を記述した時相論理式が満たすか否かを探索する操作（グラフ走査アルゴリズム）が重要である。また、予め状態空間を種々のグラフ縮小手法をもちいてサイズを小さくしたり（state space reduction）、あるいは先のLTS生成と同時に、時相論理式が満たすか否かを同時にチェックする手法（on-the-fly model checking）も重要である。LOTOSからのLTS生成、グラフ縮約、デッドロック解析、時相論理を用いたモデル検査器については、INRIA/VASY研究所（France）で開発中のCADP toolboxを利用して研究を行っている（図6）。
→もっと詳しく

図6 LOTOS統合設計・検証環境：CADP toolbox (xeuca GUIのスクリーンショット）

★キーワード
・セルオートマトン、ペトリネット、プロセス代数仕様
・非同期並列システム、behaviour-based system verification
・LTS generation、状態空間探査、グラフ縮小
・時相論理系
・モデルチェッキング、システム形式検証系
・exhaustive or on-the-fly model checking ★このテーマに関する参考資料

[1] 参考資料・リンク集：並行プロセスのモデル化と検証＆プロセス代数設計（LOTOS）
[2] Protocol Verification by using LOTOS and Tools (part 1)
[3] Communicating Sequential Processes C.A.R. Hoare, Prentice-Hall, 1985.
[4] CADP toolbox : A Software Engineering Toolbox for Protocols and Distributed Systems
[5] NuSMV model checker : A new symbolic model checker (open sources)

●定理証明系による検証系の補強

並行プロセスのモデル化と検証で使用する、各種モデル検証系は、システムの「振る舞い」の検査を対象としたもの（behaviour-based system verification）である。したがって、観測可能なプロセス内のアクションの列（言い換えれば、ソフトウェアの各種プロシージャ、ハードウェアの各信号線の状態、など）の時系列における性質が検証可能、ということである。これの検証系が、生成したLTS状態空間の探査アルゴリズムを実装した検証系に他ならない。

しかしながら、このモデルチェッキング検証系は、その内部の演算機構や、あるいはそのデータ型における演算・操作が「正しく行われているか否か」の検証は行わない。なぜならば、生成したLTSにおいて、たとえばFull-LOTOSで記述した抽象データ型は、単なるシンボル（例：!val1, !val2, ... など）としか見做されておらず、そのデータが順序であるならば値の比較は行われるにせよ、演算（例：加算、乗算、除算、剰余など）の結果が正しいか、そのデータ型の内部で閉じているか否かの検証は行わない。更に付け加えると、加算の演算操作シンボルは"＋"であって、アクション列のひとつとして「加算」という振る舞いが行われることを保証している。つまり、その"＋"が最終に実装されたシステム上で、「どのように実装されているのか」あるいは「正しく加算を行うのか」という保証は得られないのである。

上記の理由により、モデルチェッキング検証における系の補強の方策として、各種演算を対象とした操作の正当性の検証を別の形式化数学検証系にてチェックしたい、というのがこの課題である。具体的には、Mizar proof checkerを使用して、

・各種演算（加算、減算、乗算、剰余など）のハードウェアを想定した実装（論理演算回路）の正当性検証（図7～図9）
・グラフ縮小の各種手法（Ordered-BDD、partial order/bisimulation/observational reduction）などのアルゴリズム検証
・write-once, non-overwritingな計算機モデルと、Pursuit-possibilityを有するプロセス代数→LTS生成のframeworkとの関連

などを行う。
→もっと詳しく

図7 冗長2進並列加算回路の構造（シンボル○：汎化加算器）

図8 数学構造（多ソート代数）に基づいて回路構造と合成を定義し、動作の正当性と安定性に関する諸定理を記述

図9 定理証明系向け形式化記述言語（Mizar）によって、厳密証明を書いた後、プルーフチェックを行う

★キーワード
・形式検証（Formal Verification）
・description-based verification　例：Mizar、HOLなど
・automated reasoning-based verification 例：Model Checkingなど
・問題の抽象化、自然数オーダでのモデル検証
・BDD、LTS、時相論理仕様記述

★このテーマに関する参考資料

[1] 参考資料・リンク集：形式化数学検証系（MIZAR）
[2] Mizar : proof ckecking system
[3] HOL : interactive theorem proving in a higher-order logic

●上位記述・ハードウェアコンパイラ

ハードウェア設計において、関数型言語ならびにC++を台言語とした、HDLの上位言語を定義し、コンパイラを作成している。コンパイラの生成コードとしては、Verilog-HDL, VHDL, .C ならびにモデルチェッキング検証系向けコード(NuSMV)などを想定している。

上位言語で一旦仕様を書いたあとは、用途に応じたコード生成を、元の仕様の書き換え無しに得ることが可能となる。また、仕様にシステム要求を（何らかの時相論理式を用いて）併記しておくことで、システムの動作と満たすべき要求仕様を、ひとつの上位言語上で閉じることが可能となる。

現在、モデル検査に対応する上位ハードウェア記述言語”Melasy”の設計と実装について研究を実施している。

機能設計後，高級言語で対象システムを実装し，コード生成によって対象システム向けのオブジェクトや実行可能モジュールを得るための，コンパイラが開発されている．ハードウェアの設計を記述するための比較的高度な言語によって書かれたコードから，直接，回路の構成情報を生成するコンパイラ（ハードウェアコンパイラ）が開発され，業界標準として使われている．

ハードウェア設計の正当性を形式的にチェックするツールとしては，SMV,NuSMV等のモデル検査ツール (Model Checker) が存在する．これらのツールを用いることで設計の正当性の評価を自動で行うことができる．しかし，NuSMVによって実ハードウェアの設計を全て記述するには，極めて低級な言語を利用しなければならず，VHDLやVerilog等の言語で設計したシステムを，検証目的のために，改めてNuSMV 等の言語で記述しなおす工程が新たに発生する．また，同じ設計を異なる言語で複数回行うことは，実際の開発現場の状況に鑑みるとコスト・納期などの制約において困難である．

SystemCを用いた開発では，ソフトウェアとハードウェアの協調設計を行うことが可能である．これは，一つのシステムの開発にソフトウェアとハードウェアの部分を分けながら，設計は協調して行う手法である．これにより，アルゴリズムが複雑でハードウェアによる実装が難しい処理はソフトウェアで行い，ソフトウェア (MPU) で実装すると演算時間のかかるような処理部分はハードウェアによる並列化やパイプライン等の工夫によって，高速に処理できるよう設計することが可能となる．しかしながら，この方法においても，ソフトウェア処理部分の設計と，ハードウェア処理部分の設計は，各々の設計を書く必要がある．そのため，ソフト，ハード部のいずれかに仕様の変更が出た場合，もう一方の設計も修正する必要があり，仕様変更に伴って発生するコストの増大が問題となる．

本研究では，既存のハードウェア記述言語，モデル検査用の言語，ならびにシミュレーションや協調設計向けのC言語向けのコード生成器を有するような，上位ハードウェア記述言語 "Melasy" の提案と言語設計を行った．この上位言語系は，関数型プログラミング言語 Haskellとその上のパーサライブラリParsecを使用し，コンパイラ処理系を実装した．上位言語によっていったん記述したシステムは，その設計からコード生成する先の言語を選択することにより，様々な対象オブジェクトコードを得ることができる．とりわけ，システムの設計とそれが満たすべき仕様を併せて上位言語で記述し，直接モデル検査ツール(SMV) 向けのコードを生成することに成功した（図10、図11）．

次に、C++を台言語とし、XML中間系を経由してコード生成を行い、様々な言語向けのオブジェクトコードを生成する新しいバージョン "Melasy+" を開発中である。Melasy+では、上位記述に「仕様パターン」を埋め込み、繰り返し構造や信号線ラベルを解決した上で、XML中間系と同時にラベル解決済みの「仕様パターン」を生成することも検討している。

現在の従来の手法で困難さが生じていた問題が解決できる範囲，あるいは，上位言語Melasyによる設計では，どのような構文上の利点や記述性が優れているのか等に関して，種々のケーススタディによって比較・評価を行っている．
→もっと詳しく(PDF)

図10 上位記述言語 Melasy の位置づけ：設計＋仕様を入力、様々な対象コードを出力する

図11 Melasy上位記述から、モデル検査用言語NuSMVへのコード生成例（Nビットカウンタ）

★キーワード
・形式検証・モデル検査
・ハードウェア設計言語（hardware description language : HDL）
・上位記述（meta description）
・コード生成（code generation）
・仕様パターン（spec pattern）

★このテーマに関する参考資料
[1] E.M.Clarke, O.Grumberg and D.Peled, ``Model Checking'', MIT Press (2000).
[2] N.Iwasaki and K.Wasaki, ``A Meta Hardware Description Language
Melasy for Model-Checking Systems'', Proc. of 5th Int'l Conf. on
Info. Tech.:New Generations (ITNG2008), 273-278 (2008).
[3] NuSMV model checker : A new symbolic model checker (open sources)

●MPI/PCクラスタによる各種アプリケーションの実装

この課題は、MPI(Message Passing Interface)やOpenMPなどの並列化ライブラリを用いて、プロセッサをネットワークあるいは共有メモリで相互に接続（クラスタ化）し、サイズの大きな計算を均質に並列分散処理させることによって、プロセッサ単独で実行する場合よりも高いコスト/性能比を得るための、種々の並列プログラミングについて研究するものである。ノード構成としては、2次元トーラス、ハイパーキューブなど様々なモデルがある。

この課題は比較的新しい研究テーマの一つである。有限要素解析法の高速並列計算、ファジィ最適制御における決定関数の並列チューニング、遺伝的アルゴリズムの並列化、コンピュータグラフィックスにおける分散フレームバッファを利用した並列レイトレーシングなどの計算、など様々な適用例が存在するホットで新しい領域である。ただし、MPIの場合、メッセージパッシング型であるので、計算性能を出すためには、プログラミングにそれなりの工夫が必要である。OpenMPの場合には、コンパイラが自動並列化を試みる。

図12 逐次アルゴリズムから、手動・自動並列化を経て、クラスタ内の複数ワークノード上で並列計算し、結果をまとめる

具体的な実験環境は以下の通り。

Linuxシステム：Dual Xeon 3.0GHz×７ノード・Gigabit Ethernet・TurboLinux 10 Server・PVM/MPI並列ライブラリ・intel C++ 自動並列化コンパイラ・gridMathematica

SMPシステム：QuadCore Xeon 2.4GHz x Dual (16GB)・RedHat Enterprise Linux ES5・OpenMP並列ライブラリ・intel C++ 自動並列化コンパイラ（予定）

通信環境等の関係で、直接にクラスタシステムへ接続が難しい場合であっても、手元の一般的なPC上に仮想マシンを構築することで、クラスタ構成上での並列プログラミングと実行が可能な環境が構築できる。作成したプログラムは、最終的に並列システムへ転送・実行し、その性能評価を行う。

★キーワード
・逐次処理と並列処理の考え方の違い
・並列処理による効率化・問題分割
・ボトルネック、通信オーバーヘッドによる影響
・Flynnの分類
・ネットワークトポロジ
・メモリ共有型 vs 非メモリ共有型