changeset 5:05be3fd35750

edit
author Shohei KOKUBO <e105744@ie.u-ryukyu.ac.jp>
date Tue, 05 May 2015 14:24:59 +0900
parents 537ebaa79b21
children b02e6b40f470
files paper/benchmark.tex paper/conclusion.tex paper/design.tex paper/gearbox.tex paper/implement.tex paper/opencl.tex paper/sigos.pdf paper/sigos.tex paper/theory.tex
diffstat 9 files changed, 171 insertions(+), 285 deletions(-) [+]
line wrap: on
line diff
--- a/paper/benchmark.tex	Mon May 04 18:50:22 2015 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-\section{Benchmark}
-本章では、WordCount, FFT を例題として用い、本研究で実装した GpuScheduler および CudaScheduler の測定を行う。
-
-測定環境
-\begin{itemize}
-\item OS : MacOS 10.9.2
-\item CPU : 2*2.66GHz 6-Core Intel Xeon
-\item GPU : NVIDIA Quadro K5000 4096MB
-\item Memory : 16GB 1333MHz DDR3
-\item Compiler : Apple LLVM version 5.1 (clang-503.0.40) (based on LLVM 3.4svn)
-\end{itemize}
-
-\section{WordCount}
-今回は 100MB のテキストファイルに対して WordCount を行なった。
-表:\ref{table:wordcount}は実行結果である。
-
-\begin{table}[!h]
-  \begin{center}
-    \small
-    \begin{tabular}[t]{c||r} \hline
-      & Run Time \\ \hline
-      1 CPU & 0.73s \\ \hline
-      2 CPU & 0.38s \\ \hline
-      4 CPU & 0.21s \\ \hline
-      8 CPU & 0.12s \\ \hline
-      OpenCL(no pipeline) & 48.32s \\ \hline
-      OpenCL(pipeline) & 46.74s \\ \hline
-      OpenCL Data Parallel & 0.38s \\ \hline
-      CUDA(no pipeline) & 55.71s \\ \hline
-      CUDA(pipeline) & 10.26s \\ \hline
-      CUDA Data Parallel & 0.71s \\ \hline
-    \end{tabular}
-    \caption{WordCount}
-    \label{table:wordcount}
-  \end{center}
-\end{table}
-
-パイプライン処理を行うことで CUDA では5.4倍の性能向上が見られた。
-しかし、OpenCL ではパイプライン処理による性能向上が見られなかった。
-OpenCL と CUDA を用いたそれぞれの Scheduler はほぼ同等な実装である。
-OpenCL でパイプライン処理を行うために実行機構を見直す必要がある。
-一方で、データ並列による実行は 1CPU に対して OpenCL では1.9倍、CUDA では1.02倍という結果になった。
-どちらもタスク並列による実行よりは優れた結果になっている。
-CUDA によるデータ並列実行の機構を見直す必要がある。
-
-\subsection{FFT}
-次に、フーリエ変換と周波数フィルタによる画像処理を行う例題を利用し測定を行う。
-使用する画像のサイズは512*512で、画像に対して High Pass Filter をかけて変換を行う。
-表:\ref{table:fft}は実行結果である。
-
-\begin{table}[!h]
-  \begin{center}
-    \small
-    \begin{tabular}[t]{c||r} \hline
-      & Run Time \\ \hline
-      1 CPU & 0.48s \\ \hline
-      2 CPU & 0.26s \\ \hline
-      4 CPU & 0.17s \\ \hline
-      8 CPU & 0.11s \\ \hline
-      OpenCL & 0.09s \\ \hline
-      CUDA & 0.21s \\ \hline
-    \end{tabular}
-    \label{table:fft}
-    \caption{FFT}
-  \end{center}
-\end{table}
-
-1CPU に対して OpenCL ではの5.3倍、CUDA では2.2倍の性能向上が見られた。
-しかし、WordCount の場合と同様に OpenCL と CUDA で差がある。
-WordCount と FFT の結果から CudaScheduler によるデータ並列実行機構を見直す必要がある。
-また、FFT の OpenCL の kernel は cl\_float2 というベクター型を用いている。
-CUDA では cl\_float2 を float に変換して演算している。
-OpenCL ではベクターの演算なので、その部分に最適化がかかっており結果が良くなっている可能性がある。
--- a/paper/conclusion.tex	Mon May 04 18:50:22 2015 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-\section{まとめ}
--- a/paper/design.tex	Mon May 04 18:50:22 2015 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-% Theory
-\section{Monad とメタ計算}
-関数型言語では入力から出力を得る通常の計算の他にメタ計算と呼ばれるもの
-がある。
-メタ計算の例として、失敗する可能性がある計算、並行処理、入出力などの副
-作用、メモリ管理などがある。
-メタ計算の理論的な表現として、Monad を用いることが Moggi らにより提案
-されている。
-GearsOS ではメタ計算を表現するのに、Monad と軽量継続を用いる。
-
-Monad は関数が返す通常の値を含むデータ構造であり、メタ計算を表現するの
-に必要な情報を格納している。
-失敗する可能性がある計算の場合は、計算が失敗したかどうかのフラグが
-Monad に含まれる。
-並行処理の場合は、Monad は可能な計算の interleaving(並び替え) になるが、
-実際に並び替えを持っているわけではなく、マルチプロセッサで実行する環境
-そのものが Monad に対応する。
-
-通常の関数を Monad を返すように変更することにより、メタ関数が得られる。
-逆に Monad の中にある通常の戻り値のみに着目すると通常の関数に戻る。
-このように、Monad を用いたメタ計算の表現では通常の計算とメタ計算が一対
-一に対応する。
-
-一般的には複数の Monad の組み合わせが Moand になることを示すのは難しい。
-GearsOS では Code と Data を分離して、Code から他の Code への呼び出し
-を継続を用いて行う。
-GearsOS での Monad は Meta Code と Meta Data になる。
-この構成では Meta Code を順次呼び出すことにより、
-
-% Code Segment
-% Data Segment
-% Meta Code Segment
-% Meta Data Segment
-\section{Code Gear と Data Gear}
-GearsOS ではプログラムの実行単位として様々な Segment(Gear) を使う。
-Segment が平行実行の単位、データ分割、Segment 間の接続などになる。
-
-Code Segment(Code Gear) はプログラムの実行コードそのものであり、Cuda
-の kernel に相当する。
-Code Gear は複数の Data Gear を参照し、一つまたは複数の Data Gear に書
-き込む。
-Code Gear は接続された Data Gear 以外には触らない。
-Code Gear はサブルーチンコールではないので、呼び出し元に戻る概念はない。
-その代わりに、次に実行する Code 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 へのポインタを持っている。
-
-Data Gear には、int や文字列などの Primitive Data Type が入る。
-自分が持っていない Code Gear, Data Gear は名前で指し示す。
-% s/Segment/Gear
-
-% Context
-\section{継続}
-ある Code Gear から継続するときには、次に実行する Code Gear を名前で指
-定する。
-Meta Code Gear が名前を解釈して、処理を対応する Code Gear に引き渡す。
-これらは、従来の OS の dynamic loding library や command 呼び出しに対
-応する。
-名前と Code Gear へのポインタの対応は Meta Data Gear に格納される。
-この Meta Data Gear を Context と呼ぶことにする。
-これは従来の OS の Process や Thread に対応する。
-
-Context には以下のようなものが格納される。
-    Code Gear の名前とポインタの対応表
-    Data Gear の Allocation 用の情報
-    Code Gear が参照する Data Gear へのポインタ
-    Data Gear に格納される Data Type の情報
-
-[Code Gear の名前とポインタの対応表]
-[Data Gear の Allocation 用の情報]
-[Code Gear が参照する Data Gear へのポインタ]
-[Data Gear に格納される Data Type の情報]
-
-\section{Sample Code}
--- a/paper/gearbox.tex	Mon May 04 18:50:22 2015 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-\section{GearBox}
--- a/paper/implement.tex	Mon May 04 18:50:22 2015 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-\section{実装}
-\subsection{Allocator}
-\subsection{List}
-\subsection{Synchronized Queue}
-\subsection{Task Manager}
--- a/paper/opencl.tex	Mon May 04 18:50:22 2015 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,84 +0,0 @@
-\section{Parallel Computing Platform}
-\subsection{OpenCL}
-OpenCL とは、Multi Core CPU と GPU のようなヘテロジニアスな環境を利用した並列計算を支援するフレームワークである。
-演算用のプロセッサ(本研究では GPU)上で動作するプログラム OpenCL C という言語で記述する。
-OpenCL C で記述したプログラムを GPU 上で実行させるために OpenCL Runtime API を利用する。
-OpenCL ではオペレーティングシステムなどが処理されるメイン CPU のことを host、GPGPU が可能なグラフィックボードなどのことを device と定義している。
-OpenCL Application は host 側のプログラムと device 側のプログラムが一体となって動作する。
-この device 上で動作するプログラムを特別に kernel と呼ぶ。
-
-\subsubsection{CommandQueue}
-OpenCL では、device の操作に CommandQueue を使用する。
-CommandQueue は device に Operation を送るための仕組みである。
-kernel の実行、input buffer の読み込み、output buffer への書き込みなどが Operation となる。
-
-CommandQueue に投入された Operation は投入された順序で実行される。
-CommandQueue を生成するときプロパティを指定することで Operation を投入された順序を無視して(out of order)実行することが可能になる。
-また複数の CommandQueue を生成し、device に投入することでも our of order で実行することが可能である。
-
-out of order で実行する場合、データの依存関係を設定する必要がある。各 Operation を発行する関数には event\_wait\_list と event を指定することができ、これらを利用してデータの依存関係を設定することができる。
-out of order 実行を可能にするプロパティをサポートしている device が少ないため、今回は複数の CommandQueue を用いる方法で実装を行なった。
-
-\subsubsection{OpenCL におけるデータ並列}
-3D グラフィックのような多次元のデータを処理する場合に高い並列度を保つには、データを分割して並列に実行する機能が必要である。
-これを OpenCL ではデータ並列と呼んでいる。
-OpenCL では次元数に対応する index があり、OpenCL は1つの記述から index の異なる複数の kernel を自動生成する。
-その添字を global\_id と呼ぶ。
-このとき入力されたデータは WorkItem という処理単位に分割される。
-
-OpenCL は WorkItem に対して、それぞれを識別する ID(global\_id)を割り当てる。
-kernel は get\_global\_id という API によって ID を取得し、取得した ID に対応するデータに対して処理を行うことでデータ並列を実現する。
-
-データ並列による kernel 実行の場合、clEnqueueNDRangeKernel を使用する。
-この関数の引数として WorkItem の数と次元数を指定することでデータ並列で実行することができる。
-
-\subsection{CUDA}
-CUDA とは、半導体メーカー NVIDIA 社が提供する GPU コンピューティング向けの総合開発環境でコンパイラ、ライブラリ、デバッガなどから構成される。プログラミング言語である CUDA C は C 言語ベースに拡張を加えたものである。
-
-CUDA には CUDA Runtime API と CUDA Driver API の2種類がある。
-Driver API は Runtime API に比べてプログラマが管理すべきリソースが多い。
-しかし、Runtime API より柔軟な処理を行うことができる。
-今回は Driver API を使用して実装した。
-
-CUDA も OpenCL と同様に、制御を行う CPU 側を host、GPU 側を device と定義している。
-また、device 上で動作するプログラムも OpenCL と同様に kernel と呼ぶ。
-
-\subsubsection{Stream}
-CUDA には OpenCL の CommandQueue と似たような仕組みとして Stream がある。
-Stream は host 側で発行された Operation を一連の動作として device で実行する。
-Stream に発行された Operation は発行された順序で実行されることが保証されている。
-異なる Stream に発行された Operation に依存関係が存在しない場合、Operation を並列に実行することができる。
-
-Stream は cuStreamCreate という Driver API で生成される。
-引数に Stream を指定しない API はすべて host 側をブロックする同期的な処理となる。
-複数の Stream を同時に走らせ Operation を並列に実行するためには非同期な処理を行う API を利用する必要がある。
-
-\subsubsection{CUDA におけるデータ並列}
-CUDA では OpenCL の WorkItem に相当する単位を thread と定義している。
-この thread をまとめたものを block と呼ぶ。
-CUDA でデータ並列による kernel 実行をする場合、cuLaunchKernel API を使用する。
-この関数は引数として各座標の block 数と各座標の block 1つ当たりの thread 数を指定することでデータ並列で実行できる。
-
-cuLaunckKernel で kernel を実行すると各 thread に対して block ID と thread ID が割り当てられる。
-CUDA には OpenCL とは異なり、ID を取得する API は存在しない。
-代わりに、kernel に組み込み変数が準備されており、それを参照し、対応するデータに対し処理を行うことでデータ並列を実現する。
-組み込み変数は以下の通りである。
-
-\begin{itemize}
-  \item uint3 blockDim
-  \item uint3 blockIdx
-  \item uint3 threadIdx
-\end{itemize}
-
-各組み込み変数はベクター型で、blockDim.x とすると x 座標の thread 数を参照することができる。
-blockIdx.x とすると x 座標の block ID が参照でき、threadIdx.x とすると x 座標の thread ID を参照することができる。
-blockDim.x * blockIdx.x + threadIdx.x で OpenCL の get\_global\_id(0) で取得できる ID に相当する ID を算出することができる。
-例として、ある kernel で get\_global\_id(0) の返り値が13の場合、CUDA では図:\ref{fig:calculate_index}のようになる。
-
-\begin{figure}[!h]
-  \begin{center}
-    \includegraphics[scale=0.4]{./images/culculate_index.pdf}
-  \end{center}
-  \caption{Calculate Index}
-  \label{fig:calculate_index}
-\end{figure}
Binary file paper/sigos.pdf has changed
--- a/paper/sigos.tex	Mon May 04 18:50:22 2015 +0900
+++ b/paper/sigos.tex	Tue May 05 14:24:59 2015 +0900
@@ -2,26 +2,30 @@
 \usepackage[dvipdfm]{graphicx}
 \usepackage{url}
 \usepackage{listings}
