Canvas 1

研究目的

アプリケーションの信頼性を保証するために，
+アプリケーションが動作するOSの信頼性を高める必要がある

信頼性確保の方法として定理証明やモデル検査がある

当研究室では，信頼性の保証を目的としたGearsOSを開発している

証明や検証を容易に行えるよう，ファイルシステムのシンプルな実装を考えたい

Header	Header
Text	Text

Header

Text

__code raw_socket_init(){ + int sock = socket(PF_PACKET, SOCK_RAW, htons(ETH_P_ALL)); + if(sock == -1){ + perror("Failed to open socket"); + exit(1); + } + uint8_t buf[1550]; + + goto raw_socket(sock, buf, sizeof(buf)); + } +

研究目的

アプリケーションの信頼性を保証するために，
+アプリケーションが動作するOSの信頼性を高める必要がある

信頼性確保の方法として定理証明やモデル検査がある

当研究室では，信頼性の保証を目的としたGearsOSを開発している

GearsOSで未実装の機能であるファイルシステムの実装を目指す

Header	Header
Text	Text

Header

Text

__code mkdir(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) { - struct FTree* newDirectory = createFileSystemTree(context, gearsDirectory->currentDirectory); - Node* inode = new Node(); - inode->key = gearsDirectory->INodeNumber; - inode->value = newDirectory; - struct FTree* cDirectory = new FTree(); - cDirectory = gearsDirectory->iNodeTree; - goto cDirectory->put(inode, mkdir2); -} +

__code mkdir(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) {
+    struct FTree* newDirectory = createFileSystemTree(context, gearsDirectory->currentDirectory);
+    Node* inode = new Node();
+    inode->key = gearsDirectory->INodeNumber;
+    inode->value = newDirectory;
+    struct FTree* cDirectory = new FTree();
+    cDirectory = gearsDirectory->iNodeTree;
+    goto cDirectory->put(inode, mkdir2);
+}
 
-__code mkdir2(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) {
-    Node* dir = new Node();
-    dir->key = name->value;
-    Integer* iNum = new Integer();
-    iNum->value = gearsDirectory->INodeNumber;
-    dir->value = iNum;
-    gearsDirectory->INodeNumber = gearsDirectory->INodeNumber + 1;
-    struct FTree* cDirectory = new FTree();
-    cDirectory = gearsDirectory->currentDirectory;
-    goto cDirectory->put(dir, next(...));
-}
-
+__code mkdir2(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) {
+    Node* dir = new Node();
+    dir->key = name->value;
+    Integer* iNum = new Integer();
+    iNum->value = gearsDirectory->INodeNumber;
+    dir->value = iNum;
+    gearsDirectory->INodeNumber = gearsDirectory->INodeNumber + 1;
+    struct FTree* cDirectory = new FTree();
+    cDirectory = gearsDirectory->currentDirectory;
+    goto cDirectory->put(dir, next(...));
+}
+

__code mkdir(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) {
+    struct FTree* newDirectory = createFileSystemTree(context, gearsDirectory->currentDirectory);
+    Node* inode = new Node();
+    inode->key = gearsDirectory->INodeNumber;
+    inode->value = newDirectory;
+    struct FTree* cDirectory = new FTree();
+    cDirectory = gearsDirectory->iNodeTree;
+    goto cDirectory->put(inode, mkdir2);
+}
 
-__code mkdir2(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) {
-    Node* dir = new Node();
-    dir->key = name->value;
-    Integer* iNum = new Integer();
-    iNum->value = gearsDirectory->INodeNumber;
-    dir->value = iNum;
-    gearsDirectory->INodeNumber = gearsDirectory->INodeNumber + 1;
-    struct FTree* cDirectory = new FTree();
-    cDirectory = gearsDirectory->currentDirectory;
-    goto cDirectory->put(dir, next(...));
-}
-
+__code mkdir2(struct GearsDirectoryImpl* gearsDirectory, struct Integer* name, __code next(...)) {
+    Node* dir = new Node();
+    dir->key = name->value;
+    Integer* iNum = new Integer();
+    iNum->value = gearsDirectory->INodeNumber;
+    dir->value = iNum;
+    gearsDirectory->INodeNumber = gearsDirectory->INodeNumber + 1;
+    struct FTree* cDirectory = new FTree();
+    cDirectory = gearsDirectory->currentDirectory;
+    goto cDirectory->put(dir, next(...));
+}
+

GearsOSのファイルシステムとDB

研究目的

RedBlackTreeを用いたFSの実装

信頼性の保証を目的としたOS

真ん中タイトル

Bullet Points

Tables

CodeGear Transition

Code

KaTeX

References

GearsOSにおける
inodeを用いたファイルシステムの構築

研究目的

真ん中タイトル

Bullet Points

Tables

CodeGear Transition

Code

References

mkdir

mkdir

GearsOSのファイルシステムとDB

研究目的

RedBlackTreeを用いたFSの実装

信頼性の保証を目的としたOS

真ん中タイトル

Bullet Points

Tables

CodeGear Transition

Code

KaTeX

References

GearsOSにおけるinodeを用いたファイルシステムの構築

研究目的

真ん中タイトル

Bullet Points

Tables

CodeGear Transition

Code

References

mkdir

mkdir

GearsOSにおける
inodeを用いたファイルシステムの構築