|
38
|
1 \documentclass[techrep]{ipsjpapers}
|
|
|
2 \usepackage[dvipdfmx]{graphicx}
|
|
|
3 \usepackage{url}
|
|
|
4 \usepackage{listings,jlisting}
|
|
|
5 \usepackage{enumitem}
|
|
|
6
|
|
|
7 \lstset{
|
|
|
8 language=C,
|
|
|
9 tabsize=2,
|
|
|
10 frame=single,
|
|
|
11 basicstyle={\ttfamily\footnotesize},%
|
|
|
12 identifierstyle={\footnotesize},%
|
|
|
13 commentstyle={\footnotesize\itshape},%
|
|
|
14 keywordstyle={\footnotesize\bfseries},%
|
|
|
15 ndkeywordstyle={\footnotesize},%
|
|
|
16 stringstyle={\footnotesize\ttfamily},
|
|
|
17 breaklines=true,
|
|
|
18 captionpos=b,
|
|
|
19 columns=[l]{fullflexible},%
|
|
|
20 xrightmargin=0zw,%
|
|
|
21 xleftmargin=1zw,%
|
|
|
22 aboveskip=1zw,
|
|
|
23 numberstyle={\scriptsize},%
|
|
|
24 stepnumber=1,
|
|
|
25 numbersep=0.5zw,%
|
|
|
26 lineskip=-0.5ex,
|
|
|
27 }
|
|
|
28 \renewcommand{\lstlistingname}{Code}
|
|
42
|
29 \usepackage{caption}
|
|
|
30 \captionsetup[lstlisting]{font={small,tt}}
|
|
38
|
31
|
|
|
32 \input{dummy.tex} %% Font
|
|
|
33
|
|
|
34 % ユーザが定義したマクロなど．
|
|
|
35 \makeatletter
|
|
|
36
|
|
|
37 \begin{document}
|
|
|
38
|
|
|
39 % 和文表題
|
|
|
40 \title{Gears OS のモジュール化と並列 API}
|
|
|
41 % 英文表題
|
|
|
42 \etitle{}
|
|
|
43
|
|
|
44 % 所属ラベルの定義
|
|
|
45 \affilabel{1}{琉球大学大学院理工学研究科情報工学専攻 \\Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}
|
|
|
46 \affilabel{2}{琉球大学工学部情報工学科\\Information Engineering, University of the Ryukyus.}
|
|
|
47
|
|
|
48 % 和文著者名
|
|
|
49 \author{
|
|
|
50 宮城 光希\affiref{1}
|
|
|
51 \and
|
|
56
|
52 桃原 優 \affiref{1}
|
|
|
53 \and
|
|
38
|
54 河野 真治\affiref{2}
|
|
|
55 }
|
|
|
56
|
|
|
57 % 英文著者名
|
|
|
58 \eauthor{
|
|
|
59 Mitsuki MIYAGI\affiref{1}
|
|
|
60 \and
|
|
56
|
61 Yu TOBARU\affiref{1}
|
|
|
62 \and
|
|
38
|
63 Shinji KONO\affiref{2}
|
|
|
64 }
|
|
|
65
|
|
|
66 % 連絡先（投稿時に必要．製版用では無視される．）
|
|
|
67 \contact{宮城 光希\\
|
|
|
68 〒903-0213 沖縄県西原町千原1番地\\
|
|
|
69 琉球大学工学部情報工学科\\
|
|
|
70 TEL: (098)895-2221\qquad FAX: (098)895-8727\\
|
|
|
71 email: mir3636@cr.ie.u-ryukyu.ac.jp}
|
|
|
72
|
|
|
73 % 和文概要
|
|
|
74 \begin{abstract}
|
|
|
75 現代の OS では拡張性と信頼性を両立させることが要求されている。
|
|
|
76 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。
|
|
|
77 Gears OS は Continuation based C によってアプリケーションと OS そのものを記述する。
|
|
|
78 CbC はこの Code Gear と Data Gear の単位でプログラムを記述する。
|
|
|
79 システムやアプリケーションを記述するためにCode Gear と Data Gear を柔軟に再利用する必要がある。
|
|
|
80 このときに機能を接続するAPIと実装の分離が可能であることが望ましい。
|
|
|
81 Gears OS の信頼性を保証するために、形式化されたモジュールシステムを提供する必要がある。
|
|
45
|
82 本論文では、Interface を用いたモジュールシステムの説明とその応用としての並列 API について考察する。
|
|
38
|
83 並列APIは継続を基本とした関数型プログラミングと両立する必要がある。
|
|
|
84 ここでは、CbC の goto 文を拡張したpar goto 文を導入する。
|
|
|
85 par goto では並列実行のための実行 Context を生成し、TaskScheduler に登録する。
|
|
|
86 Gears OS での同期機構はData Gear の待ち合わせとして定義する。
|
|
|
87 メタレベルではこれらの同期機能はCASとそれを用いて実装した Synchronized Queue になる。
|
|
|
88 これらの Queue も Interface を用いてモジュール化されている。
|
|
|
89 モジュール化の詳細と、有効性について考察する。
|
|
|
90 \end{abstract}
|
|
|
91
|
|
|
92 % 英文概要
|
|
|
93 \begin{eabstract}
|
|
|
94 \end{eabstract}
|
|
|
95
|
|
|
96 % 表題などの出力
|
|
|
97 \maketitle
|
|
|
98
|
|
|
99 % 本文はここから始まる
|
|
|
100
|
|
40
|
101 \section{OS の拡張性と信頼性の両立}
|
|
|
102
|
|
43
|
103 さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩する
|
|
41
|
104 ハードウェア、サービスに対応して OS 自体が拡張される必要がある。
|
|
|
105 OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分であり、テストしきれない部分が残ってしまう。
|
|
|
106 これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
|
|
|
107 モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている
|
|
40
|
108 図\ref{fig:verification}。
|
|
|
109 \begin{figure}[ht]
|
|
|
110 \begin{center}
|
|
|
111 \includegraphics[width=70mm]{./pic/verification.pdf}
|
|
|
112 \end{center}
|
|
|
113 \caption{証明とモデル検査によるOSの検証}
|
|
|
114 \label{fig:verification}
|
|
|
115 \end{figure}
|
|
|
116
|
|
41
|
117 証明やモデル検査を用いて OS を検証する方法はさまざまなものが検討されている。
|
|
|
118 検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。
|
|
|
119 つまり信頼性と拡張性を両立させることが重要である。
|
|
40
|
120
|
|
41
|
121 コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意味論の定義などで規定される。
|
|
|
122 プログラミング言語で記述される部分をノーマルレベルの計算と呼ぶ。
|
|
|
123 コードが実行される時には、処理系の詳細や使用する資源、あるいは、コードの仕様や型などの言語以外の部分が服属する。
|
|
|
124 これをメタレベルの計算という。
|
|
|
125 この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼性をメタレベルから保証できるようにしたい。
|
|
40
|
126 ノーマルレベルでの正当性を保証しつつ、新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。
|
|
|
127
|
|
55
|
128 ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。
|
|
41
|
129 CbC は関数呼出時の暗黙の環境(Environment)を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。
|
|
|
130 これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。
|
|
|
131 これらを用いて、検証された Gears OS を構築したい。
|
|
40
|
132 図\ref{fig:MetaGear}。
|
|
55
|
133 検証には定理証明支援系である Agda を用いる。
|
|
|
134 Gears の記述をモジュール化するために Interface を導入した。
|
|
|
135 さらに並列処理の記述用にpar goto 構文を導入する。
|
|
|
136 これらの機能は Agda 上で継続を用いた関数型プログラムに対応するようになっている。
|
|
40
|
137 \begin{figure}[ht]
|
|
|
138 \begin{center}
|
|
|
139 \includegraphics[width=70mm]{./pic/MetaGear.pdf}
|
|
|
140 \end{center}
|
|
|
141 \caption{Gearsのメタ計算}
|
|
|
142 \label{fig:MetaGear}
|
|
|
143 \end{figure}
|
|
|
144
|
|
55
|
145 本論文では Interface と par goto の実装の詳細を記述し評価を行った。
|
|
|
146 マルチ CPU と GPU 上での par goto 文の実行を確認した。
|
|
|
147 %Go言語に比べて並列構文 par goto が遅いことがわかった。
|
|
40
|
148
|
|
55
|
149 \section{Gears におけるメタ計算}
|
|
|
150 Gears OS ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を用いる。
|
|
59
|
151 Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実現する。図\ref{fig:metaCS}
|
|
|
152
|
|
|
153 \begin{figure}[ht]
|
|
|
154 \begin{center}
|
|
|
155 \includegraphics[width=70mm]{./pic/metaCS.pdf}
|
|
|
156 \end{center}
|
|
|
157 \caption{Gears でのメタ計算}
|
|
|
158 \label{fig:metaCS}
|
|
|
159 \end{figure}
|
|
38
|
160
|
|
55
|
161 CbC は軽量継続 (goto文) による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。
|
|
|
162 CbC は LLVM\cite{llvm} と GCC\cite{gcc} 上で実装されている。
|
|
|
163 メタレベルの記述は Perl スクリプトによって生成される stub と goto meta によって Code Gear で記述される。
|
|
38
|
164
|
|
|
165 Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。
|
|
|
166 Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。
|
|
55
|
167 Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
|
|
|
168 Interface の操作に対応する Code Gear の引数は Interface に定義されている Data Gear を通して指定される。
|
|
|
169 一つの実行スレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。
|
|
|
170 この Meta Data Gear を Context という。
|
|
|
171 ノーマルレベルでは Context を直接見ることはできない。
|
|
38
|
172
|
|
55
|
173 Code Gear の継続は関数型プログラミングからみると継続先の Context を含む Closure となっている。
|
|
59
|
174 これを記述するために継続に不定長引数を追加する構文をスクプリトの変換機能として用意した。Code \ref{varargnext}
|
|
55
|
175 メタ計算側ではこれらの Context を常に持ち歩いているので goto 文で引数を用いることはなく、
|
|
|
176 行き先は Code Gear の番号のみで指定される。
|
|
38
|
177
|
|
58
|
178 \lstinputlisting[label=varargnext, caption=不定長引数を持つ継続]{./src/varargnext.cbc}
|
|
55
|
179
|
|
|
180 これにより Interface 間の呼び出しを C++ のメソッド呼び出しのように記述することができる。
|
|
|
181 Interface の実装は、Context 内に格納されているので、オブジェクトごとに実装を変える多様性を実現できている。
|
|
|
182 呼び出された Code Gear は必要な引数を Context から取り出す必要がある。
|
|
|
183 これは スクリプトで生成された stub Meta Code Gear で行われる。
|
|
38
|
184 Gears OS でのメタ計算は stub と goto のメタ計算の2箇所で実現される。
|
|
|
185
|
|
55
|
186 Context を複製して複数の CPU に割り当てることにより並列実行を可能になる。
|
|
|
187 これによりメタ計算として並列処理を記述したことになる。
|
|
|
188 Gears のスレッド生成は Agda の関数型プログラミングに対応して行われるのが望ましい。
|
|
|
189 そこで、par goto 構文を導入し、Agda の継続呼び出しに対応させることにした。
|
|
|
190 par goto では Context の複製、入力の同期、タスクスケジューラーへの Context の登録などが行われる。
|
|
|
191 par goto 文の継続として、スレッドの join に相当する \_\_exit を用意した。
|
|
|
192 \_\_exit により par goto で分岐した Code Gear の出力を元のスレッドで受け取ることができる。
|
|
|
193
|
|
|
194 関数型プログラムではメモリ管理は GC などを通して暗黙に行われる。
|
|
|
195 Gears OS ではメモリ管理は stub などのメタ計算部分で処理される。
|
|
|
196 例えば、寿命の短いスレッドでは使い捨ての線形アロケーションを用いる。
|
|
38
|
197
|
|
56
|
198 %Meta Code Gear は通常の Code Gear の直後に遷移され、メタ計算を実行する。
|
|
|
199 %これを図示したものが図\ref{fig:metaCS}である。
|
|
38
|
200
|
|
|
201 \section{Gears OS の構成}
|
|
|
202 Gears OS は以下の要素で構成される。
|
|
|
203
|
|
|
204 \begin{itemize}
|
|
|
205 \item Context
|
|
|
206 \item TaskQueue
|
|
|
207 \item TaskManager
|
|
|
208 \item Worker
|
|
|
209 \end{itemize}
|
|
|
210
|
|
|
211 図\ref{fig:gearsos} に Gears OS の構成図を示す。
|
|
|
212
|
|
|
213 \begin{figure}[ht]
|
|
|
214 \begin{center}
|
|
|
215 \includegraphics[width=70mm]{./pic/gears_structure}
|
|
|
216 \end{center}
|
|
|
217 \caption{Gears OS の構成図}
|
|
|
218 \label{fig:gearsos}
|
|
|
219 \end{figure}
|
|
|
220
|
|
|
221 Data Gear は union と struct によって表現される。
|
|
|
222 Context には Data Gear の Data Type の情報が格納されている。
|
|
|
223 この情報から確保する Data Gear のサイズなどを決定する。
|
|
|
224
|
|
40
|
225 Context は Task でもあり、Taskは通常のOSのスレッドに対応する。
|
|
|
226 Task は実行する Code Gear と Data Gear をすべて持っている。
|
|
43
|
227 TaskManager は Task を実行する Worker の生成、管理、Task の送信を行う。
|
|
40
|
228 Gears OS における Task Queue は Synchronized Queue で実現される。
|
|
43
|
229 Worker は TaskQueue から Task である Context を取得し、Task の Code Gear を実行し、Output Data Gear の書き出しを行っている。
|
|
|
230 Input/Output Data Gear の依存関係が解決されたものから並列実行される。
|
|
38
|
231
|
|
40
|
232 \section{Interface}
|
|
|
233 Interface は呼び出しの引数になる Data Gear の集合であり、そこで呼び出される Code Gear のエントリである。
|
|
|
234 呼び出される Code Gear の引数となる Data Gear はここで全て定義される。
|
|
38
|
235
|
|
40
|
236 Code\ref{interface}は stack の Interface である。
|
|
|
237 Code Gear、Data Gear に参照するために Context を通す必要があるが、
|
|
|
238 Interface を記述することでデータ構造の api と Data Gear を結びつけることが出来る。
|
|
38
|
239
|
|
40
|
240 \lstinputlisting[label=interface, caption=StackのInterface]{./src/Stack.cbc}
|
|
38
|
241
|
|
52
|
242 Code\ref{implement}は stack の実装の例である。
|
|
|
243 createImpl は関数呼び出しで呼び出され、初期化と Code Gear のスロットに対応する Code Gear の番号を入れる。
|
|
38
|
244
|
|
52
|
245 \lstinputlisting[label=implement, caption=SingleLinkedStackの実装]{./src/stackimpl.cbc}
|
|
38
|
246
|
|
40
|
247 \section{stub Code Gear の生成}
|
|
|
248
|
|
38
|
249 stub Code Gear は Code Gear 間の継続に挟まれる Code Gear が必要な Data Gear を Context から取り出す処理を行うものである。
|
|
|
250 Code Gear 毎に記述する必要があり、そのCode Gear の引数を見て取り出す Data Gear を選択する。
|
|
|
251 stub Code Gear を 自動生成する generate stub を Perl スクリプトで作成することによって Code Gear の記述量を約半分にすることができる。
|
|
|
252
|
|
|
253 stub を生成するために generate\_stub は指定された cbc ファイルの \_\_code型である Code Gear を取得し、引数から必要な Data Gear を選択する。
|
|
|
254 generate\_stub は引数と interface を照らし合わせ、Gearef または GearImpl を決定する。
|
|
|
255 また、この時既に stub Code Gear が記述されている Code Gear は無視される。
|
|
|
256
|
|
|
257 cbc ファイルから、生成した stub Code Gear を加えて stub を加えたコードに変換を行う。(Code\ref{stack_c})
|
|
|
258
|
|
40
|
259 \lstinputlisting[label=stack_c, caption=stub Code Gear を加えたコード]{./src/ex_stub}
|
|
38
|
260
|
|
|
261 \section{Context の生成}
|
|
|
262 generate\_context は Context.h、Interface.cbc、generate\_stub で生成されたImpl.cbc を見て Context を生成する Perl スクリプトである。
|
|
|
263
|
|
|
264 \begin{figure}[ht]
|
|
|
265 \begin{center}
|
|
|
266 \includegraphics[width=70mm]{./pic/generate_context3.pdf}
|
|
|
267 \end{center}
|
|
|
268 \caption{generate\_context による Context の生成}
|
|
|
269 \label{fig:gc}
|
|
|
270 \end{figure}
|
|
|
271
|
|
|
272 Context は Meta Data Gear に相当し、Code Gear や Data Gear を管理している。
|
|
|
273
|
|
|
274 generate\_context は context の定義 (Code\ref{context}) を読み宣言されている Data Gear を取得する。
|
|
|
275 Code Gear の取得は指定された generate\_stub で生成されたコードから \_\_code 型を見て行う。
|
|
|
276 取得した Code Gear、Data Gear の enum の定義は enumCode.h、enumData.h に生成される。
|
|
|
277
|
|
|
278 Code/Data Gear の名前とポインタの対応は generate\_context によって生成される enum Code、enum Data を指定することで接続を行う。
|
|
49
|
279 また、generate context は取得した Code/Data Gear から initContext の生成も行う。
|
|
38
|
280
|
|
|
281 Context には Allocation 等で生成した Data Gear へのポインタが格納されている。
|
|
|
282 Code Gear は Context を通して Data Gear へアクセスする。
|
|
|
283 Data Gear の Allocation を行うコードは dataGearInit.cに生成される。
|
|
|
284
|
|
|
285
|
|
43
|
286 \section{Gears OS の並列処理}
|
|
|
287 Gears OS では実行の Task を Code Gear と Input/Output Data Gear の組で表現する。
|
|
|
288 Input/Output Data Gear によって依存関係が決定し、それにそって並列実行を行う。
|
|
|
289 Gears OS では 並列実行する Task を Context で表現する。
|
|
|
290 Context には Task 用の情報として、実行される Code Gear、Input/Output Data Gear の格納場所、待っている Input Data Gear のカウンタ等を持っている
|
|
|
291 Task の Input Data Gear が揃っているかを TaskManager で判断し、 実行可能な Task を Worker に送信する。
|
|
|
292 Worker は送信された Task が指定した Code Gear を実行し、Output Data Gear を書き出す。
|
|
|
293
|
|
|
294 \section{SynchronizedQueue}
|
|
|
295 SynchronizedQueue は Worker の Queue として使用される。
|
|
|
296 Worker の Queue は TaskManager を経由して Task を送信するスレッドと Task を取得する Worker 自身のスレッドで扱われる。
|
|
|
297 そのため SynchronizedQueue はマルチスレッドでもデータの一貫性を保証する Queue を実装する必要がある。
|
|
|
298
|
|
|
299 データの一貫性を保証する解決例としての 1 つとしてロックを使った解決方法がある。
|
|
|
300 しかし、ロックを行ってデータを更新した場合、同じ Queue に対して操作を行う際に待ち合わせが発生し、全体の並列度が下がってしまう。
|
|
|
301 そこで、Gears OS ではデータの一貫性を保証するために CAS(Check and Set、Compare and Swap) を利用した Queue を実装している。
|
|
|
302 CAS は値の比較、更新をアトミックに行う命令である。
|
|
|
303 CAS を使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じならデータ競合がないため、データの更新に成功する。
|
|
|
304 異なる場合は他に書き込みがあったとみなされ、値の更新に失敗する。
|
|
|
305
|
|
46
|
306 Gears OS ではこの CAS を行うための Interface を定義している(Code\ref{atomicInterface})。
|
|
45
|
307 この Interface では、Data Gear 全てを内包している Data 共用体のポインタの値を更新する CAS を定義して
|
|
46
|
308 いる(Code\ref{atomicInterface} 6行目)。
|
|
45
|
309
|
|
46
|
310 \lstinputlisting[label=atomicInterface, caption=AtomicInterface]{./src/atomicInterface.h}
|
|
45
|
311
|
|
46
|
312 AtomicInterface での CAS の実際の実装を Code\ref{atomicImpl} に示す。
|
|
|
313 実際の実装では \_\_sync\_bool\_compare\_and\_swap 関数を呼び出すことで CAS を行う(Code\ref{atomicImpl} 2行目)。
|
|
45
|
314 この関数は第一引数に渡されたアドレスに対して第二引数の値から第三引数の値ヘ CAS を行う。
|
|
|
315 CAS に成功した場合、true を返し、失敗した場合は false を返す。
|
|
46
|
316 Code\ref{atomicImpl} では CAS に成功した場合と失敗した場合それぞれに対応した Code Gear へ継続する。
|
|
45
|
317
|
|
46
|
318 \lstinputlisting[caption=CAS の実装, label=atomicImpl]{./src/atomicImpl.cbc}
|
|
45
|
319
|
|
46
|
320 SynchronizedQueue の Data Gear の定義を Code\ref{synchronizedQueue} に示す。
|
|
45
|
321 SynchronizedQueue はデータのリストの先頭と、終端のポインタを持っている。
|
|
|
322 Queue を操作する際はこのポインタに対して CAS をすることでデータの挿入と取り出しを行う。
|
|
|
323
|
|
46
|
324 \lstinputlisting[caption=SynchronizedQueue の定義, label=synchronizedQueue]{./src/synchronizedQueue.h}
|
|
45
|
325
|
|
43
|
326 \section{並列構文}
|
|
51
|
327 Gears OS の並列構文は par goto文で用意されている(Code\ref{pargoto})。
|
|
|
328 \lstinputlisting[caption=par goto による並列実行, label=pargoto]{./src/parGotoCreateTask.cbc}
|
|
43
|
329 par goto の引数には Input/Output Data Gear と 実行後に継続する \_\_exit を渡す。
|
|
|
330 par goto で生成された Task は \_\_exit に継続することで終了する。
|
|
44
|
331 par goto文でも 通常の goto 分と同様にメタへの goto 文へ置き換えられるが、par goto 文では通常の goto 文とは異なるメタへと継続する。
|
|
43
|
332 Gears OS の Task は Output Data Gear を生成した時点で終了するので、par goto では直接 \_\_exit に継続するのではなく、
|
|
|
333 Output Data Gear への書き出し処理(Commit)に継続される。
|
|
|
334
|
|
44
|
335 Code Gear は Input に指定した Data Gear が全て書き込まれると実行され、実行した結果を Output に指定した Data Gear に書き出しを行う。
|
|
|
336 Code Gear の引数である\_\_next が持つ引数の Data Gear が Output Data Gear となる。
|
|
|
337
|
|
43
|
338 書き出し処理は Data Gear の Queue から、依存関係にある Task を参照する。
|
|
44
|
339 参照した Task が持つ実行に必要な Input Data Gear カウンタのデクリメントを行う。
|
|
43
|
340 カウンタが0になると Task が待っている Input Data Gear が揃ったことになり、
|
|
|
341 その Task を TaskManager 経由で 実行される Worker に送信する。
|
|
|
342
|
|
|
343 この par goto 文は通常のプログラミングの関数呼び出しのように扱うことができる。
|
|
|
344
|
|
|
345
|
|
57
|
346 %\section{比較}
|
|
|
347 %
|
|
|
348 %従来のプログラミングスタイルとの比較。
|
|
|
349 %Gears のプログラミングは関数呼出を中心とするプログラミングとはかなり異なる。
|
|
|
350 %Gears は関数呼出を禁止しているわけではなく、使用する資源の制御に問題がないなら普通に関数呼出して良い。
|
|
|
351 %%Linux kernel などでは関数呼出の大半はインライン展開されることを期待してプログラミングされており、
|
|
|
352 %関数呼出で予測できないスタックの爆発やCPU資源の浪費が起きないようにプログラミングされている。
|
|
|
353 %Gears では Gears 間のプログラミングは戻り先や使用する資源を明示する必要がある。
|
|
|
354 %
|
|
|
355 %goto 文での引数は通常の関数呼出と異なり、スタック(環境)に積むことができない。引数に必要な情報を含むData Gearを
|
|
|
356 %持ち歩くスタイルとなる。一つのインタフェース内部では、これらは共通している。実際、これらはメタレベルでは、
|
|
|
357 %Context というMeta Data Gear にすべて格納されている。メタレベルは、Data Gear の詳細な型は使用されない。
|
|
|
358 %ノーマルレベルに移行する際に stub Code Gear を通して詳細な型が接続される。
|
|
|
359 %
|
|
|
360 %インタフェースを再利用する際には、呼び出すインタフェースが持つ引数は保存される必要がある。これらは、実際には
|
|
|
361 %Context 内にあるので自動的に保存されている。ノーマルレベルの記述では、... の部分にその意味が込めれている。
|
|
|
362 %これは、可変長引数の...と同じ意味だと考えても良い。ただ、LLVM/GCC レベルでそれを実装するのは比較的難しい。
|
|
|
363 %なので、今回はScriptによる変換を採用している。
|
|
|
364 %
|
|
|
365 %ノーマルレベルの記述と関数型プログラミングの記述の比較。Gear は必ず継続を渡す必要がある。これは一段の
|
|
|
366 %関数呼出を許しているのと同等である。70年代の Fortan の関数呼出は決まった場所に戻り先を格納するので
|
|
|
367 %再起呼出ができなかったのと同じである。例えば Code Gears 以下のような型を持つ。ここで t は継続の型である。
|
|
|
368 %Stack は Stack を受けとる Stack \verb|->| t という Code Gear を継続として引数で受けとる。popStack はこの引数を
|
|
|
369 %呼び出す。
|
|
|
370 %
|
|
|
371 %\verb|popStack : {a t : Set} -> Stack |
|
|
|
372 %
|
|
|
373 %\verb| -> (Stack -> t) -> t|
|
|
|
374 %
|
|
|
375 %つまり、Code Gear は制限された関数の形式を持っている。Data Gear は、関数型言語の直積や排他的論理和(Sum)を含むデータ型に
|
|
|
376 %対応する。しかし、一つの Context で実行される Data Gear は、一つの巨大なSumに含まれるようになっている。これを
|
|
|
377 %メタレベルでは、中の型の詳細に立ち入ることなく実行する。
|
|
|
378 %
|
|
|
379 %%Context はノーマルレベル のData Gear の他に様々なメタ情報を持つ。例えば、メモリ管理情報や実行される CPU 、あるいは、Task の
|
|
|
380 %状態、待ち合わせている Data Gear などである。これらの情報は C やアセンブラのレベルで実装されるのと同時に、通常の Gear の
|
|
|
381 %プログラミングにも対応する。例えば、CPU をかそうてきに Gears で記述すればソフトウェア的な並列実行を実現し、実際の
|
|
|
382 %GPU を用いれば GPU による並列実行となる。この実行をモデル検査的な状態数え上げに対応させればモデル検査を実行できる。
|
|
|
383 %
|
|
|
384 %Haskell などを実行可能仕様記述として用いる OS の検証\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}と、Code Gear を用いる手法は類似>しているが、Code Gear の場合は、
|
|
|
385 %記述を制限し、Code と仕様の対応、さらにCodeと資源の対応が明確になる利点がある。
|
|
|
386 %
|
|
|
387 %型つきアセンブラ\cite{Yang:2010:SLI:1806596.1806610}は、より低レベルの関数型の記述であると言える。アセンブラの記述自体は小さく扱いやすいが、
|
|
|
388 %OS レベルあるいはアプリケーションレベルからの距離が大きい。型の整合性を保証するだけでは OS の検証としては
|
|
|
389 %不十分なので、証明やモデル検査を用いることになるが、記述量が多いのが、その際に欠点となる。
|
|
|
390 %Code Gear は、より大きな単位であり、プログラミングレベルの抽象化が可能になっているので、これらの記述の
|
|
|
391 %大きさの欠点をカバーできる可能性がある。
|
|
|
392 %
|
|
|
393 %証明手法は、従来では Hoare Logic \cite{Chen:2015:UCH:2815400.2815402}のような Post Condition / Pre Condition を用いる方法が使われている。
|
|
|
394 %現在のGearsは、Agda への変換は考えているが、その上の具体的な証明方法はまだ用意されていない。
|
|
|
395 %
|
|
40
|
396
|
|
57
|
397 \section{Gears OS の評価}
|
|
|
398
|
|
|
399 \subsection{実験環境}
|
|
|
400 今回 Twice、 BitonicSort をそれぞれ CPU、GPU環境で Gears OS の測定を行う。
|
|
|
401
|
|
|
402 使用する実験環境を表\ref{tab:powerEdge}、 GPU 環境を表\ref{tab:gtx1070} に示す。
|
|
|
403 また、今回は LLVM/Clang で実装した CbC コンパイラを用いて Gears OS をコンパイルする。
|
|
40
|
404
|
|
57
|
405 \begin{table}[htbp]
|
|
|
406 \begin{center}
|
|
|
407 \begin{tabular}{|l|l|} \hline
|
|
|
408 Model & Dell PowerEdgeR630 \\ \hline
|
|
|
409 OS & CentOS 7.4.1708 \\ \hline
|
|
|
410 Memory & 768GB \\ \hline
|
|
|
411 CPU & 2 x 18-Core Intel Xeon 2.30GHz \\ \hline
|
|
|
412 \end{tabular}
|
|
|
413 \caption{実行環境}
|
|
|
414 \label{tab:powerEdge}
|
|
|
415 \end{center}
|
|
|
416 \end{table}
|
|
|
417
|
|
|
418 \begin{table}[htbp]
|
|
|
419 \begin{center}
|
|
|
420 \begin{tabular}{|l||l|} \hline
|
|
|
421 GPU & GeForce GTX 1070 \\ \hline
|
|
|
422 Cores & 1920 \\ \hline
|
|
|
423 Clock Speed & 1683MHz \\ \hline
|
|
|
424 Memory Size & 8GB GDDR5 \\ \hline
|
|
|
425 Memory Bandwidth & 256GB/s \\ \hline
|
|
|
426 \end{tabular}
|
|
|
427 \caption{GPU 環境}
|
|
|
428 \label{tab:gtx1070}
|
|
|
429 \end{center}
|
|
|
430 \end{table}
|
|
|
431
|
|
|
432 \subsection{Twice}
|
|
|
433 Twice は与えられた整数配列のすべての要素を2倍にする例題である。
|
|
40
|
434
|
|
57
|
435 Twice の Task は Gears OS のデータ並列で実行される。
|
|
|
436 CPU の場合は配列ある程度の範囲に分割してTaskを生成する。
|
|
|
437 これは要素毎に Task を生成するとその分の Context を生成するために時間を取ってしまうからである。
|
|
|
438
|
|
|
439 Twice は並列実行の依存関係もなく、データ並列での実行に適した課題である。
|
|
|
440 そのため、 通信時間を考慮しなければ CPU よりコア数が多い GPU が有利となる。
|
|
|
441
|
|
|
442 要素数$2^{27}$ のデータに対する Twice の実行結果を 表\ref{tab:wice}、図\ref{fig:twice}に示す。
|
|
|
443 CPU 実行の際は $2^{27}$ のデータを 64個のTask に分割して並列実行を行っている。
|
|
|
444 GPU では1次元の block 数を $2^{15}$、 block 内の thread 数を $2^{10}$ で kernel の実行を行った。
|
|
|
445 ここでの ``GPU`` は CPU、GPU 間のデータの通信時間も含めた時間、 ``GPU(kernel only)`` は kernel のみの実行時間である。
|
|
40
|
446
|
|
57
|
447 \begin{table}[htbp]
|
|
|
448 \begin{center}
|
|
|
449 \begin{tabular}{|l||l|} \hline
|
|
|
450 Processor & Time(ms) \\ \hline
|
|
|
451 1 CPU & 1181.215 \\ \hline
|
|
|
452 2 CPUs & 627.914 \\ \hline
|
|
|
453 4 CPUs & 324.059 \\ \hline
|
|
|
454 8 CPUs & 159.932 \\ \hline
|
|
|
455 16 CPUs & 85.518\\ \hline
|
|
|
456 32 CPUs & 43.496 \\ \hline
|
|
|
457 GPU & 127.018\\ \hline
|
|
|
458 GPU(kernel only)& 6.018 \\ \hline
|
|
|
459 \end{tabular}
|
|
|
460 \caption{$2^{27}$ のデータに対する Twice}
|
|
|
461 \label{tab:twice}
|
|
|
462 \end{center}
|
|
|
463 \end{table}
|
|
40
|
464
|
|
57
|
465 \begin{figure}[htbp]
|
|
|
466 \begin{center}
|
|
|
467 \includegraphics[width=70mm]{./pic/twice.pdf}
|
|
|
468 \end{center}
|
|
|
469 \caption{$2^{27}$ のデータに対する Twice}
|
|
|
470 \label{fig:twice}
|
|
|
471 \end{figure}
|
|
|
472
|
|
|
473 ある程度の台数効果があると考えられる。
|
|
|
474
|
|
|
475 GPU での実行は kernel のみの実行時間は 32 CPU に比べて 約 7.2 倍の速度向上が見られた。
|
|
|
476 しかし、通信時間を含めると 16 CPU より遅い結果となってしまった。
|
|
|
477 CPU、GPU の通信時間かオーバーヘッドになっている事がわかる。
|
|
40
|
478
|
|
57
|
479 \subsection{BitonicSort}
|
|
|
480 BitonicSort は並列処理向けのソートアルゴリズムである。
|
|
|
481 代表的なソートアルゴリズムである Quick Sort も並列処理 を行うことが可能であるが、 QuickSort では ソートの過程で並列度が変動するため、台数効果が出づらい。
|
|
|
482 一方でBitonic Sort は最初から最後まで並列度が変わらずに並列処理を行う。
|
|
|
483 図\ref{fig:bitonicNetwork} は要素数8のデータに対する BitonicSort のソートネットワークである。
|
|
|
484
|
|
|
485 \begin{figure}[htbp]
|
|
|
486 \begin{center}
|
|
|
487 \includegraphics[width=70mm]{./pic/bitonicNetwork.pdf}
|
|
|
488 \end{center}
|
|
|
489 \caption{要素数8の BitonicNetwork}
|
|
|
490 \label{fig:bitonicNetwork}
|
|
|
491 \end{figure}
|
|
|
492
|
|
|
493 BitonicSort はステージ毎に決まった2点間の要素の入れ替えを並列に実行することによってソートを行う。
|
|
|
494 Gears OS ではこのステージ毎に Output Data Gear を書き出し、 次のステージの Code Gear の Input Data Gear として記述することで BitonicSort を実現する。
|
|
40
|
495
|
|
57
|
496 要素数$2^{24}$ のデータに対する BitonicSort の実行結果を 表\ref{tab:bitonicSort}、図\ref{fig:bitonicSort}に示す。
|
|
|
497 こちらも Twice と同じくCPU 実行の際は $2^{24}$ のデータを 64個のTask に分割して並列実行を行っている。
|
|
|
498 つまり生成される Task は 64 * ステージ数 となる。
|
|
|
499 GPU では1次元の block 数を $2^{14}$、 block 内の thread 数を $2^{10}$ で kernel の実行を行った。
|
|
|
500
|
|
|
501 \begin{table}[htbp]
|
|
|
502 \begin{center}
|
|
|
503 \begin{tabular}{|l||l|} \hline
|
|
|
504 Processor & Time(s) \\ \hline
|
|
|
505 1 CPU & 41.416 \\ \hline
|
|
|
506 2 CPUs & 23.340\\ \hline
|
|
|
507 4 CPUs & 11.952\\ \hline
|
|
|
508 8 CPUs & 6.320\\ \hline
|
|
|
509 16 CPUs & 3.336\\ \hline
|
|
|
510 32 CPUs & 1.872\\ \hline
|
|
|
511 GPU & 5.420\\ \hline
|
|
|
512 GPU(kernel only)& 0.163\\ \hline
|
|
|
513 \end{tabular}
|
|
|
514 \caption{$2^{24}$ のデータに対する BitonicSort}
|
|
|
515 \label{tab:bitonicSort}
|
|
|
516 \end{center}
|
|
|
517 \end{table}
|
|
|
518
|
|
|
519 \begin{figure}[htbp]
|
|
|
520 \begin{center}
|
|
|
521 \includegraphics[width=70mm]{./pic/bitonicSort.pdf}
|
|
|
522 \end{center}
|
|
|
523 \caption{$2^{24}$ のデータに対する BitonicSort}
|
|
|
524 \label{fig:bitonicSort}
|
|
|
525 \end{figure}
|
|
40
|
526
|
|
57
|
527 1 CPU と 32 CPU で 約22.12 倍 の速度向上が見られた。
|
|
|
528 GPU では通信時間を含めると 8 CPU の約1.16倍となり、 kernel のみの実行では 32 CPU の約11.48倍となった。
|
|
|
529 現在の Gears OS の CUDA 実装では、 Output Data Gear を書き出す際に一度 GPU から CPU へ kernel の実行結果の書き出しを行っており、その処理の時間で差が出たと考えられ
|
|
|
530 る。
|
|
|
531 GPU で実行される Task 同士の依存関係の解決の際はCuDevicePtr などのGPU のメモリへのポインタを渡し、CPU でデータが必要になったときに初めて GPU から CPU へデータの通
|
|
|
532 信を行うメタ計算の実装が必要となる。
|
|
|
533
|
|
|
534 \subsection{OpenMP との比較}
|
|
|
535 OpenMP\cite{openmp} は C、 C++ のプログラムにアノテーションを付けることで並列化を行う。
|
|
|
536 アノテーションを Code \ref{code:openMP} のように for 文の前につけることで、ループの並列化を行う。
|
|
|
537
|
|
|
538 \lstinputlisting[caption=OpenMP での Twice, label=code:openMP]{./src/openMP.c}
|
|
40
|
539
|
|
57
|
540 OpenMP は既存のコードにアノテーションを付けるだけで並列化を行えるため、変更が少なくて済む。
|
|
|
541 しかし、 ループのみの並列化ではプログラム全体の並列度が上がらずアムダールの法則により性能向上が頭打ちになってしまう。
|
|
|
542 OpenMP はループの並列化 ではなくブロック単位での並列実行もサポートしているが、アノテーションの記述が増えてしまう。
|
|
|
543 また、 OpenMPはコードとデータを厳密に分離していないため、データの待ち合わせ処理をバリア等のアノテーションで記述する。
|
|
|
544
|
|
|
545 Gears OS では Input Data Gear が揃った Code Gear は並列に実行されるため、プログラム全体の並列度を高めることが出来る。
|
|
|
546 また 並列処理のコードとデータの依存関係を par goto 文で簡潔に記述することが出来る。
|
|
|
547
|
|
|
548 Gears OS と OpenMP で実装した Twice の実行結果の比較を図\ref{fig:vsopenmp} に示す。
|
|
|
549 実行環境は 表\ref{tab:powerEdge}、 $2^{27}$ のデータに対して行い、Gears OS 側は配列を 64個のTaskに分割し、OpenMP は for 文を static スケジュールで並列実行した。
|
|
|
550 static スケジュールはループの回数をプロセッサーの数で分割し、並列実行を行う openMP のスケジュール方法である。
|
|
|
551
|
|
|
552 \begin{figure}[htbp]
|
|
|
553 \begin{center}
|
|
|
554 \includegraphics[width=70mm]{./pic/vsopenmp.pdf}
|
|
|
555 \end{center}
|
|
|
556 \caption{vs OpenMP}
|
|
|
557 \label{fig:vsopenmp}
|
|
|
558 \end{figure}
|
|
40
|
559
|
|
57
|
560 実行結果として OpenMP は 1CPUと 32CPU で約10.8 倍の速度向上がみられた。
|
|
|
561 一方 Gears OS では約 27.1 倍の速度向上のため、台数効果が高くなっている。
|
|
|
562 しかし、Gears OS は 1CPU での実行時間がOpenMP に比べて大幅に遅くなっている。
|
|
|
563
|
|
|
564 \subsection{Go 言語との比較}
|
|
|
565 Go 言語 は Google社が開発しているプログラミング言語である。
|
|
|
566 Go 言語によるTwice の実装例を code \ref{code:go}に示す。
|
|
|
567
|
|
|
568 \lstinputlisting[caption=Go 言語での Twice, label=code:go]{./src/go.go}
|
|
|
569
|
|
|
570 Go 言語は並列実行を ``go function(argv)'' のような構文で行う。
|
|
|
571 この並列実行を goroutine と呼ぶ。
|
|
40
|
572
|
|
57
|
573 Go 言語は goroutin 間のデータ送受信をチャネルというデータ構造で行う。
|
|
|
574 チャネルによるデータの送受信は ``\textless-'' を使って行われる。
|
|
|
575 例えばチャネルのデータ構造であるchannel に対して ``channel \textless- data'' とすると、 data を channel に送信を行う。
|
|
|
576 ``\textless- channel'' とすると、 channel から送信されたデータを1つ取り出す。
|
|
|
577 channel にデータが送信されていない場合はchannel にデータが送信されるまで実行をブロックする。
|
|
|
578 Go 言語はチャネルにより、データの送受信が簡潔に書ける。
|
|
|
579 しかし、チャネルは複数の goroutine で参照できるためデータの送信元が推測しづらい。
|
|
|
580
|
|
|
581 Gears OS では goroutine は par goto 文とほぼ同等に扱うことが出来る。
|
|
|
582 また、Code Gear は par goto 文で書き出す Output Data Gear を指定して実行するため、Data Gear の書き出し元が推測しやすい。
|
|
|
583
|
|
|
584 Go 言語での OpenMP と同様に Twice を実装しGears OS と比較を行う。
|
|
|
585 こちらも実行環境は 表\ref{tab:powerEdge}、 $2^{27}$ のデータに対して行い、Gears OS、Go 言語両方とも配列を64個のTask、 goroutineに分割して並列実行を行った。
|
|
|
586
|
|
|
587 \begin{figure}[ht]
|
|
|
588 \begin{center}
|
|
|
589 \includegraphics[width=70mm]{./pic/vsgo.pdf}
|
|
|
590 \end{center}
|
|
|
591 \caption{vs Go}
|
|
|
592 \label{fig:vsgo}
|
|
|
593 \end{figure}
|
|
|
594
|
|
|
595 実行結果として Go 言語は 1CPUと32CPU で約4.33 倍の速度向上が見られた。
|
|
|
596
|
|
38
|
597
|
|
52
|
598 \section{結論}
|
|
|
599 本論文では Gears OS のプロトタイプの設計と実装、メタ計算である Context と stub の生成を行う Perl スクリプトの記述、並列実行機構の実装を行った。
|
|
40
|
600 Code Gear 、Data Gear を処理とデータの単位として用いて Gears OS を設計した。
|
|
|
601 Code Gear、Data Gear にはメタ計算を記述するための Meta Code Gear、Meta Data Gear が存在する。
|
|
|
602 メタ計算を Meta Code Gear、によって行うことでメタ計算を階層化して行うことができる。
|
|
|
603 Code Gear は関数より細かく分割されてるためメタ計算を柔軟に記述できる。
|
|
52
|
604 Gears OS は Code Gear と Input/Output Data Gear の組を Task とし、並列実行を行う。
|
|
40
|
605
|
|
|
606 Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。
|
|
|
607 Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。
|
|
|
608 Interface は複数の実装をもち、Meta Data Gear として定義される。
|
|
|
609 従来の関数呼び出しでは引数をスタック上に構成し、関数の実装アドレスを Call するが、
|
|
|
610 Gears OS では引数は Context 上に用意された Interface の Data Gear に格納され、操作に対応する Code Gear に goto する。
|
|
|
611
|
|
|
612 Context は使用する Code Gear、Data Gear をすべて格納している Meta Data Gear である。
|
|
|
613 通常の計算から Context を直接扱うことはセキュリティ上好ましくない。
|
|
|
614 このため Context から必要なデータを取り出して Code Gear に接続する Meta Code Gear である stub Code Gear を定義した。
|
|
|
615 stub Code Gear は Code Gear 毎に記述され、Code Gear 間の遷移に挿入される。
|
|
|
616
|
|
52
|
617 並列処理を行う際は Context を生成し、 Code Gear と Input/Output Data Gear を Context に設定して TaskManager 経由で各 Worker の SynchronizedQueue に送信される。
|
|
|
618 Context の設定はメタレベルの記述になるため、ノーマルレベルでは par goto 文という CbC の goto 文に近い記述で並列処理を行える。
|
|
57
|
619 この par goto は通常のプログラミングの関数呼び出しのように扱える。
|
|
52
|
620
|
|
40
|
621 これらのメタ計算の記述は煩雑であるため Perl スクリプトによる自動生成を行なった。
|
|
|
622 これにより Gears OS のコードの煩雑さは改善され、ユーザーレベルではメタを意識する必要がなくなった。
|
|
38
|
623
|
|
57
|
624 Twice と BitonicSort の例題の測定結果では 1CPU と 32CPU で Twice では約 27.1 倍、BitonicSort では 約 22.12 倍の速度向上が見られた。
|
|
|
625 また、GPU 実行の測定も行い、kernel のみの実行時間では 32 CPU より Twice では約 7.2 倍、BitonicSort では約 11.48 倍の速度向上がみられ、
|
|
|
626 GPU の性能を活かすことができた。
|
|
|
627
|
|
|
628 今後の課題は、
|
|
|
629 Go、OpenMP との比較から、 Gears OS が1CPU での動作が遅いということがわかった。
|
|
|
630 Gears OS は par goto 文を使用することで Context を生成し、並列処理を行う。
|
|
|
631 しかし、Context はメモリ空間の確保や使用する全ての Code/Data Gear を設定する必要があり、生成にある程度の時間がかかってしまう。
|
|
|
632 そこで、 par goto のコンパイルタイミングで実行する Code Gear のフローをモデル検査で解析し、処理が軽い場合はContext を生成せずに、関数呼び出しを行う等の最適化を行>うといったチューニングが必要である。
|
|
|
633
|
|
38
|
634
|
|
|
635 \nocite{*}
|
|
|
636 \bibliographystyle{ipsjunsrt}
|
|
|
637 \bibliography{sigos}
|
|
|
638
|
|
|
639 \end{document}
|
