Mercurial > hg > Papers > 2024 > matac-master

changeset 45:f23602aa6fd8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mm
author matac42 <matac@cr.ie.u-ryukyu.ac.jp>
date Sun, 28 Jan 2024 15:52:08 +0900
parents a556d22b4ebd
children 9baf70df56fa
files TODO.md mindmaps/gears_fs_db.mm
diffstat 2 files changed, 109 insertions(+), 40 deletions(-) [+]
line wrap: on
line diff
--- a/TODO.md	Tue Jan 23 20:13:55 2024 +0900
+++ b/TODO.md	Sun Jan 28 15:52:08 2024 +0900
@@ -7,8 +7,13 @@
 
 - [x] レプリケーションの説明
 - [x] Nodeの説明
+
+- [ ] 4章
 - [ ] DGMによる分散ファイルシステム
+- [ ] ALLOCの説明
+- [ ] RedBlackTree構造の説明間違っている
 - [ ] 実装の説明
 - [ ] 評価
 - [ ] まとめ
-- [ ] 今後の課題
\ No newline at end of file
+- [ ] 今後の課題
+- [ ] 図の清書
\ No newline at end of file
--- a/mindmaps/gears_fs_db.mm	Tue Jan 23 20:13:55 2024 +0900
+++ b/mindmaps/gears_fs_db.mm	Sun Jan 28 15:52:08 2024 +0900
@@ -482,7 +482,7 @@
 <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="Gears Agda" ID="ID_1385168402" CREATED="1705044105795" MODIFIED="1705044111649"/>
 <node TEXT="Gears OS" ID="ID_1367848198" CREATED="1705044112079" MODIFIED="1705044114581"/>
@@ -548,8 +548,9 @@
 </node>
 </node>
 <node TEXT="GearsOSのRedBlackTree" ID="ID_594513732" CREATED="1705400358246" MODIFIED="1705400364641"/>
+<node TEXT="ALLOCの説明" ID="ID_957488458" CREATED="1706417138929" MODIFIED="1706417138929"/>
 </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"/>
@@ -569,14 +570,14 @@
 </node>
 </node>
 <node TEXT="GearsFileSystemにおけるGCとレプリケーション" 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="ファイルシステムの信頼性" FOLDED="true" ID="ID_200982245" CREATED="1704630258973" MODIFIED="1706091519737">
 <node TEXT="信頼性に関する追加機能" ID="ID_1574949535" CREATED="1704630312069" MODIFIED="1704630320377"/>
 <node TEXT="GCやレプリケーションの機能がない" ID="ID_878946385" CREATED="1704630323433" MODIFIED="1704632961588"/>
-<node TEXT="実装するためにはデータのCopyが必要" ID="ID_822351907" CREATED="1704630337081" MODIFIED="1704630382753"/>
+<node TEXT="実装するためにはデータのCopyが必要" ID="ID_822351907" CREATED="1704630337081" MODIFIED="1706091519737"/>
 <node TEXT="現状はTreeにCopyがない" ID="ID_65833123" CREATED="1704630383271" MODIFIED="1704630397371"/>
 <node TEXT="Copyを実装したい" ID="ID_1314300132" CREATED="1704632535428" MODIFIED="1704632976417"/>
 </node>
-<node TEXT="GCの種類" FOLDED="true" ID="ID_1746770811" CREATED="1704695739812" MODIFIED="1704696582051">
+<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"/>
 <node TEXT="ヒープ領域をFrom領域とTo領域に分割" ID="ID_1262852949" CREATED="1704711856815" MODIFIED="1704711932146"/>
@@ -585,6 +586,7 @@
 <node TEXT="Reference counting GC" ID="ID_776539806" CREATED="1704696590166" MODIFIED="1704696594363">
 <node TEXT="オブジェクトの被参照数を表すカウンタを用いる" ID="ID_166536665" CREATED="1704710714477" MODIFIED="1704710852447"/>
 <node TEXT="被参照数が0になった時オブジェクトが解放される" ID="ID_1678718232" CREATED="1704711836498" MODIFIED="1704711854290"/>
+<node TEXT="循環参照をGCできない" ID="ID_1787181256" CREATED="1706091526719" MODIFIED="1706091542945"/>
 </node>
 <node TEXT="Mark \&amp; Sweep GC" ID="ID_715438606" CREATED="1704696594768" MODIFIED="1704696598757">
 <node TEXT="マークフェーズとスイープフェーズからなる" ID="ID_1584128194" CREATED="1704710119330" MODIFIED="1704710167419"/>
@@ -596,7 +598,7 @@
 </node>
 </node>
 </node>
-<node TEXT="GCは併用される" FOLDED="true" 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"/>
@@ -687,44 +689,19 @@
 <node TEXT="i-node treeをbackup, replication, gc可能であることを書きたい" ID="ID_559931709" CREATED="1705551366386" MODIFIED="1705551399134"/>
 </node>
 </node>
