Mercurial > hg > Papers > 2024 > matac-master
changeset 55:d8533d9ab912
fix
author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 03 Feb 2024 14:46:07 +0900 |
parents | ab4ebfc6a1db |
children | 40e504bb5ea0 |
files | Paper/chapter/abstract.tex Paper/master_paper.pdf Paper/master_paper.tex Paper/reference.bib Paper/src/hello.cbc TODO.md mindmaps/gears_fs_db.mm |
diffstat | 7 files changed, 83 insertions(+), 66 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/chapter/abstract.tex Fri Feb 02 01:41:53 2024 +0900 +++ b/Paper/chapter/abstract.tex Sat Feb 03 14:46:07 2024 +0900 @@ -3,40 +3,24 @@ 当研究室では,Continuation based C(CbC)を用い, 定理証明やモデル検査などで信頼性を保証することを目的としたGearsOSを開発している. OSの重要な機能の一つにファイルシステムが存在し, -GearsOSにおいても分散ファイルシステムの仕組みやi-nodeベースのファイルシステムの実装がされてきた. +GearsOSにおいても分散ファイルシステムの仕組みやi-nodeベースのファイルシステムの実装を行なってきた. しかし,現状のGearsOSのファイルシステムにはデータの多重性を確保するレプリケーションやバックアップの機能や, -メモリリークやメモリのフラグメンテーションを解消するガベージコレクション機能が存在しない. +非破壊構造の増大やメモリのフラグメンテーションを解消するガベージコレクション機能が存在しない. よって,これらをGearsOSのファイルシステムのレベルで実装することで, より確実にデータの多重度やメモリの安全性の向上を図ることができると考える. -ガベージコレクションやレプリケーションを実装するにはデータをコピーする機能が必要不可欠である. +ガベージコレクションやレプリケーションを実装する際は,データをコピーする機能が必要不可欠である. GearsOSではデータをRedBlackTreeの形式で保持するため, -RedBlackTreeをコピーすることによってデータのコピーを行うことができる. -しかし,GearsOSのRedBlackTreeには木をコピーする機能が存在しない. +RedBlackTreeをコピーすることによってデータのコピーを行うことができるものの, +現状はGearsOSのRedBlackTreeには木をコピーする機能が存在しない. 本研究では,ファイルシステムのレプリケーションやガベージコレクションなどの機能を実装するために必要な RedBlackTreeのコピー機能について設計,構築,考察と それを用いたレプリケーションやガベージコレクション機能の設計,考察を行う. RedBlackTreeのコピーでそれぞれの機能を統一的に実装することで, -よりシンプルでデータの一貫性が確保された, +よりシンプルかつデータの持続性が確保された, 定理証明などの形式手法を適用しやすいシステムを実現することを目指す. \chapter*{Abstract} -In our research lab, we are developing GearsOS, -aimed at ensuring reliability through the use of Continuation based C (CbC) for theorem proving and model checking. -A critical component of any operating system is its file system, -and in GearsOS, there has been implementation of mechanisms for a distributed file system and i-node based file system structures. -However, the current GearsOS file system lacks features for data replication and backup to ensure data redundancy, -as well as garbage collection functionalities to resolve memory leaks and memory fragmentation. -Therefore, by implementing these features at the file system level of GearsOS, -we aim to more reliably enhance data redundancy and memory safety. -For the implementation of garbage collection and replication, -the capability to copy data is essential. -In GearsOS, data is stored in the form of a RedBlackTree. -Hence, copying the RedBlackTree enables data duplication. -However, GearsOS's RedBlackTree currently lacks the functionality to duplicate the tree itself. -This research involves the design, construction, and examination of the required RedBlackTree copy functionality for implementing file system replication and garbage collection. -Further, we explore the design and examination of replication and garbage collection functionalities using this capability. -By uniformly implementing these functionalities through RedBlackTree copying, -we aim to realize a simpler system with consistent data, -more conducive to formal methods applications such as theorem proving. \ No newline at end of file +In our laboratory, we are developing GearsOS with the aim of ensuring reliability through theorem proving and model checking, utilizing Continuation based C (CbC). One of the critical components of an operating system is its file system. In GearsOS, we have implemented mechanisms for distributed file systems as well as i-node based file system architectures. However, the current file system in GearsOS lacks replication and backup functionalities for data multiplicity assurance, as well as garbage collection features to address non-destructive structure growth and memory fragmentation. Implementing these features at the file system level in GearsOS would enhance data redundancy and memory safety significantly. +Implementing garbage collection and replication is imperative, necessitating the functionality to copy data. In GearsOS, data is stored in the format of RedBlackTrees. While copying data can be achieved by duplicating RedBlackTrees, currently, there is no functionality within GearsOS's RedBlackTrees for tree duplication. This research focuses on designing, constructing, and discussing the necessary copy functionality for RedBlackTrees to implement file system replication and garbage collection features. By unifying these functionalities through RedBlackTree copying, our goal is to realize a simpler system with ensured data persistence, facilitating the application of formal methods such as theorem proving. \ No newline at end of file
--- a/Paper/master_paper.tex Fri Feb 02 01:41:53 2024 +0900 +++ b/Paper/master_paper.tex Sat Feb 03 14:46:07 2024 +0900 @@ -13,7 +13,7 @@ %\input{dummy.tex} %% font -\jtitle{GearsOSのファイルシステムにおけるGCとレプリケーション} +\jtitle{GearsOSのファイルシステムにおけるGCと\\レプリケーション} \etitle{GC and Replication in the File System of GearsOS} \year{2024年 3月} \eyear{March 2024} @@ -93,28 +93,25 @@ \chapter{GearsOSにおけるファイルシステムとDB} 情報システムの信頼性を確保することは重要な課題である. -2023年には銀行システムや航空機の旅客システム, -電子決済システムなどで障害が発生した\cite{zengin,ana,glory}. -信頼性の高いシステムを構築することは, -これらのような社会的影響のあるシステムの重大な障害発生防止につながり, -サービス提供者や受容者の機会的,経済的損失を防ぐことにつながる. -情報システムはアプリケーション,OS,DB,メモリやSSDなどのハードウェア, -分散ノードやネットワークなどさまざまな要素で構成される. -それらのうちどれか1つでも信頼性を損なうと, -システム全体の信頼性の低下につながる. -情報システム全体の信頼性を確保するためには, -これらの要素それぞれにおいて,信頼性を保証する必要がある. +2023年には,銀行,航空機予約,電子決済などのシステムで障害が発生し, +社会的な影響を及ぼした\cite{zengin,ana,glory}. +これらのシステムの不具合を防ぎ, +提供者や利用者のリスクを最小限に抑えるためには,堅牢なシステム構築が不可欠である. +アプリケーション,オペレーティングシステム,データベース,そして物理的なコンポーネントまで, +様々な要素が連携してこれらのシステムを支えており, +これらの一つ一つに対する厳密な検証が,全体としての堅牢性を高めることに繋がる. -当研究室では,信頼性の保証を目的としたGearsOSを開発している. -GearsOSは,定理証明やモデル検査などの形式手法を用いて信頼性を保証できることを目標としている.\cite{modelcheck}. -一般的に信頼性を保証する手法としてテストコードを用いることが挙げられる. +当研究室では,信頼性の保証を目的としたGearsOSを開発しており, +定理証明やモデル検査などの形式手法を用いて信頼性を保証できることを目標としている.\cite{modelcheck}. +一般的にソフトウェアの動作を検証する手法としてテストコードを用いることが挙げられる. しかしながら,OSなどの大規模なソフトウェアにおいて人力で記述するテストコードのみでは カバレッジが不十分であり,検証漏れが発生する可能性がある. -GearsOSではテストコードに加え,形式手法を用いることでより高い信頼性の保証を目指している. +よって,GearsOSはテストコードに加え, +形式手法を用いることでより厳密に動作検証を行うことができるソフトウェアの構築を目指す. GearsOSは当研究室で開発しているプログラム言語であるContinuation based C(CbC)で記述されており, ノーマルレベルとメタレベルを容易に切り分けることを可能とする拡張性を有す. CbCによって本来行いたい処理をノーマルレベルで記述し, -信頼性を保証するための処理をメタレベルで記述するといった書き分け, +形式手法の処理をメタレベルで記述するといった書き分け, 拡張を比較的容易に可能とする. OSの重要な機能の1つとしてファイルシステムが挙げられる. @@ -135,13 +132,14 @@ よって,ファイルシステムとDBを同一のシステムとして実装することが可能であると考える. ファイルシステムはOSにおいて重要な機能であるためGearsOSにおいても実装をする必要があると考えられ, -当研究室では分散ファイルシステムやi-nodeを用いたファイルシステムの設計がされてきた\cite{cfile, directory}. -しかしながら,データの多重度や一貫性を確保するための機能がないため実装したい. -本研究では,GearsOSにおいてデータの一貫性を確保しつつ, -レプリケーションやガベージコレクションのを実装するためにに必要である, -RedBlackTreeのCopyの仕組みを設計,構築を行った. -また,それを用いたレプリケーションやガベージコレクション, -バックアップ機能の設計に関する考察を行った. +当研究室では分散ファイルシステムやi-nodeを用いたファイルシステムの設計をしてきた\cite{cfile, directory}. +それらのファイルシステムは基本構造として非破壊RedBlackTreeを持つ. +しかし,非破壊RedBlackTreeはデータが無尽蔵に増加するため,実用上の問題があると言える. +よって,データの増加を防ぐような仕組みが必要である. +また,本システムにはデータの多重度や一貫性を確保するための機能がないため実装したい. +本研究では,GearsOSのデータの多重度や一貫性の確保, +非破壊RedBlackTreeの無尽蔵な増加を防ぐためのGCとレプリケーション,バックアップ機構の設計を行い, +それらを実現するために必要なRedBlackTreeのコピーの仕組みの設計,構築,考察を行った. \chapter{軽量継続を基本とする言語CbC} @@ -156,7 +154,7 @@ \section{Gearの概念} CbCには処理の単位のCodeGearとデータの単位であるDataGearという概念が存在する. -CodeGearは\emph{\_\_code}という記述で宣言することができる. +CodeGearは\texttt{\_\_code}という記述で宣言することができる. CbCはC言語の下位言語であるため,通常の関数も使用することは可能だが, 基本的にCodeGearの単位でプログラミングを行う. DataGearはCodeGearで入出力される変数データである. @@ -187,9 +185,9 @@ リフレクションはプログラム自身のメタデータを分析し, それによってプログラムを実行時に書き換える一種のメタプログラミング手法である. 一般的にクラスやメソッド,関数の単位で書き換えが行われる. -手法の例としてJavaにおけるAspectJライブラリを用いたプログラミングが挙げられる. +手法の例としてJavaにおけるAspectJライブラリを用いたプログラミングが挙げられる\cite{10.1145/1353482.1353504}. 軽量継続の場合,CodeGear遷移のどの地点においてもメタな処理を挿入することが可能であるため, -より柔軟なリフレクションが可能と考える。 +より柔軟なリフレクションが可能と考える. \section{CodeGearの記述例} @@ -197,11 +195,12 @@ CbCのプログラム例をソースコード\ref{src:cbc}に示す. まずmain関数においてadd1 CodeGearへgotoを行う. その際add1へInput DataGearとしてnを渡す. -Cのgotoが\emph{goto label;}という記法で,ラベリングした箇所へjmpを行うのに対し, -CbCのgotoは\emph{goto add1(n);}という記法で,add1 CodeGearへn DataGearを渡してjmpを行う. +Cのgotoが\texttt{goto label;}という記法で,ラベリングした箇所へjmpを行うのに対し, +CbCのgotoは\texttt{goto add1(n);}という記法で,add1 CodeGearへn DataGearを渡してjmpを行う. add1は処理の最後にadd2 CodeGearへgotoを行う. その際Output DataGear out\_nをadd2のInput DataGearとして渡す. -このようにCbCではCodeGearのOutput DataGearを次のCodeGearのInput DataGearとして渡すことを繰り返すことで処理を進める. +このようにCbCではCodeGearのOutput DataGearを次のCodeGearのInput DataGearとして渡すことを繰り返すことで処理を進め, +最後はexitへgotoすることで処理を終了する. \lstinputlisting[caption=CbCのプログラム例,label=src:cbc]{src/hello.cbc} @@ -434,7 +433,7 @@ プロセスの管理に用いられる重要なシステムである. そのため,GearsOSにおいてもi-nodeを用いたディレクトリシステムや, DataGearManagerによる分散ファイルシステムの仕組みをもつ, -GearsFileSystemの取り組みがいくつかされてきた. +GearsFileSystemの取り組みを行ってきた. \section{i-nodeを用いたディレクトリシステム} @@ -443,10 +442,10 @@ ファイルの属性情報が書かれたデータである. inodeにおけるファイルの属性情報は表\ref{table:inode}のようなものがある. またinodeは識別番号としてinode numberを持つ. -inode numberは一つのファイルシステム内で一意の番号であり,\emph{ls -i}コマンドで確認可能である. +inode numberは一つのファイルシステム内で一意の番号であり,\texttt{ls -i}コマンドで確認可能である. inodeはファイルシステム始動時にinode領域をディスク上に確保する. そのためinode numberには上限があり,それに伴いファイルシステム上で扱えるファイル数の上限も決まる. -inode numberの最大値は\emph{df -i}コマンドで確認可能である. +inode numberの最大値は\texttt{df -i}コマンドで確認可能である. \begin{table}[htpb] \begin{center} @@ -607,8 +606,7 @@ \section{ファイルシステムの信頼性に関する機能} -ファイルシステムはデータを保持することを基本的な機能としている. -信頼性に関する機能など,その他の機能は追加機能として実装する. +ファイルシステムはデータを保持することを基本的な機能とし,その他の機能は追加機能として実装する. ファイルシステムやDBにおける信頼性に関する追加機能として, システムの電源断時にデータが残るpersistency, データを書き込めたかどうかを判定するatomic write, @@ -623,15 +621,15 @@ メモリ管理の機能としてはガーベージコレクションが挙げられる. ガベージコレクションは通常プログラム言語のレイヤで行われる. これらの機能をファイルシステムのレベルで実装することで, -より信頼性の高いファイルシステムを構築したい. +より堅牢なファイルシステムを構築したい. \section{メモリの管理手法} GCのアルゴリズムは大きく分けてMark \& Sweep GC,Reference counting GC, Copying GCの3つの種類が存在する. -Mark \& Sweep GCはマークフェーズとスイープフェーズからなる。 +Mark \& Sweep GCはマークフェーズとスイープフェーズからなる. マークフェーズはヒープ上でルートから参照することができるオブジェクト全てにマークをし, -その後、スイープフェーズでマークされていないオブジェクトを +その後,スイープフェーズでマークされていないオブジェクトを 使用されていないオブジェクトのリストであるフリーリストに接続することでGCを行う. Reference counting GCはオブジェクトの被参照数を表すReference counterを用いるGCである. 新たに参照される度にReference counterをインクリメントし, @@ -841,7 +839,7 @@ \lstinputlisting[label=src:TreeCopy.h, caption=Tree Interfaceの使用定義(Copy追加後)]{src/TreeCopy.h} -10行目にcopy()が追加されており,inputDataGearは\emph{\_\_code} nextのみとしている. +10行目にcopy()が追加されており,inputDataGearは\texttt{\_\_code} nextのみとしている. これにより, \texttt{goto tree->copy(next);}といった記述でRedBlackTreeのコピーを行うことができる. 次にRedBlackTreeの実装の型定義をソースコード\ref{src:CopyRedBlackTree.h}に示す.
--- a/Paper/reference.bib Fri Feb 02 01:41:53 2024 +0900 +++ b/Paper/reference.bib Sat Feb 03 14:46:07 2024 +0900 @@ -146,4 +146,22 @@ title = {2月14日から2月19日にかけて発生した電子マネー決済システム(iD決済)の障害に関するお詫びとお知らせ}, author = {グローリー株式会社}, howpublished = {https://www.glory.co.jp/news/detail/id=2017} +} + +@inproceedings{10.1145/1353482.1353504, + author = {Golbeck, Ryan M. and Davis, Samuel and Naseer, Immad and Ostrovsky, Igor and Kiczales, Gregor}, + title = {Lightweight virtual machine support for AspectJ}, + year = {2008}, + isbn = {9781605580449}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/1353482.1353504}, + doi = {10.1145/1353482.1353504}, + abstract = {Advice weaving can be efficiently supported with only lightweight enhancements to existing Virtual Machines. Performing weaving at the Java bytecode (JBC) level while preserving appropriate metadata enables the VM to understand the AspectJ-specific semantics of the code and optimize it. This allows the overhead of advice weaving and performing non-local advice dispatch optimization to occur prior to runtime. It also allows the VM to perform optimizations that are unavailable to a bytecode level weaver.An experimental implementation shows that this approach can take advantage of previously known macro optimizations of expensive constructs, including cflow, as well as micro optimizations including those based on improved type analysis unavailable to JBC-based advice dispatch. A thorough benchmark evaluation confirms that the use of this architecture does not result in runtime performance overhead and benefits from the implemented optimizations.}, + booktitle = {Proceedings of the 7th International Conference on Aspect-Oriented Software Development}, + pages = {180–190}, + numpages = {11}, + keywords = {AspectJ, aspect-oriented programming}, + location = {Brussels, Belgium}, + series = {AOSD '08} } \ No newline at end of file
--- a/Paper/src/hello.cbc Fri Feb 02 01:41:53 2024 +0900 +++ b/Paper/src/hello.cbc Sat Feb 03 14:46:07 2024 +0900 @@ -10,6 +10,7 @@ __code end(int in_n) { printf("%d", n); + goto exit(0); } int main(int argc, char *arcv[]) {
--- a/TODO.md Fri Feb 02 01:41:53 2024 +0900 +++ b/TODO.md Sat Feb 03 14:46:07 2024 +0900 @@ -25,4 +25,16 @@ 確認したいこと -- [ ] ある程度木が大きくなると動かなくなる(詳細未調査) \ No newline at end of file +- [ ] ある程度木が大きくなると動かなくなる(詳細未調査) + +助言一覧 + +- [x] タイトル改行 +- [x] されてきた -> してきた +- [x] 非破壊の問題点とGCの話を入れる +- [x] However, 信頼性の連発をなくす +- [x] __codeのフォントを直す +- [ ] AspectJの引用 +- [x] CbCの記述例(exit code) +- [ ] 英語の文献をもっと入れよう + - [ ] LFSやFilesystem Fragmentationへ言及する \ No newline at end of file
--- a/mindmaps/gears_fs_db.mm Fri Feb 02 01:41:53 2024 +0900 +++ b/mindmaps/gears_fs_db.mm Sat Feb 03 14:46:07 2024 +0900 @@ -851,7 +851,12 @@ </node> </node> <node TEXT="CopyRedBlackTreeの実装" POSITION="right" ID="ID_1875155929" CREATED="1706686273106" MODIFIED="1706691080675" HGAP_QUANTITY="-10.75 pt" VSHIFT_QUANTITY="267.74999 pt"> -<node TEXT="説明" ID="ID_1618684595" CREATED="1706689938660" MODIFIED="1706689944053"/> +<node TEXT="説明" ID="ID_1618684595" CREATED="1706689938660" MODIFIED="1706689944053"> +<node TEXT="TreeのAPIのひとつとして実装" ID="ID_1013219955" CREATED="1706934961492" MODIFIED="1706934969874"/> +<node TEXT="アルゴリズム" ID="ID_73867053" CREATED="1706934970286" MODIFIED="1706934976931"/> +<node TEXT="登場する主なCodeGear" ID="ID_1955149593" CREATED="1706934987471" MODIFIED="1706935007665"/> +<node TEXT="CodeGearのおおまかな遷移" ID="ID_872667908" CREATED="1706935010066" MODIFIED="1706935017591"/> +</node> <node TEXT="Tree InterfaceのAPIにCopyを追加する" ID="ID_746343495" CREATED="1705735678228" MODIFIED="1705735715335"> <node TEXT="tree->copy" ID="ID_1447270137" CREATED="1706690663705" MODIFIED="1706690668279"/> <node TEXT="copyの使用方法" ID="ID_1242421499" CREATED="1706429162944" MODIFIED="1706429182896"/> @@ -871,7 +876,6 @@ </p> </body> </html> - </richcontent> </node> </node>