\documentclass[twocolumn,twoside,9.5pt]{jarticle}
\usepackage[dvips]{graphicx}
\usepackage{picins}
\usepackage{fancyhdr}
%\pagestyle{fancy}
\lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
\rhead{}
\cfoot{}

\setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
\setlength{\headheight}{0mm}
\setlength{\headsep}{5mm}
\setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
\setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
\setlength{\textwidth}{181mm}
\setlength{\textheight}{261mm}
\setlength{\footskip}{0mm}
\pagestyle{empty}

\begin{document}
\title{Monad に基づくメタ計算を基本とする Gears OS の設計}
\author{125716B 伊波 立樹{}{} 指導教員 : 河野 真治}
\date{}
\maketitle
\thispagestyle{fancy} 

\section{先行研究}
本研究室では並列プログラミングフレームワーク Cerium\cite{cerium} と分散ネットフレームワーク Alice\cite{alice} の開発を行なってきた。

CeriumではTaskと呼ばれる分割されたプログラムを依存関係に沿って実行することで並列実行を実現する。
依存関係はプログラマ自身が意識して記述する必要があり、
Taskの種類が増えると記述が複雑になり、 負担が大きくなる。
Taskの依存関係がデータの依存関係を正しく保証しない場合があるという問題がある。
また、Taskの取り扱うデータに型情報がないため、 汎用ポインタをキャストして利用するしかなく、型の検査が行われていない。
Cerium は C++で実装されているが、オブジェクトと並列処理が直接対応していないのでオブジェクト指向で記述する利点が少ない。

Alice では処理の単位である Code Segment、 データの単位である Data Segment を用いてプログラムを記述\cite{segment}する。
Code Segment は使用する Input Data Segment, Output Data Segment を指定することで処理とデータの依存関係を解決する。
Alice は Javaで実装されており、実効速度が遅いという問題がある。
また、 Data SegmentをアクセスするAPIのシンタックスが特殊なため、Aliceを用いてプログラムを作成するには慣れが必要になる。

\section{Gears OS}
Cerium と Alice を開発して得られた知見から、並列実行をサポートするだけでなく、信頼性も確保したGears OS の設計・開発を行う。

Gears OS では Gear という単位を用いてプログラムを Code Gear, Data Gear に細かく分割する。
Code Gear は Input Data Gear  から Output Data Gearを生成する。
Input と Outputの関係から Code Gear 同士の依存関係を解決し、並列実行を行う。

Ceriumは初め、Cell\cite{cell} 向けのフレームワークとして設計されたという経緯からプロセッサ毎の実行形式が異なる。
Gears OSでは Many Core CPU、GPUをはじめとする様々なプロセッサを同等な実行機構でサポートする。

従来の OS が行う排他制御、メモリ管理、並列実行などは Meta Computation に相当する。
Meta Computationは本論のComputationを支えるComputationのことである。
関数型言語では Meta Computation に Monad を用いる手法\cite{monad}がある。
Gears OS では、Meta Code/Data Gear を Monadとして定義し、Meta Computationを実現する。

Gears OS は並列実行をサポートするだけでなく、 信頼性も確保する。
そのために Gears OSを用いて作成されたプログラムに対する Model Checkingを行う機能\cite{model-check}を提供する。
並列プログラムに Model Checking を行うことでそのプログラムがとり得る状態を列挙する。
これにより、並列実行時のデッドロックの検出などを行うことでプログラムの信頼性を確保する。
Model Checking の実現には Meta Code/Data Gearを用いる。

Gears OS は Many Core CPU, GPU といった並列実行環境に合わせた設計・実装を行う。
また、接続する Gear を変更することでプログラムの振る舞いを変更することを可能にする柔軟性、Monad に基づくメタ計算による並行制御、Model Checking を用いた信頼性の確保を目的とする。

\section{Code Gear と Data Gear}
Gears OS ではプログラムの実行単位として様々な Gear を使う。
Gear が平行実行の単位、データ分割、Gear 間の接続などになる。

Code Gear はプログラムの実行コードそのものであり、OpenCL\cite{opencl}/CUDA\cite{cuda}
の kernel に相当する。
Code Gear は複数の Input Data Gear を参照し、一つまたは複数の Output Data Gear に書
き込む。
Code Gear は接続された Data Gear 以外には参照を行わない。
Code Gear はfunction callではないので、呼び出し元に戻る概念はない。
その代わりに、次に実行する Code Gear を指定する機能(軽量継続)を持つ。

Data Gear には、int や文字列などの Primitive Data Type が入る。
自分が持っていない Code Gear, Data Gear は名前で指し示す。

Gear の特徴の一つはその処理が Code Gear, Data Gear に閉じていることに
ある。
これにより、Code Gear の実行時間、メモリ使用量を予測可能なものにする。

Code Gear, Data Gear はポインタを直接には扱わない。
これにより、Code と Data の分離性を上げて、ポインタ関連のセキュリティフ
ローを防止する。

Code Gear, Data Gear はそれぞれ関係を持っている。
例えば、ある Code Gear の次に実行される Code Gear、全体で木構造を持つ
Data Gear などである。
Gear の関連付けは Meta Gear を通して行う。
Meta Gear は、いままでの OS におけるライブラリや内部のデータ構造に相当
する。
なので、Meta Gear は Code Gear, Data Gear へのポインタを持っている。

\section{Context}


\section{List}

\section{Synchronized Queue}

\begin{thebibliography}{9}

\bibitem{1}

\end{thebibliography}
\end{document}