Mercurial > hg > Papers > 2024 > matac-master
changeset 34:78ca77ccccc5
abstract
author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 19 Jan 2024 15:28:28 +0900 |
parents | c1323b737cfd |
children | 849ec71b87c3 |
files | Paper/chapter/abstract.tex Paper/master_paper.pdf TODO.md mindmaps/gears_fs_db.mm |
diffstat | 4 files changed, 52 insertions(+), 35 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/chapter/abstract.tex Thu Jan 18 19:37:19 2024 +0900 +++ b/Paper/chapter/abstract.tex Fri Jan 19 15:28:28 2024 +0900 @@ -1,29 +1,23 @@ \chapter*{要旨} -当研究室では,Continuation based C(CbC)を用い,定理証明やモデル検査などで信頼性を保証することを目的としたGearsOSを開発している. -OSにおいてファイルシステムは重要な機能の一つであるため実装する必要がある. -現在,一般的なアプリケーションはファイルシステムとデータベースを併用する形で構成される. -アプリケーションのデータベースとしてファイルシステムを使用する構成が取れるようにしたい. -ファイルシステムとデータベースの違いについて考え,データベースとしても利用可能なファイルシステムを構築したい. -本研究では,ファイルシステムとデータベースの違いについて考察し,Gears OSのファイルシステムの設計について述べる. - -当研究室では,Continuation based C(CbC)を用い,定理証明やモデル検査などで信頼性を保証することを目的としたGearsOSを開発している. -OSの重要な機能の1にファイルシステムが存在する. -そのため,GearsOSにおいてもファイルシステムやそれに関する機能の設計構築を行なっている. -しかしながら,ファイルシステムのレプリケーションやガベージコレクションなどの -信頼性に関する追加機能がない. -本研究では,DB +当研究室では,Continuation based C(CbC)を用い, +定理証明やモデル検査などで信頼性を保証することを目的としたGearsOSを開発している. +OSの重要な機能の一つにファイルシステムが存在し, +GearsOSにおいても分散ファイルシステムの仕組みやi-nodeベースのファイルシステムの実装がされてきた. +しかし,現状のGearsOSのファイルシステムにはレプリケーションやバックアップなどの +信頼性に関する機能が実装されていない. +これらをファイルシステムのレベルで実装することで, +より確実にデーターの多重性を確保できると考えられるため実装したい. +また,GearsOSではメモリとディスク上のデータを同一にし, +データの一貫性を確保することを考えている. +そのため,ファイルシステムにおいてもガベージコレクションなどのメモリ管理機能が重要となる. +しかし,そのような機能は現状存在しない. +本研究では,ファイルシステムのレプリケーションやガベージコレクションなどの機能を実装するために必要な +RedBlackTreeのコピー機能について設計,構築,考察を行う. +RedBlackTreeのコピーでそれぞれの機能を統一的に実装することで, +よりシンプルでデータの一貫性が確保された, +定理証明などの形式手法を適用しやすいシステムを実現することを目指す. \chapter*{Abstract} -In our laboratory, we are developing GearsOS, -aimed at ensuring reliability through the use of Continuation based C (CbC) -along with theorem proving and model checking. -Implementing a file system is a necessary task in an OS as it's one of the critical features. -Currently, general applications are structured to use both file systems and databases. -While databases allow data insertion and modification through SQL, -they require predefined schemas and the specification of these schemas at the time of insertion. -In the GearsOS file system, we aim to implement interfaces equivalent to SQL functions such as grep and find, -enabling the use of the file system as a database for applications. -We want to construct a file system that can also function as a database by considering the differences between file systems and databases. -This research discusses these differences and describes the design of the file system for Gears OS. \ No newline at end of file +In our laboratory, \ No newline at end of file
--- a/TODO.md Thu Jan 18 19:37:19 2024 +0900 +++ b/TODO.md Fri Jan 19 15:28:28 2024 +0900 @@ -1,5 +1,4 @@ - [ ] 要旨 - - mm書いた - [ ] 1章 最後 - [ ] GearsOSのRedBlackTreeの説明 - [ ] DGMによる分散ファイルシステム @@ -7,5 +6,4 @@ - [ ] 実装の説明 - [ ] まとめ - [ ] 今後の課題 -- [x] 謝辞 -- [ ] 付録? \ No newline at end of file +- [x] 謝辞 \ No newline at end of file
--- a/mindmaps/gears_fs_db.mm Thu Jan 18 19:37:19 2024 +0900 +++ b/mindmaps/gears_fs_db.mm Fri Jan 19 15:28:28 2024 +0900 @@ -133,9 +133,6 @@ </node> </node> </node> -<node TEXT="現状" ID="ID_932050028" CREATED="1703310897416" MODIFIED="1703310899956"> -<node TEXT="" ID="ID_166710427" CREATED="1703310900268" MODIFIED="1703310900268"/> -</node> <node TEXT="CbC" ID="ID_740206957" CREATED="1701695838712" MODIFIED="1701695841654"> <node TEXT="Cの下位言語" ID="ID_1949462311" CREATED="1702109769687" MODIFIED="1702109804650"> <node TEXT="CのLLVMに変更を加えている" ID="ID_591487528" CREATED="1702110861488" MODIFIED="1702110890767"/> @@ -292,11 +289,11 @@ <node TEXT="木を辿るためにStackを使う" ID="ID_788381426" CREATED="1699849561986" MODIFIED="1699849582652"> <node TEXT="コピー後に消されるので使って良い" ID="ID_1063130872" CREATED="1701690823328" MODIFIED="1701690834394"/> </node> -<node TEXT="アルゴリズム" ID="ID_529312839" CREATED="1699849518269" MODIFIED="1699849522647"> +<node TEXT="アルゴリズム" ID="ID_529312839" CREATED="1699849518269" MODIFIED="1705568929841"> <node TEXT="左側を深さ優先で辿る" ID="ID_468694757" CREATED="1699849525266" MODIFIED="1699849604742"> <node TEXT="Stack push" ID="ID_1123969398" CREATED="1699849778090" MODIFIED="1699849781012"/> </node> -<node TEXT="アロケートしたノードは別のContext上に作る" ID="ID_320048499" CREATED="1699849620905" MODIFIED="1699849638042"> +<node TEXT="アロケートしたノードは別のContext上に作る" ID="ID_320048499" CREATED="1699849620905" MODIFIED="1705568929840"> <node TEXT="GCのため" ID="ID_1239006804" CREATED="1699849638520" MODIFIED="1699849668501"/> <node TEXT="Copy後古いContextを消す" ID="ID_1485480555" CREATED="1699849646521" MODIFIED="1699849693755"/> <node TEXT="メモリ管理をモナドで表していることになる" ID="ID_1271994335" CREATED="1699849705089" MODIFIED="1699849715878"/> @@ -399,6 +396,34 @@ </node> <node TEXT="評価方法" POSITION="right" ID="ID_1979397312" CREATED="1699850131177" MODIFIED="1699850137060"/> <node TEXT="章立て" POSITION="left" ID="ID_378600647" CREATED="1699848424709" MODIFIED="1702112473403"> +<node TEXT="要旨" ID="ID_1862870052" CREATED="1705571598152" MODIFIED="1705571620770"> +<node TEXT="CbCでGearsOSを開発している" ID="ID_1596447160" CREATED="1705571621398" MODIFIED="1705571639432"/> +<node TEXT="OSの重要な機能の一つにファイルシステムがある" ID="ID_1812705807" CREATED="1705571640078" MODIFIED="1705571676397"> +<node TEXT="プロセス管理やデータの保持" ID="ID_1002371513" CREATED="1705636979706" MODIFIED="1705636992169"/> +</node> +<node TEXT="FSはGearsOSでも設計実装がされている" ID="ID_213132822" CREATED="1705571677040" MODIFIED="1705571697134"> +<node TEXT="i-node directory system" ID="ID_581456334" CREATED="1705637000846" MODIFIED="1705637008111"/> +<node TEXT="DataGearManagerを用いた分散ファイルシステム" ID="ID_428549418" CREATED="1705637008536" MODIFIED="1705637025285"/> +</node> +<node TEXT="FSの信頼性に関する機能がない" ID="ID_1765028343" CREATED="1705571772335" MODIFIED="1705571797140"> +<node TEXT="多重性" ID="ID_1553948100" CREATED="1705637129978" MODIFIED="1705637132992"> +<node TEXT="バックアップ" ID="ID_1196024079" CREATED="1705571952708" MODIFIED="1705571955785"/> +<node TEXT="レプリケーション" ID="ID_693585860" CREATED="1705571956248" MODIFIED="1705571960387"/> +</node> +<node TEXT="一貫性" ID="ID_465667054" CREATED="1705637437811" MODIFIED="1705637441519"> +<node TEXT="トランザクション" ID="ID_793477817" CREATED="1705637062637" MODIFIED="1705637066804"/> +</node> +</node> +<node TEXT="メモリ管理機能もない" ID="ID_582237136" CREATED="1705636449288" MODIFIED="1705636458393"> +<node TEXT="GC" ID="ID_504953107" CREATED="1705636459464" MODIFIED="1705636461733"/> +</node> +<node TEXT="バックアップ,レプリケーション,GCを実装したい" ID="ID_209049582" CREATED="1705636465798" MODIFIED="1705636493249"/> +<node TEXT="実装したい機能は基本的にRedBlackTreeのコピー操作となる" ID="ID_401787855" CREATED="1705636494950" MODIFIED="1705636514799"/> +<node TEXT="しかし現状のRedBlackTreeにCopyの機能がない" ID="ID_1368822025" CREATED="1705636520674" MODIFIED="1705636536996"/> +<node TEXT="追加機能を実装するにあたりCopyRBTreeが必要" ID="ID_104907185" CREATED="1705571941402" MODIFIED="1705571990070"/> +<node TEXT="CopyRedBlackTreeを実装した" ID="ID_832191870" CREATED="1705571803160" MODIFIED="1705571938071"/> +<node TEXT="CopyRedBlackTreeの設計,構築,考察を述べる" ID="ID_1223240785" CREATED="1705636541738" MODIFIED="1705636559635"/> +</node> <node TEXT="Gears OSのファイルシステムとDB" FOLDED="true" ID="ID_446325287" CREATED="1701690660393" MODIFIED="1701690902283"> <node TEXT="重要なシステムの障害" ID="ID_780032066" CREATED="1704365424619" MODIFIED="1704365554685"> <node TEXT="例" ID="ID_561763413" CREATED="1704365743851" MODIFIED="1704365747240"> @@ -516,7 +541,7 @@ </node> <node TEXT="GearsOSのRedBlackTree" ID="ID_594513732" CREATED="1705400358246" MODIFIED="1705400364641"/> </node> -<node TEXT="GearsOSのファイルシステムとDB(現状の話" ID="ID_667012992" CREATED="1701694178540" MODIFIED="1705549429213"> +<node TEXT="GearsOSのファイルシステムとDB(現状の話" FOLDED="true" ID="ID_667012992" CREATED="1701694178540" MODIFIED="1705549429213"> <node TEXT="GearsOSのファイルシステムとDB" ID="ID_188577314" CREATED="1704630094596" MODIFIED="1705549436675"> <node TEXT="ファイルシステムはOSの重要な機能である" ID="ID_46805604" CREATED="1704630103040" MODIFIED="1704630119191"/> <node TEXT="分散ファイルシステムとi-nodeを用いたファイルシステムが存在する" ID="ID_1509553363" CREATED="1704630119858" MODIFIED="1704630152926"/> @@ -535,7 +560,7 @@ <node TEXT="RedBlackTreeのトランザクション" ID="ID_1088328123" CREATED="1701696247760" MODIFIED="1702112463420" HGAP_QUANTITY="14.75 pt" VSHIFT_QUANTITY="3.75 pt"/> </node> </node> -<node TEXT="GearsFileSystemにおけるGCとレプリケーション" ID="ID_1092227909" CREATED="1701690558237" MODIFIED="1704632532265" HGAP_QUANTITY="16.25 pt" VSHIFT_QUANTITY="-1.5 pt"> +<node TEXT="GearsFileSystemにおけるGCとレプリケーション" FOLDED="true" ID="ID_1092227909" CREATED="1701690558237" MODIFIED="1705569492385" HGAP_QUANTITY="16.25 pt" VSHIFT_QUANTITY="-1.5 pt"> <node TEXT="ファイルシステムの信頼性" FOLDED="true" ID="ID_200982245" CREATED="1704630258973" MODIFIED="1704630267498"> <node TEXT="信頼性に関する追加機能" ID="ID_1574949535" CREATED="1704630312069" MODIFIED="1704630320377"/> <node TEXT="GCやレプリケーションの機能がない" ID="ID_878946385" CREATED="1704630323433" MODIFIED="1704632961588"/> @@ -571,7 +596,7 @@ <node TEXT="それぞれのGCの利点を享受できる" ID="ID_704438541" CREATED="1704776762298" MODIFIED="1704776776709"/> </node> <node TEXT="Rustのスマートポインタ" ID="ID_881149259" CREATED="1704696608959" MODIFIED="1704696615328"/> -<node TEXT="CopyingGCを用いる" FOLDED="true" ID="ID_1639428535" CREATED="1704692768575" MODIFIED="1704692777490"> +<node TEXT="CopyingGCを用いる" FOLDED="true" ID="ID_1639428535" CREATED="1704692768575" MODIFIED="1705569492385"> <node TEXT="どのように利用するか" ID="ID_549509034" CREATED="1704696775586" MODIFIED="1704696779463"> <node TEXT="通常のCopyingGCではヒープ領がコピーされる" ID="ID_830576894" CREATED="1704692782815" MODIFIED="1704692814222"/> <node TEXT="GearsFileSystemの場合は木をコピーする" ID="ID_1003156855" CREATED="1704692814851" MODIFIED="1704692831840"/>