Binary file Paper/master_paper.pdf has changed

--- a/Paper/reference.bib	Wed Feb 07 17:24:31 2024 +0900
+++ b/Paper/reference.bib	Wed Feb 07 17:39:37 2024 +0900
@@ -164,4 +164,62 @@
   keywords  = {AspectJ, aspect-oriented programming},
   location  = {Brussels, Belgium},
   series    = {AOSD '08}
+}
+
+@article{10.1007/s00165-006-0022-3,
+  author     = {Joshi, Rajeev and Holzmann, Gerard J.},
+  title      = {A mini challenge: build a verifiable filesystem},
+  year       = {2007},
+  issue_date = {Jun 2007},
+  publisher  = {Springer-Verlag},
+  address    = {Berlin, Heidelberg},
+  volume     = {19},
+  number     = {2},
+  issn       = {0934-5043},
+  url        = {https://doi.org/10.1007/s00165-006-0022-3},
+  doi        = {10.1007/s00165-006-0022-3},
+  abstract   = {We propose tackling a “mini challenge” problem: a nontrivial verification effort that can be completed in 2–3 years, and will help establish notational standards, common formats, and libraries of benchmarks that will be essential in order for the verification community to collaborate on meeting Hoare’s 15-year verification grand challenge. We believe that a suitable candidate for such a mini challenge is the development of a filesystem that is verifiably reliable and secure. The paper argues why we believe a filesystem is the right candidate for a mini challenge and describes a project in which we are building a small embedded filesystem for use with flash memory.},
+  journal    = {Form. Asp. Comput.},
+  month      = {jun},
+  pages      = {269–272},
+  numpages   = {4},
+  keywords   = {Formal verification, Filesystem design, Verification grand challenge}
+}
+
+@inproceedings{10.1145/3477132.3483581,
+  author    = {Liu, Jing and Rebello, Anthony and Dai, Yifan and Ye, Chenhao and Kannan, Sudarsun and Arpaci-Dusseau, Andrea C. and Arpaci-Dusseau, Remzi H.},
+  title     = {Scale and Performance in a Filesystem Semi-Microkernel},
+  year      = {2021},
+  isbn      = {9781450387095},
+  publisher = {Association for Computing Machinery},
+  address   = {New York, NY, USA},
+  url       = {https://doi.org/10.1145/3477132.3483581},
+  doi       = {10.1145/3477132.3483581},
+  abstract  = {We present uFS, a user-level filesystem semi-microkernel. uFS takes advantage of a high-performance storage development kit to realize a fully-functional, crash-consistent, highly-scalable filesystem, with relative developer ease. uFS delivers scalable high performance with a number of novel techniques: careful partitioning of in-memory and on-disk data structures to enable concurrent access without locking, inode migration for balancing load across filesystem threads, and a dynamic scaling algorithm for determining the number of filesystem threads to serve the current workload. Through measurements, we show that uFS has good base performance and excellent scalability; for example, uFS delivers nearly twice the throughput of ext4 for LevelDB on YCSB workloads.},
+  booktitle = {Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles},
+  pages     = {819–835},
+  numpages  = {17},
+  keywords  = {Microkernel, Filesystem, Direct Access},
+  location  = {Virtual Event, Germany},
+  series    = {SOSP '21}
+}
+
+@article{10.1145/2501620.2501623,
+  author     = {Rodeh, Ohad and Bacik, Josef and Mason, Chris},
+  title      = {BTRFS: The Linux B-Tree Filesystem},
+  year       = {2013},
+  issue_date = {August 2013},
+  publisher  = {Association for Computing Machinery},
+  address    = {New York, NY, USA},
+  volume     = {9},
+  number     = {3},
+  issn       = {1553-3077},
+  url        = {https://doi.org/10.1145/2501620.2501623},
+  doi        = {10.1145/2501620.2501623},
+  abstract   = {BTRFS is a Linux filesystem that has been adopted as the default filesystem in some popular versions of Linux. It is based on copy-on-write, allowing for efficient snapshots and clones. It uses B-trees as its main on-disk data structure. The design goal is to work well for many use cases and workloads. To this end, much effort has been directed to maintaining even performance as the filesystem ages, rather than trying to support a particular narrow benchmark use-case.Linux filesystems are installed on smartphones as well as enterprise servers. This entails challenges on many different fronts.---Scalability. The filesystem must scale in many dimensions: disk space, memory, and CPUs.---Data integrity. Losing data is not an option, and much effort is expended to safeguard the content. This includes checksums, metadata duplication, and RAID support built into the filesystem.---Disk diversity. The system should work well with SSDs and hard disks. It is also expected to be able to use an array of different sized disks, which poses challenges to the RAID and striping mechanisms.This article describes the core ideas, data structures, and algorithms of this filesystem. It sheds light on the challenges posed by defragmentation in the presence of snapshots, and the tradeoffs required to maintain even performance in the face of a wide spectrum of workloads.},
+  journal    = {ACM Trans. Storage},
+  month      = {aug},
+  articleno  = {9},
+  numpages   = {32},
+  keywords   = {B-trees, RAID, concurrency, copy-on-write, filesystem, shadowing, snapshots}
 }
\ No newline at end of file