-title:  検証を自身で表現できるハードウェア、ソフトウェア記述言語 Continuation based C と、そのCell への応用

-author: 河野真治

-title-e:     Self descriptive verification in Continuation based C and it's application to Cell architecture

-abstract-e:

CPU performance is achieved in Many Core Architecture rather than
high clock speed recently. The complicated nature of this
architecture makes reliable program difficult. We present a
subset of C Programming Language with continuation: Continuation based C
to make a program for Many Core Architecture. We use this method
for a rendering engine ``Cerium'' for Cell Broadband Engine.

-abstract:

近年、CPUの性能向上は、クロックサイクルをあげることよりも、
複数のCPUコア(Many Core Architecture)を導入することにより
得られるようになって来てい
る。しかし、Many Core Architecture のプログラムは複雑であり、
その信頼性を確保することは難しい。本論文では、本研究室で開
発した Cのサブセット であるContination based C を用いて、Many
Core Architecture のプログラミングと、その検証を行う手法に
ついて考察する。ここでは例題として、Cell Broadband Engine
を用いたレンダリングエンジンを用いる。

-abstract-e:



--Multi core system

複数のCPUを載せたコンピュータは昔から使われて来たが、最近の
傾向は、一つのChipに複数のCPUコアを載せたものの登場である。
従来のマルチプロセッサは同期をサポートしたキャッシュを経由し
メインメモリにアクセスすることが多いが、最近開発されたMulti
Core では、CPU間の通信に特別なポートを用意している。
例えば、IntelはQuick Pathと言う通信ポートががある。
これにより、メインメモリへのアクセスによる競合を避けることが
できる。しかし、その分、複雑なプログラミングが必要となる。

Cell Broadband Engine\cite{Cell} は、SCEIとIBMによって開発された
PS3ゲーム
機用のCPUであり、2 thread のPPU(PowerPC Unit)と、8個のSPU (Synergetic
Processing Unit) を持つ(図\ref{cellarch})。本研究で用いたPS3Linux (FedoreCore 6)
では、6個のSPUを使うことが出来る。SPUはそれぞれ256kbのローカル
メモリを持ち、バスに負担をかけることなく並列に計算を進めること
が出来る。SPUからメインメモリへは、SPUの機械語から直接アクセス
することは出来ず、CellのMFC(Memory Flow Controller)へDMA
(Direct Memory Access) 命令を送ることで行われる。
SPUはグラフィックスに適した、4つの固定小数点、浮動小数点を同時に
演算する命令などを持ち、PPUに比べて高速な演算が可能であり、
ほとんどの演算をSPU上で進めることが推奨されている。

<center><img src="fig/cell.jpg" alt="cellarch"></center>

--Many Core 上のプログラムの特徴

従来の逐次型のプログラムでは、Many Coreの性能を十分に引き出す
ことは出来ない。ここでは、その性能を活かすMany Core プログラム
の特徴について考察する。ここでは、{\tt 定常的な並列度の必要性、
データ並列、パイプライン実行、
プログラムとデータの分割、
同期の問題、
マルチスレッド、
デバッグ}に関して考察を行う。

---定常的な並列度の必要性

並列実行にはAmdahl則\cite{java-conncurrecy}があり、プログラムの並列化率が
低ければ、その性能を活かすことは出来ない。0.8 程度の並列化
率では、6CPUでも3倍程度の性能向上しか得られない(\ref{amdahl})。

<center><img src="fig/amdahl.jpg" alt="amdahl"></center>

高い並列
度ではなくとも、恒常的に並列度を維持する必要がある。このため、

   逐次型のプログラムの一部を並列化する

という手法では不十分である。LSIなどのハードウェア場合は演算の
対象がもともと多量の演算とデータパスを持つので並列計算の効果を
定常的に得られることが多いが、C等で記述されたプログラムでは、
for 文や配列のアクセスなどに並列性が隠されてしまい、それを引き出す
ことが難しい。

プログラムの中の並列度は、主に二つの形で取り出すことが出来る。
一つは、配列や木の中の個々の要素に対して並列に実行する

    データ並列

である。もう一つは、複数の逐次処理の隣同士を重ねて実行する

    パイプライン処理

である。この二つを同時に用いることで定常的な並列度を維持することが
可能となることがある。パイプライン処理は、プログラム中で階層的に
使われることが多い。

---プログラムとデータの分割

データ並列とパイプライン処理を可能にするためには、プログラムと
データの適切な分割を行う必要がある。for文、あるいは、木をだとって
処理する個々のステートメントがプログラムの分割の対象となる。
データは自明に分割できるわけではなく、分割できるデータ構造を採用し、
必要ならばコピーを行う。

分割されたデータは、メモリ上に置かれるが、Cellの場合はSPUのローカル
メモリ上に置かれることになる。共有メモリベースの場合でもキャッシュを
考慮した配置をする必要がある。具体的には、データのアライメントをそろ
える必要がある。メインメモリ上で計算を行う逐次型プログラムと異なり、
コピーのコストを払ってでもデータを分割し、複数のCPUで独立に処理する
必要がある。特に、DMA中心のアクセスになるCellの場合は、
コピーしやすいように、数Kbyte毎の配列にする方が良い。

Cellの場合はさらにコードもローカルメモリ上に置かれるために、
コードをロードする仕組みも必要になる。

---同期の問題

ここで言う同期は、複数のCPUがデータの待ち合わせ、または、整合性を
維持するために、他のCPUとの待ち合わせを行うことである。従来の
マルチCPUでは、並列度が低いために同期は希であり、キャッシュ上の
Spin lock を用いることが多かった。これは、メモリの特定の場所を
test and set 等の特殊な命令で繰り返しアクセスして待ち合わせる手法
である。Unix OSのkernel、POSIX Thread など同期機構の実装に使われている。

Many Core では、待ち合わせを行うと並列度が下がってしまうので、
同期自体を減らす必要がある。そのためには、各CPUが独立に(Lock無しに)
データにアクセス出来るようにデータを分割すれば良い。Cell では、
SPUがローカルメモリを持っているので、そちらにコピーすることになる。
しかし、SPUはメインメモリからデータを取得する必要があるので、その
取得の際には同期を取る必要がある。
Cellでは、SPUとPPU間の同期にはMail box というFIFOメッセージ
キューが用意されていて、readch,writech という命令でSPUから
アクセスする。Spin lock と違って、メッセージ交換なので待ち合わせを
避けることが可能である。

共有メモリベースのシステムの場合でも、同じ場所をアクセスする場合は
キャッシュの競合が生じるので、コピーなどを用いて領域の分割を
行う必要がある。Thread local などを用いる場合もある。

複数のCPUが出力する結果を一つのキューに挿入するようなことをすると、
挿入時に必ず同期が必要になるので同期のコストが高い。

---マルチスレッド

従来の共有メモリ型のマルチCPUでは、POSIX Thread を用いて並列実行
を実現することが多い。特にHyper Thread では、複数の命令ストリーム
を使って、メモリアクセス時等のの命令実行パイプラインのストールを
スレッドを切替えて隠すことが出来る。しかし、Many Core の場合に、
個々のCoreに複数のThreadを割り当てるとワーキングセット(Threadが
使用するデータ)の大きさが大きくなりキャッシュやローカルメモリに
入らなくなる場合がある。

スレッド(Hyper Thread)は本来、I/O待ちやメインメモリアクセス等に対して
有効であり、ほとんどのデータがキャッシュやローカルメモリにあると
考えられるMany Coreには向いていない。個々のタスクを実行するCPU
上で複数のスレッドを使用するメリットはほとんどないと思われる。
一方で、個々のCPUは細分化されたタスクを十分に持っていなければ
恒常的な並列度を維持できない。

一方で、同期機構で待ち合わせを行う場合に、Spin lockを避けるとすれば、
条件付変数などのスレッドのタスクの待ち合わせ機構が必要となる。

Many Core の台数にも寄るが、実行するタスクの管理を行うマネージャー
を複数スレッドで構成し、そのうちの一つが、ポーリングベースで
複数のCoreに対する待ち合わせを行うようにするのが良いと思われる。
Cellでは、SPURS\cite{spurs}という仕組みが提案されている。

---デバッグ

