\chapter{メタ計算を使った並列処理}
並列処理は現在主流のマルチコアCPU の性能を発揮するには重要なものになっている。
しかし、並列処理のプログラミングはスレッド間の共通資源の競合など非決定的な実行を持っており、その信頼性を保証するには従来のテストやデバッグでは不十分であり、テストしきれない部分が残ってしまう。

また、マルチコア CPU 以外にも  GPU や CPU と GPU を複合したヘテロジニアスなプロセッサも並列処理をする上で無視できない。
これらのプロセッサで性能を出すためにはアーキテクチャに合わせた並列プログラミングが必要になる。
並列プログラミングフレームワークでは様々なプロセッサを抽象化し、CPU と同等に扱えるようにする柔軟性が求められる。

本研究室では通常の計算をノーマルレベルとし、並列処理の信頼性をノーマルレベルの計算に対して保証し、拡張性をノーマルレベルとは別の階層のメタレベルの計算で実現することを目標に Gears OS\cite{kkb-master}を設計、開発中である。
Gears OS では処理を Code Gear、データを Data Gear という単位を用いてプログラムを記述する。
Code Gear は入力の Input Data Gear が揃ったら実行され、Output Data Gear を出力する。
この Input/Output Data Gear の関係から依存関係を決定し、Input Data Gear が揃った Code Gear が並列に実行される。

Gears OS のプログラムの信頼性の確保はモデル検査、検証を使用して行う。
この信頼性のための計算はメタ計算として記述される。
このメタ計算は信頼性の他に CPU、GPU などのアーキテクチャに沿った実行環境の切り替え、データの拡張等の拡張性を提供する。
メタ計算の処理は Meta Code Gear、Meta Data Gear で表現する。
Meta Code Gear は 通常の Code Gear 間に実行される。

従来の研究では OS の実装言語として Python\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596} をノーマルレベルとして採用し、メタレベルで検証を行う研究や、メタ計算の実装を型付きアセンブラ(Typed Assembler)\cite{Yang:2010:SLI:1806596.1806610} を用いる例もある。
Gears OS は ノーマルレベルとメタレベルを共通して表現出来る Continuation Based C(CbC)\cite{utah-master} で実装を行い、証明支援系 Agda\cite{agda} を用いて証明を行う。
CbC は Code Gear の単位でプログラムを記述し、軽量継続を用いてコード間を移動する。
軽量継続は関数呼び出しとは異なり、呼び出し元に戻らないため、呼び出し元の環境を覚えずに行き先のみを指定する。
この CbC は C と互換性のある言語で、型付きアセンブラに比べると大きな表現力を提供する。また Haskell などに比べて関数呼び出しではなく軽量継続を採用しているため、スタック上に隠された環境を持たない。
そのためメタレベルで使用する資源を明確にできる利点がある。

Code Gear 間の継続は次の Code Gear の番号と Context という全ての Code Gear と Data Gear を参照できる Meta Data Gear で行われる。
Context からノーマルレベルのCode Gear へ接続する際は stub Code Gear という Meta Code Gear を用いる。
この stub Code Gear はメタレベルの計算であるため、継続先の Code Gear から自動的に生成されるのが望ましい。生成に必要な情報は Code Gear と Data Gear の集まりから得る。 この集まりを Interface\cite{mitsuki-prosym} として定義している。

Gears OS でのプロセス、スレッドは Context が担う。
並列実行する際は新しく Context を生成し、それを CPU、GPU に割り振る事によって実現される。
生成された Context には実行する Code Gear と対応する Input/Output Data Gear が登録され、割り振られた先で Context に設定された Code Gear を実行する。
このContext を用いた並列処理は新規に実行環境を作り、引数を設定するなどの煩雑なメタレベルの処理であり、ノーマルレベルでは Go 言語\cite{go}の goroutine のような簡潔な並列構文があることが望ましい。

本研究では Gears OS の基本設計、マルチコアCPU と CUDA による GPUでの実行機構、並列構文を実装し、例題を用いて Gears OS の並列処理の評価を行う。

% これはryokka 向きかなぁ

%現代の OS では拡張性と信頼性を両立させることが要求されている。
%時代と主に進歩するハードウェア、サービスに対して OS 自体が拡張される必要がある。
%しかし、OSには非決定的な実行を持っており、その信頼性を保証するには従来のテストとデバッグでは不十分であり、テスト仕切れない部分が残ってしまう。
%これに対処するために証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
% 証明やモデル検査を用いて OS の検証する方法は様々なものが検討されている。
% 型付きアセンブラ\cite{Yang:2010:SLI:1806596.1806610}
% 従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。
% また SPIN などのモデル検査を OS の検証に用いた例もである。
% 本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。