-<node TEXT="CopyRedBlackTreeの実装" ID="ID_1619882257" CREATED="1701697553803" MODIFIED="1703491075408" VSHIFT_QUANTITY="-4.5 pt">
-<node TEXT="実装方法" ID="ID_1774988166" CREATED="1705735668943" MODIFIED="1705735677711">
-<node TEXT="Tree InterfaceのAPIにCopyを追加する" ID="ID_95904284" CREATED="1705735678228" MODIFIED="1705735715335"/>
-</node>
-<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">
-<node TEXT="Stack push" ID="ID_1718409210" CREATED="1699849778090" MODIFIED="1699849781012"/>
-</node>
-<node TEXT="アロケートしたノードは別のContext上に作る" ID="ID_573859973" CREATED="1699849620905" MODIFIED="1699849638042">
-<node TEXT="GCのため" ID="ID_259949416" CREATED="1699849638520" MODIFIED="1699849668501"/>
-<node TEXT="Copy後古いContextを消す" ID="ID_1297792398" CREATED="1699849646521" MODIFIED="1699849693755"/>
-<node TEXT="メモリ管理をモナドで表していることになる" ID="ID_152951728" CREATED="1699849705089" MODIFIED="1699849715878"/>
-</node>
-<node TEXT="リーフまで降りたらroot方向に木を戻る" ID="ID_1233772087" CREATED="1699849731393" MODIFIED="1699849765553">
-<node TEXT="Stack pop" ID="ID_1907664340" CREATED="1699849765982" MODIFIED="1699849773214"/>
-<node TEXT="右側を呼び出す" ID="ID_1658933965" CREATED="1699849789218" MODIFIED="1699849803550"/>
-</node>
-<node TEXT="Stackを2つ使うならば" ID="ID_804128791" CREATED="1699849785880" MODIFIED="1699850937824">
-<node TEXT="全体のStack" ID="ID_1465604948" CREATED="1699850965212" MODIFIED="1699858010811">
-<node TEXT="originの木を辿るために使う" ID="ID_1918769190" CREATED="1699858046929" MODIFIED="1699858071837"/>
-</node>
-<node TEXT="途中のStack" ID="ID_1149999446" CREATED="1699850966215" MODIFIED="1699858024318">
-<node TEXT="右側を呼び出す際にそれまでの左側部分木を保持" ID="ID_225633027" CREATED="1699851138198" MODIFIED="1699858042178"/>
+<node TEXT="CopyRedBlackTreeの実装" ID="ID_1054164602" CREATED="1706417542077" MODIFIED="1706417548592">
+<node TEXT="実装方法" ID="ID_1491466672" CREATED="1705735668943" MODIFIED="1705735677711">
+<node TEXT="Tree InterfaceのAPIにCopyを追加する" ID="ID_535524915" CREATED="1705735678228" MODIFIED="1705735715335"/>
+<node TEXT="RedBlackTreeのコピーとして実装する" ID="ID_878630835" CREATED="1706417169892" MODIFIED="1706417179625"/>
 </node>
 </node>
-</node>
-</node>
-<node TEXT="コード説明" ID="ID_1352482727" CREATED="1704630501155" MODIFIED="1704630507416"/>
-<node TEXT="Copyのタイミング処理" ID="ID_39116936" CREATED="1706002572872" MODIFIED="1706002587228"/>
-<node TEXT="証明のしやすさについて" ID="ID_2776247" CREATED="1703492904417" MODIFIED="1703492910899">
-<node TEXT="Stackの使用に関して" ID="ID_432827984" CREATED="1703492856041" MODIFIED="1703492863503"/>
-</node>
-</node>
+<node TEXT="評価" ID="ID_1053436711" CREATED="1702112499515" MODIFIED="1702112509004">
 <node TEXT="信頼性" ID="ID_1221084016" CREATED="1702289777950" MODIFIED="1702289781581">
 <node TEXT="モデル検査とAgdaによる実装" ID="ID_1438858883" CREATED="1702289781790" MODIFIED="1702289794818"/>
 </node>
-<node TEXT="評価" ID="ID_1053436711" CREATED="1702112499515" MODIFIED="1702112509004"/>
+<node TEXT="RedBlackTreeの信頼性は定理証明する" ID="ID_12400408" CREATED="1706417749855" MODIFIED="1706417762632"/>
+<node TEXT="copyの信頼性は？" ID="ID_1159602829" CREATED="1706417738889" MODIFIED="1706417747056"/>
+</node>
 <node TEXT="今後" ID="ID_87524419" CREATED="1702112509364" MODIFIED="1702112512270"/>
 </node>
 <node TEXT="修論で言いたいこと" POSITION="right" ID="ID_1194781583" CREATED="1701690732709" MODIFIED="1701696321975" HGAP_QUANTITY="29 pt" VSHIFT_QUANTITY="134.25 pt">