複数のCoreを走らせた状態でのデバッグは難しい。並列プログラムの
特徴として、実行が非決定的(同じ状態で実行しても結果が異なる)こと
があり、バグの状態を再現することが難しいことがある。また、個々の
Core上のデータを調べる必要があり、デバッガが複数のCoreを取り扱える
ことが必須である。

--Many Core 上のプログラムの作り方

本論文では、本研究室で作成したPS3上のレンダリングエンジンであるCerium
Rendering Engine を例題として使う。詳細は別な論文\cite{kono08b}
に譲り、ここでは簡単に記述する。

Cerium は、Scene Graph (3Dオブジェクトを木構造にしたもの)をフレームバッファ
上にSPUを用いて描画するRendering Engine であり、教育用としてシンプルな
構成を持っている。Cerium は、

    1. Scene GraphのPolygonの座標から表示する
    2. 座標の計算を行い PolygonPack を生成する
    3. PolygonPack から、同じY座標を持つ線分の集合SpanPackを生成する
    4. SpanPackを(Texture を読込ながら)Z bufferを用いて描画する。

という4つのタスクを持つ。並列実行は、Scene Graphの木、PolygonPack,
SpanPack に対してデータ並列実行を行う。さらに、この4つが表示画面毎に
パイプライン的に実行される。

これらのタスクは、SPUで実行するために小さなセグメントに分割される
必要がある。分割されたタスクを、PPUまたはSPUで実行するのは
Cerium task manager である。Task manager はタスク依存を解決する
機能を持っていて、タスク依存が満たされたものをアクティブキューに
入れ、SPUを起動する。SPUはアクティブキューから、処理するコードと
データを取得し自律的に実行を行う。

Cerium Rendering engine を作るには、以下の手順に
実装とテストを行う。

    1. 普通のCで実装した Rendering algorithm 
    2. データ構造(PolygonPack, SpanPack)を導入したもの
    3. コードをタスクに分割し、FIFOキューでシーケンシャルに実行する
    4. タスクをSPUに割り当て並列実行する

これにより、Algorithmの正しさを確認した上で並列実行に移行することが出来る。


--Continuation based C

CbC (Continuation based C)は、Cからサブルーチンやループ構造
を除いたCの下位言語であり、ハードウェアとソフトウェア、特に
組込みシステムの記述言語として本研究室で提案している言語で
ある。

Cの関数の代わりに、
たコード・
セグメントという単位を持つ。コードセグメントには、入口に相当する
Input interface と、出口に相当するParameterized goto 文が存在する。

<center><img src="fig/code.jpg"></center>

以下は簡単なCbCのプログラムである。

    code fact(int n,int result, 
           code print()){
        if(n>0){
            result *= n;
            n--;
            goto fact(n,result,print);      
        } else  
            goto (*print)(result);  
    }
間接gotoと、直接gotoが、プログラムの単位の結び付きをボトムアップに
規定して、自然なグループを構成する。

CbCの継続は、Schemeなどの継続とは異なり環境(関数の呼び出し履歴)を持たない。
コードセグメントは、関数呼び出しではないので環境を持つ必要がない。

Cにコードセグメントと引数つきgoto文を付加したCwCは、Cのスーパセット
であり、
コードセグメント内から通常のCの関数を呼び出すことも可能ある。また、
通常の関数からコードセグメントへgotoしたり、コードセグメントから、
呼び出された関数へ値を戻すことも出来る。

コードセグメントは状態遷移記述と対応しているので、ハードウェア記述
とも相性が良い。

CbCコンパイラは、micro-C base のものと GCC base, TCC base のものが
動いており、実用的に使うことができる。{\tt sourceforge.jp} 上\cite{cbc-sourceforge}で公開されている。


---CからCbCへの変換

Cのスタックを明示的に構成することによりCのプログラムをCbCに
変換することが可能である。

        j = g(i+3);

のようなCの関数呼び出しは、 \verb+struct f_g0_save+ などの
明示的なスタックの中身を表す構造体を用いて、
        struct f_g0_interface *c = 
          (struct f_g0_save *)(sp -= 
          sizeof(struct f_g0_save));
        c = sp;
        c->ret = f_g1;
        goto g(i+3,sp);
