Mercurial > hg > Papers > 2024 > matac-master
changeset 35:849ec71b87c3
...
| author | matac42 <matac@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 19 Jan 2024 15:34:06 +0900 |
| parents | 78ca77ccccc5 |
| children | 5294b155ad72 |
| files | Paper/chapter/abstract.tex Paper/master_paper.pdf TODO.md |
| diffstat | 3 files changed, 10 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/chapter/abstract.tex Fri Jan 19 15:28:28 2024 +0900 +++ b/Paper/chapter/abstract.tex Fri Jan 19 15:34:06 2024 +0900 @@ -20,4 +20,12 @@ \chapter*{Abstract} -In our laboratory, \ No newline at end of file +In our laboratory, we are developing GearsOS, which aims to ensure reliability through theorem proving and model checking using Continuation based C (CbC). +One of the important functions of an OS is the file system, and in GearsOS, mechanisms of distributed file systems and implementations of i-node based file systems have been done. +However, the current GearsOS file system does not have reliability-related functions such as replication and backup. +We want to implement these at the file system level to ensure more reliable data redundancy. +Also, in GearsOS, we are considering making the data on memory and disk identical to ensure data consistency. +Therefore, memory management functions such as garbage collection are important in the file system. +However, such functions do not currently exist. +In this study, we design, construct, and consider the copy function of RedBlackTree, which is necessary to implement functions such as replication and garbage collection of the file system. +By implementing each function uniformly with the copy of RedBlackTree, we aim to realize a system that is simpler, ensures data consistency, and is easier to apply formal methods such as theorem proving.