@@ -775,5 +752,92 @@
 </node>
 </node>
 </node>
+<node TEXT="実装" POSITION="left" ID="ID_1462455862" CREATED="1706417525408" MODIFIED="1706417530681">
+<node TEXT="CopyRedBlackTreeの実装" ID="ID_1619882257" CREATED="1701697553803" MODIFIED="1703491075408" VSHIFT_QUANTITY="-4.5 pt">
+<node TEXT="実装方法" ID="ID_1774988166" CREATED="1705735668943" MODIFIED="1705735677711">
+<node TEXT="Tree InterfaceのAPIにCopyを追加する" ID="ID_95904284" CREATED="1705735678228" MODIFIED="1705735715335"/>
+<node TEXT="RedBlackTreeのコピーとして実装する" ID="ID_748405331" CREATED="1706417169892" MODIFIED="1706417179625"/>
+</node>
+<node TEXT="使い方（test）" ID="ID_952766134" CREATED="1706417138868" MODIFIED="1706417138868">
+<node TEXT="Copy()にはtree以外何も渡さない" ID="ID_1081702361" CREATED="1706417367338" MODIFIED="1706417401749">
+<node TEXT="何か渡すことも考えられる" ID="ID_1227095307" CREATED="1706417402206" MODIFIED="1706417409509"/>
+<node TEXT="GCする場合とreplicationする場合で動作を切り替えるとか" ID="ID_431028898" CREATED="1706417409901" MODIFIED="1706417421736"/>
+</node>
+</node>
+<node TEXT="コピーのアルゴリズム" ID="ID_64994373" CREATED="1703491215841" MODIFIED="1703491223454">
+<node TEXT="アルゴリズム" ID="ID_972208221" CREATED="1699849518269" MODIFIED="1699849522647">
+<node TEXT="Stackを使う" ID="ID_799370781" CREATED="1706417204202" MODIFIED="1706417282682">
+<node TEXT="2つのStack" ID="ID_1829045504" CREATED="1706417283299" MODIFIED="1706417289209">
+<node TEXT="nodeStack" ID="ID_651682201" CREATED="1706417210255" MODIFIED="1706417229905">
+<node TEXT="From木を辿るためのStack" ID="ID_1782478294" CREATED="1706417237281" MODIFIED="1706417257704"/>
+</node>
+<node TEXT="inputStack" ID="ID_1409216675" CREATED="1706417230497" MODIFIED="1706417233217">
+<node TEXT="To木にAllocationするための木" ID="ID_602717814" CREATED="1706417260099" MODIFIED="1706417273222"/>
+</node>
+</node>
+<node TEXT="SingleLinkedStack" ID="ID_1528506233" CREATED="1706417294502" MODIFIED="1706417299177"/>
+</node>
+<node TEXT="左側を深さ優先で辿る" ID="ID_239741561" CREATED="1699849525266" MODIFIED="1699849604742">
+<node TEXT="子にcurrentを付け替えて親をnodeStackにpush" ID="ID_1852624670" CREATED="1706417608144" MODIFIED="1706417658172"/>
+<node TEXT="nodeStackはcurrentより以前のノードを持つ" ID="ID_304892775" CREATED="1706417633577" MODIFIED="1706417700399"/>
+<node TEXT="allocateした新しいnodeはinputStackにpush" ID="ID_749123856" CREATED="1706418475694" MODIFIED="1706418497889"/>
+</node>
+<node TEXT="アロケートしたノードは別のContext上に作る" ID="ID_573859973" CREATED="1699849620905" MODIFIED="1699849638042">
+<node TEXT="GCのため" ID="ID_259949416" CREATED="1699849638520" MODIFIED="1699849668501"/>
+<node TEXT="Copy後古いContextを消す" ID="ID_1297792398" CREATED="1699849646521" MODIFIED="1699849693755"/>
+<node TEXT="メモリ管理をモナドで表していることになる" ID="ID_152951728" CREATED="1699849705089" MODIFIED="1699849715878"/>
+<node TEXT="ALLOCで別のContextに書き込むようにしたいな" ID="ID_1289215093" CREATED="1706417832741" MODIFIED="1706417849017"/>
+</node>
+<node TEXT="リーフまで降りたらroot方向に木を戻る" ID="ID_1233772087" CREATED="1699849731393" MODIFIED="1699849765553">
+<node TEXT="Stack pop" ID="ID_1907664340" CREATED="1699849765982" MODIFIED="1699849773214"/>
+<node TEXT="右側を呼び出す" ID="ID_1658933965" CREATED="1699849789218" MODIFIED="1699849803550"/>
+</node>
+</node>
+</node>
+<node TEXT="コード説明" ID="ID_1352482727" CREATED="1704630501155" MODIFIED="1704630507416">
+<node TEXT="ALLOCATEの部分" ID="ID_933840077" CREATED="1706418297855" MODIFIED="1706418365645"/>
+<node TEXT="stackの操作" ID="ID_1586156552" CREATED="1706418375086" MODIFIED="1706418391025">
+<node TEXT="結構面倒......" ID="ID_1797610218" CREATED="1706418380222" MODIFIED="1706418386258"/>
+</node>
+<node TEXT="copied flag" ID="ID_1969296096" CREATED="1706418407467" MODIFIED="1706418411865"/>
+<node TEXT="CodeGear数" ID="ID_1895007656" CREATED="1706419226010" MODIFIED="1706419230666"/>
+<node TEXT="swap" ID="ID_1623826858" CREATED="1706419333510" MODIFIED="1706419355159">
+<node TEXT="木の切り替え" ID="ID_1128223367" CREATED="1706419356104" MODIFIED="1706419360642"/>
+</node>
+<node TEXT="それぞれのCodeGearの説明" ID="ID_1842361863" CREATED="1706419379317" MODIFIED="1706419389831">
+<node TEXT="up" ID="ID_1622585016" CREATED="1706419390124" MODIFIED="1706419396255"/>
+<node TEXT="leftDown" ID="ID_1893485106" CREATED="1706419396762" MODIFIED="1706419399051"/>
+<node TEXT="rightDown" ID="ID_1843132193" CREATED="1706419399509" MODIFIED="1706419403818"/>
+<node TEXT="swap" ID="ID_11264463" CREATED="1706419404827" MODIFIED="1706419406275"/>
+</node>
+<node TEXT="記述時に気づいた言語バグ" ID="ID_696764717" CREATED="1706418932388" MODIFIED="1706418940900">
+<node TEXT="ifにてnextを持つCGへのgotoをするとうまく変換されない" ID="ID_1841484842" CREATED="1706418941366" MODIFIED="1706418994628"/>
+<node TEXT="gotoする時にCGを3つ以上チェーンできない" ID="ID_694782376" CREATED="1706419095962" MODIFIED="1706419119983">
+<node TEXT="tree-&gt;nodeStack-&gt;push" ID="ID_319569355" CREATED="1706419141188" MODIFIED="1706419149014"/>
+</node>
+</node>
+</node>
+<node TEXT="動作確認" ID="ID_793097790" CREATED="1706419438278" MODIFIED="1706419442565">
+<node TEXT="テストケース" ID="ID_596576048" CREATED="1706420024765" MODIFIED="1706420029622"/>
+</node>
+<node TEXT="証明のしやすさについて" ID="ID_2776247" CREATED="1703492904417" MODIFIED="1703492910899">
+<node TEXT="Stackの使用に関して" ID="ID_432827984" CREATED="1703492856041" MODIFIED="1703492863503">
+<node TEXT="使用していることを明示しているので問題ない" ID="ID_203410953" CREATED="1706418581660" MODIFIED="1706418592724"/>
+<node TEXT="それはそれで証明する必要があるんだけども" ID="ID_1283008974" CREATED="1706418601289" MODIFIED="1706418613023"/>
+<node TEXT="単方向結合だからStackが必要になってる" ID="ID_375847761" CREATED="1706418656484" MODIFIED="1706418674708"/>
+<node TEXT="ノードを双方向結合すれば...いやむずいか" ID="ID_1860358006" CREATED="1706418675221" MODIFIED="1706418808704"/>
+<node TEXT="状態はある程度に限られる" ID="ID_1218545539" CREATED="1706418867539" MODIFIED="1706418877317"/>
+</node>
+</node>
+</node>
+</node>
+<node TEXT="評価" POSITION="left" ID="ID_186645686" CREATED="1706418118012" MODIFIED="1706418120523">
+<node TEXT="スタックを使ってることに関して" ID="ID_1617928125" CREATED="1706417138929" MODIFIED="1706417138929"/>
+<node TEXT="フラグメンテーション解消できてないことにかんして" ID="ID_912797279" CREATED="1706417138929" MODIFIED="1706417138929"/>
+<node TEXT="GearsFileSystemで重要なCopyの機能を実装できた" ID="ID_1040965600" CREATED="1706418258268" MODIFIED="1706418270889"/>
+<node TEXT="copy機能が追加されたことにより信頼性を確保する機能が実装できるようになるだろう" ID="ID_759285029" CREATED="1706424528708" MODIFIED="1706424548485"/>
+<node TEXT="今回は簡易的なGCに留まる" ID="ID_945220922" CREATED="1706424556818" MODIFIED="1706424564389"/>
+<node TEXT="ここまで動作確認はした" ID="ID_1964377761" CREATED="1706424650365" MODIFIED="1706424656184"/>
+</node>
 </node>
 </map>