のような形で、明示的なスタック操作に変換される。これは変換の
一例であり、他の方法、例えばリンクトリストなどを用いても良い。
\verb+f_g1+ は、関数呼び出しの後の継続であり、\verb+g+ では、
    code g(int i,stack sp) {
        goto (* ((struct 
         f_g0_save *)sp)->ret)
           (i+4,sp);
    }
のように間接的に呼び出される。スタックの中は、継続と
中間変数などを格納する構造体である。スタックそのものは、
これらの構造体を格納するメモリである。

これらの変換は自動的に行うことが出来き、試作変換系を実装した
報告\cite{kono01g}もあるが、実用レベルの変換系はまだ存在しない。
現在は変換と、その後の最適化はは手動で行う必要がある。

---CbCでの並列実行記述

並列実行記述ではタスクの生成と同期機構の記述が問題になる。Verilog
やVHDLなどでも並列タスクの記述があり、POSIX Thread ではライブラリ
コールとして\verb+pthread_create+や\verb+pthread_mutex_lock+などが
ある。

これらの動作記述は、マニュアルやFormal Description で示されている。
例えば、以下のような記述である。
{\tt
The pthread\_mutex\_lock() function locks mutex. If the mutex
is already locked, the calling thread will block until the 
mutex becomes available. 
}

このようは記述は曖昧で誤解を招きやすい。しかし、同期機構の検証
では、これらの動作の正確な意味を知る必要がある。

CbC ではad-hoc な並列記述プリミティブは必要ではなく、自分自身で
並列実行を記述することが可能である。これは、コードセグメントには
隠された情報が存在しないので、実行に必要な情報をすべてInput
interface から取得できるからである。

実行キューを作成しCbC自体でSchedulerを記述することにより、
並列実行を記述する。この場合の並列実行単位はコードセグメン
トとなる。goto 文を規則的にscheduler へのgoto文に書き換える
ことにより、並列実行を記述することが出来る。

以下は、CbCで記述した Dining Philosopher の状態の一部である。
    code pickup_rfork(PhilsPtr self)
    {
        if (self->right_fork->owner == NULL) {
                self->right_fork->owner = self;
                goto eating(self);
        } else {
                goto hungry2(self);
        }
    }

これを並列実行するためには、

    code pickup_rfork(PhilsPtr self, TaskPtr current_task)
    {
        if (self->right_fork->owner == NULL) {
                self->right_fork->owner = self;
                self->next = eating;
                goto scheduler(self, current_task);
        } else {
                self->next = hungry2;
                goto scheduler(self, current_task);
        }
    }

という形に記述を変える。Scheduler の実装は例えば、FIFOであれば、

    code scheduler(PhilsPtr self, TaskPtr list)
    {
        TaskPtr t = list;
        TaskPtr e;
        list = list->next;
        goto list->phils->next(list->phils,list);
    }

という形になる。このように自分自身で並列実行スケジューラを
記述できることがCbCの特徴である。同期機構であるが、ここでは
\verb+right_fork+の排他制御は、
コードセグメントが同時に実行されることはないので、自動的に
保証されている。条件付変数のような待ち合わせを実現したい場合は、
TaskPtr への操作として実現すれば良い。

---CbCでの並列実行の実装

FIFO scheduler を例えば Cell のSPUのactive task queue への
挿入とし、active task queue を各SPUが自律的に取得するように
する(SPU scheduler)と、実際にCbCのコードセグメントを並列実
行することが出来る。

FIFO schedulerと実際の並列実行の同期機構が一致するようにする
のは、一般的には自明ではない。同期機構をコードセグメントで記述
して、SPU scheduler によって実現しても良いし、コードセグメント
内部で、例えば、\verb+pthread_mutex_lock+を呼び出しても良い。


--CbCでのCellのプログラムの流れ

CbCを用いて、Many Core Architecture のプログラムを作成する
流れは以下のようになる。

    1. C によりアルゴリズムをシーケンシャルに記述する
    2. データを並列用に分割した構造に変更する
    3. Cの記述をCbCの記述に変換する(必要な部分のみ。手動)
    4. コードセグメントを並列実行用に分割する
    5. FIFOスケジューラにより動作を確認する
    6. SPUスケジューラによりCell上での動作を確認する

これらの各過程すべてでエラーが入る可能性がある。また、
論理的なエラーだけなく、仕様に沿った十分な性能が出るか
どうかも検証する必要がある。

1 の段階は通常のCのプログラミングであり、この部分がちゃんと
動くことが必須である。この段階では、入力に対して出力が
一意に決まる状況であり、テストは容易である。バグも
実行トレースの二分法により容易に行うことが出来る。

4段階まではプログラム変換の問題であり、一つ前の段階と
同じ結果を得られるかどうか検証する必要がある。

5 段階以前はアーキテクチャに依存しないので、ターゲット
が開発途中の段階でも記述することが可能である。しかし、
5段階では、FIFOスケジューラの替わりに、Randomスケジューラ
などを使うことができ、並列実行特有の非決定的な実行が
導入される。

非決定的な実行は、クロックベースのハードウェアでは
入力の任意性から生じることが多い。ハードウェアでも
複数のタスクを使用したり、外界と相互作用する場合は
非決定的な実行が現れる。

段階5では、これらの非決定的な実行でも4段階までと
同じ仕様を満たすことを検証する必要がある。これは、
逐次型のプログラムでは出て来ない問題である。

段階6では、段階5まできちんと動いていれば、問題なく
動作すると期待される。しかし、FIFOスケジューラと
SPUスケジューラでは、同期機構の実現が異なることが
ある。これは、並列実行と同期機構のの粒度と意味論
が異なるために起きると考えられる。

ここで、段階1が仕様であり段階5が実装であると
考えることもできる。実際のプログラムとは別に、
実行時に満たして欲しい仕様の記述がある場合もある。
これらの記述は、例えば、「計算がいつか終る」
等の時相論理的な記述になる。時相論理としては、
LTTL\cite{wolper82}, CTL*\cite{synBTTL}, ITL\cite{kono93b}
などを使うことができる。


--CbCでのCellのプログラムの検証

CbCでの検証は、プログラム作成の各段階で行われる。
CbC では実行要素はコードセグメントであり、その
Input interface の値により動作は一意に決まる。
従って、検証はコードセグメント単位良い。コードセグメント
内部の正当性はテストあるいは証明こ行われるべきである。

---コードセグメントの入出力テスト

これは、通常のプログラムのテスト手法と同じであり、
FIFOスケジューラを導入する前の段階では、入力と
出力に対応するテストを行う。

コードセグメント毎にテストデータを作成するべきで
あるが、結果の正しさを確認するプログラムを書く必要とする
場合もある。

データ及びコードの分割が終った段階では、データを
Multi Core CPUがアクセスできるようにコピーする
コードが入ることがある。このコピーは、FIFOスケジューラ
レベルでは、ポインタ渡しに避けても良い。しかし、
コピーコード自体にエラーが出る場合も多い。例えば、
Cellでは、MFCによるDMAは64bit alignmentが必要であり、
これが満たされないと例外が発生してしまう。


---FIFOスケジューラレベルでのテスト

FIFOスケジューラレベルのテストでは、非決定性が
導入される。Cell では組み込まれたSPUは、すべて
決定的に動作するが、データによってSPUの演算の
終了結果は異なり、結果的に非決定性が生じる。

これらの非決定性を、網羅的に調べることも可能であり、
モデル検査と呼ばれる。

CbCでは、状態を記録しながら、すべての可能な非決定的実行を行
うスケジューラを実装することが可能である。

    メモリ状態をデータベースから調べる
    すでにあれば、一つ前の状態に戻して他の実行を探す
    なければ、一段深い実行に進み状態を探す

という形である。実際の実装は以下のようになっている。

    code tableau(TaskPtr list)
    {
        if (lookup_StateDB(&st, &state_db, &out)) {
            // found in the state database
            printf("found %d\n",count);
            while(!(list = next_task_iterator(task_iter))) {
                // no more branch, go back to the previous one
                TaskIteratorPtr prev_iter = task_iter->prev;
                if (!prev_iter) {
                    printf("All done count %d\n",count);
                    ....
                }
                printf("no more branch %d\n",count);
                depth--;
                free_task_iterator(task_iter);
                task_iter = prev_iter;
            }
            // return to previous state
            // here we assume task list is fixed, we don't have to
            // recover task list itself
            restore_memory(task_iter->state->memory);
            printf("restore list %x next %x\n",(int)list,(int)(list->next));
        } else {
            // one step further
            depth++;
            task_iter = create_task_iterator(list,out,task_iter);
        }
        goto list->phils->next(list->phils,list);
    }

この検証系は、SPUを使った実機上で動かすには、SPU内部のメモリを記録
するなどの工夫が必要となる。また、探索空間が膨大になる場合もある。

探索空間を小さくするには、並列実行の粒度を大きくしたり、メモリの
状態を抽象化したりする方法が考えられる。これらの手法は、CbC自身で
記述することが可能である。

--本手法の利点と欠点

CbCという特殊な処理系を使うことになるので、ソースの変更が
必要となる。現状では、C++には対応していない。

コードセグメントのテストをSingle core上とMulti core 上の
両方でテスト出来るので、Multi coreになれていなくても、
動作のテストが容易である。また、Multi core になれるための
準備、教育的ツールとして使うことも出来る。アルゴリズム
の正しさを並列実行とは別にテスト出来るのが利点である。

CellはヘテロなMulti Coreであり、
SPU では、その性能を活かすためには、特殊なアセンブラ命令、
例えば4つの浮動小数点の値の同時演算などを使用する必要がある。
これらは、gcc の拡張あるいはasmステートメントなどで使用する
ことができるが、他のアーキテクチャ上では動作しない。
従って、同じ機能を持つコードセグメントで代用してテスト
することになる。異なるアーキテクチャでの異なるコードセグメント
の同等性を直接テストすることは出来ない。

Many Core 向けのデータ分割、コード分割は自動ではないので、
試行錯誤することになる。必要な性能が出るかどうかは、
分割のために生じるコピーのコストなどの要素が関係し、
アーキテクチャに依存するのでSingle Core上のテストで
見積もることは難しい。

データ分割、コード分割が手動なので間違いが入りやすい。
FIFOスケジューラレベルで、Single Coreと同等な動作を
する場合は、このようなエラーを見つけるのは容易である。

しかし、非決定的な動作をする場合は、自明な動作比較をする
ことは出来ず、モデル検査などのコストの高い方法を使う
必要が出て来る。コードセグメントレベルのモデル検査は
実機上の同期動作との差があるので、正確ではない。

モデル検査のコストが重い場合は、スケジューラを挟む
部分を大まかにして状態数を減らす手法が使える。正確さは
落ちるが、高速に検査することが出来る。

スケジューラを挟む部分の変更は手動であり、マクロあるいは
スクリプトで生成する必要がある。

--学生による実際の実装の現状

本手法を、PS3 Linux 上のSPUを用いた 3D Rendering Engine
の作成に適用した。詳細は別な論文で述べるので、ここでは
学生の反応について報告する。

Single Core でプログラムを動作させることは容易である。これは、
従来のプログラムと差がないからであり、学生にとっては入りやすい。
データとコードの分割を自力で求めるのは、並列処理の経験がない
学生には難しい。なんらかのひな型か指示が必要である。

FIFOスケジューラから、SPUスケジューラを実装する時点で、
なるべく早く動かそうとするために ad-hoc なコードが入りやすい。
特に、一旦、SPUスケジューラに移ってしまうと、元の
ソースを
FIFOスケジューラ/Single Core 上で動かすことを考慮せずに
変更を加えてしまう。そのような場合は、この方法のメリット
である、並列実装部分のバグと、アルゴリズム/データ分割のバグ
を分離することが出来なくなってしまう。しかし、常に
両方で動作させるように変更するのは、手間がかかることも
確かである。

データやコードの分割において、Cellでは6個のSPUを使うことが
出来るが、必ず6個に分割することを仮定してプログラムを書いて
しまうという問題も見られた。分割したコードにどれだけの
Coreを割り振るかは、後で調整する必要があるので、必ず
最大値を使うとは限らない。

--CbCを用いた検証手法と他の手法との比較