-\lstset{%
-  language={C++},%使用言語
-  basicstyle={\small},%書体
-  commentstyle={\small\itshape},%コメントの書体
-  keywordstyle={\small\bfseries},%キーワードの書体
-  %identifierstyle={\small},%
-  %ndkeywordstyle={\small},%
-  stringstyle={\small},%文字列の書体
-  frame={trlb},%外枠
-  breaklines=true,%改行
+\usepackage{enumitem}
+
+\lstset{
+  language=C,
+  tabsize=2,
+  frame=single,
+  basicstyle={\footnotesize},%
+  identifierstyle={\footnotesize},%
+  commentstyle={\footnotesize\itshape},%
+  keywordstyle={\footnotesize\bfseries},%
+  ndkeywordstyle={\footnotesize},%
+  stringstyle={\footnotesize\ttfamily},
+  breaklines=true,
+  captionpos=b,
   columns=[l]{fullflexible},%
   xrightmargin=0zw,%
-  xleftmargin=3zw,%
-  %numbers=none,%行番号の表示
-  %numberstyle={\scriptsize},%行番号の書体
-  %numbersep=1zw,%
-  %stepnumber=1,
-  lineskip=-0.5ex,%
-  captionpos=b,%キャプションの位置
+  xleftmargin=1zw,%
+  aboveskip=1zw,
+  numberstyle={\scriptsize},%
+  stepnumber=1,
+  numbersep=1zw,%
+  lineskip=-0.5ex%
 }
+
 \renewcommand{\lstlistingname}{Code}
 \input{dummy.tex} %% Font 
 
@@ -64,10 +68,10 @@
 
 % 和文概要
 \begin{abstract}
-  本研究室では Code Segment, Data Segment を用いた並列フレームワークの開発を行なっている。
+  本研究室では Code Gear, Data Gear を用いた並列フレームワークの開発を行なっている。
   並列実行に必要な Meta な機能を関数型言語における Monad の原理に基づいて、実現することにした。
-  今回設計した Gears OS では Code Segment, Data Segment それぞれに Meta Code Segment と  Meta Data Segment を付属させる。
-  Code Segment が実行されるとそれに属する Meta Code Segment が実行され、Meta Computation が行われる。
+  今回設計した Gears OS では Code Gear, Data Gear それぞれに Meta Code Gear と  Meta Data Gear を付属させる。
+  Code Gear が実行されるとそれに属する Meta Code Gear が実行され、Meta Computation が行われる。
   Meta Computation は OS が行うネットワーク管理、メモリ管理等の資源制御を行う。
   本論文では基本的な機能を CbC(Continuation based C) で実装し、評価する。
 \end{abstract}
@@ -81,21 +85,156 @@
 
 % 本文はここから始まる
 
-\input{introduction}
-\input{theory}
-\input{design}
-\input{gearbox}
-\input{implement}
-\input{conclusion}
+% Introduce
+\section{Gears OS}
+並列実行は Code の並列実行だけでなく、Data の単位が重要である。
+本研究では Code Gear, Data Gear という単位で細かく分割し、依存関係を記述することで並列実行するフレームワーク Gears OS の開発を行なっている。
+Code Gear, Data Gear はそれぞれ他の Code Gear, Data Gear に接続することで機能や Data 自体を拡張することが可能である。
+
+従来の OS が行う排他制御、メモリ管理、並列実行などは Meta Computation に相当する。
+Gears OS では、Meta な機能を関数型言語における Monad に基づいて実現する。
+
+Gears OS を用いて作成されたプログラムに対する Model Checking を行う機能を提供する。
+これにより、生成されたプログラムの信頼性を保証する。
+
+Gears OS は Gear を継続することによる柔軟性、Monad に基づくメタ計算による並行制御、Model Checking を用いた信頼性の確保を目的とする。
+
+% Theory
+\section{Monad とメタ計算}
+関数型言語では入力から出力を得る通常の計算の他にメタ計算と呼ばれるもの
+がある。
+メタ計算の例として、失敗する可能性がある計算、並行処理、入出力などの副
+作用、メモリ管理などがある。
+メタ計算の理論的な表現として、Monad を用いることが Moggi らにより提案
+されている。
+Gears OS ではメタ計算を表現するのに、Monad と軽量継続を用いる。
+
+Monad は関数が返す通常の値を含むデータ構造であり、メタ計算を表現するの
+に必要な情報を格納している。
+失敗する可能性がある計算の場合は、計算が失敗したかどうかのフラグが
+Monad に含まれる。
+並行処理の場合は、Monad は可能な計算の interleaving(並び替え) になるが、
+実際に並び替えを持っているわけではなく、マルチプロセッサで実行する環境
+そのものが Monad に対応する。
+
+通常の関数を Monad を返すように変更することにより、メタ関数が得られる。
+逆に Monad の中にある通常の戻り値のみに着目すると通常の関数に戻る。
+このように、Monad を用いたメタ計算の表現では通常の計算とメタ計算が一対
+一に対応する。
+
+一般的には複数の Monad の組み合わせが Monad になることを示すのは難しい。
+Gears OS では Code と Data を分離して、Code から他の Code への呼び出し
+を継続を用いて行う。
+Gears OS での Monad は Meta Code と Meta Data になる。
+
+% Code Gear
+% Data Gear
+% Meta Code Gear
+% Meta Data Gear
+\section{Code Gear と Data Gear}
+Gears OS ではプログラムの実行単位として様々な Gear を使う。
+Gear が平行実行の単位、データ分割、Gear 間の接続などになる。
+
+Code Gear はプログラムの実行コードそのものであり、Cuda
+の kernel に相当する。
+Code Gear は複数の Data Gear を参照し、一つまたは複数の Data Gear に書
+き込む。
+Code Gear は接続された Data Gear 以外には触らない。
+Code Gear はサブルーチンコールではないので、呼び出し元に戻る概念はない。
+その代わりに、次に実行する 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 へのポインタを持っている。
+
+% s/Segment/Gear
+
+% Context
+\section{継続}
+ある Code Gear から継続するときには、次に実行する Code Gear を名前で指
+定する。
+Meta Code Gear が名前を解釈して、処理を対応する Code Gear に引き渡す。
+これらは、従来の OS の Dynamic Loading Library や Command 呼び出しに対
+応する。
+名前と Code Gear へのポインタの対応は Meta Data Gear に格納される。
+この Meta Data Gear を Context と呼ぶことにする。
+これは従来の OS の Process や Thread に対応する。
+
+Context には以下のようなものが格納される。
+\begin{itemize}
+\item Code Gear の名前とポインタの対応表
+\item Data Gear の Allocation 用の情報
+\item Code Gear が参照する Data Gear へのポインタ
+\item Data Gear に格納される Data Type の情報
+\end{itemize}
+
+\lstinputlisting[caption=Context]{source/context.h}
+
+\textbf{Code Gear の名前とポインタの対応表}
+
+Code Gear の名前とポインタの対応は enum と関数ポインタによって表現される。
+これにより、実行時に比較ルーチンなどを動的に変更することが可能になる。
+
+\textbf{Data Gear の Allocation 用の情報}
+
+Context の生成時にある程度の領域を確保する。
+Context にはその領域へのポインタとサイズが格納されている。
+そのポインタを必要な Data Gear のサイズに応じて、インクリメントすることによって Data Gear の Allocation を実現する。
+
+\textbf{Code Gear が参照する Data Gear へのポインタ}
+
+Context には Data Gear へのポインタが格納されている。
+Code Gear は Context を通して Data Gear へアクセスする。
+
+\textbf{Data Gear に格納される Data Type の情報}
+
+Data Gear は union と struct によって表現される。
+Context には Data Gear の Data Type の情報が格納されている。
+この情報から確保する Data Gear のサイズなどを決定する。
+
+\lstinputlisting[caption=initContext]{source/context.c}
+
+% Persistent
+\section{Persistent Data Gear}
+Data Gear の管理には木構造を用いる。
+この木構造は非破壊で構築される。
+非破壊的木構造では、編集元の木構造を破壊することなく新しい木構造を構成する。
+破壊的木構造と異なりロックの必要がなく、平行して読み書き、参照を行うことが可能である。
+また、変更前の木構造をすべて保持しているので過去のデータにアクセスすることができる。
+
+\begin{figure}[!h]
+  \centering
+  \includegraphics[width=70mm]{images/nondestructive_tree_modification.pdf}
+  \caption{木構造の非破壊的編集}
+\end{figure}
+
+% allocator
+\section{Allocator}
+Gears OS では Context の生成時にある程度の領域を確保し、その領域を指すポインタをインクリメントすることで Allocation を実現する。
+
+Context には Allocation 用の Data Gear が格納されている。
+この Data Gear に確保するサイズと確保後に接続する Code Gear の名前を書き込み、Allocation を行う Code Gear に接続することで必要な領域を確保する。
+
+\lstinputlisting[caption=Allocator]{source/allocate.h}
+
+\section{}
 \nocite{*}
-%\nocite{opencl}
-%\nocite{opencl:ref}
-%\nocite{opencl:applied}
-%\nocite{yutaka:os}
 \bibliographystyle{ipsjunsrt}
 \bibliography{sigos}
-%\bibliography{cerium,book}
-
 
 \end{document}
--- a/paper/theory.tex	Mon May 04 18:50:22 2015 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-\section{Model Checking}