# HG changeset patch # User anatofuz # Date 1588069279 -32400 # Node ID babdf0b27d62d17cc9105c0b0b625d979643b96f # Parent 0eb7e20b76450bf999e9cba51974d487db264151 update mindmap diff -r 0eb7e20b7645 -r babdf0b27d62 .hgignore --- a/.hgignore Tue Apr 28 14:26:03 2020 +0900 +++ b/.hgignore Tue Apr 28 19:21:19 2020 +0900 @@ -274,3 +274,5 @@ *.glstex # End of https://www.gitignore.io/api/latex + +paper/lint diff -r 0eb7e20b7645 -r babdf0b27d62 etc/xv6model.mm --- a/etc/xv6model.mm Tue Apr 28 14:26:03 2020 +0900 +++ b/etc/xv6model.mm Tue Apr 28 19:21:19 2020 +0900 @@ -1,7 +1,81 @@ - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r 0eb7e20b7645 -r babdf0b27d62 etc/xv6model.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/etc/xv6model.svg Tue Apr 28 19:21:19 2020 +0900 @@ -0,0 +1,948 @@ + + +xv6の構成要素の継続の分析目次まとめCbCの導入XV6のファイルシステムの分析XV6 OSの概要OSの信頼性XV6の分析書き換えを行う状態を持つcontextそもそもcontextの種類はどれくらいあるのかkernelのcontextinode cache割り込みのフラグprocessどういう要素をもつべきか書き換えを行う際の状態単位CodeGear同士に移動CodeGearに分割する処理の詳細現状で書き換えたい処理xv6の状態どの様に遷移していく? 何で繊維する?特定の処理における状態数プロセスの状態kernelの状態xv6の概要軽量継続で表現し直す小さなunixファイルシステムelfbreadlogシステムコールselectwriteopenreadx86をサポート今回はarmのものを使うラズパイで動かしたいarmサポートのものもある学習用のOSOSの信頼性状態遷移ベースでのプログラミング既存のOSで信頼性を高めたい箇所を継続ベースで書く軽量継続で書いていく必要があるCbCを使うのに適している形式手法で解決したい状態遷移での表現再利用性各処理の状態が明確になる継続を用いたプログラムになる定理証明モデル検査テストで全て発見するのは難しいOSそのものの信頼性が重要