コードセグメントを使わずに、Cの関数による分割を行って
も良い。この場合は、分割された関数を順々に呼び出す
マネージャを記述する必要がある。CbCのようにモデル検査を
自分で記述するようなことは出来ないが、分割に関しては
同等である。

モデル検査では SPIN\cite{holzmann97model}が有名だが、SPINでは
問題を Promela という仕様記述言語で記述する必要があり、
Promela を直接実装に使うことは出来ない。

実装言語を直接モデル検査するシステムとしては、
Java PathFinder\cite{havelund98model}、
CBMC\cite{groce04understanding}などが知られている。これらはオブジェクト指向
記述に対しても適用できるという利点がある。
これらで並列処理を記述する場合は、一般的にはThread の
機能を用いることになる。

CbCでは、スケジューラ及びモデル検査器を自分で記述出来るので、
検査する並列性や抽象度を自分で制御できると言う利点がある。
現状では、そういう可能性があるというだけで実装は行っていない。

現在用いているCbC用のモデル検査器は比較的単純に作られており、
大きなプログラムの検証をするのには向かない。2.8GHz Pentinum 4
では、Dining Philosphers の例題に対して以下のような性能が
出ている。

\begin{table}[htbp]
\begin{center}
\caption{Dining Philosophers ProblemのCbCによるモデル検査}
\label{tab:dpp_tableau}
\begin{tabular}{|r|r|r|} \hline
プロセス数 & 状態数 & 実行時間(秒) \\ \hline
3 & 1,340 & 0.01 \\ \hline
4 & 6,115 & 0.08 \\ \hline
5 & 38,984 & 0.66 \\ \hline
6 & 159,299 & 3.79 \\ \hline
7 & 845,529 & 27.59 \\ \hline
8 & 3915,727 & 199.80 \\ \hline
\end{tabular}
\end{center}
\end{table}

\begin{table}[htbp]
\begin{center}
\caption{SPINによるDining Philosophers Problemのモデル検査}
\label{tab:spin_dpp}
\begin{tabular}{|r|r|r|} \hline
プロセス数 & 状態数 & 実行時間(秒) \\ \hline
5 & 94 & 0.008 \\ \hline
6 & 212 & 0.01 \\ \hline
7 & 494 & 0.03 \\ \hline
8 & 1,172 & 0.04 \\ \hline
\end{tabular}
\end{center}
\end{table}

\begin{table}[htbp]
\begin{center}
\caption{JPFによるDining Philosophers Problemのモデル検査}
\label{tab:jpf_dpp}
\begin{tabular}{|r|r|r|} \hline
プロセス数 & 状態数 & 実行時間(秒) \\ \hline
5 & 不明 & 3.98 \\ \hline
6 & 不明 & 7.33 \\ \hline
7 & 不明 & 26.29 \\ \hline
8 & 不明 & 123.16 \\ \hline
\end{tabular}
\end{center}
\end{table}

Java Path Finder とSPINの丁度間の性能となっているが、プロセス数が
多くなると、Java Path Finder よりも性能が落ちる。これは、モデル
検査のための状態格納のアルゴリズムに問題があると考えている。
SPINの性能が良いのは、元々の状態記述の抽象度が高く状態数そのものが
小さいからであると考えられる。

CbCの記述を変更して、スケジューラを呼び出す頻度を下げると、
状態するが下がりSPINに近い性能を得ることも可能である。
Java Path Finder では、そのような変更を行うことは原理的に
出来ない。

--まとめ

May Core Architecture のプログラムを作成する手法として、
シーケンシャルなCの記述を、CbCに分解する手法を提案し実践してみた。
また、その手法に対するテスト及び検証法について述べた。

CbCでは、モデル検査部と実装部分を混在し、同時にプログラムすることが
出来るので、並列実行部分を作成しながら、それをテストするための
モデル検査部を作成していくことが可能である。

現在のモデル検査部で、SPIN と Java Path Finder の中間的な性能を
得ることが出来ているが、より高性能なアルゴリズムを実装する必要が
ある。

Cerium Rendering Engine はCell上で動作しているが、テスト及び
モデル検査は行っていないので、これらを実装して、実際の効果を
調べることが必要である。