|
0
|
1 \documentclass[twocolumn,twoside,9.5pt]{jarticle}
|
|
|
2 \usepackage[dvipdfmx]{graphicx}
|
|
|
3 \usepackage{picins}
|
|
|
4 \usepackage{fancyhdr}
|
|
|
5 \usepackage{listings}
|
|
|
6 \usepackage{caption}
|
|
|
7 \usepackage{latexsym}
|
|
3
|
8 \usepackage{url}
|
|
|
9 \usepackage{abstract}
|
|
|
10 \usepackage{float}
|
|
0
|
11
|
|
|
12 %\pagestyle{fancy}
|
|
|
13 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
|
|
|
14 \rhead{}
|
|
|
15 \cfoot{}
|
|
|
16
|
|
|
17 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
|
|
|
18 \setlength{\headheight}{0mm}
|
|
|
19 \setlength{\headsep}{5mm}
|
|
|
20 \setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
|
|
|
21 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
|
|
|
22 \setlength{\textwidth}{181mm}
|
|
|
23 \setlength{\textheight}{261mm}
|
|
|
24 \setlength{\footskip}{0mm}
|
|
|
25 \pagestyle{empty}
|
|
|
26
|
|
3
|
27 \usepackage{comment}
|
|
|
28 \usepackage{listings}
|
|
|
29 \lstset{
|
|
|
30 language=C,
|
|
|
31 tabsize=2,
|
|
|
32 frame=single,
|
|
|
33 basicstyle={\ttfamily\footnotesize}, %
|
|
|
34 identifierstyle={\footnotesize}, %
|
|
|
35 commentstyle={\footnotesize\itshape}, %
|
|
|
36 keywordstyle={\footnotesize\bfseries}, %
|
|
|
37 ndkeywordstyle={\footnotesize}, %
|
|
|
38 stringstyle={\footnotesize\ttfamily},
|
|
|
39 breaklines=true,
|
|
|
40 captionpos=b,
|
|
|
41 columns=[l]{fullflexible}, %
|
|
|
42 xrightmargin=0zw, %
|
|
|
43 xleftmargin=1zw, %
|
|
|
44 aboveskip=1zw,
|
|
|
45 numberstyle={\scriptsize}, %
|
|
|
46 stepnumber=1,
|
|
|
47 numbersep=0.5zw, %
|
|
|
48 lineskip=-0.5ex,
|
|
|
49 }
|
|
|
50 \renewcommand{\lstlistingname}{Code}
|
|
|
51 \usepackage{caption}
|
|
|
52 \captionsetup[lstlisting]{font={small, tt}}
|
|
|
53
|
|
|
54 \renewcommand{\abstractname}{概要}
|
|
|
55
|
|
0
|
56 \begin{document}
|
|
3
|
57 \title{xv6 kernel上でのCbCによるinterfaceの実装\\CbC interface implementation in xv6 kernel}
|
|
0
|
58 \author{学籍番号 : 165723C 氏名 : 坂本昂弘 {}{} 指導教員 : 河野真治}
|
|
13
|
59 \date{2019年10月23日}
|
|
0
|
60 \maketitle
|
|
|
61 \thispagestyle{fancy}
|
|
|
62
|
|
18
|
63 \section{xv6のOSの信頼性保証}
|
|
9
|
64 現代ではOSの信頼性の保証と拡張性の実現が求められている.
|
|
11
|
65 信頼性をノーマルレベルの計算に対して保 証し，拡張性をメタレベルの計算で実現することを目標にContinuation based C (CbC)を用いて Gears OS を設計中である.
|
|
18
|
66 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換えようとしている.
|
|
11
|
67
|
|
18
|
68 CbCにはCodeGearという処理の基本的な単位があり,これらを利用する事によってstackに値を積む事なくCodeGear間を遷移することができる.
|
|
|
69 %そのため,CbCのInterfaceを使うとモジュール化ができる.また,
|
|
|
70 stackが無い事によってOS内部の明確化が実現できる.
|
|
9
|
71 %CbCを用いた Gears OSの研究を行なっている.
|
|
|
72 %しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える.
|
|
11
|
73 %形式手法
|
|
|
74 さらにCbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,CbCの関数などが正常な動きをしているのかどうかを判断することが可能となる．
|
|
|
75 %CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる.
|
|
20
|
76 CbCのInterface は Gears OS のモジュール化の仕組みである. このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応し,導入することで仕様と実装に分けて記述することが出来る.そのため,CbCのInterfaceを使うとモジュール化ができる.
|
|
0
|
77
|
|
12
|
78 これらのことを用い,CbCのInterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい.
|
|
|
79 また,xv6のInterface実装によりモジュール化が可能とし,拡張性の実現を目指す.
|
|
5
|
80
|
|
|
81 \section{xv6}
|
|
12
|
82 xv6\cite{xv6}とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである.
|
|
10
|
83 xv6 はオリジナルである v6 が非常に古いC言語で書かれている為, ANSI-Cに書き換えられ x86 に再実装された. xv6 はreadやwriteなどのsystemcall,プロセス,仮想メモリ,カーネルとユーザーの分離,割り込み,ファイルシステムなどUnixの基本的な構造を持っている.
|
|
9
|
84
|
|
0
|
85 \section{Continuation based C}
|
|
4
|
86 xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語 Continuation based C (CbC)を用いる.
|
|
|
87 CbC は基本的な処理単位を CodeGearとして定義し，CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である.
|
|
10
|
88 CodeGearは返り値を持たない為,関数内で処理が終了すると呼び出し元の関数に戻ることがなく別のCodeGearへ遷移する.
|
|
11
|
89 以下のCode1にCodeGear遷移時のコード例を示す.
|
|
|
90 \lstinputlisting[label=cbcexample, caption=CodeGearの継続の例]{src/cbc_example.cbc}
|
|
10
|
91 %図かコードを入れても良いかも
|
|
11
|
92
|
|
4
|
93 またCbCにおけるCodeGear間の継続にはスタックが使用できず,呼び出し元の環境などを持たない為軽量継続と呼ぶ.
|
|
5
|
94 現在CbCはCコンパイラであるGCC及びLLVMをバックエンドとしたclang上で実装されている．
|
|
15
|
95 %今回 ,このCbCに存在するInterfaceをxv6に実装していく.
|
|
11
|
96
|
|
5
|
97
|
|
0
|
98
|
|
9
|
99 \section{CbCとAgdaの対応}
|
|
|
100 Agdaとは定理証明を支援する関数型のプログラミング言語である.
|
|
|
101 数学の証明に使われる自然演繹と型付きλ計算については対応があり,Agdaでは型付きλ計算を記述する事によって検証することができる.
|
|
5
|
102
|
|
9
|
103 CbCでは継続を用いてプログラムを記述する.同じくAgdaにも継続の記述方式が存在する.これらの記述は対応している.
|
|
|
104 以上のことよりCbCをAgdaに書き換える事ができ,CbCで記述されたプログラムはAgdaによって検証することが可能である.
|
|
5
|
105 %CbCはAgdaに変換できるように設計されている為,CbCで実装したプログラムはAgdaによって定理証明が可能である.ー＞ってことを書けば良い？
|
|
|
106
|
|
|
107
|
|
|
108 \section{context}
|
|
9
|
109 contextとは一連の実行が行われる際に使用されるCodeGearとDataGearの集合である.
|
|
|
110 従来のスレッドやプロセスに対応する.Context は接続可能な CodeGear, Data Gear のリスト. Data Gear を確保するメモリ空間,実行される Task への Code Gear 等を持っている.
|
|
11
|
111 CodeGearが別のCodeGearに遷移する際,必ずcontextを参照しenumで定義されたCodeGearの番号を指定し遷移する.ノーマルレベルで見た際のCodeGar,DataGerおよびcontextの関係を以下の図1に簡潔に示す.
|
|
|
112
|
|
|
113 \begin{figure}[ht]
|
|
|
114 \begin{center}
|
|
|
115 \includegraphics[width=65mm]{pic/context.pdf}
|
|
|
116 \end{center}
|
|
|
117 \caption{CodeGear,DataGear,contxtの関係図}
|
|
|
118 \label{fig:perl6buil}
|
|
|
119 \end{figure}
|
|
|
120
|
|
6
|
121
|
|
10
|
122 %metaGearの話もした方が良い
|
|
9
|
123 %CbCのcontextには引数の置き場所が書いてある.contextの中にDatagearが存在し.enumの番号で管理している。
|
|
5
|
124 %dataの保存先と実行するdategearの保存先
|
|
|
125
|
|
|
126 %パルスさんの修論
|
|
|
127
|
|
|
128 %コンテキストには引数置き場所が書いてあるー＞CodeGear
|
|
12
|
129 \section{CbCのInterface}
|
|
18
|
130 先述した通り, CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり，そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される. Interface を定義することで複数の実装を持つことができる.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応し,導入することで仕様と実装に分けて記述することが出来る.%CbCを agdaに対応するために関数プログラミングスタイルで書く事によってInterfaceの検証も可能になる.
|
|
12
|
131
|
|
17
|
132 以下の図2は, QueueのInterfaceとSingleLinkedQueueの実装例である.
|
|
16
|
133
|
|
|
134 %\lstinputlisting[label=cbcexample, caption=CodeGearの継続の例]{src/cbc_queue.cbc}
|
|
12
|
135
|
|
|
136 \begin{figure}[ht]
|
|
|
137 \begin{center}
|
|
|
138 \includegraphics[width=65mm]{pic/gotoInterface.pdf}
|
|
|
139 \end{center}
|
|
17
|
140 \caption{QueueのInterfaceとSingleLinkedQueueの実装例}
|
|
12
|
141 \label{fig:perl6buil}
|
|
|
142 \end{figure}
|
|
11
|
143
|
|
17
|
144 \section{xv6のinterface}
|
|
11
|
145
|
|
17
|
146 %CbCのCodeGear間の遷移時はstackに値を積むことがない.よってCbCのInterfaceを用いる事によってxv6のInterfaceを実装した際, OSの内部が明確化され信頼性を保証することができる.
|
|
|
147 先述したCbCのInterfaceをxv6のInterfaceに実装する事によって仕様と実装を分けて記述できる.
|
|
12
|
148
|
|
|
149 先行研究\cite{CbC}ではxv6のkernelの一部であるsyscallの部分をCbCによって書き換えされている.それを元にxv6のkernel部のどの部分Interfaceをし,実装するべきかを考察した.以下の図3では, syscallのさらに一部分であるsys\_readをInterfaceを用いて実装するとどうなるか考慮したものを簡潔に表した.
|
|
16
|
150
|
|
12
|
151 %\newpage
|
|
|
152 \begin{figure}[ht]
|
|
|
153 \begin{center}
|
|
|
154 \includegraphics[width=65mm]{pic/xv6_interface.pdf}
|
|
|
155 \end{center}
|
|
|
156 \caption{sys\_readのInterfaceとその実装の考案}
|
|
|
157 \label{fig:perl6buil}
|
|
|
158 \end{figure}
|
|
|
159
|
|
|
160 xv6のkernel部がどのような動きをし,処理はどんな手順を踏むのかを考慮しながらxv6にInterfaceを実装していく.
|
|
|
161
|
|
5
|
162 %呼び出されたCodeGearの番号とcontext上のinterfaceの引数で状態が分かる．
|
|
0
|
163 \section{今後の課題}
|
|
12
|
164 先行研究\cite{CbC}によって,xv6のkernelの一部をCbCの特徴でもある継続を用いモジュール化された.
|
|
|
165 しかし現在では, xv6にinterfaceはまだ搭載されていない.そのため今後, xv6のkernelをinterfaceを用いる事によってどのようにモジュール化できるかInterfaceとその実装を考察しながらCbCのinterfaceをxv6に実装していく必要がある.
|
|
|
166 また,CbCのIntterfaceを利用しているためAgdaを用いて検証することが可能であるため,実装が正しい実装なのか検証することも求められる.
|
|
|
167
|
|
0
|
168 %\begin{thebibliography}{9}
|
|
|
169
|
|
|
170 \nocite{*}
|
|
8
|
171 \bibliographystyle{junsrt}
|
|
0
|
172 \bibliography{reference}
|
|
|
173
|
|
|
174 %\end{thebibliography}
|
|
|
175 \end{document} |
