0
|
1 % withpage: ページ番号をつける (著者確認用)
|
|
2 % english: 英語原稿用フォーマット
|
|
3 \documentclass{ipsjprosym}
|
|
4 %\documentclass[withpage,english]{ipsjprosym}
|
2
|
5 \usepackage{listings}
|
0
|
6 \usepackage[dvipdfmx]{graphicx}
|
|
7 \usepackage{latexsym}
|
|
8 \usepackage{comment}
|
|
9 \lstset{
|
|
10 language=C,
|
|
11 tabsize=2,
|
|
12 frame=single,
|
|
13 basicstyle={\ttfamily\footnotesize},%
|
|
14 identifierstyle={\footnotesize},%
|
|
15 commentstyle={\footnotesize\itshape},%
|
|
16 keywordstyle={\footnotesize\bfseries},%
|
|
17 ndkeywordstyle={\footnotesize},%
|
|
18 stringstyle={\footnotesize\ttfamily},
|
|
19 breaklines=true,
|
|
20 captionpos=b,
|
|
21 columns=[l]{fullflexible},%
|
|
22 xrightmargin=0zw,%
|
|
23 xleftmargin=1zw,%
|
|
24 aboveskip=1zw,
|
|
25 numberstyle={\scriptsize},%
|
|
26 stepnumber=1,
|
|
27 numbersep=0.5zw,%
|
|
28 lineskip=-0.5ex,
|
|
29 }
|
|
30 \renewcommand{\lstlistingname}{Code}
|
5
|
31 \usepackage{caption}
|
|
32 \captionsetup[lstlisting]{font={small,tt}}
|
0
|
33
|
|
34 \begin{document}
|
|
35
|
|
36 % Title, Author %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
37 \title{Code Gear と Data Gear を持つ\\Gears OS の設計}
|
|
38
|
|
39 \affiliate{IPSJ}{情報処理学会}
|
|
40
|
|
41 \author{宮城 光希}{Mitsuki MIYAGI}{}[mir3636@cr.ie.u-ryukyu.ac.jp]
|
|
42 \author{河野 真治}{Shinji KONO}{IPSJ}[kono@ie.u-ryukyu.ac.jp]
|
|
43
|
|
44 % はじめに
|
|
45 \begin{abstract}
|
6
|
46 現代の OS では拡張性と信頼性を両立させることが要求されている。
|
0
|
47 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。
|
6
|
48 Gears OS は Continuation based C(CbC) によってアプリケーションと OS そのものを記述する。
|
|
49 OS の下ではプログラムの記述は通常の処理の他に、メモリ管理、スレッドの待ち合わせやネットワークの管理、エラーハンドリング等の記述しなければならない処理が存在する。
|
|
50 これらの計算をメタ計算と呼ぶ。
|
|
51 メタ計算を通常の計算から切り離して記述するために、Code Gear、Data Gear という単位を提案している。
|
|
52 CbC はこの Code Gear と Data Gear の単位でプログラムを記述する。
|
|
53 Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在する。
|
|
54 Code Gear 間の接続は次の Code Gear の番号と thread structure に相当する Context によって行われる。
|
|
55 ユーザーレベルではメタ構造を直接見ることはなく、継続を用いた関数型プログラミングに見える。
|
|
56 メタレベルから見た Data Gear をユーザーレベルの Code Gear に接続するには stub という Meta Code Gear を用いる。
|
|
57 stub と Meta はユーザーレベル Code Gear と Data Gear からスクリプトにより作成される。
|
|
58 変換に必要な情報はプログラムを構成する Code Gear と Data Gear の集まりから得る。
|
|
59 この集まりを Interface として定義している。
|
|
60 本論文では、Interfaceを用いたプログラミングと、メタ計算の実例を示す。
|
0
|
61 \end{abstract}
|
|
62
|
|
63 \begin{jkeyword}
|
5
|
64 OS, プログラミング言語, コンパイラ, CbC, Gears OS
|
0
|
65 \end{jkeyword}
|
|
66
|
|
67 \maketitle
|
|
68
|
|
69 % Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
15
|
70 \section{OS の拡張性と信頼性の両立}
|
14
|
71
|
15
|
72 さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩する。
|
|
73 ハードウェア、サービスに対応して OS 自体が拡張される必要がある。OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分
|
14
|
74 であり、テストしきれない部分が残ってしまう。これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法が
|
|
75 ある。モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている
|
|
76 図\ref{fig:verification}。
|
|
77 \begin{figure}[ht]
|
|
78 \begin{center}
|
|
79 \includegraphics[width=70mm]{./pic/verification.pdf}
|
|
80 \end{center}
|
|
81 \caption{証明とモデル検査によるOSの検証}
|
|
82 \label{fig:verification}
|
|
83 \end{figure}
|
|
84
|
15
|
85 証明やモデル検査を用いて OS を検証する方法はさまざまなものが検討されている。検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しく
|
14
|
86 なることに検証をやり直す必要がある。つまり信頼性と拡張性を両立させることが重要である。
|
|
87
|
|
88 コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意味論の定義などで規定される。プログラミング言語で記述される部分を
|
|
89 ノーマルレベルの計算と呼ぶ。コードが実行される時には、処理系の詳細や使用する資源、あるいは、コードの仕様や型などの言語以外の部分が服属する。
|
|
90 これをメタレベルの計算という。この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼性をメタレベルから保証できるようにしたい。
|
|
91 ノーマルレベルでの正当性を保証しつつ、新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。
|
|
92
|
|
93 本論文では、ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。CbC は関数呼出時の暗黙の環境(Environment)
|
15
|
94 を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。これを用いて、Code Gear と Data Gear、さらに
|
|
95 そのメタ構造を導入する。これらを用いて、検証された Gears OS を構築したい。
|
14
|
96 図\ref{fig:MetaGear}。
|
|
97 \begin{figure}[ht]
|
|
98 \begin{center}
|
15
|
99 \includegraphics[width=70mm]{./pic/MetaGear.pdf}
|
14
|
100 \end{center}
|
|
101 \caption{Gearsのメタ計算}
|
|
102 \label{fig:MetaGear}
|
|
103 \end{figure}
|
|
104
|
15
|
105 本論文では、Gears OS の要素である Code Gear、Data Gear、そして、Meta Code Gear 、Meta Data Gear の構成を示す。これらは、CbC に変換されて実行される。
|
|
106 Gears OS は、Task Scheduler を CPU や GPU 毎に持ち、一つの Task に対応する Context という Meta Data Gear を使用しながら計算を実行する。
|
14
|
107
|
15
|
108 Meta Gear を入れかえることにより、ノーマルレベルの Gear をモデル検査することができるようにしたい。ノーマルレベルでの Code Gear と Data Gear は
|
|
109 継続を基本とした関数型プログラミング的な記述に対応する。この記述を定理証明支援系である Agda を用いて直接に証明できるようにしたい。
|
14
|
110
|
15
|
111 従来の研究でメタ計算を用いる場合は、関数型言語では Monad を用いる\cite{Moggi:1989:CLM:77350.77353}。これは Hakell では実行時の環境を記述する構文として使われている。
|
|
112 OS の研究では、メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。Python や Haskell による記述をノーマルレベルとして
|
|
113 採用した OS の検証の研究もある\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}。
|
|
114 SMIT などのモデル検査を OS の検証に用いた例もある\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}。
|
14
|
115
|
15
|
116 本研究で用いる Meta Gear は制限された Monad に相当し、型つきアセンブラよりは大きな表現単位を提供する。
|
|
117 Haskell などの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。CbC はスタック上に隠された
|
14
|
118 環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。ただし、Gear のプログラミングスタイルは、従来の関数呼出
|
15
|
119 を中心としたものとはかなり異なる。本研究では、Gears の記述をモジュールかするためにインターフェースを導入した。これにより、
|
14
|
120 見通しの良いプログラミングが可能になった。
|
|
121
|
|
122
|
0
|
123 \section{メタ計算の重要性}
|
|
124 プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理、スレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。
|
|
125 これらの計算をメタ計算と呼ぶ。
|
|
126
|
|
127 従来の OS では、メタ計算はシステムコールやライブラリーコールの単位で行われる。
|
|
128 実行時にメタ計算の変更を行う場合には、OS 内部のパラメータの変更を使用し、
|
|
129 実行されるユーザープログラム自体への変更は限定的である。
|
|
130 しかし、メタ計算は性能測定あるいはプログラム検証、さらに並列分散計算のチューニングなど細かい処理が必要で
|
|
131 実際のシステムコール単位では不十分である。
|
|
132 例えば、モデル検査ではアセンブラあるいはバイトコード、インタプリタレベルでのメタ計算が必要になる。
|
|
133 しかし、バイトコードレベルでは粒度が細かすぎて扱いが困難になっている。
|
|
134 具体的にはメタ計算の実行時間が大きくなってしまう。
|
|
135
|
|
136 メタ計算を通常の計算から切り離して記述するためには処理を細かく分割する必要がある。しかし、関数やクラスなどの単位は容易に分割できない。
|
|
137 そこで当研究室ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を提案している。
|
|
138 これによりシステムコードよりも細かくバイトコードよりも大きなメタ計算の単位を提供できる。
|
|
139
|
|
140 Code Gear は処理の単位である。
|
|
141 関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。
|
|
142 Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実現する。
|
|
143
|
|
144 Continuation based C (CbC)\cite{cbc} はこの Code Gear 単位を用いたプログラミング言語として開発している。
|
|
145
|
15
|
146 CbC は軽量継続による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。
|
0
|
147
|
|
148 また、当研究室で開発している Gears OS\cite{gears} は Code Gear、 Data Gear の単位を用いて開発されており、CbC で記述されている。
|
|
149 CbC での記述はメタ計算を含まないノーマルレベルでの記述と、 Code Gear、Data Gear の記述を含むメタレベルの記述の2種類がある。
|
|
150 メタレベルでもさらに、メタ計算を用いることが可能になっている。
|
|
151 この2つのレベルはプログラミング言語レベルでの変換として実現される。
|
|
152 CbC は LLVM\cite{llvm} 上で実装されており、メタレベルでの変換系は本論文では、Perl による変換スクリプトにより実装されている。
|
|
153
|
|
154 Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。
|
|
155 Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。
|
|
156 Interface は複数の実装を持つことができ、Meta Data Gear によって定義される。
|
|
157 Interface の操作に対応する Code Gear の引数は Interface に定義されている Data Gear を通して行われる。
|
|
158
|
|
159 従来の関数呼び出しでは引数をスタック上に構成し、関数の実装アドレスを Call する。
|
|
160 Gears OS では引数は Context 上に用意された Interface の Data Gear に格納され、
|
|
161 操作に対応する Code Gear に goto する。
|
|
162 Context とは使用される Code Gear と Data Gear を全て格納している Meta Data Gear である。
|
|
163 これは従来のスレッド構造体に対応する。
|
|
164 つまり Gears OS では従来はコンパイラが定義する ABI(Application Binary Interface)
|
|
165 を Meta Data Gear として CbC で表現し、メタ計算として操作することができる。
|
|
166
|
|
167 ノーマルレベルでは Context を直接見ることはできず、引数は Code Gear の引数を明示する必要がある。
|
|
168 この時に呼び出し側の引数を不定長引数として追加する構文を CbC に追加した。
|
|
169 これにより Interface 間の呼び出しを簡潔に記述することが出来るようになった。
|
|
170 メタレベルでは Code Gear の引数は単一または複数の Data Gear として見ることができる。
|
|
171 これは Context を直接操作することができることを意味する。
|
|
172 この部分はノーマルレベルの Code Gear を呼び出す stub として生成される。
|
15
|
173 ノーマルレベルでの goto 文はメタ計算への goto で置き換えられる。
|
0
|
174 Gears OS でのメタ計算は stub と goto のメタ計算の2箇所で実現される。
|
|
175
|
|
176 メタ計算の例としては並列処理があり、Context を切り替えることによって複数のスレッドを実現している。
|
|
177 Context を複数の CPU に割り当てることにより並列実行を可能にしている。
|
|
178
|
|
179 \section{Continuation based C (CbC)}
|
|
180 CbC は Code Gear という処理の単位を用いて記述するプログラミング言語である。
|
|
181 Code Gear は CbC における最も基本的な処理単位である。
|
|
182 Code Gear は入力と出力を持ち、CbC では引数が入出力となっている。
|
|
183 CbC では Code Gear は \_\_code という型を持つ関数の構文で定義される。
|
|
184 ただし、これは \_\_code 型の戻り値を返すという意味ではなく、Code Gear であることを示すフラグである。
|
|
185 Code Gear は戻り値を持たないので、Cの関数とは異なり return 文は存在しない。
|
|
186
|
|
187 Code Gear から次の Code Gear への遷移は goto による継続で処理を行い、次の Code Gear へ引数として入出力を与える。
|
|
188 図\ref{fig:cs}は Code Gear 間の処理の流れを表している。
|
|
189
|
|
190 \begin{figure}[ht]
|
|
191 \begin{center}
|
|
192 \includegraphics[width=70mm]{./pic/codesegment.pdf}
|
|
193 \end{center}
|
|
194 \caption{goto による Code Gear 間の継続}
|
|
195 \label{fig:cs}
|
|
196 \end{figure}
|
|
197
|
|
198 CbC の goto による継続は Scheme の継続と異なり呼び出し元の環境がないので、この継続は単なる行き先である。
|
|
199 したがってこれを軽量継続と呼ぶ。
|
|
200 軽量継続により、並列化、ループ制御、関数コールとスタックの操作を意識した最適化がソースコードレベルで行えるようにする。
|
|
201
|
|
202 \section{Gears OS}
|
|
203 Gears OS は Code Gear とデータの単位である Data Gear を用いて開発されており、CbC で記述されている。
|
|
204 Gears OS では、並列実行するための Task を、実行する Code Gear と、実行に必要な Input Data Gear 、Output Data Gear の組で表現する。
|
|
205 Gears OS は Input/Output Data Gear の依存関係が解決された CodeGear を並列実行する。
|
|
206 Data Gear はデータの単位であり、int や文字列などの Primitive Type を持っている。
|
|
207 Code Gear は任意の数の Input Data Gear を参照して処理を行い、Output Data Gear を出力し処理を終える。
|
|
208 また、接続された Data Gear 以外には参照を行わない。
|
|
209 処理やデータの構造が Code Gear、Data Gear に閉じているため、これにより実行時間、メモリ使用量などを予測可能なものにすることができる。
|
|
210
|
|
211 Gears OS では メタ計算 を Meta Code Gear、Meta Data Gear で表現する。
|
|
212 Meta Code Gear は通常の Code Gear の直後に遷移され、メタ計算を実行する。
|
7
|
213 これを図示したものが図\ref{fig:metaCS}である。
|
|
214 %Meta Code Gear で OS の機能であるメモリ管理やスレッド管理を行う。
|
|
215
|
|
216 \begin{figure}[ht]
|
|
217 \begin{center}
|
|
218 \includegraphics[width=70mm]{./pic/metaCS.pdf}
|
|
219 \end{center}
|
|
220 \caption{Gears でのメタ計算}
|
|
221 \label{fig:metaCS}
|
|
222 \end{figure}
|
0
|
223
|
10
|
224 Gears OS は Context と呼ばれる使用されるすべての Code Gear、Data Gear 持っている Meta Data Gear を持つ。
|
12
|
225 Gears OS は必要な Code Gear、Data Gear を参照したい場合、この Context を通す必要がある。
|
7
|
226
|
|
227 しかし Context を通常の計算から直接扱うのはセキュリティ上好ましくない。
|
|
228 そこで Context から必要なデータを取り出して Code Gear に接続するMeta Code Gear である stub Code Gear を定義し、
|
|
229 これを介して間接的に必要な Data Gear にアクセスする。
|
|
230 stub Code Gear は Code Gear 毎に生成され、次の Code Gear へと継続する前に挿入される。
|
|
231 goto による継続を行うと、実際には次の Code Gear の stub Code Gear を呼び出す。
|
|
232
|
|
233 %CbC は Code Gear を処理の単位として用いたプログラミング言語であるため、Gears OS の Code Gear を記述するのに適している。
|
0
|
234
|
|
235 \section{Gears OS の構成}
|
|
236 Gears OS は以下の要素で構成される。
|
|
237
|
|
238 \begin{itemize}
|
|
239 \item Context
|
|
240 \item TaskQueue
|
|
241 \item TaskManager
|
|
242 \item Worker
|
|
243 \end{itemize}
|
|
244
|
|
245 図\ref{fig:gearsos} に Gears OS の構成図を示す。
|
|
246
|
|
247 \begin{figure}[ht]
|
|
248 \begin{center}
|
|
249 \includegraphics[width=70mm]{./pic/gears_structure}
|
|
250 \end{center}
|
|
251 \caption{Gears OS の構成図}
|
|
252 \label{fig:gearsos}
|
|
253 \end{figure}
|
|
254
|
7
|
255 %Gears OS には Context と呼ばれる接続可能な Code Gear、Data Gear のリスト、Temporal Data Gear のためのメモリ空間等を持っている Meta Data Gear を持つ。
|
|
256 %Gears OS は必要な Code Gear、Data Gear に参照したい場合、この Context を通す必要がある。
|
3
|
257 Code\ref{context} は Context の定義で Code\ref{initcontext} は Context の生成である。
|
0
|
258
|
12
|
259 \lstinputlisting[caption=Contextの定義, label=context]{./src/context1.c}
|
|
260 \lstinputlisting[label=initcontext, caption=Contextの生成]{./src/initcontext.c}
|
0
|
261
|
|
262 Data Gear は union と struct によって表現される。
|
|
263 Context には Data Gear の Data Type の情報が格納されている。
|
|
264 この情報から確保する Data Gear のサイズなどを決定する。
|
10
|
265 %Temporal Data Gear のためのメモリ空間は Context 毎に異なり、互いに干渉することはできない。
|
0
|
266
|
7
|
267 Context は Task でもあり、Taskは通常のOSのスレッドに対応する。
|
|
268 Task は実行する Code Gear と Data Gear をすべて持っている。
|
12
|
269 TaskManager によって Context が生成され TaskQueue へ挿入する。
|
0
|
270 Gears OS における Task Queue は Synchronized Queue で実現される。
|
|
271 Worker は TaskQueue から Task である Context を取得し、 Input/Output Data Gear の依存関係が解決されたものから並列実行される。
|
|
272
|
7
|
273 %\section{CbC のコードの例}
|
0
|
274
|
7
|
275 %Code\ref{excbc}は CbC で記述された stack のコードの一部である。
|
|
276 %Code Gear は \_\_code Code Gear の記述から始まり、次の Code Gear へ goto で遷移する。
|
0
|
277
|
2
|
278 %...の説明
|
0
|
279 %codegearの説明もっとする?
|
|
280
|
7
|
281 %\lstinputlisting[label=excbc, caption=CbC で記述された stack のコード]{./src/ex_stack.cbc}
|
5
|
282
|
8
|
283 \section{Interface}
|
|
284 Interface は呼び出しの引数になる Data Gear の集合であり、そこで呼び出される Code Gear のエントリである。
|
0
|
285 呼び出される Code Gear の引数となる Data Gear はここで全て定義される。
|
|
286
|
8
|
287 Code\ref{interface}は stack の Interface である。
|
0
|
288 Code Gear、Data Gear に参照するために Context を通す必要があるが、
|
8
|
289 Interface を記述することでデータ構造の api と Data Gear を結びつけることが出来る。
|
0
|
290
|
12
|
291 \lstinputlisting[label=interface, caption=StackのInterface]{./src/Stack.cbc}
|
1
|
292
|
8
|
293 Code\ref{implement}は stack の Implement の例である。
|
|
294 createImpl は関数呼び出しで呼び出され、Implement の初期化と Code Gear のスロットに対応する Code Gear の番号を入れる。
|
2
|
295 %return で interface を返し、その先で Code Gear や Data Gear へ継続できるようになる。
|
1
|
296
|
12
|
297 \lstinputlisting[label=implement, caption=SingleLinkedStackのImplement]{./src/stackimpl.cbc}
|
0
|
298
|
7
|
299 %\section{Gearef、GearImpl}
|
0
|
300
|
7
|
301 %Context には Allocation 等で生成した Data Gear へのポインタが格納されている。
|
|
302 %Code Gear が Context にアクセスする際、ポインタを使用してデータを取り出すため、Code\ref{gearef1} のようにコードが煩雑になってしまう。
|
|
303 %そこで Code Gear がデータを参照するための Gearef というマクロを定義した。
|
|
304 %Gearef に Context と型を渡すことでデータの参照が行える。
|
|
305 %また interface の実装を参照する際も、ポインタでの記述が複雑になってしまうため 同様に GearImpl を定義した。
|
|
306 %GearImpl は Context と interface 名、interface の変数名を指定して参照する。
|
|
307 %Gearef と GearImpl を用いたコードが Code\ref{gearef2}である。
|
0
|
308
|
7
|
309 %\lstinputlisting[label=gearef1, caption=定義前のコード]{./src/ex_code1}
|
|
310 %\lstinputlisting[label=gearef2, caption=Gearef、GearImplを用いたコード]{./src/ex_code2}
|
0
|
311
|
7
|
312 \section{stub Code Gear の生成}
|
2
|
313
|
|
314 Gears OS を CbC で実装する上でメタ計算の記述が煩雑であることがわかった。
|
|
315 これらのメタ計算を自動生成することにより Gears OS を記述する上においてより良い構文をユーザーに提供することにした。
|
|
316
|
0
|
317 stub Code Gear は Code Gear 間の継続に挟まれる Code Gear が必要な Data Gear を Context から取り出す処理を行うものである。
|
|
318 Code Gear 毎に記述する必要があり、そのCode Gear の引数を見て取り出す Data Gear を選択する。
|
|
319 stub Code Gear を 自動生成する generate stub を Perl スクリプトで作成することによって Code Gear の記述量を約半分にすることができる。
|
|
320
|
|
321 stub を生成するために generate\_stub は指定された cbc ファイルの \_\_code型である Code Gear を取得し、引数から必要な Data Gear を選択する。
|
|
322 generate\_stub は引数と interface を照らし合わせ、Gearef または GearImpl を決定する。
|
|
323 また、この時既に stub Code Gear が記述されている Code Gear は無視される。
|
|
324
|
|
325 cbc ファイルから、生成した stub Code Gear を加えて stub を加えたコードに変換を行う。(Code\ref{stack_c})
|
|
326
|
12
|
327 \lstinputlisting[label=stack_c, caption=stub Code Gear を加えたコード]{./src/ex_stub}
|
0
|
328
|
|
329 \section{Context の生成}
|
|
330 generate\_context は Context.h、Interface.cbc、generate\_stub で生成されたImpl.cbc を見て Context を生成する Perl スクリプトである。
|
|
331
|
|
332 \begin{figure}[ht]
|
|
333 \begin{center}
|
|
334 \includegraphics[width=70mm]{./pic/generate_context3.pdf}
|
|
335 \end{center}
|
|
336 \caption{generate\_context による Context の生成}
|
|
337 \label{fig:gc}
|
|
338 \end{figure}
|
|
339
|
|
340 Context は Meta Data Gear に相当し、Code Gear や Data Gear を管理している。
|
|
341
|
|
342 generate\_context は context の定義 (Code\ref{context}) を読み宣言されている Data Gear を取得する。
|
|
343 Code Gear の取得は指定された generate\_stub で生成されたコードから \_\_code 型を見て行う。
|
|
344 取得した Code Gear、Data Gear の enum の定義は enumCode.h、enumData.h に生成される。
|
|
345
|
|
346 Code/Data Gear の名前とポインタの対応は generate\_context によって生成される enum Code、enum Data を指定することで接続を行う。
|
|
347 また、generate context は取得した Code/Data Gear から Context の生成を行うコード (Code\ref{init_context}) も生成する。
|
|
348
|
|
349 Context には Allocation 等で生成した Data Gear へのポインタが格納されている。
|
|
350 Code Gear は Context を通して Data Gear へアクセスする。
|
|
351 Data Gear の Allocation を行うコードは dataGearInit.cに生成される。
|
|
352
|
|
353 Data Gear は union Data とその中の struct によって表現される。
|
|
354 Context には Data Gear の Data Type の情報が格納されている。
|
|
355 この情報から確保される Data Gear のサイズなどを決定する。
|
|
356
|
12
|
357 \lstinputlisting[label=init_context, caption=Perlスクリプトで生成されたinitContext]{./src/gencontext.c}
|
0
|
358
|
14
|
359 \section{比較}
|
|
360
|
|
361 従来のプログラミングスタイルとの比較。
|
|
362 Gears のプログラミングは関数呼出を中心とするプログラミングとはかなり異なる。
|
|
363 Gears は関数呼出を禁止しているわけではなく、使用する資源の制御に問題がないなら普通に関数呼出して良い。
|
|
364 Linux kernel などでは関数呼出の大半はインライン展開されることを期待してプログラミングされており、
|
|
365 関数呼出で予測できないスタックの爆発やCPU資源の浪費が起きないようにプログラミングされている。
|
|
366 Gears では Gears 間のプログラミングは戻り先や使用する資源を明示する必要がある。
|
|
367
|
|
368 goto 文での引数は通常の関数呼出と異なり、スタック(環境)に積むことができない。引数に必要な情報を含むData Gearを
|
|
369 持ち歩くスタイルとなる。一つのインタフェース内部では、これらは共通している。実際、これらはメタレベルでは、
|
15
|
370 Context というMeta Data Gear にすべて格納されている。メタレベルは、Data Gear の詳細な型は使用されない。
|
14
|
371 ノーマルレベルに移行する際に stub Code Gear を通して詳細な型が接続される。
|
|
372
|
|
373 インタフェースを再利用する際には、呼び出すインタフェースが持つ引数は保存される必要がある。これらは、実際には
|
|
374 Context 内にあるので自動的に保存されている。ノーマルレベルの記述では、... の部分にその意味が込めれている。
|
15
|
375 これは、可変長引数の...と同じ意味だと考えても良い。ただ、LLVM/GCC レベルでそれを実装するのは比較的難しい。
|
14
|
376 なので、今回はScriptによる変換を採用している。
|
|
377
|
|
378 ノーマルレベルの記述と関数型プログラミングの記述の比較。Gear は必ず継続を渡す必要がある。これは一段の
|
15
|
379 関数呼出を許しているのと同等である。70年代の Fortan の関数呼出は決まった場所に戻り先を格納するので
|
|
380 再起呼出ができなかったのと同じである。例えば Code Gears 以下のような型を持つ。ここで t は継続の型である。
|
|
381 Stack は Stack を受けとる Stack \verb|->| t という Code Gear を継続として引数で受けとる。popStack はこの引数を
|
14
|
382 呼び出す。
|
|
383
|
15
|
384 \verb|popStack : {a t : Set} -> Stack |
|
|
385
|
|
386 \verb| -> (Stack -> t) -> t|
|
14
|
387
|
|
388 つまり、Code Gear は制限された関数の形式を持っている。Data Gear は、関数型言語の直積や排他的論理和(Sum)を含むデータ型に
|
15
|
389 対応する。しかし、一つの Context で実行される Data Gear は、一つの巨大なSumに含まれるようになっている。これを
|
14
|
390 メタレベルでは、中の型の詳細に立ち入ることなく実行する。
|
|
391
|
15
|
392 Context はノーマルレベル のData Gear の他に様々なメタ情報を持つ。例えば、メモリ管理情報や実行される CPU 、あるいは、Task の
|
|
393 状態、待ち合わせている Data Gear などである。これらの情報は C やアセンブラのレベルで実装されるのと同時に、通常の Gear の
|
|
394 プログラミングにも対応する。例えば、CPU をかそうてきに Gears で記述すればソフトウェア的な並列実行を実現し、実際の
|
|
395 GPU を用いれば GPU による並列実行となる。この実行をモデル検査的な状態数え上げに対応させればモデル検査を実行できる。
|
14
|
396
|
15
|
397 Haskell などを実行可能仕様記述として用いる OS の検証\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}と、Code Gear を用いる手法は類似しているが、Code Gear の場合は、
|
14
|
398 記述を制限し、Code と仕様の対応、さらにCodeと資源の対応が明確になる利点がある。
|
|
399
|
15
|
400 型つきアセンブラ\cite{Yang:2010:SLI:1806596.1806610}は、より低レベルの関数型の記述であると言える。アセンブラの記述自体は小さく扱いやすいが、
|
|
401 OS レベルあるいはアプリケーションレベルからの距離が大きい。型の整合性を保証するだけでは OS の検証としては
|
14
|
402 不十分なので、証明やモデル検査を用いることになるが、記述量が多いのが、その際に欠点となる。
|
15
|
403 Code Gear は、より大きな単位であり、プログラミングレベルの抽象化が可能になっているので、これらの記述の
|
14
|
404 大きさの欠点をカバーできる可能性がある。
|
|
405
|
15
|
406 証明手法は、従来では Hoare Logic \cite{Chen:2015:UCH:2815400.2815402}のような Post Condition / Pre Condition を用いる方法が使われている。
|
14
|
407 現在のGearsは、Agda への変換は考えているが、その上の具体的な証明方法はまだ用意されていない。
|
|
408
|
8
|
409 %従来の OS は、ユーザーレベルとシステムレベルを持っているが、
|
|
410 %システムレベルではメタ計算の分離ができない。
|
|
411 %しかし Gears ではメタ計算を Meta Code Gear 単位で記述するため、メタ計算を階層化できる。
|
|
412 %また既存の OS ではプロセスやファイルが型を持っていないが、Gears は型を持っている。
|
|
413 %既存のOSでメタ計算を使おうとするとOSを書き換える必要がある。
|
|
414
|
|
415 %リアルタイムモニタ
|
|
416 %OSの一種の簡略バージョン
|
|
417 %Gearsに近い
|
|
418 %APIを使って資源管理を行う
|
|
419 %Gears OSの場合はメタ計算を使って行う
|
|
420
|
|
421 %GPGPU
|
|
422
|
7
|
423 %\section{結論}
|
|
424
|
8
|
425 %GearsOSのメタ計算部分の実装例を示した
|
|
426 %メタ計算の有効性
|
|
427 %Interfaceの有用性
|
|
428
|
0
|
429 \section{今後の課題}
|
10
|
430 本論文では Code Gear、 Data Gear によって構成される Gears OS のプロトタイプの設計、実装、CbC ファイルから Gears OS の記述に必要な Context と stub の生成を行う Perl スクリプトの生成を行なった。
|
|
431 Code Gear 、Data Gear を処理とデータの単位として用いて Gears OS を設計した。
|
|
432 Code Gear、Data Gear にはメタ計算を記述するための Meta Code Gear、Meta Data Gear が存在する。
|
|
433 メタ計算を Meta Code Gear、によって行うことでメタ計算を階層化して行うことができる。
|
|
434 Code Gear は関数より細かく分割されてるためメタ計算を柔軟に記述できる。
|
|
435
|
|
436 Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。
|
|
437 Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。
|
|
438 Interface は複数の実装をもち、Meta Data Gear として定義される。
|
|
439 従来の関数呼び出しでは引数をスタック上に構成し、関数の実装アドレスを Call するが、
|
|
440 Gears OS では引数は Context 上に用意された Interface の Data Gear に格納され、操作に対応する Code Gear に goto する。
|
|
441
|
|
442 Context は使用する Code Gear、Data Gear をすべて格納している Meta Data Gear である。
|
|
443 通常の計算から Context を直接扱うことはセキュリティ上好ましくない。
|
|
444 このため Context から必要なデータを取り出して Code Gear に接続する Meta Code Gear である stub Code Gear を定義した。
|
|
445 stub Code Gear は Code Gear 毎に記述され、Code Gear 間の遷移に挿入される。
|
|
446
|
|
447 これらのメタ計算の記述は煩雑であるため Perl スクリプトによる自動生成を行なった。
|
|
448 これにより Gears OS のコードの煩雑さは改善され、ユーザーレベルではメタを意識する必要がなくなった。
|
0
|
449
|
|
450 今後の課題は Code Gear からメタ計算を行う meta Code Gear を生成できるようにし、ユーザーがメタレベルの処理を意識せずにコードを記述できるようにする。
|
|
451 また、今回 Perl スクリプトによって Context や stub の生成を行なったが、LLVM/clang 上で実装しコンパイラで直接 CbC を実行できるようにすることを目的とする。
|
|
452
|
|
453 % BibTeX を使用する場合 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
454 \bibliographystyle{ipsjsort}
|
|
455 \bibliography{prosym}
|
|
456
|
|
457 % BibTeX を使用しない場合
|
|
458 %\begin{thebibliography}{9}
|
|
459 %\bibitem{latex}玉城将士、谷成雄,河野真治 : \textbf{Cassandraを使ったスケーラビリティのあるCMSの設計 }. 情報処理学会システムソフトウェアとオペレーティング・システム研究会、 2011.
|
|
460 %\bibitem{latex}玉城将士 : \textbf{非破壊的木構造を用いた分散CMSの設計と実装 }. 琉球大学理工学研究科修士論文、2013
|
|
461 %\bibitem{latex}大城信康 、杉本優 、河野真治 : \textbf{Data Segment の分散データベースへの応用}. 日本ソフトウェア科学会第30回大会論文集. 、2013
|
|
462 %\bibitem{latex}大城信康 : \textbf{分散Database Jungleに関する研究}. 琉球大学理工学研究科修士論文、2014
|
|
463 %\bibitem{latex}金川竜己、河野真治 : \textbf{非破壊的木構造データベースJungleとその評価 }. 情報処理学会システムソフトウェアとオペレーティング・システム研究会、 2015.
|
|
464 %\end{thebibliography}
|
|
465 \end{document}
|
|
466
|