Mercurial > hg > Papers > 2024 > matac-master

--- a/Paper/master_paper.lol	Mon Feb 12 15:13:00 2024 +0900
+++ b/Paper/master_paper.lol	Mon Feb 12 17:54:36 2024 +0900
@@ -1,12 +1,12 @@
 \contentsline {lstlisting}{\numberline {2.1}CbCのプログラム例}{8}{}%
 \contentsline {lstlisting}{\numberline {3.1}Queueのインターフェース}{12}{}%
 \contentsline {lstlisting}{\numberline {3.2}Interfaceの呼び出し}{13}{}%
-\contentsline {lstlisting}{\numberline {3.3}Queueのインターフェース}{13}{}%
+\contentsline {lstlisting}{\numberline {3.3}Queueのインターフェース}{14}{}%
 \contentsline {lstlisting}{\numberline {3.4}SingleLinkedQueueの型定義}{15}{}%
 \contentsline {lstlisting}{\numberline {3.5}Treeの仕様}{15}{}%
 \contentsline {lstlisting}{\numberline {3.6}RedBlackTreeの実装}{16}{}%
 \contentsline {lstlisting}{\numberline {3.7}RedBlackTreeの実装の型定義}{16}{}%
-\contentsline {lstlisting}{\numberline {3.8}Nodeの型定義}{17}{}%
+\contentsline {lstlisting}{\numberline {3.8}Nodeの型定義}{18}{}%
 \contentsline {lstlisting}{\numberline {3.9}ALLOCATEの定義}{18}{}%
 \contentsline {lstlisting}{\numberline {5.1}実行するCodeGearの切り替えのコード}{29}{}%
 \contentsline {lstlisting}{\numberline {6.1}Tree Interfaceの使用定義(Copy追加後)}{34}{}%
Binary file Paper/master_paper.pdf has changed
--- a/Paper/master_paper.tex	Mon Feb 12 15:13:00 2024 +0900
+++ b/Paper/master_paper.tex	Mon Feb 12 17:54:36 2024 +0900
@@ -232,7 +232,7 @@

 GearsOSには現在3つの種類がある．
 1つ目が形式手法による信頼性の向上を目的とした，GearsAgdaと呼ばれるGearsOSである\cite{gearsagda}．
-これは，Agdaによって実装されており，
+これは，定理証明支援系であるAgdaによって実装されており，
 森 逸汰によるGearsAgdaによるRed Black Treeの検証などの取り組みがされている\cite{garbtree}．
 2つ目はスタンドアロンOSの開発を目的とした，CbC\_xv6と呼ばれるGearsOSがある\cite{cbcxv6}．
 これは，教育用に開発されたx.v6\cite{xv6}をCbCで書き換える形で実装している．
@@ -245,6 +245,15 @@
 ファイルシステムのレプリケーションやGC機能の実装を考える．
 以下，GearsOSはユーザーレベルタスクマネジメント実装のGearsOSを指す．

+\section{GearsOSとGearsAgda}
+
+GearsAgdaではRedBlackTreeの証明が進められており，
+それはGearsOSの信頼性の保証につながっている．
+GearsAgdaはGearsOSの実行単位CodeGearと直接対応しており，
+GearsAgdaでRedBlackTreeを証明できれば，GearsOSの大部分の構造を証明できたことになる．
+なぜならば，GearsOSの構造の多くはRedBlackTreeで構成されているからである．
+RedBlackTreeの証明の現状はfindの証明が完了し，insertの証明を進めているところである．
+
 \section{メタ処理を記述するmetaGear}

 図\ref{fig:meta-cgdg}はCodeGearの遷移とMetaCodeGearの関係を表している．
@@ -656,6 +665,11 @@
 データのバックアップやシステム自体のレプリケーションをすることが挙げられる．
 メモリ管理の機能としてはガーベージコレクションが挙げられる．
 ガベージコレクションは通常プログラム言語のレイヤで行われる．
+GearsFilesystemはメモリとディスクを同等に扱うので，
+ここにおけるGCとはFilesystem Fragmentationを解消するためのdefragmentation機能であるとも言える．
+Filesystem Fragmentationはパフォーマンスの低下につながるため，
+FragPickerといったdefragmentationツールが開発されるなど，
+現代的なファイルシステムにおいても必要な機能である\cite{10.1145/3611386}．

 現状のGearsOSには分散ファイルシステムの通信機能やUnix Likeな
 インターフェースを持つi-nodeファイルシステムの基本機能は存在するものの，
--- a/Paper/reference.bib	Mon Feb 12 15:13:00 2024 +0900
+++ b/Paper/reference.bib	Mon Feb 12 17:54:36 2024 +0900
@@ -206,4 +206,24 @@
   articleno  = {9},
   numpages   = {32},
   keywords   = {B-trees, RAID, concurrency, copy-on-write, filesystem, shadowing, snapshots}
+}
+
+@article{10.1145/3611386,
+  author     = {Park, Jonggyu and Eom, Young Ik},
+  title      = {Filesystem Fragmentation on Modern Storage Systems},
+  year       = {2023},
+  issue_date = {November 2023},
+  publisher  = {Association for Computing Machinery},
+  address    = {New York, NY, USA},
+  volume     = {41},
+  number     = {1–4},
+  issn       = {0734-2071},
+  url        = {https://doi.org/10.1145/3611386},
+  doi        = {10.1145/3611386},
+  abstract   = {Filesystem fragmentation has been one of the primary reasons for computer systems to get slower over time. However, there have been rapid changes in modern storage systems over the past decades, and modern storage devices such as solid state drives have different mechanisms to access data, compared with traditional rotational ones. In this article, we revisit filesystem fragmentation on modern computer systems from both performance and fairness perspectives. According to our extensive experiments, filesystem fragmentation not only degrades I/O performance of modern storage devices, but also incurs various problems related to I/O fairness, such as performance interference. Unfortunately, conventional defragmentation tools are designed primarily for hard disk drives and thus generate an unnecessarily large amount of I/Os for data migration. To mitigate such problems, this article present FragPicker, a new defragmentation tool for modern storage devices. FragPicker analyzes the I/O behaviors of each target application and defragments only necessary pieces of data whose migration can contribute to performance improvement, thereby effectively minimizing the I/O amount for defragmentation. Our evaluation with YCSB workload-C shows FragPicker reduces the total amount of I/O for defragmentation by around 66\% and the elapsed time by around 84\%, while showing a similar level of defragmentation effect.},
+  journal    = {ACM Trans. Comput. Syst.},
+  month      = {dec},
+  articleno  = {3},
+  numpages   = {27},
+  keywords   = {Linux I/O stack, storage systems, Filesystem fragmentation}
 }
\ No newline at end of file