\section{ CbCでのCellのプログラムの流れ}

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

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

\end{verbatim}
}

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

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

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

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

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

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

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

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