Mercurial > hg > Papers > 2024 > matac-master

Binary file Paper/master_paper.pdf has changed
--- a/Paper/master_paper.tex	Mon Jan 08 20:22:51 2024 +0900
+++ b/Paper/master_paper.tex	Tue Jan 09 16:27:48 2024 +0900
@@ -225,13 +225,19 @@
 \section{3種類のGearsOS}

 GearsOSには現在3つの種類がある．
-1つ目が型式手法による信頼性の向上を目的とした，GearsAgdaと呼ばれるGearsOSである．
-これは，Agdaによって実装されている．
-2つ目がユーザーレベルタスクマネジメントの実装を目的としたGearsOSがある．
+1つ目が形式手法による信頼性の向上を目的とした，GearsAgdaと呼ばれるGearsOSである\cite{gearsagda}．
+これは，Agdaによって実装されており，
+森 逸汰によるGearsAgdaによるRed Black Treeの検証などの取り組みがされている\cite{garbtree}．
+2つ目はスタンドアロンOSの開発を目的とした，CbC\_xv6と呼ばれるGearsOSがある\cite{cbcxv6}．
+これは，教育用に開発されたx.v6\cite{xv6}をCbCで書き換える形で実装している．
+CbC\_xv6では仲吉 菜々子によるGears OSのCodeGear Managementの取り組みがされている\cite{gearscodemngment}．
+3つ目はユーザーレベルタスクマネジメントの実装を目的としたGearsOSがある．
 これは，CbCによって実装されており，
-RedBlackTreeでのディレクトリシステムの構築するなどの取り組みもされている\cite{directory}．
-3つ目はスタンドアロンOSの開発を目的とした，CbC\_xv6と呼ばれるGearsOSがある\cite{cbcxv6}．
-これは，教育用に開発されたx.v6\cite{xv6}をCbCで書き換える形で実装する．
+分散ファイルシステムの設計やRedBlackTreeでのディレクトリシステムの構築などの取り組みがされている\cite{cfile, directory}．
+
+本研究では，CbCによって実装されたユーザーレベルタスクマネジメント実装のGearsOSを対象に
+ファイルシステムのレプリケーションやGC機能の実装を考える．
+以下，GearsOSはユーザーレベルタスクマネジメント実装のGearsOSを指す．

 \section{メタ処理を記述するmetaGear}

@@ -245,6 +251,7 @@
 その際，MetaCodeGearに渡されるDataGearのことは特にMetaDataGearと呼ばれる．
 また，CodeGearの前に実行されるMetaCodeGearは特にstubCodeGearと呼ばれ，
 メタレベルを含めるとstubCodeGearとCodeGearを交互に実行する形で遷移していく．
+
 \begin{figure}[ht]
   \begin{center}
       \includegraphics[width=160mm]{fig/meta-cg-dg.pdf}
@@ -254,6 +261,8 @@
 \end{figure}

 \section{CodeGearの遷移}
+
+
 \section{全てのGearを参照するContext}

 ContextはGearsOS上全てのCodeGear，DataGearの参照を持ち，CodeGearとDataGearの接続に用いられる．
@@ -271,6 +280,7 @@
 Contextはいくつかの種類に分けることができる．
 OS全体のContextを管理するKernel Contextやユーザープログラムごとに存在するUser Context，
 CPUやGPUごとに存在するCPU Contextがある．
+
 \begin{figure}[ht]
   \begin{center}
       \includegraphics[width=150mm]{fig/context.pdf}
--- a/Paper/reference.bib	Mon Jan 08 20:22:51 2024 +0900
+++ b/Paper/reference.bib	Tue Jan 09 16:27:48 2024 +0900
@@ -18,6 +18,29 @@
   howpublished = {http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC\_xv6/}
 }

