Mercurial > hg > Papers > 2023 > matac-sigos
changeset 14:c0cdf7130bd8
...
author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 17 Apr 2023 09:42:47 +0900 |
parents | bb32b4cbb6d6 |
children | 619ba13d0661 |
files | Paper/paper.aux Paper/paper.log Paper/paper.pdf Paper/paper.synctex.gz Paper/paper.tex |
diffstat | 5 files changed, 66 insertions(+), 50 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/paper.aux Mon Apr 17 03:24:55 2023 +0900 +++ b/Paper/paper.aux Mon Apr 17 09:42:47 2023 +0900 @@ -3,7 +3,7 @@ \citation{cbcllvm} \citation{cbc} \newlabel{ipsj@firstpage}{{}{1}} -\@writefile{toc}{\contentsline {section}{\numberline {1}\hskip 1zw{GearsOSにおけるファイルシステム}}{1}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {1}\hskip 1zw{GearsOSにおけるファイルシステムとDB}}{1}{}\protected@file@percent } \@writefile{toc}{\contentsline {section}{\numberline {2}\hskip 1zw{Continuation based C}}{1}{}\protected@file@percent } \citation{gears} \citation{gearsos} @@ -27,23 +27,25 @@ \bibstyle{ipsjunsrt} \bibdata{matac-bib} \bibcite{modelcheck}{1} +\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{RedBlackTreeのトランザクション}}{4}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {8}\hskip 1zw{ファイルシステムにおけるスキーマ}}{4}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {9}\hskip 1zw{RedBlackTreeによる権限の表現}}{4}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {10}\hskip 1zw{まとめと今後の課題}}{4}{}\protected@file@percent } \bibcite{cbcllvm}{2} \bibcite{cbc}{3} \bibcite{gears}{4} \bibcite{gearsos}{5} \bibcite{cr}{6} \bibcite{file}{7} -\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{RedBlackTreeのトランザクション}}{4}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {8}\hskip 1zw{ファイルシステムにおけるスキーマ}}{4}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {9}\hskip 1zw{i-node numberによるインデックス}}{4}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {10}\hskip 1zw{RedBlackTreeによる権限の表現}}{4}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {11}\hskip 1zw{今後の課題}}{4}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {12}\hskip 1zw{まとめ}}{4}{}\protected@file@percent } \bibcite{cfile}{8} \bibcite{xv6kernel}{9} \bibcite{xv6component}{10} \bibcite{xv6}{11} \bibcite{christie}{12} \bibcite{directory}{13} +\@writefile{toc}{\contentsline {subsection}{\numberline {10.1}{ログなどの時系列データの保存}}{5}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {10.2}{スタンドアロンなDB}}{5}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {10.3}{インデックスの更新・作成}}{5}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {10.4}{データクエリ言語}}{5}{}\protected@file@percent } \newlabel{ipsj@lastpage}{{}{5}} \gdef \@abspage@last{5}
--- a/Paper/paper.log Mon Apr 17 03:24:55 2023 +0900 +++ b/Paper/paper.log Mon Apr 17 09:42:47 2023 +0900 @@ -1,4 +1,4 @@ -This is e-pTeX, Version 3.141592653-p4.0.0-220214-2.6 (utf8.euc) (TeX Live 2022) (preloaded format=platex 2022.6.9) 17 APR 2023 03:24 +This is e-pTeX, Version 3.141592653-p4.0.0-220214-2.6 (utf8.euc) (TeX Live 2022) (preloaded format=platex 2022.6.9) 17 APR 2023 09:42 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -3166,32 +3166,33 @@ LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <11.82813> not available (Font) Font shape `JY1/gt/m/n' tried instead on input line 99. LaTeX Font Info: Kanji font shape `JY1/gt/m/it' undefined -(Font) No change on input line 122. +(Font) No change on input line 127. File: figs/cgdg.pdf Graphic file (type pdf) <figs/cgdg.pdf> -LaTeX Font Info: Kanji font shape `JY1/gt/m/it' undefined -(Font) No change on input line 149. -LaTeX Font Info: Kanji font shape `JY1/gt/m/it' undefined -(Font) No change on input line 150. (I search kanjifont definition file: . . ) (I search font definition file: . . . . . . . ) -LaTeX Font Info: Trying to load font information for OMS+txsy on input line 154. +LaTeX Font Info: Trying to load font information for OMS+txsy on input line 150. (/usr/local/texlive/2022/texmf-dist/tex/latex/txfonts/omstxsy.fd File: omstxsy.fd 2000/12/15 v3.1 ) -LaTeX Font Info: Trying to load font information for OT1+txsy on input line 154. -LaTeX Font Info: No file OT1txsy.fd. on input line 154. +LaTeX Font Info: Trying to load font information for OT1+txsy on input line 150. +LaTeX Font Info: No file OT1txsy.fd. on input line 150. LaTeX Font Warning: Font shape `OT1/txsy/m/n' undefined -(Font) using `OT1/cmr/m/n' instead on input line 154. - -LaTeX Font Info: Trying to load font information for OT1+ptm on input line 154. +(Font) using `OT1/cmr/m/n' instead on input line 150. + +LaTeX Font Info: Trying to load font information for OT1+ptm on input line 150. (/usr/local/texlive/2022/texmf-dist/tex/latex/psnfss/ot1ptm.fd File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm. ) [1 -] (./src/hello.cbc) +] +LaTeX Font Info: Kanji font shape `JY1/gt/m/it' undefined +(Font) No change on input line 154. +LaTeX Font Info: Kanji font shape `JY1/gt/m/it' undefined +(Font) No change on input line 155. + (./src/hello.cbc) File: figs/context.pdf Graphic file (type pdf) <figs/context.pdf> File: figs/meta-cg-dg.pdf Graphic file (type pdf) @@ -3199,13 +3200,14 @@ [2] File: figs/nonDestroyTreeEdit.pdf Graphic file (type pdf) <figs/nonDestroyTreeEdit.pdf> - [3] (./paper.bbl + [3] LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <9.61035> not available -(Font) Font shape `JT1/gt/m/n' tried instead on input line 1. +(Font) Font shape `JT1/gt/m/n' tried instead on input line 372. LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <9.61035> not available -(Font) Font shape `JY1/gt/m/n' tried instead on input line 1. +(Font) Font shape `JY1/gt/m/n' tried instead on input line 372. + (./paper.bbl LaTeX Font Info: Calculating math sizes for size <8.8711> on input line 1. - + [4] Underfull \hbox (badness 10000) in paragraph at lines 9--10 []\JY1/mc/m/n/8.8711 並列信頼研究室 []\OT1/cmr/m/n/8.8711 CbC, http://www.cr.ie.u- [] @@ -3215,7 +3217,7 @@ []\JY1/mc/m/n/8.8711 並列信頼研究室 []\OT1/cmr/m/n/8.8711 GearsOS, http://www.cr.ie.u- [] -[4] + Underfull \hbox (badness 10000) in paragraph at lines 41--43 \OT1/cmr/m/n/8.8711 a sim-ple, Unix-like teach-ing op-er-at-ing sys-tem, [] @@ -3235,10 +3237,10 @@ Here is how much of TeX's memory you used: 5097 strings out of 478724 81242 string characters out of 5858393 - 628481 words of memory out of 5000000 + 627481 words of memory out of 5000000 23499 multiletter control sequences out of 15000+600000 499135 words of font info for 160 fonts, out of 8000000 for 9000 929 hyphenation exceptions out of 8191 55i,10n,63p,294b,1365s stack positions out of 10000i,1000n,20000p,200000b,200000s -Output written on paper.dvi (5 pages, 39016 bytes). +Output written on paper.dvi (5 pages, 40056 bytes).
--- a/Paper/paper.tex Mon Apr 17 03:24:55 2023 +0900 +++ b/Paper/paper.tex Mon Apr 17 09:42:47 2023 +0900 @@ -96,7 +96,7 @@ \maketitle %1 -\section{GearsOSにおけるファイルシステム} +\section{GearsOSにおけるファイルシステムとDB} アプリケーションの信頼性を保証することは 情報システムやコンピュータを用いる業務の信頼性の保障につながる重要な課題である. @@ -106,14 +106,19 @@ GearsOSは,OSの信頼性を定理証明やモデル検査を行うことで保証することを目指している\cite{modelcheck}. 同じく,当研究室で開発しているプログラム言語であるCbC(Continuation based C)で記述されており, ノーマルレベルとメタレベルを簡単に切り分けることを可能としている. -そのようにして,CbCでメタレベルの処理を切り出したものに対して,定理証明やモデル検査を行うことで信頼性を保証する. +そのようにして,CbCでメタレベルの処理を切り出したものに対して, +定理証明やモデル検査を行うことで信頼性を保証する. -GearsOSは現在OSとして重要な機能がいくつか未実装であり,その一つとしてファイルシステムが挙げられる. +GearsOSは現在OSとして重要な機能がいくつか未実装であり, +その一つとしてファイルシステムが挙げられる. ファイルシステムはファイルやディレクトリといった構造を持ち,データの保存,整理を行う. -また,OSが管理するデータの操作を人間が行いやすいようにインターフェースを提供する. OSの機能の中でも特に重要な機能であるため,GearsOSにも実装を行う必要がある. -今回GearsOSへファイルシステムを実装するにあたり, +GearsOSへファイルシステムとDBを実装するにあたり,RedBlackTreeを用いる. +DBはファイルシステムと本質的に同じ役割を持っているため同じRedBlackTreeで +表現することが可能であると考える. +よって,今回はGearsOSにおけるファイルシステムとDBをRedBlackTreeで実装するための +設計を行う. \section{Continuation based C} @@ -162,15 +167,6 @@ 同様にGearの概念を持つContinuation based C(CbC)で記述されており,ノーマルレベルとメタレベルの処理を切り分けることが容易である. また,GearsOSは現在開発途上であり,OSとして動作するために今後実装しなければならない機能がいくつか残っている. -GearsOSには現在3つの種類がある. -1つ目が型式手法による信頼性の向上を目的とした,GearsAgdaと呼ばれるGearsOSである. -これは,Agdaによって実装されている. -2つ目がユーザーレベルタスクマネジメントの実装を目的としたGearsOSがある. -これは,CbCによって実装されている. -3つ目はスタンドアロンOSの開発を目的とした,CbC\_xv6と呼ばれるGearsOSがある. -これは,教育用に開発されたx.v6 OSをCbCで書き換える形で実装している. -今回,ファイルシステムを実装する対象は3つ目のCbC\_xv6である. - ContextはGearsOS上全てのCodeGear,DataGearの参照を持ち,CodeGearとDataGearの接続に用いられる. OS上の処理の実行単位で,従来のOSにおけるプロセスに相当する機能であるといえる. また,CodeGearをDataGearの一種であると考えると,ContextはGearの概念ではMetaDataGearに当たる. @@ -212,12 +208,21 @@ \label{fig:meta-cgdg} \end{figure} +GearsOSには現在3つの種類がある. +1つ目が型式手法による信頼性の向上を目的とした,GearsAgdaと呼ばれるGearsOSである. +これは,Agdaによって実装されている. +2つ目がユーザーレベルタスクマネジメントの実装を目的としたGearsOSがある. +これは,CbCによって実装されている. +3つ目はスタンドアロンOSの開発を目的とした,CbC\_xv6と呼ばれるGearsOSがある. +これは,教育用に開発されたx.v6 OSをCbCで書き換える形で実装している. +今回,ファイルシステムを実装する対象は3つ目のCbC\_xv6である. + \section{RedBlackTreeよるファイルシステムの構成} ファイルシステムは全てRedBlackTreeで構成する. それにより,プログラムの証明がより簡単になるからである. また,ファイルシステムとDBはデータを保管するという本質的な役割は同じである. -よって,それらをまとめてRedBlackTreeで構成する. +よって,それらはまとめてRedBlackTreeで構成する. ファイルシステムとDBの違いとして,スキーマが挙げられる. DBは事前にスキーマを定義し,それに沿ってデータを挿入したり参照したりする. @@ -265,8 +270,6 @@ よって,ディスク上とメモリ上のデータ構造をRedBlackTreeに統一することが考えられる. そうすることによって,ディスク上とメモリ上のデータのやりとりは単純なコピーで実装できる. -% メモリからディスクに書き戻すタイミングの話をしたい - \section{データのロールバックとバックアップ} DBの重要な機能の一つにロールバックがある. @@ -350,10 +353,6 @@ DataGearはKernelのContextからプロセスのContextを経由して全て繋がっている. よって,KernelのContext上にキーを用いたDataGearの参照を書き込む. -\section{i-node numberによるインデックス} - - - \section{RedBlackTreeによる権限の表現} ファイルの権限はファイルシステムの重要な機能の一つであるため実装する必要がある. @@ -362,9 +361,22 @@ ルートに対してアクセスする権限がなければ, 読み書きができないといった実装になると考える. -\section{今後の課題} +\section{まとめと今後の課題} + +本論文ではGearsOSのファイルシステムとDBの設計について説明した. +今後,実装を行いながら設計と動作の確認,計測を行い, +設計の意図が反映されていることやプログラムの検証ができることを確認する必要がある. + +また,今後の課題や議題として次のようなものが挙げられる. -\section{まとめ} +\subsection{ログなどの時系列データの保存} + +\subsection{スタンドアロンなDB} + +\subsection{インデックスの更新・作成} + +\subsection{データクエリ言語} + \nocite{*} \bibliographystyle{ipsjunsrt}