Mercurial > hg > Papers > 2024 > matac-master

comparison marp-slide/slide.md @ 74:8c087f2ae631

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author matac42 <matac@cr.ie.u-ryukyu.ac.jp>
date Wed, 14 Feb 2024 09:44:07 +0900
parents c4b013299ff6
children c6d41c973c8a
comparison
equal deleted inserted replaced
73:c4b013299ff6 74:8c087f2ae631
108 - GearsOSのCodeGearと直接対応している 108 - GearsOSのCodeGearと直接対応している
109 - GearsAgdaでRedBlackTreeの証明が進められている 109 - GearsAgdaでRedBlackTreeの証明が進められている
110 - find完了、insert証明中 110 - find完了、insert証明中
111 - GearsOSの構造はRedBlackTreeが多くを占める 111 - GearsOSの構造はRedBlackTreeが多くを占める
112 112
113 GearsAgdaでRedBlackTreeが証明できれば、GearsOSの大部分を証明したことになる 113 GearsAgdaでRedBlackTreeが証明できれば、GearsOSのファイルシステムの大部分を証明したことになる
114 114
115 --- 115 ---
116 116
117 ## CodeGear遷移の流れ 117 ## CodeGear遷移の流れ
118 118
147 147
148 --- 148 ---
149 149
150 ## メモリ管理や多重性の機能がない 150 ## メモリ管理や多重性の機能がない
151 151
152 <!-- それぞれが何のためにあるのか説明する感じでやると良い -->
153
152 メモリ管理 154 メモリ管理
153 155
156 - アロケーション
154 - GC(ガベージコレクション) 157 - GC(ガベージコレクション)
155 158
156 多重性 159 多重性
157 160
158 - レプリケーション 161 - レプリケーション
161 164
162 --- 165 ---
163 166
164 ## メモリ管理や多重性の機能の要件 167 ## メモリ管理や多重性の機能の要件
165 168
169 <!-- 照明のしやすさの維持が唐突な感じ
170 動作の正しさがわかりやすい実装で証明しやすく -->
171
172 - 信頼性を上げたい
173 - 証明のしやすい実装
166 - データの持続性 174 - データの持続性
167 - 証明のしやすさの維持 175 - 持続性のあるストレージにちゃんとコピーする
168 - データを破壊しない 176 - 適切なタイミングでコピーを行う
169 - 非破壊RedBlackTreeの増大抑制 177 - 非破壊RedBlackTreeのメモリ管理
170 - 非破壊RedBlackTreeは履歴を全て持つ 178 - 非破壊RedBlackTreeは履歴を全て持つ
171 - そのままにすると増大し、メモリを圧迫する 179 - 過去の履歴分のメモリを解放する必要がある
172 180
173 --- 181 ---
174 182
175 ## GearsOSにおけるGC 183 ## GearsOSにおけるGC
176 184 <!-- -->
177 CopyingGCを採用する 185 CopyingGCを採用する
186 - 新しいContextのメモリに新規にコピーする
187 - 古いContextをそのまま全部解放する
178 188
179 --- 189 ---
180 190
181 ## GearsOSにおけるレプリケーション 191 ## GearsOSにおけるレプリケーション
182 192
193 <!-- -->
194
183 単純に木をコピーする 195 単純に木をコピーする
196 複数のストレージに同時に木を置く
197 そのうちの一部は持続的なストレージにする
198 システム起動時には必要な分をメモリにコピーする
199
200 トランザクションも考慮する
201
202 ---
203
204 ## RedBlackTreeのトランザクション
205
206 - 木のルートのすげ替えがトランザクションになる
207 - read
208 - write
184 209
185 --- 210 ---
186 211
187 ## copyRedBlackTreeの実装をした 212 ## copyRedBlackTreeの実装をした
188 213
231 非破壊RedBlackTreeの増大抑制できる 256 非破壊RedBlackTreeの増大抑制できる
232 コピーするだけなので木が持続的 257 コピーするだけなので木が持続的
233 課題点 258 課題点
234 同一Contextへコピーしている 259 同一Contextへコピーしている
235 コピーの正しさ 260 コピーの正しさ
236 261 Stack使っているので余計なメモリを消費する
262 Stackも非破壊であるという問題がある
263 -> 証明しやすさを優先しているから
264 Stackが非破壊である意味があまりない？のでここを破壊でやる。
237 265
238 --- 266 ---
239 267
240 ## 今後の研究方針 268 ## 今後の研究方針
241 269
242 別Contextコピー 270 別Contextコピー
271 GearsAgdaでの記述
272 Stack領域の圧縮
273 - Stackの再利用？
243 GC，レプリケーションの実装 274 GC，レプリケーションの実装
244 多重性以外の機能 275 多重性以外の機能
245 276
246 --- 277 ---
247 278
248 ## まとめ 279 ## まとめ
249 280
250 copyRedBlackTreeを実装した 281 - copyRedBlackTreeを実装した
251 それにより多重性を確保できるようになった 282 - それにより多重性を確保できるようになった
252 多重性はシステムの信頼性を向上させる 283 - 多重性はシステムの信頼性を向上させる
253 非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった 284 - 非破壊RedBlackTreeの増大抑制により実用的なシステム構築が可能になった