\section{ CbCでのCellのプログラムの検証}

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

\subsection{ コードセグメントの入出力テスト}

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

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

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


\subsection{ FIFOスケジューラレベルでのテスト}

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

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

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

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

\end{verbatim}
}

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

{\small
\begin{verbatim}
    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);
    }

\end{verbatim}
}

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

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