# HG changeset patch
# User autobackup
# Date 1621005003 -32400
# Node ID 4732666a0dce6ae27c7ee90608047d7a0e9a1002
# Parent  27e5f3533d9c91e6cc923a2db0788215157ec401
backup 2021-05-15

diff -r 27e5f3533d9c -r 4732666a0dce user/matac42/note/2021/05/14.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/note/2021/05/14.md	Sat May 15 00:10:03 2021 +0900
@@ -0,0 +1,30 @@
+# 研究目的
+
+アプリケーションの信頼性を保証するために、アプリケーションが動作するOSの信頼性を高める必要がある。
+
+本研究室では、信頼性に重きを置いたGearsOSを開発している。
+信頼性とは
+
+- どのユーザーがどのようなファイル操作をしたかわかること
+- logが残ること
+- item 操作の辻褄があっていること
+
+を指す。
+
+GearsOSはノーマルレベル、メタレベルの処理を切り分けることができるCbC(Continuation Based C)で記述されている。
+
+GearsOSにはAgdaで記述された、GearsAgdaがある。
+GearsAgdaはOSの信頼性を検証するために作成された。
+しかしながら、Agdaはcontinuationでなく、速度も遅い。
+よって、信頼性が検証されたGearsAgdaをCbCに変換する必要がある。
+
+また、GearsOSには現在未実装の機能があり、その一つにファイルシステムが挙げられる。信頼性を確保するため、ファイルシステムは
+
+- ファイルシステム全体のトランザクション化
+- ファイルシステム全体のバックアップ\&ロギング
+
+を取り入れたい。
+
+本卒業研究では、GearsAgdaのCbCへの変換後、ファイルシステムの実装を目指す。
+
+# その他