Mercurial > hg > Papers > 2024 > matac-master
annotate marp-slide/slide.md @ 74:8c087f2ae631
...
| author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 14 Feb 2024 09:44:07 +0900 |
| parents | c4b013299ff6 |
| children | c6d41c973c8a |
| rev | line source |
|---|---|
| 72 | 1 --- |
| 2 marp: true | |
| 3 theme: cr | |
| 4 paginate: true | |
| 5 --- | |
| 6 | |
| 7 <!-- 全体の流れ | |
| 8 - 目的 | |
| 9 - 基礎概念 | |
| 10 - 問題提起 -> 解決 の繰り返し | |
| 11 - 評価 --> | |
| 12 | |
| 13 # GearsOSのファイルシステムにおける GCとレプリケーション | |
| 14 | |
| 15 <!-- | |
| 16 スピーカーノート | |
| 17 --> | |
| 18 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
19 琉球大学 理工学研究科 工学専攻 知能情報プログラム |
| 72 | 20 河野研究室 |
| 21 | |
| 22 又吉 雄斗 | |
| 23 | |
| 24 --- | |
| 25 | |
| 26 <!-- 目的 --> | |
| 27 | |
| 28 ## システム全体の信頼性を上げたい | |
| 29 | |
| 30 - システムの構成要素全体の信頼性を上げる必要がある | |
| 31 - アプリケーション | |
| 32 - OS | |
| 33 - ファイルシステム | |
| 34 - DB | |
| 35 - メモリとSSD | |
| 36 - 分散ノード | |
| 37 - ネットワーク | |
| 38 | |
| 39 --- | |
| 40 | |
| 41 ## Gears OSを使って実現する | |
| 42 | |
| 43 - CodeGear | |
| 44 - 処理の単位 | |
| 45 - DataGear | |
| 46 - データの単位 | |
| 47 - metaGear | |
| 48 - データの整合性 | |
| 49 - 資源管理 | |
| 50 | |
| 51 --- | |
| 52 | |
| 53 ## 信頼性を上げる方法 | |
| 54 | |
| 55 - 証明 | |
| 56 - GearsAgdaを使ってinvariantを証明する | |
| 57 - テスト | |
| 58 - モデル検査 | |
| 59 - システムの構成要素全体にこれらの方法を適用したい | |
| 60 - 既存システムの信頼性における問題点の解決 | |
| 61 | |
| 62 --- | |
| 63 | |
| 64 <!-- ここからGears OSの基礎概念だと明示する --> | |
| 65 | |
| 66 ## Continuation based C | |
| 67 | |
| 68 - Cの下位言語である | |
| 69 - 処理の単位 CodeGear | |
| 70 - データの単位 DataGear | |
| 71 - ノーマルレベルとメタレベルの切り分け | |
| 72 - gotoによる軽量継続 | |
| 73 | |
| 74 --- | |
| 75 | |
| 76 ## CodeGearとmetaCodeGearの関係 | |
| 77 | |
| 78 - ノーマルレベルとメタレベルの存在 | |
| 79 | |
| 80  | |
| 81 | |
| 82 --- | |
| 83 | |
| 84 ## Context | |
| 85 | |
| 86 - Gears OS上全てのCodeGear，DataGearの参照を持つ | |
| 87 - OS上の処理の実行単位 | |
| 88 - プロセスに相当 | |
| 89 - Gearの概念ではmetaDataGearに当たる | |
| 90 - ノーマルレベルから直接参照されない | |
| 91 - metaCodeGearから参照される | |
| 92 | |
| 93 --- | |
| 94 | |
| 95 ## 3種類のGears OS | |
| 96 | |
| 97 - GearsAgda(Agda) | |
| 98 - 形式手法による信頼性の向上 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
99 - CbC x.v6 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
100 - スタンドアロンOS |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
101 - Gears OS(CbC) ← 今回の実装対象 |
| 72 | 102 - ユーザーレベルタスクマネージメント |
| 103 | |
| 104 --- | |
| 105 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
106 ## GearsAgdaとGearsOSの対応 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
107 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
108 - GearsOSのCodeGearと直接対応している |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
109 - GearsAgdaでRedBlackTreeの証明が進められている |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
110 - find完了、insert証明中 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
111 - GearsOSの構造はRedBlackTreeが多くを占める |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
112 |
| 74 | 113 GearsAgdaでRedBlackTreeが証明できれば、GearsOSのファイルシステムの大部分を証明したことになる |
| 72 | 114 |
| 115 --- | |
| 116 | |
| 117 ## CodeGear遷移の流れ | |
| 118 | |
| 119  | |
| 120 | |
| 121 --- | |
| 122 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
123 ## 非破壊RedBlackTree |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
124 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
125  |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
126 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
127 --- |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
128 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
129 <!-- ここまでがGears OSの基礎概念だと明示する --> |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
130 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
131 ## GearsFilesystem |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
132 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
133 - GearsOSで書かれたファイルシステム |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
134 - i-nodeによるディレクトリシステム |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
135 - 分散ファイルシステムの通信機能 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
136 - 非破壊RedBlackTreeで構成される |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
137 - ディスク上とメモリ上のデータ構造を統一する |
| 72 | 138 |
| 139 --- | |
| 140 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
141 ## ファイルシステムの信頼性 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
142 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
143 - 電源断時にデータが残るpersistency |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
144 - データを書き込めたかどうかを判定するatomic write |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
145 - ノード喪失時にデータを保護する多重性 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
146 - 複数のコピーを調停するコミット機構 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
147 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
148 --- |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
149 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
150 ## メモリ管理や多重性の機能がない |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
151 |
| 74 | 152 <!-- それぞれが何のためにあるのか説明する感じでやると良い --> |
| 153 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
154 メモリ管理 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
155 |
| 74 | 156 - アロケーション |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
157 - GC(ガベージコレクション) |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
158 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
159 多重性 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
160 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
161 - レプリケーション |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
162 - バックアップ |
| 72 | 163 |
| 164 | |
| 165 --- | |
| 166 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
167 ## メモリ管理や多重性の機能の要件 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
168 |
| 74 | 169 <!-- 照明のしやすさの維持が唐突な感じ |
| 170 動作の正しさがわかりやすい実装で証明しやすく --> | |
| 171 | |
| 172 - 信頼性を上げたい | |
| 173 - 証明のしやすい実装 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
174 - データの持続性 |
| 74 | 175 - 持続性のあるストレージにちゃんとコピーする |
| 176 - 適切なタイミングでコピーを行う | |
| 177 - 非破壊RedBlackTreeのメモリ管理 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
178 - 非破壊RedBlackTreeは履歴を全て持つ |
| 74 | 179 - 過去の履歴分のメモリを解放する必要がある |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
180 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
181 --- |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
182 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
183 ## GearsOSにおけるGC |
| 74 | 184 <!-- --> |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
185 CopyingGCを採用する |
| 74 | 186 - 新しいContextのメモリに新規にコピーする |
| 187 - 古いContextをそのまま全部解放する | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
188 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
189 --- |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
190 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
191 ## GearsOSにおけるレプリケーション |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
192 |
| 74 | 193 <!-- --> |
| 194 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
195 単純に木をコピーする |
| 74 | 196 複数のストレージに同時に木を置く |
| 197 そのうちの一部は持続的なストレージにする | |
| 198 システム起動時には必要な分をメモリにコピーする | |
| 199 | |
| 200 トランザクションも考慮する | |
| 201 | |
| 202 --- | |
| 203 | |
| 204 ## RedBlackTreeのトランザクション | |
| 205 | |
| 206 - 木のルートのすげ替えがトランザクションになる | |
| 207 - read | |
| 208 - write | |
| 72 | 209 |
| 210 --- | |
| 211 | |
| 212 ## copyRedBlackTreeの実装をした | |
| 213 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
214 - RedBlackTreeのコピーを行う |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
215 - GCやレプリケーションの機能のために木のコピーが必要 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
216 |
| 72 | 217 --- |
| 218 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
219 ## copyRedBlackTreeによって出来ること |
| 72 | 220 |
| 221 多重性やメモリ管理に関する機能を追加できる | |
| 222 GC(defragmentation) | |
| 223 レプリケーション | |
| 224 バックアップ | |
| 225 | |
| 226 --- | |
| 227 | |
| 228 ## Tree InterfaceのAPIとして実装 | |
| 229 | |
| 230 --- | |
| 231 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
232 ## コピーのアルゴリズム詳細 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
233 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
234  |
| 72 | 235 |
| 236 --- | |
| 237 | |
| 238 ## アロケーション部分 | |
| 239 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
240  |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
241 |
| 72 | 242 --- |
| 243 | |
| 244 ## swap | |
| 245 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
246  |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
247 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
248 --- |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
249 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
250 ## 実行方法 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
251 |
| 72 | 252 --- |
| 253 | |
| 254 ## 評価 | |
| 255 | |
| 256 非破壊RedBlackTreeの増大抑制できる | |
| 257 コピーするだけなので木が持続的 | |
| 258 課題点 | |
| 259 同一Contextへコピーしている | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
260 コピーの正しさ |
| 74 | 261 Stack使っているので余計なメモリを消費する |
| 262 Stackも非破壊であるという問題がある | |
| 263 -> 証明しやすさを優先しているから | |
| 264 Stackが非破壊である意味があまりない？のでここを破壊でやる。 | |
| 72 | 265 |
| 266 --- | |
| 267 | |
| 268 ## 今後の研究方針 | |
| 269 | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
270 別Contextコピー |
| 74 | 271 GearsAgdaでの記述 |
| 272 Stack領域の圧縮 | |
| 273 - Stackの再利用？ | |
|
73
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
274 GC，レプリケーションの実装 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
275 多重性以外の機能 |
|
c4b013299ff6
outline(slide & poster)
matac42 <matac@cr.ie.u-ryukyu.ac.jp>
parents:
72
diff
changeset
|
276 |
| 72 | 277 --- |
| 278 | |
| 279 ## まとめ | |
| 280 | |
| 74 | 281 - copyRedBlackTreeを実装した |
| 282 - それにより多重性を確保できるようになった | |
| 283 - 多重性はシステムの信頼性を向上させる | |
| 284 - 非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった |