Mercurial > hg > Papers > 2024 > matac-master
annotate Paper/master_paper.tex @ 16:110cf95f4106
...
author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 08 Jan 2024 16:06:55 +0900 |
parents | e1326b7826e6 |
children | 66e1b4c4df1f |
rev | line source |
---|---|
2
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 \documentclass[12pt,a4paper,platex]{jreport} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 \usepackage{master_paper} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 \usepackage{ascmac} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 \usepackage[dvipdfmx]{graphicx} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 \usepackage{here} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 \usepackage{listings} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 \usepackage{comment} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 \usepackage{url} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 \usepackage[deluxe, multi]{otf} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 %\input{dummy.tex} %% font |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
14 | 16 \jtitle{GearsOSのファイルシステムにおけるGCとレプリケーション} |
17 \etitle{GC and Replication in the File System of GearsOS} | |
2
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 \year{2024年 3月} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 \eyear{March 2024} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 \author{又吉 雄斗} |
6 | 21 \eauthor{Matayoshi Yuto} |
22 \chife{指導教員:教授 和田 知久} | |
23 \echife{Supervisor: Prof. Wada Tomohisa} | |
2
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 \marklefthead{% 左上に挿入 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 \begin{minipage}[b]{.4\textwidth} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 琉球大学大学院学位論文(修士) |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 \end{minipage}} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 % \markleftfoot{% 左下に挿入 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 % \begin{minipage}{.8\textwidth} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 % Gears OS の Paging |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 % \end{minipage}} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 \newcommand\figref[1]{図 \ref{fig:#1}} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 \newcommand\coderef[1]{ソースコード \ref{code:#1}} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 \lstset{ |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 frame=single, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 keepspaces=true, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 stringstyle={\ttfamily}, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 commentstyle={\ttfamily}, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 identifierstyle={\ttfamily}, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 keywordstyle={\ttfamily}, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 basicstyle={\ttfamily}, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 breaklines=true, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 xleftmargin=0zw, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 xrightmargin=0zw, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 framerule=.2pt, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 columns=[l]{fullflexible}, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 numbers=left, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 stepnumber=1, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 numberstyle={\scriptsize}, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 numbersep=1em, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 language={}, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 tabsize=4, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 lineskip=-0.5zw, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 escapechar={@}, |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 } |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 \def\lstlistingname{ソースコード} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 \def\lstlistlistingname{ソースコード目次} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 %%% 索引のために以下の2行を追加 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 \usepackage{makeidx,multicol} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 \makeindex |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 \begin{document} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 %rome |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 \maketitle |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 \pagenumbering{roman} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 \setcounter{page}{0} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 \newpage |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 \makecommission |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 %\input{chapter/signature.tex} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 \newpage |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 %要旨 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 \input{chapter/abstract.tex} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 %発表履歴 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 \input{chapter/history.tex} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 \addcontentsline{toc}{chapter}{研究関連論文業績} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 \mainmatter |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 %目次 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 \tableofcontents |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
90 %図目次 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
91 \listoffigures |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
92 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
93 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
94 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
95 %リスト目次 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
96 % \lstlistoflistings |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
97 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
98 %chapters |
9 | 99 |
100 \chapter{GearsOSにおけるファイルシステムとDB} | |
101 | |
12 | 102 |
103 | |
104 情報システムの信頼性を確保することは重要な課題である. | |
105 2023年には銀行システムや航空機の旅客システム, | |
106 電子決済システムなどで障害が発生した\cite{zengin,ana,glory}. | |
107 信頼性の高いシステムを構築することは, | |
108 これらのような社会的影響のあるシステムの重大な障害発生防止につながり, | |
109 サービス提供者や受容者の機会的,経済的損失を防ぐことにつながる. | |
110 情報システムはアプリケーション,OS,DB,メモリやSSDなどのハードウェア, | |
111 分散ノードやネットワークなどさまざまな要素で構成される. | |
112 それらのうちどれか1つでも信頼性を損なうと, | |
113 システム全体の信頼性の低下につながる. | |
114 情報システム全体の信頼性を確保するためには, | |
115 これらの要素それぞれにおいて,信頼性を保証する必要がある. | |
9 | 116 |
117 当研究室では,信頼性の保証を目的としたGearsOSを開発している. | |
12 | 118 GearsOSは,定理証明やモデル検査などの形式手法を用いて信頼性を保証できることを目標としている.\cite{modelcheck}. |
119 一般的に信頼性を保証する手法としてテストコードを用いることが挙げられる. | |
120 しかしながら,OSなどの大規模なソフトウェアにおいて人力で記述するテストコードのみでは | |
121 カバレッジが不十分であり,検証漏れが発生する可能性がある. | |
122 GearsOSではテストコードに加え,形式手法を用いることでより高い信頼性の保証を目指している. | |
123 GearsOSは当研究室で開発しているプログラム言語であるContinuation based C(CbC)で記述されており, | |
124 ノーマルレベルとメタレベルを容易に切り分けることを可能とする拡張性を有す. | |
125 CbCによって本来行いたい処理をノーマルレベルで記述し, | |
126 信頼性を保証するための処理をメタレベルで記述するといった書き分け, | |
127 拡張を比較的容易に可能とする. | |
128 | |
129 OSの重要な機能の1つとしてファイルシステムが挙げられる. | |
130 ファイルシステムはOSのプロセスやユーザーデータの管理などに必要不可欠であるため, | |
131 GearsOSにおいても実装をする必要があると考えられ, | |
132 当研究室では分散ファイルシステムやi-nodeを用いたファイルシステムの設計がされてきた\cite{cfile, directory}. | |
9 | 133 |
12 | 134 ファイルシステムには可変長の文字列を格納するファイルと, |
135 そのファイルにアクセスするための名前管理の機能がある. | |
136 ファイルの名前の一貫性は名前管理によって保証される. | |
137 しかし,ファイルに同時に書き込まれた際の一貫性を保証する機能を | |
138 ファイルシステムとしては持っておらず, | |
139 ファイルの書き込みを制御するロック機構をアプリケーションが持つことによって, | |
140 ファイルの一貫性を保証している.ファイルシステムによく似たものとしてDBが挙げられる. | |
141 DBは入力の属性名と型の組み合わせを複数持つレコードと, | |
142 特定の属性をキーとしたテーブルがある. | |
143 また,レコードのinsert,delete,updateの直列化可能性を保証する機能を持つ. | |
144 ファイルシステムとDBは格納するものの形式やそれにアクセスする方法, | |
145 直列化可能性を保証する手法が異なるが, | |
146 データをある形式で保持する仕組みであるという本質的な部分において違いはない. | |
147 よって,ファイルシステムとDBを同一のシステムとして実装することが可能であると考える. | |
9 | 148 |
12 | 149 データのレプリケーションやガベージコレクションの仕組みに必要である, |
150 RedBlackTreeのCopyの仕組みを実装した. | |
151 | |
152 | |
153 | |
9 | 154 |
10 | 155 \chapter{軽量継続を基本とする言語CbC} |
156 | |
12 | 157 Continuation based C(CbC)\cite{cbcllvm,cbc}はC言語の下位言語であり, |
158 関数呼び出しを行わない軽量な継続を基本とするプログラミング言語である. | |
159 CbCは処理の単位のCodeGear,データの単位のDataGearといったGearの概念をもつ. | |
160 CodeGearはC言語などにおける関数と違い,gotoによるjmp命令が用いられ, | |
161 プログラムの継続においてコールスタックを持たない. | |
162 これを通常の関数による継続と区別して,軽量継続と呼ぶ. | |
163 軽量継続によってリフレクションのような処理の挿入や切り分けを容易にしている. | |
164 | |
165 \section{Gearの概念} | |
9 | 166 |
12 | 167 CbCには処理の単位のCodeGearとデータの単位であるDataGearという概念が存在する. |
9 | 168 CodeGearは\emph{\_\_code}という記述で宣言することができる. |
12 | 169 CbCはC言語の下位言語であるため,通常の関数も使用することは可能だが, |
170 基本的にCodeGearの単位でプログラミングを行う. | |
171 DataGearはCodeGearで入出力される変数データである. | |
172 図\ref{fig:dgcg}はCodeGearとDataGearの入出力の関係を表している. | |
173 CodeGearはDataGearを複数入力として受け取ることができ, | |
174 別のDataGearに複数書き込み出力することができる. | |
9 | 175 特に,入力のDataGearをInput DataGear,出力のDataGearをOutput DataGearと呼ぶ. |
12 | 176 gotoで次のCodeGearに遷移する際,Output DataGearを次のCodeGearのInput DataGearとして渡すことができる. |
9 | 177 |
178 \begin{figure}[ht] | |
179 \begin{center} | |
12 | 180 \includegraphics[width=100mm]{fig/cgdg.pdf} |
9 | 181 \end{center} |
182 \caption{CodeGearと入出力の関係図} | |
183 \label{fig:dgcg} | |
184 \end{figure} | |
185 | |
12 | 186 \section{gotoによる軽量継続} |
187 | |
9 | 188 CodeGearから次のCodeGearに遷移していく一連の動作を継続と呼ぶ. |
189 通常の関数の場合,関数から次の関数へ遷移する時にfunction callが行われる. | |
190 function callは前の関数へ戻る場合があり,そのためにcall stackを保存する. | |
191 他方,CbCの継続はfunction callをせずにgotoによるjmpで行われる. | |
12 | 192 jmpはfunction callと異なり,call stackによる変数などの環境を保存しない. |
9 | 193 よって,CbCのgotoによる継続はfunction callによる継続と比較して軽量であるといえる. |
194 そのことから,CbCにおける継続をfunction callによる継続と区別して,軽量継続と呼ぶ. | |
12 | 195 軽量継続の利点としてリフレクションのような処理をより柔軟に行える点が挙げられる. |
196 リフレクションはプログラム自身のメタデータを分析し, | |
197 それによってプログラムを実行時に書き換える一種のメタプログラミング手法である. | |
198 一般的にクラスやメソッド,関数の単位で書き換えが行われる. | |
199 手法の例としてJavaにおけるAspectJライブラリを用いたプログラミングが挙げられる. | |
200 軽量継続の場合,CodeGear遷移のどの地点においてもメタな処理を挿入することが可能であるため, | |
201 より柔軟なリフレクションが可能と考える。 | |
202 | |
203 | |
204 \section{CodeGearの記述例} | |
9 | 205 |
206 CbCのプログラム例をソースコード\ref{src:cbc}に示す. | |
207 まずmain関数においてadd1 CodeGearへgotoを行う. | |
208 その際add1へInput DataGearとしてnを渡す. | |
209 Cのgotoが\emph{goto label;}という記法で,ラベリングした箇所へjmpを行うのに対し, | |
210 CbCのgotoは\emph{goto add1(n);}という記法で,add1 CodeGearへn DataGearを渡してjmpを行う. | |
211 add1は処理の最後にadd2 CodeGearへgotoを行う. | |
212 その際Output DataGear out\_nをadd2のInput DataGearとして渡す. | |
213 このようにCbCではCodeGearのOutput DataGearを次のCodeGearのInput DataGearとして渡すことを繰り返すことで処理を進める. | |
214 | |
215 \lstinputlisting[caption=CbCのプログラム例,label=src:cbc]{src/hello.cbc} | |
216 | |
217 \chapter{信頼性の保証を目的としたGearsOS} | |
218 | |
219 GearsOS\cite{gears,gearsos,cr}は当研究室で開発している,信頼性と拡張性の両立を目的としたOSである. | |
220 GearsOSにはGearという概念があり,実行の単位をCodeGear,データの単位をDataGearと呼ぶ. | |
221 軽量継続を基本とし,stackを持たない代わりに全てをContext経由で実行する. | |
222 同様にGearの概念を持つContinuation based C(CbC)で記述されており,ノーマルレベルとメタレベルの処理を切り分けることが容易である. | |
223 また,GearsOSは現在開発途上であり,OSとして動作するために今後実装しなければならない機能がいくつか残っている. | |
224 | |
12 | 225 \section{3種類のGearsOS} |
226 | |
227 GearsOSには現在3つの種類がある. | |
228 1つ目が型式手法による信頼性の向上を目的とした,GearsAgdaと呼ばれるGearsOSである. | |
229 これは,Agdaによって実装されている. | |
230 2つ目がユーザーレベルタスクマネジメントの実装を目的としたGearsOSがある. | |
231 これは,CbCによって実装されており, | |
232 RedBlackTreeでのディレクトリシステムの構築するなどの取り組みもされている\cite{directory}. | |
233 3つ目はスタンドアロンOSの開発を目的とした,CbC\_xv6と呼ばれるGearsOSがある\cite{cbcxv6}. | |
234 これは,教育用に開発されたx.v6\cite{xv6}をCbCで書き換える形で実装する. | |
235 | |
236 \section{メタ処理を記述するmetaGear} | |
237 | |
238 図\ref{fig:meta-cgdg}はCodeGearの遷移とMetaCodeGearの関係を表している. | |
239 OSのプログラムはユーザーが実際に行いたい処理を表現するノーマルレベルと, | |
240 カーネルが行う処理を表現するメタレベルが存在する. | |
241 ノーマルレベルで見るとCodeGearがDataGearを受け取り, | |
242 処理後にDataGearを次のCodeGearに渡すという動作をしているように見える. | |
243 しかしながら,実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し, | |
244 それらの計算はMetaCodeGearで行われる. | |
245 その際,MetaCodeGearに渡されるDataGearのことは特にMetaDataGearと呼ばれる. | |
246 また,CodeGearの前に実行されるMetaCodeGearは特にstubCodeGearと呼ばれ, | |
247 メタレベルを含めるとstubCodeGearとCodeGearを交互に実行する形で遷移していく. | |
248 \begin{figure}[ht] | |
249 \begin{center} | |
250 \includegraphics[width=160mm]{fig/meta-cg-dg.pdf} | |
251 \end{center} | |
252 \caption{CodeGearとMetaCodeGearの関係} | |
253 \label{fig:meta-cgdg} | |
254 \end{figure} | |
255 | |
256 \section{CodeGearの遷移} | |
257 \section{全てのGearを参照するContext} | |
258 | |
9 | 259 ContextはGearsOS上全てのCodeGear,DataGearの参照を持ち,CodeGearとDataGearの接続に用いられる. |
260 OS上の処理の実行単位で,従来のOSにおけるプロセスに相当する機能であるといえる. | |
261 また,CodeGearをDataGearの一種であると考えると,ContextはGearの概念ではMetaDataGearに当たる. | |
262 Contextはノーマルレベルから直接参照されず,必ずMetaDataGearとしてMetaCodeGearから参照される. | |
263 それは,ノーマルレベルのCodeGearがContextを直接参照してしまうと, | |
264 メタレベルを切り分けた意味がなくなってしまうためである. | |
265 | |
266 図\ref{fig:context}はContextを参照する流れを表したものである. | |
267 まずCodeGearがOutputDataGearへデータをoutputする. | |
268 stubCodeGearはInputDataGear(前のCodeGearのOutputDataGear)とOutputDataGearをContextから参照し,次のCodeGearへgotoを行う. | |
269 CodeGearでの処理後,OutputDataGearへデータをoutputする. | |
270 | |
271 Contextはいくつかの種類に分けることができる. | |
272 OS全体のContextを管理するKernel Contextやユーザープログラムごとに存在するUser Context, | |
273 CPUやGPUごとに存在するCPU Contextがある. | |
274 \begin{figure}[ht] | |
275 \begin{center} | |
12 | 276 \includegraphics[width=150mm]{fig/context.pdf} |
9 | 277 \end{center} |
278 \caption{Contextを参照する流れ} | |
279 \label{fig:context} | |
280 \end{figure} | |
281 | |
12 | 282 \section{GearsOSの記述例} |
283 \section{GearsOSの現状} | |
9 | 284 |
14 | 285 \chapter{GearsOSのファイルシステム} |
11 | 286 \section{DataGearManagerによる分散ファイルシステム} |
287 \section{i-nodeを用いたファイルシステム} | |
288 \section{非破壊RedBlackTreeによる構成} | |
15 | 289 |
290 ディスク上とメモリ上でデータの構造は,RedBlackTreeに統一する. | |
291 一般的に,ディスク上のデータ構造としてB-Treeが用いられることが多い. | |
292 なぜならば,HDDを用いる場合はブロックへのアクセス回数を減らしデータアクセスの時間を短くするために, | |
293 B-Treeのようなノードを複数持つことができる構造が効果的だからである. | |
294 その点ではRedBlackTreeはB-Treeに劣る. | |
295 しかしながら,SSDはランダムアクセスによってデータにアクセスするため, | |
296 RedBlackTreeでなくB-Treeを用いる利点は少ないと考える. | |
297 よって,ディスク上とメモリ上のデータ構造をRedBlackTreeに統一することが考えられる. | |
298 そうすることによって,ディスク上とメモリ上のデータのやりとりは単純なコピーで実装できる. | |
299 | |
11 | 300 \section{RedBlackTreeのトランザクション} |
9 | 301 |
302 トランザクションはDBの重要な機能の一つである. | |
303 データの競合を防ぎ信頼性を向上させ,DBとしても扱えるよう | |
304 トランザクションの仕組みを考える必要がある. | |
305 今回,ファイルシステムは全てRedBlackTreeで実装するため, | |
306 RedBlackTreeのノードに対するトランザクションを考える. | |
307 | |
308 トランザクションをwriteとreadに分けて考える. | |
309 writeする場合,トランザクションはRedBlackTreeのルートの置き換えと対応する. | |
310 writeするために,まずルートを生やし書き込みが終わった後ルートを置き換える. | |
311 そのため,書き込みの並列度はルートの数と一致する. | |
312 しかしながら,ルートの置き換えは競合的なので, | |
313 複数プロセスから同時に書き込みを行っても1つしか成功しない. | |
314 よって,単一のRedBlackTreeに複数の書き込みポイントを作り, | |
315 並行実行可能にする必要がある. | |
316 | |
317 % TODO: writeトランザクションの図を入れたい | |
318 | |
319 RedBlackTreeに複数の書き込みポイントを作るために, | |
320 キーごとのルートを作成する. | |
321 ノードはそれぞれがキーとRedBlackTreeを持つ状態になる. | |
322 writeする際は,そのキーのルートを置き換える. | |
323 それによって,RedBlackTreeは複数の書き込みポイントを持つことができ, | |
324 writeを並行実行することが可能となる. | |
325 | |
326 図\ref{fig:Transaction}にトランザクショナルなwrite操作を表す. | |
327 Aの木はファイルシステム全体を表すRedBlackTreeである. | |
328 ノードNのデータに対して書き込みすることを考えると, | |
329 キーがaであるBの木のルートからロックしCの木を作成して, | |
330 Bの木からCの木のルートに入れ替えることで書き込みを行う. | |
331 この書き込みを行っている際, | |
332 Aの木のノードはロックしないのでAの木のどのノードに対しても並行して書き込み可能となる. | |
333 | |
334 \begin{figure}[ht] | |
335 \begin{center} | |
12 | 336 \includegraphics[width=100mm]{fig/transaction.drawio.pdf} |
9 | 337 \end{center} |
338 \caption{トランザクショナルなwrite操作} | |
339 \label{fig:Transaction} | |
340 \end{figure} | |
341 | |
342 % TODO: read時常に最新の情報が取れないことを説明する図を入れたい | |
343 | |
344 readはデータに変更を加えないため,複数同時に同じノードを読み込むことが可能である. | |
345 しかし,常に最新の情報を読み込めるとは限らない. | |
346 最新の情報が欲しい場合は書き込みを一旦止めるような処理が必要になる. | |
347 | |
11 | 348 \section{ディスク上とメモリ上のデータ構造} |
9 | 349 |
11 | 350 |
351 ファイルシステムは全てRedBlackTreeで構成する. | |
352 それにより,プログラムの証明がより簡単になるからである. | |
353 また,ファイルシステムとDBはデータを保管するという本質的な役割は同じである. | |
354 よって,それらはまとめてRedBlackTreeで構成する. | |
355 | |
356 ファイルシステムとDBの違いとして,スキーマが挙げられる. | |
357 DBは事前にスキーマを定義し,それに沿ってデータを挿入,参照する. | |
358 対して,ファイルシステムにはスキーマに当たるものがなく, | |
359 データはファイルパスによって管理される. | |
360 スキーマを定義することによってデータは構造化され, | |
361 構造化されたデータは非構造化データと比較して, | |
362 インデックスを作成することが容易であり,データの検索性が向上する利点がある. | |
363 しかしながら,スキーマはDBの運用中に変更されることがあり, | |
364 スキーマを変更した以前へロールバックができない問題がある. | |
365 | |
366 ロールバックがスキーマの変更によって出来なくなることは信頼性に問題があると考えると, | |
367 スキーマを定義する必要のないスキーマレスなDBが必要になる. | |
368 ファイルシステムはスキーマレスなDBといえるので,ファイルシステムを構築しつつ | |
369 DBがスキーマによって実現していた機能を付け加えることを試みる. | |
370 | |
371 RedBlackTreeは実装によって,操作が破壊的なものとそうでないものがある. | |
372 今回用いるのは,非破壊的な実装のRedBlackTreeである. | |
373 図\ref{fig:TreeEdit}は非破壊的編集を行うRedBlackTreeを表している. | |
374 編集前の木構造の6のノードをAにアップデートすることを考える. | |
375 まず,ルートノードからアップデートしたいノード6までをコピーする. | |
376 その後,コピーしたもののノード6をAにアップデートする. | |
377 これにより,アップデート前のノード6を破壊することなくAにアップデートが可能である. | |
378 参照する時は,黒のルートノードから辿れば古い6が,赤のルートノードから辿れば新しいAが見える. | |
379 この仕組みは,データのバックアップやDBのロールバックに用いることが可能だと考える. | |
380 | |
381 \begin{figure}[ht] | |
382 \begin{center} | |
12 | 383 \includegraphics[width=160mm]{fig/nonDestroyTreeEdit.pdf} |
11 | 384 \end{center} |
385 \caption{非破壊的なTree編集} | |
386 \label{fig:TreeEdit} | |
387 \end{figure} | |
388 | |
389 | |
14 | 390 \chapter{GearsFileSystemにおけるGCとレプリケーション} |
391 \section{ファイルシステムの信頼性に関する機能} | |
392 | |
393 ファイルシステムはデータを保持することを基本的な機能としている. | |
394 信頼性に関する機能など,その他の機能は追加機能として実装する. | |
395 ファイルシステムやDBにおける信頼性に関する追加機能として, | |
396 システムの電源断時にデータが残るpersistency, | |
397 データを書き込めたかどうかを判定するatomic write, | |
398 1つのノードが失われた際にデータを保護する多重性, | |
399 複数のコピーを調停するコミット機構などが挙げられる. | |
15 | 400 |
14 | 401 現状のGearsOSには分散ファイルシステムの通信機能やUnix Likeな |
402 インターフェースを持つi-nodeファイルシステムの基本機能は存在するものの, | |
403 多重性やメモリ管理などの信頼性を確保するための機能が存在しない. | |
404 データの多重度を確保するための一般的な手法として, | |
405 データのバックアップやシステム自体のレプリケーションをすることが挙げられる. | |
406 メモリ管理の機能としてはガーベージコレクションが挙げられる. | |
15 | 407 ガベージコレクションは通常プログラム言語のレイヤで行われる. |
408 これらの機能を実装することでファイルシステムの信頼性を高めたい. | |
14 | 409 |
16 | 410 \section{メモリの管理手法} |
14 | 411 |
15 | 412 GCのアルゴリズムは大きく分けてMark \& Sweep GC,Reference counting GC, |
413 Copying GCの3つの種類が存在する. | |
16 | 414 Mark \& Sweep GC |
415 Reference counting GC | |
15 | 416 CopyingGCはメモリ上のヒープ領域をFrom領域とTo領域に分割し, |
417 ルートから参照できるオブジェクトをFrom領域からTo領域にコピーすることで | |
418 ガベージコレクションを行う. | |
419 | |
420 また,Rust言語のスマートポインタによるメモリ管理手法も存在する. | |
421 | |
16 | 422 \section{GearsFileSystemのGC} |
423 | |
15 | 424 GearsFileSystemのGCはCopyingGCを基本的なアルゴリズムとする. |
425 | |
426 GearsFileSystemにおけるデータは全てRedBlackTreeに格納する. | |
14 | 427 また,ディスク上とメモリ上のデータ構造は同一である. |
15 | 428 よって,RedBlackTreeの単なるコピーによってGCを行うことによって, |
429 データの透過性が確保され,単純なプログラムで実装することが可能と考える. | |
14 | 430 |
431 | |
432 \section{GearsFileSystemのレプリケーション} | |
11 | 433 |
434 \chapter{CopyRedBlackTreeの実装} | |
14 | 435 |
436 データのバックアップやレプリケーション,GCの機能を実装するためには, | |
437 データのコピーをする必要がある. | |
438 GearsOSのファイルシステムにおいて,データは全てRedBlackTreeに格納される. | |
439 しかしながら,現状のRedBlackTreeには木をコピーする機能が無い. | |
440 よって,RedBlackTreeに木のコピー機能を実装する必要がある. | |
441 | |
11 | 442 \section{コピーのアルゴリズム} |
443 \section{Stackの使用に関して} | |
444 \section{証明のしやすさについて} | |
445 | |
446 | |
447 DBの重要な機能の一つにロールバックがある. | |
448 RDBのロールバックは, | |
449 コミットするまではトランザクションの開始時点に戻ることができる機能を持つ. | |
450 コミットが完了するとそれ以前の状態に戻すことはできないが, | |
451 データのバックアップをとっておくことで復元を行う. | |
452 このような,ロールバックとバックアップの仕組みをファイルシステムに実装したい. | |
453 | |
454 今回は,RedBlackTreeのルートノードがデータのバージョンの役割を果たしていることを利用し, | |
455 データの復元が行える仕組みを構築することを考える. | |
456 非破壊的なTree編集はアップデートのたびに,ルートノードを増やす. | |
457 つまり,ルートノードはアップデートのログと言えその時点のデータのバージョンを表していると考えることができる. | |
458 よって,ロールバックを行いたい場合は参照を過去のルートノードに切り替える. | |
459 | |
460 ルートノードはデータのアップデート時に増えるため, | |
461 データが際限なく増加していく問題がある. | |
462 この問題はCopyingGCを行うことによって解決する. | |
463 まず,RedBlackTreeを丸ごとコピーして最新のルートを残して他のルートは削除する. | |
464 その後,コピーしたものはバックアップないしログとしてディスクに書き込む. | |
465 そうすることで,データの増加によるリソースの枯渇を防ぎ, | |
466 かつデータのログ付きバックアップを作成することで信頼性の向上が期待できる. | |
467 | |
468 % TODO: バックアップのフローを図にしたい | |
469 | |
470 | |
471 \chapter{まとめと今後の課題} | |
472 | |
473 本論文ではGearsOSのファイルシステムとDBの設計について説明した. | |
474 今後,実装を行いながら設計と動作の確認,計測を行い, | |
475 設計の意図が反映されていることやプログラムの検証ができることを確認する必要がある. | |
476 | |
477 また,今後の課題や議題として次のようなものが挙げられる. | |
478 | |
479 \section{ファイルシステムにおけるスキーマ} | |
9 | 480 |
481 従来のRDBのようなスキーマが存在すると, | |
482 個別にバックアップなどを取らない限り | |
483 スキーマの変更以前にロールバックすることができない. | |
484 しかしながら,実際運用する上でスキーマを変更することは多々ある. | |
485 これは,データの信頼性を低下させると考える. | |
486 また,DB上のデータ構造とプログラム上で扱うデータ構造に差が生まれる | |
487 インピーダンスミスマッチが発生し,DBのデータをプログラムが扱う際に | |
488 その差を埋めるような変換を必要とする場合が生まれる. | |
489 一方で,スキーマがあることによってデータに対して高度な操作を行うことができ, | |
490 また,インデックスを容易に作成することができるといったメリットがある. | |
491 よって,スキーマフルなDBとスキーマレスなDBはそれぞれメリットデメリットがあり, | |
492 状況によって使い分けるのが良いと考える. | |
493 | |
494 今回は,非構造化データ内であれば構造化データを扱うことが可能であることと, | |
495 信頼性を保証したいという点から, | |
496 スキーマレスなDBとしてのファイルシステムを考える. | |
497 しかしながら,トランザクションの仕組みを作る上でRedBlackTreeに対し, | |
498 キーを設定することから完全なスキーマレスとは言えない構成となる. | |
499 | |
500 GearsOSのデータは全てDataGearで表される. | |
501 よって,GearsOSにおけるファイルシステムはDataGearの集合となる. | |
502 スキーマレスとはキーがない状態のことといえるが, | |
503 DataGearはキーが設定されていないため,その集合自体にスキーマは無い. | |
504 そのことから,GearsOSにおけるスキーマとはDataGear上のキーの構成であることがわかる. | |
505 なお,今回のRedBlackTreeによる構成の場合,キーはRedBlackTreeを指す. | |
506 DataGearはKernelのContextからプロセスのContextを経由して全て繋がっている. | |
507 よって,KernelのContext上にキーを用いたDataGearの参照を書き込む. | |
508 | |
11 | 509 \section{RedBlackTreeによる権限の表現} |
9 | 510 |
511 ファイルの権限はファイルシステムの重要な機能の一つであるため実装する必要がある. | |
512 今回のRedBlackTreeによる構成の場合,木のルートの所持者を設定することが | |
513 ファイルに対して権限を設定することにあたる. | |
514 ルートに対してアクセスする権限がなければ, | |
515 読み書きができないといった実装になると考える. | |
516 \section{データクエリ言語} | |
517 | |
518 ユーザーやアプリケーションがDBのデータにアクセスするための言語設計を | |
519 する必要がある. | |
520 RedBlackTreeのキーを用いたインデックスに対応し, | |
521 従来のSQLと比較してより柔軟なクエリを実行できることを目指したい. | |
522 | |
523 \section{ログなどの時系列データの保存} | |
524 | |
525 時系列データは通常のデータと違った保存の方法を考えることができる. | |
526 時系列に並んでいることを生かしたデータの保存方式や, | |
527 時間経過に伴うデータの重要性の変化を考慮に入れたデータ圧縮の方法をとることで, | |
528 より効率的な保存が可能だと考える. | |
529 | |
530 \section{スタンドアロンなDB} | |
531 | |
532 MySQLやPostgreSQLなどはOSの機能としてではなく, | |
533 それ自体が一つのアプリケーションとして自立的に動作している. | |
534 自立的に動作するのは,データのポータビリティを向上させるためである. | |
535 スタンドアロンなDBの形にするか, | |
536 その他の方法でポータビリティを向上させる手法を考えたい. | |
2
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
537 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
538 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
539 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
540 % %謝辞 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
541 \input{chapter/thanks.tex} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
542 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
543 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
544 %参考文献 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
545 \nocite{*} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
546 \bibliography{reference} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
547 \bibliographystyle{junsrt} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
548 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
549 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
550 %発表履歴 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
551 %\addcontentsline{toc}{chapter}{発表履歴} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
552 %\input{chapter/history.tex}] |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
553 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
554 %付録 |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
555 \addcontentsline{toc}{chapter}{付録} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
556 \appendix |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
557 \input{chapter/appendix.tex} |
c8151a82f313
copy tex files from ikki master
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
558 \end{document} |