|
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
|
|
|
52 河野 真治\affiref{2}
|
|
|
53 }
|
|
|
54
|
|
|
55 % 英文著者名
|
|
|
56 \eauthor{
|
|
|
57 Mitsuki MIYAGI\affiref{1}
|
|
|
58 \and
|
|
|
59 Shinji KONO\affiref{2}
|
|
|
60 }
|
|
|
61
|
|
|
62 % 連絡先（投稿時に必要．製版用では無視される．）
|
|
|
63 \contact{宮城 光希\\
|
|
|
64 〒903-0213 沖縄県西原町千原1番地\\
|
|
|
65 琉球大学工学部情報工学科\\
|
|
|
66 TEL: (098)895-2221\qquad FAX: (098)895-8727\\
|
|
|
67 email: mir3636@cr.ie.u-ryukyu.ac.jp}
|
|
|
68
|
|
|
69 % 和文概要
|
|
|
70 \begin{abstract}
|
|
|
71 現代の OS では拡張性と信頼性を両立させることが要求されている。
|
|
|
72 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。
|
|
|
73 Gears OS は Continuation based C によってアプリケーションと OS そのものを記述する。
|
|
|
74 CbC はこの Code Gear と Data Gear の単位でプログラムを記述する。
|
|
|
75 システムやアプリケーションを記述するためにCode Gear と Data Gear を柔軟に再利用する必要がある。
|
|
|
76 このときに機能を接続するAPIと実装の分離が可能であることが望ましい。
|
|
|
77 Gears OS の信頼性を保証するために、形式化されたモジュールシステムを提供する必要がある。
|
|
45
|
78 本論文では、Interface を用いたモジュールシステムの説明とその応用としての並列 API について考察する。
|
|
38
|
79 並列APIは継続を基本とした関数型プログラミングと両立する必要がある。
|
|
|
80 ここでは、CbC の goto 文を拡張したpar goto 文を導入する。
|
|
|
81 par goto では並列実行のための実行 Context を生成し、TaskScheduler に登録する。
|
|
|
82 Gears OS での同期機構はData Gear の待ち合わせとして定義する。
|
|
|
83 メタレベルではこれらの同期機能はCASとそれを用いて実装した Synchronized Queue になる。
|
|
|
84 これらの Queue も Interface を用いてモジュール化されている。
|
|
|
85 モジュール化の詳細と、有効性について考察する。
|
|
|
86 \end{abstract}
|
|
|
87
|
|
|
88 % 英文概要
|
|
|
89 \begin{eabstract}
|
|
|
90 \end{eabstract}
|
|
|
91
|
|
|
92 % 表題などの出力
|
|
|
93 \maketitle
|
|
|
94
|
|
|
95 % 本文はここから始まる
|
|
|
96
|
|
|
97 % Introduce
|
|
|
98 % Code Gear は関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。
|
|
|
99
|
|
|
100 % 研究目的
|
|
|
101
|
|
|
102 % 信頼性の高いOS
|
|
|
103 % これをアセンブラにしていろいろなアプリケーションを作る
|
|
|
104 % きょだいなCDGの上で動かすと既存のアプリケーションを動かすことができる
|
|
|
105
|
|
40
|
106 \section{OS の拡張性と信頼性の両立}
|
|
|
107
|
|
43
|
108 さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩する
|
|
41
|
109 ハードウェア、サービスに対応して OS 自体が拡張される必要がある。
|
|
|
110 OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分であり、テストしきれない部分が残ってしまう。
|
|
|
111 これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
|
|
|
112 モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている
|
|
40
|
113 図\ref{fig:verification}。
|
|
|
114 \begin{figure}[ht]
|
|
|
115 \begin{center}
|
|
|
116 \includegraphics[width=70mm]{./pic/verification.pdf}
|
|
|
117 \end{center}
|
|
|
118 \caption{証明とモデル検査によるOSの検証}
|
|
|
119 \label{fig:verification}
|
|
|
120 \end{figure}
|
|
|
121
|
|
41
|
122 証明やモデル検査を用いて OS を検証する方法はさまざまなものが検討されている。
|
|
|
123 検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。
|
|
|
124 つまり信頼性と拡張性を両立させることが重要である。
|
|
40
|
125
|
|
41
|
126 コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意味論の定義などで規定される。
|
|
|
127 プログラミング言語で記述される部分をノーマルレベルの計算と呼ぶ。
|
|
|
128 コードが実行される時には、処理系の詳細や使用する資源、あるいは、コードの仕様や型などの言語以外の部分が服属する。
|
|
|
129 これをメタレベルの計算という。
|
|
|
130 この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼性をメタレベルから保証できるようにしたい。
|
|
40
|
131 ノーマルレベルでの正当性を保証しつつ、新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。
|
|
|
132
|
|
41
|
133 本論文では、ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。
|
|
|
134 CbC は関数呼出時の暗黙の環境(Environment)を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。
|
|
|
135 これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。
|
|
|
136 これらを用いて、検証された Gears OS を構築したい。
|
|
40
|
137 図\ref{fig:MetaGear}。
|
|
|
138 \begin{figure}[ht]
|
|
|
139 \begin{center}
|
|
|
140 \includegraphics[width=70mm]{./pic/MetaGear.pdf}
|
|
|
141 \end{center}
|
|
|
142 \caption{Gearsのメタ計算}
|
|
|
143 \label{fig:MetaGear}
|
|
|
144 \end{figure}
|
|
|
145
|
|
41
|
146 本論文では、Gears OS の要素である Code Gear、Data Gear、そして、Meta Code Gear 、Meta Data Gear の構成を示す。
|
|
|
147 これらは、CbC に変換されて実行される。
|
|
40
|
148 Gears OS は、Task Scheduler を CPU や GPU 毎に持ち、一つの Task に対応する Context という Meta Data Gear を使用しながら計算を実行する。
|
|
|
149
|
|
41
|
150 Meta Gear を入れかえることにより、ノーマルレベルの Gear をモデル検査することができるようにしたい。
|
|
|
151 ノーマルレベルでの Code Gear と Data Gear は継続を基本とした関数型プログラミング的な記述に対応する。
|
|
|
152 この記述を定理証明支援系である Agda を用いて直接に証明できるようにしたい。
|
|
40
|
153
|
|
41
|
154 従来の研究でメタ計算を用いる場合は、関数型言語では Monad を用いる\cite{Moggi:1989:CLM:77350.77353}。
|
|
|
155 これは Hakell では実行時の環境を記述する構文として使われている。
|
|
|
156 OS の研究では、メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。
|
|
|
157 Python や Haskell による記述をノーマルレベルとして
|
|
40
|
158 採用した OS の検証の研究もある\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}。
|
|
|
159 SMIT などのモデル検査を OS の検証に用いた例もある\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}。
|
|
|
160
|
|
|
161 本研究で用いる Meta Gear は制限された Monad に相当し、型つきアセンブラよりは大きな表現単位を提供する。
|
|
41
|
162 Haskell などの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。
|
|
|
163 CbC はスタック上に隠された環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。
|
|
|
164 ただし、Gear のプログラミングスタイルは、従来の関数呼出を中心としたものとはかなり異なる。
|
|
48
|
165 本研究では、Gears の記述をモジュール化するためにインターフェースを導入した。
|
|
41
|
166 これにより、見通しの良いプログラミングが可能になった。
|
|
40
|
167
|
|
38
|
168 \section{メタ計算の重要性}
|
|
|
169 従来の OS では、メタ計算はシステムコールやライブラリーコールの単位で行われる。
|
|
|
170 実行時にメタ計算の変更を行う場合には、OS 内部のパラメータの変更を使用し、
|
|
|
171 実行されるユーザープログラム自体への変更は限定的である。
|
|
|
172 しかし、メタ計算は性能測定あるいはプログラム検証、さらに並列分散計算のチューニングなど細かい処理が必要で
|
|
|
173 実際のシステムコール単位では不十分である。
|
|
|
174 例えば、モデル検査ではアセンブラあるいはバイトコード、インタプリタレベルでのメタ計算が必要になる。
|
|
|
175 しかし、バイトコードレベルでは粒度が細かすぎて扱いが困難になっている。
|
|
|
176 具体的にはメタ計算の実行時間が大きくなってしまう。
|
|
|
177
|
|
|
178 メタ計算を通常の計算から切り離して記述するためには処理を細かく分割する必要がある。しかし、関数やクラスなどの単位は容易に分割できない。
|
|
|
179 そこで当研究室ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を提案している。
|
|
|
180 これによりシステムコードよりも細かくバイトコードよりも大きなメタ計算の単位を提供できる。
|
|
|
181
|
|
|
182 Code Gear は処理の単位である。
|
|
|
183 関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。
|
|
|
184 Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実現する。
|
|
|
185
|
|
41
|
186 CbC はこの Code Gear 単位を用いたプログラミング言語として開発している。
|
|
38
|
187
|
|
40
|
188 CbC は軽量継続による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。
|
|
38
|
189
|
|
41
|
190 CbC での記述はメタ計算を含まないノーマルレベルでの記述と、Meta Code Gear、Meta Data Gear の記述を含むメタレベルの記述の2種類がある。
|
|
38
|
191 メタレベルでもさらに、メタ計算を用いることが可能になっている。
|
|
|
192 この2つのレベルはプログラミング言語レベルでの変換として実現される。
|
|
|
193 CbC は LLVM\cite{llvm} 上で実装されており、メタレベルでの変換系は本論文では、Perl による変換スクリプトにより実装されている。
|
|
|
194
|
|
|
195 Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。
|
|
|
196 Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。
|
|
|
197 Interface は複数の実装を持つことができ、Meta Data Gear によって定義される。
|
|
|
198 Interface の操作に対応する Code Gear の引数は Interface に定義されている Data Gear を通して行われる。
|
|
|
199
|
|
|
200 従来の関数呼び出しでは引数をスタック上に構成し、関数の実装アドレスを Call する。
|
|
|
201 Gears OS では引数は Context 上に用意された Interface の Data Gear に格納され、
|
|
|
202 操作に対応する Code Gear に goto する。
|
|
|
203 Context とは使用される Code Gear と Data Gear を全て格納している Meta Data Gear である。
|
|
|
204 これは従来のスレッド構造体に対応する。
|
|
40
|
205 つまり Gears OS では従来はコンパイラが定義する ABI(Application Binary Interface)
|
|
38
|
206 を Meta Data Gear として CbC で表現し、メタ計算として操作することができる。
|
|
|
207
|
|
|
208 ノーマルレベルでは Context を直接見ることはできず、引数は Code Gear の引数を明示する必要がある。
|
|
|
209 この時に呼び出し側の引数を不定長引数として追加する構文を CbC に追加した。
|
|
|
210 これにより Interface 間の呼び出しを簡潔に記述することが出来るようになった。
|
|
|
211 メタレベルでは Code Gear の引数は単一または複数の Data Gear として見ることができる。
|
|
|
212 これは Context を直接操作することができることを意味する。
|
|
|
213 この部分はノーマルレベルの Code Gear を呼び出す stub として生成される。
|
|
|
214 ノーマルレベルでの goto 文はメタ計算への goto で置き換えられる。
|
|
|
215 Gears OS でのメタ計算は stub と goto のメタ計算の2箇所で実現される。
|
|
|
216
|
|
|
217 メタ計算の例としては並列処理があり、Context を切り替えることによって複数のスレッドを実現している。
|
|
|
218 Context を複数の CPU に割り当てることにより並列実行を可能にしている。
|
|
|
219
|
|
|
220 \section{Continuation based C (CbC)}
|
|
|
221 CbC は Code Gear という処理の単位を用いて記述するプログラミング言語である。
|
|
|
222 Code Gear は CbC における最も基本的な処理単位である。
|
|
|
223 Code Gear は入力と出力を持ち、CbC では引数が入出力となっている。
|
|
|
224 CbC では Code Gear は \_\_code という型を持つ関数の構文で定義される。
|
|
|
225 ただし、これは \_\_code 型の戻り値を返すという意味ではなく、Code Gear であることを示すフラグである。
|
|
40
|
226 Code Gear は戻り値を持たないので、Cの関数とは異なり return 文は存在しない。
|
|
38
|
227
|
|
40
|
228 Code Gear から次の Code Gear への遷移は goto による継続で処理を行い、次の Code Gear へ引数として入出力を与える。
|
|
38
|
229 図\ref{fig:cs}は Code Gear 間の処理の流れを表している。
|
|
|
230
|
|
|
231 \begin{figure}[ht]
|
|
|
232 \begin{center}
|
|
|
233 \includegraphics[width=70mm]{./pic/codesegment.pdf}
|
|
|
234 \end{center}
|
|
|
235 \caption{goto による Code Gear 間の継続}
|
|
|
236 \label{fig:cs}
|
|
|
237 \end{figure}
|
|
|
238
|
|
40
|
239 CbC の goto による継続は Scheme の継続と異なり呼び出し元の環境がないので、この継続は単なる行き先である。
|
|
38
|
240 したがってこれを軽量継続と呼ぶ。
|
|
|
241 軽量継続により、並列化、ループ制御、関数コールとスタックの操作を意識した最適化がソースコードレベルで行えるようにする。
|
|
|
242
|
|
|
243 \section{Gears OS}
|
|
40
|
244 Gears OS は Code Gear とデータの単位である Data Gear を用いて開発されており、CbC で記述されている。
|
|
|
245 Gears OS では、並列実行するための Task を、実行する Code Gear と、実行に必要な Input Data Gear 、Output Data Gear の組で表現する。
|
|
|
246 Gears OS は Input/Output Data Gear の依存関係が解決された CodeGear を並列実行する。
|
|
38
|
247 Data Gear はデータの単位であり、int や文字列などの Primitive Type を持っている。
|
|
|
248 Code Gear は任意の数の Input Data Gear を参照して処理を行い、Output Data Gear を出力し処理を終える。
|
|
|
249 また、接続された Data Gear 以外には参照を行わない。
|
|
40
|
250 処理やデータの構造が Code Gear、Data Gear に閉じているため、これにより実行時間、メモリ使用量などを予測可能なものにすることができる。
|
|
38
|
251
|
|
|
252 Gears OS では メタ計算 を Meta Code Gear、Meta Data Gear で表現する。
|
|
40
|
253 Meta Code Gear は通常の Code Gear の直後に遷移され、メタ計算を実行する。
|
|
|
254 これを図示したものが図\ref{fig:metaCS}である。
|
|
|
255 %Meta Code Gear で OS の機能であるメモリ管理やスレッド管理を行う。
|
|
38
|
256
|
|
40
|
257 \begin{figure}[ht]
|
|
|
258 \begin{center}
|
|
|
259 \includegraphics[width=70mm]{./pic/metaCS.pdf}
|
|
|
260 \end{center}
|
|
|
261 \caption{Gears でのメタ計算}
|
|
|
262 \label{fig:metaCS}
|
|
|
263 \end{figure}
|
|
|
264
|
|
|
265 Gears OS は Context と呼ばれる使用されるすべての Code Gear、Data Gear 持っている Meta Data Gear を持つ。
|
|
|
266 Gears OS は必要な Code Gear、Data Gear を参照したい場合、この Context を通す必要がある。
|
|
|
267
|
|
|
268 しかし Context を通常の計算から直接扱うのはセキュリティ上好ましくない。
|
|
|
269 そこで Context から必要なデータを取り出して Code Gear に接続するMeta Code Gear である stub Code Gear を定義し、
|
|
|
270 これを介して間接的に必要な Data Gear にアクセスする。
|
|
|
271 stub Code Gear は Code Gear 毎に生成され、次の Code Gear へと継続する前に挿入される。
|
|
|
272 goto による継続を行うと、実際には次の Code Gear の stub Code Gear を呼び出す。
|
|
38
|
273
|
|
|
274 \section{Gears OS の構成}
|
|
|
275 Gears OS は以下の要素で構成される。
|
|
|
276
|
|
|
277 \begin{itemize}
|
|
|
278 \item Context
|
|
|
279 \item TaskQueue
|
|
|
280 \item TaskManager
|
|
|
281 \item Worker
|
|
|
282 \end{itemize}
|
|
|
283
|
|
|
284 図\ref{fig:gearsos} に Gears OS の構成図を示す。
|
|
|
285
|
|
|
286 \begin{figure}[ht]
|
|
|
287 \begin{center}
|
|
|
288 \includegraphics[width=70mm]{./pic/gears_structure}
|
|
|
289 \end{center}
|
|
|
290 \caption{Gears OS の構成図}
|
|
|
291 \label{fig:gearsos}
|
|
|
292 \end{figure}
|
|
|
293
|
|
40
|
294 Code\ref{context} は Context の定義で Code\ref{initcontext} は Context の生成である。
|
|
38
|
295
|
|
40
|
296 \lstinputlisting[caption=Contextの定義, label=context]{./src/context1.c}
|
|
|
297 \lstinputlisting[label=initcontext, caption=Contextの生成]{./src/initcontext.c}
|
|
38
|
298
|
|
|
299 Data Gear は union と struct によって表現される。
|
|
|
300 Context には Data Gear の Data Type の情報が格納されている。
|
|
|
301 この情報から確保する Data Gear のサイズなどを決定する。
|
|
|
302
|
|
40
|
303 Context は Task でもあり、Taskは通常のOSのスレッドに対応する。
|
|
|
304 Task は実行する Code Gear と Data Gear をすべて持っている。
|
|
43
|
305 TaskManager は Task を実行する Worker の生成、管理、Task の送信を行う。
|
|
40
|
306 Gears OS における Task Queue は Synchronized Queue で実現される。
|
|
43
|
307 Worker は TaskQueue から Task である Context を取得し、Task の Code Gear を実行し、Output Data Gear の書き出しを行っている。
|
|
|
308 Input/Output Data Gear の依存関係が解決されたものから並列実行される。
|
|
38
|
309
|
|
40
|
310 \section{Interface}
|
|
|
311 Interface は呼び出しの引数になる Data Gear の集合であり、そこで呼び出される Code Gear のエントリである。
|
|
|
312 呼び出される Code Gear の引数となる Data Gear はここで全て定義される。
|
|
38
|
313
|
|
40
|
314 Code\ref{interface}は stack の Interface である。
|
|
|
315 Code Gear、Data Gear に参照するために Context を通す必要があるが、
|
|
|
316 Interface を記述することでデータ構造の api と Data Gear を結びつけることが出来る。
|
|
38
|
317
|
|
40
|
318 \lstinputlisting[label=interface, caption=StackのInterface]{./src/Stack.cbc}
|
|
38
|
319
|
|
40
|
320 Code\ref{implement}は stack の Implement の例である。
|
|
|
321 createImpl は関数呼び出しで呼び出され、Implement の初期化と Code Gear のスロットに対応する Code Gear の番号を入れる。
|
|
38
|
322
|
|
40
|
323 \lstinputlisting[label=implement, caption=SingleLinkedStackのImplement]{./src/stackimpl.cbc}
|
|
38
|
324
|
|
40
|
325 \section{stub Code Gear の生成}
|
|
|
326
|
|
38
|
327 Gears OS を CbC で実装する上でメタ計算の記述が煩雑であることがわかった。
|
|
|
328 これらのメタ計算を自動生成することにより Gears OS を記述する上においてより良い構文をユーザーに提供することにした。
|
|
|
329
|
|
|
330 stub Code Gear は Code Gear 間の継続に挟まれる Code Gear が必要な Data Gear を Context から取り出す処理を行うものである。
|
|
|
331 Code Gear 毎に記述する必要があり、そのCode Gear の引数を見て取り出す Data Gear を選択する。
|
|
|
332 stub Code Gear を 自動生成する generate stub を Perl スクリプトで作成することによって Code Gear の記述量を約半分にすることができる。
|
|
|
333
|
|
|
334 stub を生成するために generate\_stub は指定された cbc ファイルの \_\_code型である Code Gear を取得し、引数から必要な Data Gear を選択する。
|
|
|
335 generate\_stub は引数と interface を照らし合わせ、Gearef または GearImpl を決定する。
|
|
|
336 また、この時既に stub Code Gear が記述されている Code Gear は無視される。
|
|
|
337
|
|
|
338 cbc ファイルから、生成した stub Code Gear を加えて stub を加えたコードに変換を行う。(Code\ref{stack_c})
|
|
|
339
|
|
40
|
340 \lstinputlisting[label=stack_c, caption=stub Code Gear を加えたコード]{./src/ex_stub}
|
|
38
|
341
|
|
|
342 \section{Context の生成}
|
|
|
343 generate\_context は Context.h、Interface.cbc、generate\_stub で生成されたImpl.cbc を見て Context を生成する Perl スクリプトである。
|
|
|
344
|
|
|
345 \begin{figure}[ht]
|
|
|
346 \begin{center}
|
|
|
347 \includegraphics[width=70mm]{./pic/generate_context3.pdf}
|
|
|
348 \end{center}
|
|
|
349 \caption{generate\_context による Context の生成}
|
|
|
350 \label{fig:gc}
|
|
|
351 \end{figure}
|
|
|
352
|
|
|
353 Context は Meta Data Gear に相当し、Code Gear や Data Gear を管理している。
|
|
|
354
|
|
|
355 generate\_context は context の定義 (Code\ref{context}) を読み宣言されている Data Gear を取得する。
|
|
|
356 Code Gear の取得は指定された generate\_stub で生成されたコードから \_\_code 型を見て行う。
|
|
|
357 取得した Code Gear、Data Gear の enum の定義は enumCode.h、enumData.h に生成される。
|
|
|
358
|
|
|
359 Code/Data Gear の名前とポインタの対応は generate\_context によって生成される enum Code、enum Data を指定することで接続を行う。
|
|
49
|
360 また、generate context は取得した Code/Data Gear から initContext の生成も行う。
|
|
38
|
361
|
|
|
362 Context には Allocation 等で生成した Data Gear へのポインタが格納されている。
|
|
|
363 Code Gear は Context を通して Data Gear へアクセスする。
|
|
|
364 Data Gear の Allocation を行うコードは dataGearInit.cに生成される。
|
|
|
365
|
|
|
366 Data Gear は union Data とその中の struct によって表現される。
|
|
|
367 Context には Data Gear の Data Type の情報が格納されている。
|
|
|
368 この情報から確保される Data Gear のサイズなどを決定する。
|
|
|
369
|
|
43
|
370 \section{Gears OS の並列処理}
|
|
|
371 Gears OS では実行の Task を Code Gear と Input/Output Data Gear の組で表現する。
|
|
|
372 Input/Output Data Gear によって依存関係が決定し、それにそって並列実行を行う。
|
|
|
373 Gears OS では 並列実行する Task を Context で表現する。
|
|
|
374 Context には Task 用の情報として、実行される Code Gear、Input/Output Data Gear の格納場所、待っている Input Data Gear のカウンタ等を持っている
|
|
|
375 Task の Input Data Gear が揃っているかを TaskManager で判断し、 実行可能な Task を Worker に送信する。
|
|
|
376 Worker は送信された Task が指定した Code Gear を実行し、Output Data Gear を書き出す。
|
|
|
377
|
|
|
378 \section{SynchronizedQueue}
|
|
|
379 SynchronizedQueue は Worker の Queue として使用される。
|
|
|
380 Worker の Queue は TaskManager を経由して Task を送信するスレッドと Task を取得する Worker 自身のスレッドで扱われる。
|
|
|
381 そのため SynchronizedQueue はマルチスレッドでもデータの一貫性を保証する Queue を実装する必要がある。
|
|
|
382
|
|
|
383 データの一貫性を保証する解決例としての 1 つとしてロックを使った解決方法がある。
|
|
|
384 しかし、ロックを行ってデータを更新した場合、同じ Queue に対して操作を行う際に待ち合わせが発生し、全体の並列度が下がってしまう。
|
|
|
385 そこで、Gears OS ではデータの一貫性を保証するために CAS(Check and Set、Compare and Swap) を利用した Queue を実装している。
|
|
|
386 CAS は値の比較、更新をアトミックに行う命令である。
|
|
|
387 CAS を使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じならデータ競合がないため、データの更新に成功する。
|
|
|
388 異なる場合は他に書き込みがあったとみなされ、値の更新に失敗する。
|
|
|
389
|
|
46
|
390 Gears OS ではこの CAS を行うための Interface を定義している(Code\ref{atomicInterface})。
|
|
45
|
391 この Interface では、Data Gear 全てを内包している Data 共用体のポインタの値を更新する CAS を定義して
|
|
46
|
392 いる(Code\ref{atomicInterface} 6行目)。
|
|
45
|
393
|
|
46
|
394 \lstinputlisting[label=atomicInterface, caption=AtomicInterface]{./src/atomicInterface.h}
|
|
45
|
395
|
|
46
|
396 AtomicInterface での CAS の実際の実装を Code\ref{atomicImpl} に示す。
|
|
|
397 実際の実装では \_\_sync\_bool\_compare\_and\_swap 関数を呼び出すことで CAS を行う(Code\ref{atomicImpl} 2行目)。
|
|
45
|
398 この関数は第一引数に渡されたアドレスに対して第二引数の値から第三引数の値ヘ CAS を行う。
|
|
|
399 CAS に成功した場合、true を返し、失敗した場合は false を返す。
|
|
46
|
400 Code\ref{atomicImpl} では CAS に成功した場合と失敗した場合それぞれに対応した Code Gear へ継続する。
|
|
45
|
401
|
|
46
|
402 \lstinputlisting[caption=CAS の実装, label=atomicImpl]{./src/atomicImpl.cbc}
|
|
45
|
403
|
|
46
|
404 SynchronizedQueue の Data Gear の定義を Code\ref{synchronizedQueue} に示す。
|
|
45
|
405 SynchronizedQueue はデータのリストの先頭と、終端のポインタを持っている。
|
|
|
406 Queue を操作する際はこのポインタに対して CAS をすることでデータの挿入と取り出しを行う。
|
|
|
407
|
|
46
|
408 \lstinputlisting[caption=SynchronizedQueue の定義, label=synchronizedQueue]{./src/synchronizedQueue.h}
|
|
45
|
409
|
|
|
410 %\section{依存関係の解決}
|
|
43
|
411
|
|
|
412 \section{並列構文}
|
|
|
413 Gears OS の並列構文は par goto文で用意されている。
|
|
|
414 par goto の引数には Input/Output Data Gear と 実行後に継続する \_\_exit を渡す。
|
|
|
415 par goto で生成された Task は \_\_exit に継続することで終了する。
|
|
44
|
416 par goto文でも 通常の goto 分と同様にメタへの goto 文へ置き換えられるが、par goto 文では通常の goto 文とは異なるメタへと継続する。
|
|
43
|
417 Gears OS の Task は Output Data Gear を生成した時点で終了するので、par goto では直接 \_\_exit に継続するのではなく、
|
|
|
418 Output Data Gear への書き出し処理(Commit)に継続される。
|
|
|
419
|
|
44
|
420 Code Gear は Input に指定した Data Gear が全て書き込まれると実行され、実行した結果を Output に指定した Data Gear に書き出しを行う。
|
|
|
421 Code Gear の引数である\_\_next が持つ引数の Data Gear が Output Data Gear となる。
|
|
|
422
|
|
43
|
423 書き出し処理は Data Gear の Queue から、依存関係にある Task を参照する。
|
|
44
|
424 参照した Task が持つ実行に必要な Input Data Gear カウンタのデクリメントを行う。
|
|
43
|
425 カウンタが0になると Task が待っている Input Data Gear が揃ったことになり、
|
|
|
426 その Task を TaskManager 経由で 実行される Worker に送信する。
|
|
|
427
|
|
|
428 この par goto 文は通常のプログラミングの関数呼び出しのように扱うことができる。
|
|
|
429
|
|
|
430
|
|
40
|
431 \section{比較}
|
|
|
432
|
|
|
433 従来のプログラミングスタイルとの比較。
|
|
|
434 Gears のプログラミングは関数呼出を中心とするプログラミングとはかなり異なる。
|
|
|
435 Gears は関数呼出を禁止しているわけではなく、使用する資源の制御に問題がないなら普通に関数呼出して良い。
|
|
|
436 Linux kernel などでは関数呼出の大半はインライン展開されることを期待してプログラミングされており、
|
|
|
437 関数呼出で予測できないスタックの爆発やCPU資源の浪費が起きないようにプログラミングされている。
|
|
|
438 Gears では Gears 間のプログラミングは戻り先や使用する資源を明示する必要がある。
|
|
|
439
|
|
|
440 goto 文での引数は通常の関数呼出と異なり、スタック(環境)に積むことができない。引数に必要な情報を含むData Gearを
|
|
|
441 持ち歩くスタイルとなる。一つのインタフェース内部では、これらは共通している。実際、これらはメタレベルでは、
|
|
|
442 Context というMeta Data Gear にすべて格納されている。メタレベルは、Data Gear の詳細な型は使用されない。
|
|
|
443 ノーマルレベルに移行する際に stub Code Gear を通して詳細な型が接続される。
|
|
|
444
|
|
|
445 インタフェースを再利用する際には、呼び出すインタフェースが持つ引数は保存される必要がある。これらは、実際には
|
|
|
446 Context 内にあるので自動的に保存されている。ノーマルレベルの記述では、... の部分にその意味が込めれている。
|
|
|
447 これは、可変長引数の...と同じ意味だと考えても良い。ただ、LLVM/GCC レベルでそれを実装するのは比較的難しい。
|
|
|
448 なので、今回はScriptによる変換を採用している。
|
|
|
449
|
|
|
450 ノーマルレベルの記述と関数型プログラミングの記述の比較。Gear は必ず継続を渡す必要がある。これは一段の
|
|
|
451 関数呼出を許しているのと同等である。70年代の Fortan の関数呼出は決まった場所に戻り先を格納するので
|
|
|
452 再起呼出ができなかったのと同じである。例えば Code Gears 以下のような型を持つ。ここで t は継続の型である。
|
|
|
453 Stack は Stack を受けとる Stack \verb|->| t という Code Gear を継続として引数で受けとる。popStack はこの引数を
|
|
|
454 呼び出す。
|
|
|
455
|
|
|
456 \verb|popStack : {a t : Set} -> Stack |
|
|
|
457
|
|
|
458 \verb| -> (Stack -> t) -> t|
|
|
|
459
|
|
|
460 つまり、Code Gear は制限された関数の形式を持っている。Data Gear は、関数型言語の直積や排他的論理和(Sum)を含むデータ型に
|
|
|
461 対応する。しかし、一つの Context で実行される Data Gear は、一つの巨大なSumに含まれるようになっている。これを
|
|
|
462 メタレベルでは、中の型の詳細に立ち入ることなく実行する。
|
|
|
463
|
|
|
464 Context はノーマルレベル のData Gear の他に様々なメタ情報を持つ。例えば、メモリ管理情報や実行される CPU 、あるいは、Task の
|
|
|
465 状態、待ち合わせている Data Gear などである。これらの情報は C やアセンブラのレベルで実装されるのと同時に、通常の Gear の
|
|
|
466 プログラミングにも対応する。例えば、CPU をかそうてきに Gears で記述すればソフトウェア的な並列実行を実現し、実際の
|
|
|
467 GPU を用いれば GPU による並列実行となる。この実行をモデル検査的な状態数え上げに対応させればモデル検査を実行できる。
|
|
|
468
|
|
|
469 Haskell などを実行可能仕様記述として用いる OS の検証\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}と、Code Gear を用いる手法は類似>しているが、Code Gear の場合は、
|
|
|
470 記述を制限し、Code と仕様の対応、さらにCodeと資源の対応が明確になる利点がある。
|
|
|
471
|
|
|
472 型つきアセンブラ\cite{Yang:2010:SLI:1806596.1806610}は、より低レベルの関数型の記述であると言える。アセンブラの記述自体は小さく扱いやすいが、
|
|
|
473 OS レベルあるいはアプリケーションレベルからの距離が大きい。型の整合性を保証するだけでは OS の検証としては
|
|
|
474 不十分なので、証明やモデル検査を用いることになるが、記述量が多いのが、その際に欠点となる。
|
|
|
475 Code Gear は、より大きな単位であり、プログラミングレベルの抽象化が可能になっているので、これらの記述の
|
|
|
476 大きさの欠点をカバーできる可能性がある。
|
|
|
477
|
|
|
478 証明手法は、従来では Hoare Logic \cite{Chen:2015:UCH:2815400.2815402}のような Post Condition / Pre Condition を用いる方法が使われている。
|
|
|
479 現在のGearsは、Agda への変換は考えているが、その上の具体的な証明方法はまだ用意されていない。
|
|
38
|
480
|
|
|
481 \section{今後の課題}
|
|
40
|
482 本論文では Code Gear、 Data Gear によって構成される Gears OS のプロトタイプの設計、実装、CbC ファイルから Gears OS の記述に必要な Context と stub の生成を行う Perl スクリプトの生成を行なった。
|
|
|
483 Code Gear 、Data Gear を処理とデータの単位として用いて Gears OS を設計した。
|
|
|
484 Code Gear、Data Gear にはメタ計算を記述するための Meta Code Gear、Meta Data Gear が存在する。
|
|
|
485 メタ計算を Meta Code Gear、によって行うことでメタ計算を階層化して行うことができる。
|
|
|
486 Code Gear は関数より細かく分割されてるためメタ計算を柔軟に記述できる。
|
|
|
487
|
|
|
488 Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。
|
|
|
489 Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。
|
|
|
490 Interface は複数の実装をもち、Meta Data Gear として定義される。
|
|
|
491 従来の関数呼び出しでは引数をスタック上に構成し、関数の実装アドレスを Call するが、
|
|
|
492 Gears OS では引数は Context 上に用意された Interface の Data Gear に格納され、操作に対応する Code Gear に goto する。
|
|
|
493
|
|
|
494 Context は使用する Code Gear、Data Gear をすべて格納している Meta Data Gear である。
|
|
|
495 通常の計算から Context を直接扱うことはセキュリティ上好ましくない。
|
|
|
496 このため Context から必要なデータを取り出して Code Gear に接続する Meta Code Gear である stub Code Gear を定義した。
|
|
|
497 stub Code Gear は Code Gear 毎に記述され、Code Gear 間の遷移に挿入される。
|
|
|
498
|
|
|
499 これらのメタ計算の記述は煩雑であるため Perl スクリプトによる自動生成を行なった。
|
|
|
500 これにより Gears OS のコードの煩雑さは改善され、ユーザーレベルではメタを意識する必要がなくなった。
|
|
38
|
501
|
|
|
502 今後の課題は Code Gear からメタ計算を行う meta Code Gear を生成できるようにし、ユーザーがメタレベルの処理を意識せずにコードを記述できるようにする。
|
|
|
503 また、今回 Perl スクリプトによって Context や stub の生成を行なったが、LLVM/clang 上で実装しコンパイラで直接 CbC を実行できるようにすることを目的とする。
|
|
|
504
|
|
|
505 \nocite{*}
|
|
|
506 \bibliographystyle{ipsjunsrt}
|
|
|
507 \bibliography{sigos}
|
|
|
508
|
|
|
509 \end{document}
|
