Mercurial > hg > Papers > 2019 > menikon-midterm

comparison midterm.tex @ 3:f0db7d006b4f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add hgignore
author e165723 <e165723@ie.u-ryukyu.ac.jp>
date Sat, 19 Oct 2019 14:48:19 +0900
parents 61fe443393a5
children afaa3a0ba58d
comparison
equal deleted inserted replaced
2:2e8286b5f43b 3:f0db7d006b4f
3 \usepackage{picins} 3 \usepackage{picins}
4 \usepackage{fancyhdr} 4 \usepackage{fancyhdr}
5 \usepackage{listings} 5 \usepackage{listings}
6 \usepackage{caption} 6 \usepackage{caption}
7 \usepackage{latexsym} 7 \usepackage{latexsym}
8 \usepackage{url}
9 \usepackage{abstract}
10 \usepackage{float}
8 11
9 %\pagestyle{fancy} 12 %\pagestyle{fancy}
10 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿} 13 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
11 \rhead{} 14 \rhead{}
12 \cfoot{} 15 \cfoot{}
19 \setlength{\textwidth}{181mm} 22 \setlength{\textwidth}{181mm}
20 \setlength{\textheight}{261mm} 23 \setlength{\textheight}{261mm}
21 \setlength{\footskip}{0mm} 24 \setlength{\footskip}{0mm}
22 \pagestyle{empty} 25 \pagestyle{empty}
23 26
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
24 \begin{document} 56 \begin{document}
25 \title{継続を用いたxv6 kernelの書き換え} 57 \title{xv6 kernel上でのCbCによるinterfaceの実装\\CbC interface implementation in xv6 kernel}
26 \author{学籍番号 : 165723C 氏名 : 坂本昂弘 {}{} 指導教員 : 河野真治} 58 \author{学籍番号 : 165723C 氏名 : 坂本昂弘 {}{} 指導教員 : 河野真治}
27 \date{} 59 \date{}
28 \maketitle 60 \maketitle
29 \thispagestyle{fancy} 61 \thispagestyle{fancy}
30 62
31 \section{xv6を継続で書き換える意味} 63 \section{研究目的}
32 現代の OS では拡張性と信頼性を両立させることが要求されている．
33 信頼性をノーマルレベルの計算に対して保証し，拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である．
34
35 Gears OS は Continuation based C (CbC)\cite{cbc} によってアプリケーションと OS そのものを記述する．
36 OS の下ではプログラムの記述は通常の処理の他に，メモリ管理，スレッドの待ち合わせやネットワークの管理，
37 エラーハンドリング等の記述しなければならない処理が存在する．
38 これらの計算をメタ計算と呼ぶ．
39 メタ計算を通常の計算から切り離して記述するために，Code Gear，Data Gear という単位を提案している．
40 CbC はこの Code Gear と Data Gear の単位でプログラムを記述する．
41 % OS は時代とともに複雑さが増し，OS の信頼性を保証することは難しい．
42
43
44 Code Gear は goto による継続で処理を表すことができる．
45 これにより，状態遷移による OS の記述が可能となり，複雑な OS のモデル検査を可能とする．
46 また，CbC は 定理証明支援系 Agda に置き換えることができるように構築されている．
47
48 これらを用いて OS の信頼性を保証したい．
49 CbCの有効性を示すために，基本的な機能を揃えた OS である xv6 を CbC で書き換える.
50 これにより，OS の個々のシステムコールの持つ状態を明確にすることができると考えている.
51
52 CbC でシステムやアプリケーションを記述するためには，Code Gear と Data Gear を柔軟に再利用する必要があり，
53 機能を接続するAPIと実装の分離が可能であることが望ましい．
54 CbC では形式化されたモジュールシステムが提供されている.
55 xv6 の CbC 書き換えでは, このモジュールシステムを用いる.
56
57 書き換えはまだ部分的であるが, 既存の部分と両立するように設計されている. 従って, xv6 の基本的な
58 動作には変更はない. 実際に実行速度などはほとんど差がない. 逆に言えばオーバヘッドが存在しないことが確認できた.
59
60 64
61 \section{Continuation based C} 65 \section{Continuation based C}
62 CbC は処理を Code Gear という単位を用いて記述するプログラミ 66 xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語Continuation based C (CbC)を用いる.
63 ング言語である． Code Gear 間では軽量継続 (goto 文) による 67 CbCは基本的な処理単位をCodeGearとして定義し，CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である.
64 遷移を行うので，継続前の Code Gear に戻 ることはない．この記述方法は
65 図1のように状態
66 遷移ベースのプログラミングに適している．
67 68
68 \begin{figure}[ht] 69 %\lstinputlisting[label=cbcexample, caption=cbc\_example.cbc]{src/cbc_example.cbc}
69 \begin{center}
70 \includegraphics[width=70mm]{pic/codesegment.pdf}
71 \end{center}
72 \caption{goto による code gear 間の継続}
73 \label{fig:cbc}
74 \end{figure}
75 70
76 現在CbCはCコンパイラであるGCC\cite{gcc}及びLLVM\cite{llvm}をバックエンドとしたclang 71 \section{xv6}
77 % MicroCコンパイラ 72 xv6とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである.
78 上で実装されている．今回 xv6 のkernelの部分をこの CbC を 用いて書き換える． 73 \\xv6はシンプルでUnixに似た構造を持っている.
79 74
80 \section{section3} 75 \section{xv6のinterface}
81 76
82 \section{今後の課題} 77 \section{今後の課題}
83 78
84 %\begin{thebibliography}{9} 79 %\begin{thebibliography}{9}
85 80
86 \nocite{*} 81 \nocite{*}
87 %\bibliographystyle{ipsjunsrt} 82 \bibliographystyle{ipsjunsrt}
88 \bibliography{reference} 83 \bibliography{reference}
89 84
90 %\end{thebibliography} 85 %\end{thebibliography}
91 \end{document} 86 \end{document}