# HG changeset patch
# User matac42 <matac@cr.ie.u-ryukyu.ac.jp>
# Date 1706591829 -32400
# Node ID e45254ac5d48f33a8dbb367a16b99211de9e6c17
# Parent  49c1503c917646499c230cff92ac0c303580cf06
fix abstract

diff -r 49c1503c9176 -r e45254ac5d48 Paper/chapter/abstract.tex
--- a/Paper/chapter/abstract.tex	Mon Jan 29 18:45:13 2024 +0900
+++ b/Paper/chapter/abstract.tex	Tue Jan 30 14:17:09 2024 +0900
@@ -4,28 +4,39 @@
 定理証明やモデル検査などで信頼性を保証することを目的としたGearsOSを開発している．
 OSの重要な機能の一つにファイルシステムが存在し，
 GearsOSにおいても分散ファイルシステムの仕組みやi-nodeベースのファイルシステムの実装がされてきた．
-しかし，現状のGearsOSのファイルシステムにはレプリケーションやバックアップなどの
-信頼性に関する機能が実装されていない．
-これらをファイルシステムのレベルで実装することで，
-より確実にデーターの多重性を確保できると考えられるため実装したい．
-また，GearsOSではメモリとディスク上のデータを同一にし，
-データの一貫性を確保することを考えている．
-そのため，ファイルシステムにおいてもガベージコレクションなどのメモリ管理機能が重要となる．
-しかし，そのような機能は現状存在しない．
+しかし，現状のGearsOSのファイルシステムにはデータの多重性を確保するレプリケーションやバックアップの機能や，
+メモリリークやメモリのフラグメンテーションを解消するガベージコレクション機能が存在しない．
+よって，これらをGearsOSのファイルシステムのレベルで実装することで，
+より確実にデータの多重度やメモリの安全性の向上を図ることができると考える．
+ガベージコレクションやレプリケーションを実装するにはデータをコピーする機能が必要不可欠である．
+GearsOSではデータをRedBlackTreeの形式で保持するため，
+RedBlackTreeをコピーすることによってデータのコピーを行うことができる．
+しかし，GearsOSのRedBlackTreeには木をコピーする機能が存在しない．
 本研究では，ファイルシステムのレプリケーションやガベージコレクションなどの機能を実装するために必要な
-RedBlackTreeのコピー機能について設計，構築，考察を行う．
+RedBlackTreeのコピー機能について設計，構築，考察と
+それを用いたレプリケーションやガベージコレクション機能の設計，考察を行う．
 RedBlackTreeのコピーでそれぞれの機能を統一的に実装することで，
 よりシンプルでデータの一貫性が確保された，
 定理証明などの形式手法を適用しやすいシステムを実現することを目指す．
 
+
 \chapter*{Abstract}
 
-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.
+In our research lab, we are developing GearsOS, 
+aimed at ensuring reliability through the use of Continuation based C (CbC) for theorem proving and model checking. 
+A critical component of any operating system is its file system, 
+and in GearsOS, there has been implementation of mechanisms for a distributed file system and i-node based file system structures. 
+However, the current GearsOS file system lacks features for data replication and backup to ensure data redundancy, 
+as well as garbage collection functionalities to resolve memory leaks and memory fragmentation. 
+Therefore, by implementing these features at the file system level of GearsOS, 
+we aim to more reliably enhance data redundancy and memory safety.
+For the implementation of garbage collection and replication, 
+the capability to copy data is essential. 
+In GearsOS, data is stored in the form of a RedBlackTree. 
+Hence, copying the RedBlackTree enables data duplication. 
+However, GearsOS's RedBlackTree currently lacks the functionality to duplicate the tree itself. 
+This research involves the design, construction, and examination of the required RedBlackTree copy functionality for implementing file system replication and garbage collection. 
+Further, we explore the design and examination of replication and garbage collection functionalities using this capability. 
+By uniformly implementing these functionalities through RedBlackTree copying, 
+we aim to realize a simpler system with consistent data, 
+more conducive to formal methods applications such as theorem proving.
\ No newline at end of file
diff -r 49c1503c9176 -r e45254ac5d48 Paper/master_paper.pdf
Binary file Paper/master_paper.pdf has changed