\chapter{結論}
本研究では Gears OS の並列実行機構の実装を行った。
Gears OS は処理を Code Gear、データを Data Gear を用いて処理を実行する。
Code Gear と Input/Output Data Gear の組を Task とし、並列実行を行う。

Gears OS のプログラミングは Interface という 一部の Code Gear と Data Gear の集合を表現する Meta Data Gear を用いて行われる。
この Interface は stub Code Gear という全ての Code Gear に対応する Meta Code Gear で Data Gear を参照する。

Gears OS の Task は Context という全ての Code/Data Gear を参照できる Meta Data Gear が対応する。
並列処理を行う際は Context を生成し、 Code Gear と Input/Output Data Gear を Context に設定して TaskManager 経由で各 Worker の SynchronizedQueue に送信される。
Context の設定はメタレベルの記述になるため、ノーマルレベルでは par goto 文というCbC の goto 文に近い記述で並列処理を行える。
この par goto は通常のプログラミングの関数呼び出しのように扱える。

Gears OS の GPU 対応はアーキテクチャ用の Worker と Executor、 Buffer を用意することでアーキテクチャ毎に合わせた実行を行える。
本研究では CUDA 実装として CUDAWorker、 CUDAExecutor、 CUDABufferの実装を行い、実行確認を行った。
また、 CPU、 GPUの実行の切り替えは並列実行される Code Gear の stub Code Gear で継続先を切り替えることでメタレベルで記述することが可能となった。

Twice と BitonicSort の例題の測定結果では 1CPU と 32CPU で Twice では約 27.1 倍、BitonicSort では 約22.12 倍の速度向上が見られた。
また、GPU 実行の測定も行い、 kernel のみの実行時間では 32 CPU より Twice では約7.2倍、BitonicSort では約11.48倍の速度向上がみられ、GPU の性能を活かすことができた。

\section{今後の課題}
今後の課題として、Gears OS の並列処理の信頼性の保証、 チューニングを行う。

Gears OS では証明とモデル検査をメタレベルで実行することで信頼性を保証する。

証明は CbC のプログラムを証明支援系の Agda に対応させて証明を行う。
現在は Gears OS の Interface 部分の動作の証明を行っており、Stack や Tree の動作の証明を行っている。
Gears OS の並列処理の信頼性を証明するには Synchronized Queue の証明を行う必要がある。

モデル検査では CbC で記述されたモデル検査器である akasha \cite{atton-ipsj}を使用して行う。
モデル検査の方針としては、Code Gear の実行を擬似並列で実行し、全ての組合せを列挙する方法で行う。

Go、OpenMP との比較から、 Gears OS が1CPU での動作が遅いということがわかった。
Gears OS は par goto 文を使用することで Context を生成し、並列処理を行う。
しかし、Context はメモリ空間の確保や使用する全ての Code/Data Gear を設定する必要があり、生成にある程度の時間がかかってしまう。
そこで、 par goto のコンパイルタイミングで実行する Code Gear のフローをモデル検査で解析し、処理が軽い場合はContext を生成せずに、関数呼び出しを行う等の最適化を行うといったチューニングが必要である。

今回の CUDA 実装では Output Data Gear を書き出す際に一度 GPU から CPU にデータの送信する必要があった。
しかし、CPU、 GPU 間のデータの通信はコストが高いことが例題の結果からわかった。
GPU にあるデータは CPU 側ではポインタで持つことが出来る。
そこで Meta Data Gear に Data Gear が CPU、GPU のどこで所持されているかを持たせる。
GPU にある Data Gear が CPU で必要になったときに初めてデータの通信を行うことで、最低限のデータ通信で処理を実行できる。