+@misc{gearsagda,
+  title        = {GearsAgda},
+  author       = {並列信頼研究室},
+  organization = {琉球大学},
+  howpublished = {http://www.cr.ie.u-ryukyu.ac.jp/hg/Gears/GearsAgda/}
+}
+
+@misc{garbtree,
+  author  = {森 逸汰, 河野 真治(琉球大学)},
+  title   = {GearsAgdaによるRed Black Treeの検証},
+  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
+  month   = {May},
+  year    = 2023
+}
+
+@misc{gearscodemngment,
+  author  = {仲吉 菜々子, 河野 真治(琉球大学)},
+  title   = {Gears OSのCodeGear Management},
+  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
+  month   = {May},
+  year    = 2023
+}
+
 @article{cbc,
   author  = {河野 真治},
   title   = {継続を持つCの下位言語によるシステム記述},
--- a/mindmaps/gears_fs_db.mm	Mon Jan 08 20:22:51 2024 +0900
+++ b/mindmaps/gears_fs_db.mm	Tue Jan 09 16:27:48 2024 +0900
@@ -397,15 +397,24 @@
 <node TEXT="gotoによる軽量継続" ID="ID_726882949" CREATED="1703307895880" MODIFIED="1703307911540"/>
 <node TEXT="CodeGearの記述例" ID="ID_1731637915" CREATED="1703307784821" MODIFIED="1703307887307"/>
 </node>
-<node TEXT="信頼性の保証を目的としたGearsOS" FOLDED="true" ID="ID_1315567458" CREATED="1701692210913" MODIFIED="1703311040671">
+<node TEXT="信頼性の保証を目的としたGearsOS" ID="ID_1315567458" CREATED="1701692210913" MODIFIED="1703311040671">
 <node TEXT="3種類のGearsOS" ID="ID_1326415213" CREATED="1703309744902" MODIFIED="1703309750565"/>
-<node TEXT="メタ処理を記述するmetaGear" FOLDED="true" ID="ID_1666892566" CREATED="1703309692742" MODIFIED="1703309713823">
-<node TEXT="ノーマルレベルとメタレベルの切り分け" ID="ID_719507396" CREATED="1703308470210" MODIFIED="1703308478844">
-<node TEXT="リフレクション" ID="ID_355579006" CREATED="1703308504930" MODIFIED="1703308513027"/>
+<node TEXT="メタ処理を記述するmetaGear" ID="ID_1666892566" CREATED="1703309692742" MODIFIED="1703309713823">
+<node TEXT="ノーマルレベルとメタレベルの切り分け" ID="ID_719507396" CREATED="1703308470210" MODIFIED="1703308478844"/>
+</node>
+<node TEXT="全てのGearを参照するContext" ID="ID_91888278" CREATED="1703309731224" MODIFIED="1703310166027">
+<node TEXT="全てのCodeGear, DataGearの参照を持つ" ID="ID_816175749" CREATED="1704777710835" MODIFIED="1704777722631"/>
+<node TEXT="従来OSのプロセスに相当する概念" ID="ID_485427631" CREATED="1704777731086" MODIFIED="1704777739954"/>
+<node TEXT="Gearの概念ではmetaDataGearにあたる" ID="ID_1983036538" CREATED="1704777794150" MODIFIED="1704777819739"/>
+<node TEXT="ノーマルレベルから直接参照されない" ID="ID_280262393" CREATED="1704777824342" MODIFIED="1704777833700"/>
+<node TEXT="metaCodeGearから参照される" ID="ID_526551168" CREATED="1704777838132" MODIFIED="1704778973371"/>
+<node TEXT="ノーマルレベルから直接参照されるとどうなるか" ID="ID_1998855779" CREATED="1704778991437" MODIFIED="1704779001760">
+<node TEXT="ノーマルレベルでメタレベルを書き換えることが可能になる" ID="ID_517717354" CREATED="1704779027195" MODIFIED="1704779037558"/>
+<node TEXT="メタレベルを分けた意味がなくなる" ID="ID_1293544989" CREATED="1704779038072" MODIFIED="1704779046632"/>
 </node>
 </node>
+<node TEXT="Contextを含めたGear遷移" ID="ID_1897519980" CREATED="1704779305504" MODIFIED="1704779324312"/>
 <node TEXT="CodeGearの遷移" ID="ID_1403713795" CREATED="1703310522532" MODIFIED="1703310534184"/>
-<node TEXT="全てのGearを参照するContext" ID="ID_91888278" CREATED="1703309731224" MODIFIED="1703310166027"/>
 <node TEXT="GearsOSのinterface" ID="ID_227287316" CREATED="1703310975416" MODIFIED="1704626095237"/>
 <node TEXT="GearsOSのRedBlackTree" ID="ID_894257471" CREATED="1704625749056" MODIFIED="1704625759342">
 <node TEXT="Treeを継承している" ID="ID_830044324" CREATED="1704625938387" MODIFIED="1704625986222"/>
@@ -432,7 +441,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="1704632532265" HGAP_QUANTITY="16.25 pt" VSHIFT_QUANTITY="-1.5 pt">
 <node TEXT="ファイルシステムの信頼性" 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"/>
@@ -440,7 +449,6 @@
 <node TEXT="現状はTreeにCopyがない" ID="ID_65833123" CREATED="1704630383271" MODIFIED="1704630397371"/>
 <node TEXT="Copyを実装したい" ID="ID_1314300132" CREATED="1704632535428" MODIFIED="1704632976417"/>
 </node>
-<node TEXT="GearsFileSystemのGC" ID="ID_442801060" CREATED="1704692757836" MODIFIED="1704692764197">
 <node TEXT="GCの種類" ID="ID_1746770811" CREATED="1704695739812" MODIFIED="1704696582051">
 <node TEXT="CopyingGCとは" ID="ID_344664264" CREATED="1704692777863" MODIFIED="1704692782352">
 <node TEXT="正確なGC" ID="ID_267216671" CREATED="1704696904268" MODIFIED="1704696908732"/>
@@ -461,7 +469,13 @@
 </node>
 </node>
 </node>
-<node TEXT="GCは併用される" ID="ID_1496671439" CREATED="1704696631667" MODIFIED="1704696640285"/>
+<node TEXT="GCは併用される" ID="ID_1496671439" CREATED="1704696631667" MODIFIED="1704696640285">
+<node TEXT="一般的にGCは組み合わせで使われる" ID="ID_1275851809" CREATED="1704776562321" MODIFIED="1704776594813"/>
+<node TEXT="例えば世代別GC" ID="ID_1572156993" CREATED="1704776595339" MODIFIED="1704776711350"/>
+<node TEXT="メジャーGCでMark &amp; Sweep GC" ID="ID_118548516" CREATED="1704776713708" MODIFIED="1704776746730"/>
+<node TEXT="マイナーでCopying GC" ID="ID_332663516" CREATED="1704776747163" MODIFIED="1704776761598"/>
+<node TEXT="それぞれのGCの利点を享受できる" ID="ID_704438541" CREATED="1704776762298" MODIFIED="1704776776709"/>
+</node>
 <node TEXT="Rustのスマートポインタ" ID="ID_881149259" CREATED="1704696608959" MODIFIED="1704696615328"/>
 <node TEXT="CopyingGCを用いる" ID="ID_1639428535" CREATED="1704692768575" MODIFIED="1704692777490">
 <node TEXT="なぜCopyingGCなのか" ID="ID_1226680678" CREATED="1704696722580" MODIFIED="1704696736347">
@@ -479,10 +493,14 @@
 <node TEXT="参照しているオブジェクトは木のルートから辿れる" ID="ID_1653048898" CREATED="1704696789481" MODIFIED="1704696806177"/>
 <node TEXT="辿れるノードのみコピーするだけでGCになる" ID="ID_355389629" CREATED="1704696807343" MODIFIED="1704696829530"/>
 </node>
-<node TEXT="併用はしないのか" ID="ID_939269191" CREATED="1704696736711" MODIFIED="1704696742433"/>
+<node TEXT="GC併用はしないのか" ID="ID_939269191" CREATED="1704696736711" MODIFIED="1704776977043">
+<node TEXT="今回は単純な実装をしたい" ID="ID_91131104" CREATED="1704776780918" MODIFIED="1704776789505">
+<node TEXT="単なる木のコピー" ID="ID_532595291" CREATED="1704776790471" MODIFIED="1704776797065"/>
+<node TEXT="証明のしやすさにつながる" ID="ID_297159546" CREATED="1704776798186" MODIFIED="1704776845819"/>
+</node>
+</node>
 <node TEXT="Rustのスマートポインタのような仕組みにしないのか" ID="ID_110730790" CREATED="1704696742911" MODIFIED="1704696758432"/>
 </node>
-</node>
 <node TEXT="RedBlackTreeのコピーを用いる" ID="ID_1495626047" CREATED="1704630409263" MODIFIED="1704632465291">
 <node TEXT="Copy" ID="ID_1713857745" CREATED="1699848476363" MODIFIED="1699848479936">
 <node TEXT="単なる2分木のコピー" ID="ID_1165724596" CREATED="1699849455588" MODIFIED="1699849469353"/>
@@ -521,7 +539,7 @@
 </node>
 <node TEXT="CopyRedBlackTreeによるレプリケーションの仕組み" ID="ID_1106336919" CREATED="1703490971550" MODIFIED="1703491035629"/>
 </node>
-<node TEXT="CopyRedBlackTreeの実装" ID="ID_1619882257" CREATED="1701697553803" MODIFIED="1703491075408" VSHIFT_QUANTITY="-4.5 pt">
+<node TEXT="CopyRedBlackTreeの実装" FOLDED="true" ID="ID_1619882257" CREATED="1701697553803" MODIFIED="1703491075408" VSHIFT_QUANTITY="-4.5 pt">
 <node TEXT="コピーのアルゴリズム" ID="ID_64994373" CREATED="1703491215841" MODIFIED="1703491223454">
 <node TEXT="アルゴリズム" ID="ID_972208221" CREATED="1699849518269" MODIFIED="1699849522647">
 <node TEXT="左側を深さ優先で辿る" ID="ID_239741561" CREATED="1699849525266" MODIFIED="1699849604742">