@misc{gearsos,
  title        = {GearsOS},
  author       = {並列信頼研究室},
  organization = {琉球大学},
  howpublished = {http://www.cr.ie.u-ryukyu.ac.jp/hg/Gears/Gears/}
}

@misc{cbcllvm,
  title        = {CbC},
  author       = {並列信頼研究室},
  organization = {琉球大学},
  howpublished = {http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC\_llvm/}
}
@misc{cbcxv6,
  title        = {CbC\_xv6},
  author       = {並列信頼研究室},
  organization = {琉球大学},
  howpublished = {http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC\_xv6/}
}

@misc{gearsagda,
  title        = {GearsAgda},
  author       = {並列信頼研究室},
  organization = {琉球大学},
  howpublished = {http://www.cr.ie.u-ryukyu.ac.jp/hg/Gears/GearsAgda/}
}

@article{garbtree,
  author  = {森 逸汰, 河野 真治(琉球大学)},
  title   = {GearsAgdaによるRed Black Treeの検証},
  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
  month   = {May},
  year    = 2023
}

@article{gearscodemngment,
  author  = {仲吉 菜々子, 河野 真治(琉球大学)},
  title   = {Gears OSのCodeGear Management},
  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
  month   = {May},
  year    = 2023
}

@article{cbc,
  author  = {河野 真治},
  title   = {継続を持つCの下位言語によるシステム記述},
  journal = {日本ソフトウェア科学会第17回大会論文集},
  month   = {September},
  year    = 2000
}

@article{cr,
  author      = {伊波 立樹},
  title       = {GearsOSの並列処理},
  institution = {琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科},
  journal     = {修士 (工学) 学位論文},
  month       = {March},
  year        = 2018
}

@article{gears,
  author      = {清水隆博},
  title       = {GearsOSのメタ計算},
  institution = {琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科},
  journal     = {修士 (工学) 学位論文},
  month       = {March},
  year        = 2021
}

@article{file,
  author  = {一木 貴裕, 河野 真治(琉球大学)},
  title   = {GearsOSの分散ファイルシステムの設計},
  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
  month   = {May},
  year    = 2021
}

@article{cfile,
  author      = {一木 貴裕},
  title       = {GearsOSの分散ファイルシステム設計},
  institution = {琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科},
  journal     = {修士 (工学) 学位論文},
  month       = {March},
  year        = 2022
}

@article{modelcheck,
  author  = {東恩納 琢偉，奥田 光希，河野 真治(琉球大学)},
  title   = {Gears OSでモデル検査を実現する手法について},
  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
  month   = {May},
  year    = 2020
}

@misc{xv6,
  author       = {{Russ Cox, Frans Kaashoek, Robert Morris}},
  title        = {xv6 a simple, Unix-like teaching operating system},
  howpublished = {https://pdos.csail.mit.edu/6.828/2018/xv6/book-rev11.pdf}
}

@misc{christie,
  author  = {{河野 真治}},
  title   = {分散フレームワーク Christie と分散木構造データベースJungle},
  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
  month   = {May},
  year    = 2018
}

@misc{directory,
  author  = {又吉 雄斗，河野 真治(琉球大学)},
  title   = {GearsOSにおけるinodeを用いたファイルシステムの構築},
  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
  month   = {May},
  year    = 2022
}

@misc{zengin,
  title        = {全国銀行データ通信システムの障害について},
  author       = {一般社団法人 全国銀行資金決済ネットワーク},
  howpublished = {https://www.zengin-net.jp/announcement/pdf/announcement\_20231201.pdf}
}

@misc{ana,
  title        = {4月3日に発生した国内線システム不具合の原因及び再発防止策について},
  author       = {全日本空輸株式会社},
  howpublished = {https://www.anahd.co.jp/group/pr/202304/notification-2.html}
}

@misc{glory,
  title        = {2月14日から2月19日にかけて発生した電子マネー決済システム（iD決済）の障害に関するお詫びとお知らせ},
  author       = {グローリー株式会社},
  howpublished = {https://www.glory.co.jp/news/detail/id=2017}
}

@inproceedings{10.1145/1353482.1353504,
  author    = {Golbeck, Ryan M. and Davis, Samuel and Naseer, Immad and Ostrovsky, Igor and Kiczales, Gregor},
  title     = {Lightweight virtual machine support for AspectJ},
  year      = {2008},
  isbn      = {9781605580449},
  publisher = {Association for Computing Machinery},
  address   = {New York, NY, USA},
  url       = {https://doi.org/10.1145/1353482.1353504},
  doi       = {10.1145/1353482.1353504},
  abstract  = {Advice weaving can be efficiently supported with only lightweight enhancements to existing Virtual Machines. Performing weaving at the Java bytecode (JBC) level while preserving appropriate metadata enables the VM to understand the AspectJ-specific semantics of the code and optimize it. This allows the overhead of advice weaving and performing non-local advice dispatch optimization to occur prior to runtime. It also allows the VM to perform optimizations that are unavailable to a bytecode level weaver.An experimental implementation shows that this approach can take advantage of previously known macro optimizations of expensive constructs, including cflow, as well as micro optimizations including those based on improved type analysis unavailable to JBC-based advice dispatch. A thorough benchmark evaluation confirms that the use of this architecture does not result in runtime performance overhead and benefits from the implemented optimizations.},
  booktitle = {Proceedings of the 7th International Conference on Aspect-Oriented Software Development},
  pages     = {180–190},
  numpages  = {11},
  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}
}

@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}
}