Mercurial > hg > Papers > 2019 > mitsuki-master

--- a/paper/abstract.tex	Fri Feb 08 14:39:46 2019 +0900
+++ b/paper/abstract.tex	Fri Feb 08 17:23:51 2019 +0900
@@ -1,5 +1,4 @@
 %OS研究会のまま、要相談
-%これ俺のも par goto 書くの？
 \chapter*{要旨}
 現代の OS では拡張性と信頼性を両立させることが要求されている。
 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。
@@ -19,5 +18,28 @@
 ハードウェア上でメタレベルの処理、および並列実行を可能とするために、
 Raspberry Pi 上での Gears OS の実装についての考察も行う。

+ハードウェア上でのメタレベルの計算や並列実行を行うために、基本的な OS の機能を揃えたうえ、
+シンプルである xv6 を Gears OS に置き換えることによって実現させる。
+
 \chapter*{Abstract}
 %英語論文
+Contemporary OS is required to achieve both scalability and reliability.
+We are designing Gears OS with the goal of guaranteeing reliability for normal level computation and realizing extensibility with meta level computation.
+
+Gears OS describes applications and OS themselves with Continuation based C (CbC).
+In addition to normal processing, the description of the program under the OS includes memory management, queuing of threads, management of the network,
+There is a process that must be described such as error handling.
+These computation are called meta computation.
+In order to describe the meta computation separately from normal computation, we propose a unit called Code Gear, Data Gear.
+CbC describes the program in units of Code Gear and Data Gear.
+
+It is necessary to flexibly reuse Code Gear and Data Gear to describe systems and applications.
+At this time it is desirable that it is possible to separate API and implementation connecting functions.
+In order to guarantee the reliability of the Gears OS, it is necessary to provide a formatted module system.
+
+In this paper, we describe the module system using Interface,
+In order to enable meta computation and parallel execution on hardware,
+We also consider the implementation of Gears OS on Raspberry Pi.
+
+In order to meta computation on hardware and execute it in parallel, basic OS functions are aligned,
+It is realized by replacing simple xv 6 with Gears OS.
--- a/paper/conclusion.tex	Fri Feb 08 14:39:46 2019 +0900
+++ b/paper/conclusion.tex	Fri Feb 08 17:23:51 2019 +0900
@@ -1,5 +1,7 @@
 \chapter{結論}
-本論文では Gears OS のプロトタイプの設計と実装、メタ計算である Context と stub の生成を行う Perl スクリプトの記述、並列実行機構の実装を行った。
+本論文では Gears OS のプロトタイプの設計と実装、メタ計算である Context と stub の生成を行う Perl スクリプトの記述を行った。
+さらに Raspberry Pi 上での Gears OS 実装の考察、xv6 の機能の一部を CbC で書き換えを行った。
+
 Code Gear 、Data Gear を処理とデータの単位として用いて Gears OS を設計した。
 Code Gear、Data Gear にはメタ計算を記述するための Meta Code Gear、Meta Data Gear が存在する。
 メタ計算を Meta Code Gear、によって行うことでメタ計算を階層化して行うことができる。
@@ -15,18 +17,18 @@
 Context は使用する Code Gear、Data Gear をすべて格納している Meta Data Gear である。
 通常の計算から Context を直接扱うことはセキュリティ上好ましくない。
 このため Context から必要なデータを取り出して Code Gear に接続する Meta Code Gear である stub Code Gear を定義した。
-stub Code Gear は Code Gear 毎に記述され、Code Gear 間の遷移に挿入される。
-
-並列処理を行う際は Context を生成し、 Code Gear と Input/Output Data Gear を Context に設定して TaskManager 経由で各 Worker の SynchronizedQueue に送信される。
-Context の設定はメタレベルの記述になるため、ノーマルレベルでは par goto 文という CbC の goto 文に近い記述で並列処理を行える。
-この par goto は通常のプログラミングの関数呼び出しのように扱える。
+stub Code Gear は Code Gear 毎に記述され、Code Gear 間の遷移の前に挿入される。

 これらのメタ計算の記述は煩雑であるため Perl スクリプトによる自動生成を行なった。
 これにより Gears OS のコードの煩雑さは改善され、ユーザーレベルではメタを意識する必要がなくなった。

+ハードウェア上での Gears OS の実装を実現させるために Raspberry Pi 上での実装を考察した。
+比較的シンプルな OS である xv6 を CbC に書き換えることにした。
+
+xv6 を CbC で書き換えることによって、実行可能な CbC プログラムで記述された OS がそのまま、
+状態遷移モデルによるモデル検査、Agda による定理証明が可能となる。
+
 今後の課題は、
-Go、との比較から、 Gears OS が1CPU での動作が遅いということがわかった。
-Gears OS は par goto 文を使用することで Context を生成し、並列処理を行う。
-しかし、Context はメモリ空間の確保や使用する全ての Code/Data Gear を設定する必要があり、生成にある程度の時間がかかってしまう。
-そこで、 par goto のコンパイルタイミングで実行する Code Gear のフローをモデル検査で解析し、処理が軽い場合はContext を生成せずに、関数呼び出しを行う等の最適化を行なうといったチューニングが必要である。
-
+現在は xv6 のシステムコールの一部のみの書き換えと、設計のみしか行っていないので、カーネル全ての書き換えと、
+Gears OS の TaskManager の置き換えを行い、Gears OS の機能を xv6 に組み込む必要がある。
+また、xv6-rpi は QEMU のみの動作でしか確認してないため、実機上での動作を行う必要がある。
--- a/paper/introduction.tex	Fri Feb 08 14:39:46 2019 +0900
+++ b/paper/introduction.tex	Fri Feb 08 17:23:51 2019 +0900
@@ -52,7 +52,7 @@
 ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。
 CbC は関数呼出時の暗黙の環境(Environment)を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。
 これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。
-これらを用いて、検証された Gears OS を構築したい。
+これらを用いて、検証された Gears OS\cite{gears} を構築したい。
 図\ref{fig:MetaGear}。

 本論文では、Gears OS の要素である Code Gear、Data Gear、そして、Meta Code Gear 、Meta Data Gear の構成を示す。これらは、CbC に変換されて実行される。
@@ -64,7 +64,7 @@
 Gears OS の記述はそのまま Agda に落ちる。
 Code Gear、Data Gear を用いた言語である CbC で記述することによって検証された OS を実装することができる。

-従来の研究でメタ計算を用いる場合は、関数型言語では Monad を用いる\cite{Moggi:1989:CLM:77350.77353}。これは Hakell では実行時の環境を記述する構文として使われている。
+従来の研究でメタ計算を用いる場合は、関数型言語では Monad を用いる\cite{moggi-monad}。これは Hakell では実行時の環境を記述する構文として使われている。
 OS の研究では、メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。Python や Haskell による記述をノーマルレベルとして
 採用した OS の検証の研究もある\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}。
 SMIT などのモデル検査を OS の検証に用いた例もある\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}。
@@ -77,7 +77,7 @@

 また、本研究では Gears の記述をモジュール化するために Interface を導入した。
 さらに並列処理の記述用にpar goto 構文を導入する。
-これらの機能は Agda 上で継続を用いた関数型プログラムに対応するようになっている。
+これらの機能は Agda \cite{agda} 上で継続を用いた関数型プログラムに対応するようになっている。\cite{agda-ryokka}
 これにより Code Gear、Data Gear の Agda による証明が可能となり、
 モデル検査を入れられるように Gears OS の構築を行った。

@@ -90,3 +90,8 @@
 \end{figure}

 本研究では Gears OS のモジュール化の仕組みである Interface を用いた Gears OS の構築を行った。
+
+また、ハードウェア上でメタレベルの処理、および並列実行を可能とするために、Raspberry Pi\cite{rpi} 上での Gears OS の実装についての考察を行う。
+ここでは、Linax 等に比べてシンプルである xv6 の機能の一部を Gears OS に置き換えることで実現させる。
+xv6 は UNIX V6 を x86 へ再実装したものであるが、ここでは Raspberry pi 用に移植した xv6-rpi\cite{xv6rpi} を用いて実装した。
+
--- a/paper/master_paper.sty	Fri Feb 08 14:39:46 2019 +0900
+++ b/paper/master_paper.sty	Fri Feb 08 17:23:51 2019 +0900
@@ -210,10 +210,10 @@
       (主　査)　　　　和田　知久
       \vskip 2 em
       \underline{　　　　　　　　　　　　　　　　　　印}\\
-      (副　査)　　　　名嘉村　盛和
+      (副　査)　　　　岡\UTF{FA11} 威生
       \vskip 2 em
       \underline{　　　　　　　　　　　　　　　　　　印}\\
-      (副　査)　　　　長田　智和
+      (副　査)　　　　赤嶺　有平
       \vskip 2 em
       \underline{　　　　　　　　　　　　　　　　　　印}\\
       (副　査)　　　　河野　真治
--- a/paper/master_paper.tex	Fri Feb 08 14:39:46 2019 +0900
+++ b/paper/master_paper.tex	Fri Feb 08 17:23:51 2019 +0900
@@ -11,7 +11,7 @@

 %\input{dummy.tex} %% font

-\jtitle{Gears OS のモジュール化と並列 API}
+\jtitle{継続を基本とした言語による OS のモジュール化}
 \etitle{} % 英文例題まだ
 \year{2019年 3月}
 \eyear{March 2019}
--- a/paper/reference.bib	Fri Feb 08 14:39:46 2019 +0900
+++ b/paper/reference.bib	Fri Feb 08 17:23:51 2019 +0900
@@ -1,136 +1,31 @@
-@inproceedings{queue,
-    author = {Michael, Maged M. and Scott, Michael L.}, title = {Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algorithms},
-    booktitle = {Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing},
-    series = {PODC '96},
-    year = {1996},
-    isbn = {0-89791-800-2},
-    location = {Philadelphia, Pennsylvania, USA},
-    pages = {267--275},
-    numpages = {9},
-    url = {http://doi.acm.org/10.1145/248052.248106},
-    doi = {10.1145/248052.248106},
-    acmid = {248106},
-    publisher = {ACM},
-    address = {New York, NY, USA},
-    keywords = {compare_and_swap, concurrent queue, lock-free, multiprogramming, non-blocking},
-}
+@article{os,
+    author = {Andrew S.Tanenbaum, Herbert Bos},
+    title = "{Modern Operating Systems}",
+    publisher = {PEASON},
+    year = {2015},
+}

-@inproceedings{agda,
- author = {Norell, Ulf},
- title = {Dependently Typed Programming in Agda},
- booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
- series = {TLDI '09},
- year = {2009},
- isbn = {978-1-60558-420-1},
- location = {Savannah, GA, USA},
- pages = {1--2},
- numpages = {2},
- url = {http://doi.acm.org/10.1145/1481861.1481862},
- doi = {10.1145/1481861.1481862},
- acmid = {1481862},
- publisher = {ACM},
- address = {New York, NY, USA},
- keywords = {dependent types, programming},
+@misc{rpi,
+title     = "{Raspberry Pi — Teach, Learn, and Make with Raspberry Pi}",
+howpublished    = {https://www.raspberrypi.org}
 }

-@inproceedings{Chen:2015:UCH:2815400.2815402,
- author = {Chen, Haogang and Ziegler, Daniel and Chajed, Tej and Chlipala, Adam and Kaashoek, M. Frans and Zeldovich, Nickolai},
- title = {Using Crash Hoare Logic for Certifying the FSCQ File System},
- booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles},
- series = {SOSP '15},
- year = {2015},
- isbn = {978-1-4503-3834-9},
- location = {Monterey, California},
- pages = {18--37},
- numpages = {20},
- url = {http://doi.acm.org/10.1145/2815400.2815402},
- doi = {10.1145/2815400.2815402},
- acmid = {2815402},
- publisher = {ACM},
- address = {New York, NY, USA},
-}
-
-@inproceedings{Klein:2009:SFV:1629575.1629596,
- author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
- title = {seL4: Formal Verification of an OS Kernel},
- booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
- series = {SOSP '09},
- year = {2009},
- isbn = {978-1-60558-752-3},
- location = {Big Sky, Montana, USA},
- pages = {207--220},
- numpages = {14},
- url = {http://doi.acm.org/10.1145/1629575.1629596},
- doi = {10.1145/1629575.1629596},
- acmid = {1629596},
- publisher = {ACM},
- address = {New York, NY, USA},
- keywords = {isabelle/hol, l4, microkernel, sel4},
-}
-
-
-@inproceedings{Sigurbjarnarson:2016:PVF:3026877.3026879,
- author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi},
- title = {Push-button Verification of File Systems via Crash Refinement},
- booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation},
- series = {OSDI'16},
- year = {2016},
- isbn = {978-1-931971-33-1},
- location = {Savannah, GA, USA},
- pages = {1--16},
- numpages = {16},
- url = {http://dl.acm.org/citation.cfm?id=3026877.3026879},
- acmid = {3026879},
- publisher = {USENIX Association},
- address = {Berkeley, CA, USA},
-}
-
-@inproceedings{Yang:2010:SLI:1806596.1806610,
- author = {Yang, Jean and Hawblitzel, Chris},
- title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System},
- booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation},
- series = {PLDI '10},
- year = {2010},
- isbn = {978-1-4503-0019-3},
- location = {Toronto, Ontario, Canada},
- pages = {99--110},
- numpages = {12},
- url = {http://doi.acm.org/10.1145/1806596.1806610},
- doi = {10.1145/1806596.1806610},
- acmid = {1806610},
- publisher = {ACM},
- address = {New York, NY, USA},
- keywords = {operating system, run-time system, type safety, verification},
+@misc{xv6rpi,
+author    = {Zhiyi Wang},
+title     = "{xv6-rpi}",
+howpublished      = "{https://code.google.com/archive/p/xv6-rpi/}",
+year      = {2013}
 }

-@article{atton-ipsj,
-author="比嘉 健太 and 河野 真治",
-title="Verification Method of Programs Using Continuation based C",
-journal="情報処理学会論文誌プログラミング（PRO）",
-ISSN="1882-7802",
-publisher="",
-year="2017",
-month="feb",
-volume="10",
-number="2",
-pages="5-5",
-URL="https://ci.nii.ac.jp/naid/170000148438/en/",
-DOI="",
+@article{
+    cbc,
+    author = "Kaito TOKKMORI and Shinji KONO",
+    title = "Implementing Continuation based language in LLVM and Clang",
+    journal = "LOLA 2015",
+    month = "July",
+    year = 2015
 }

-@article{go,
-author={J. Meyerson},
-journal={IEEE Software},
-title={The Go Programming Language},
-year={2014},
-volume={31},
-number={5},
-pages={104-104},
-keywords={Andrew Gerrand;C;Go;Google;arrays;build times;compilers;garbage collection;golang;imports;interfaces;open source;readability;scalability;slices;standard library;syntax},
-doi={10.1109/MS.2014.127},
-ISSN={0740-7459},
-month={Sept},}
-
 @article{moggi-monad,
     author     = {Moggi, Eugenio},
     title      = {Notions of Computation and Monads},
@@ -150,26 +45,84 @@
     address    = {Duluth, MN, USA},
 }

-@inproceedings{nobu-prosym,
-    author = "大城信康 and 河野真治",
-    title = "Continuation based C の GCC4.6 上の実装について",
-    booktitle = "第53回プログラミング・シンポジウム予稿集",
-    year  = "2012",
-    volume = "2012",
-    pages = "69--78",
-    month = "jan"
+@inproceedings{Yang:2010:SLI:1806596.1806610,
+ author = {Yang, Jean and Hawblitzel, Chris},
+ title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System},
+ booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ series = {PLDI '10},
+ year = {2010},
+ isbn = {978-1-4503-0019-3},
+ location = {Toronto, Ontario, Canada},
+ pages = {99--110},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/1806596.1806610},
+ doi = {10.1145/1806596.1806610},
+ acmid = {1806610},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {operating system, run-time system, type safety, verification},
 }

-@inproceedings{mitsuki-prosym,
-    author = "宮城光希 and 河野真治",
-    title = "Code Gear と Data Gear を持つ Gears OS の設計",
-    booktitle = "第59回プログラミング・シンポジウム予稿集",
-    year  = "2018",
-    volume = "2018",
-    pages = "197--206",
-    month = "jan"
+@inproceedings{Klein:2009:SFV:1629575.1629596,
+ author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
+ title = {seL4: Formal Verification of an OS Kernel},
+ booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
+ series = {SOSP '09},
+ year = {2009},
+ isbn = {978-1-60558-752-3},
+ location = {Big Sky, Montana, USA},
+ pages = {207--220},
+ numpages = {14},
+ url = {http://doi.acm.org/10.1145/1629575.1629596},
+ doi = {10.1145/1629575.1629596},
+ acmid = {1629596},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {isabelle/hol, l4, microkernel, sel4},
+}
+
+@inproceedings{Sigurbjarnarson:2016:PVF:3026877.3026879,
+ author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi},
+ title = {Push-button Verification of File Systems via Crash Refinement},
+ booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation},
+ series = {OSDI'16},
+ year = {2016},
+ isbn = {978-1-931971-33-1},
+ location = {Savannah, GA, USA},
+ pages = {1--16},
+ numpages = {16},
+ url = {http://dl.acm.org/citation.cfm?id=3026877.3026879},
+ acmid = {3026879},
+ publisher = {USENIX Association},
+ address = {Berkeley, CA, USA},
 }

+@article{
+    agda-ryokka,
+    author = "Hokama MASATAKA and Shinji KONO",
+    title = "GearsOS の Hoare Logic をベースにした検証手法",
+    journal = "ソフトウェアサイエンス研究会",
+    month = "Jan",
+    year = 2019
+}
+
+@inproceedings{agda,
+ author = {Norell, Ulf},
+ title = {Dependently Typed Programming in Agda},
+ booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
+ series = {TLDI '09},
+ year = {2009},
+ isbn = {978-1-60558-420-1},
+ location = {Savannah, GA, USA},
+ pages = {1--2},
+ numpages = {2},
+ url = {http://doi.acm.org/10.1145/1481861.1481862},
+ doi = {10.1145/1481861.1481862},
+ acmid = {1481862},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {dependent types, programming},
+}

 @InProceedings{llvm,
 author    = {Chris Lattner and Vikram Adve},
@@ -180,54 +133,27 @@
 year      = {2004}
 }

-@article{kaito-lola,
-    author  = "Kaito, Tokumori and Shinji, Kono",
-    title   = "Implementing Continuation based language in LLVM and Clang",
-    journal = "LOLA 2015, Kyoto",
-    month   = "July",
-    year    =  2015
-
-}
-
-@article{kkb-sigos,
-    author  = "小久保翔平 and 伊波立樹 and 河野真治",
-    title   = "Monad に基づくメタ計算を基本とする Gears OS の設計",
-    journal = "第133回情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
-    month   = "May",
-    year    = 2015
-}
-
-@article{ikkun-sigos,
-    author  = "東恩納琢偉 and 伊波立樹 and 河野真治",
-    title   = "Gears OS における並列処理",
-    journal = "第140回 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
-    month   = "May",
-    year    = 2017
+@manual{gcc,
+author = "{GNU Compiler Collection (GCC) Internals}",
+title ="{http://gcc.gnu.org/onlinedocs/gccint/}",
 }

-@misc{openmp,
-    title = "OpenMP: Simple, portable, scalable SMP programming",
-    howpublished = {\url{http://www.openmp.org,}},
-    note = {Accessed: 2018/02/05(Mon)}
-}
-
-@misc{cuda,
-    title = {CUDA Zone | NVIDIA Developer},
-    howpublished = {\url{https://developer.nvidia.com/cuda-zone}},
-    note = {Accessed: 2018/02/05(Mon)}
+@article{
+    gears,
+    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
+    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
+    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+    month = "May",
+    year = 2016
 }

-@mastersthesis{utah-master,
-    author = "徳森海斗",
-    title  = "LLVM Clang 上の Continuation based C コンパイラ の改良",
-    school = "琉球大学 大学院理工学研究科 情報工学専攻",
-    year   = "2016"
+@manual{arm,
+author     = "{ARM Architecture Reference Manual}",
+title  = "{http://infocenter.arm.com/help/topic/com.arm.\\doc.subset.architecture.reference/index.html}"
 }

-@mastersthesis{kkb-master,
-    author = "小久保 翔平",
-    title  = "Code Segment と Data Segment を持つ Gears OS の 設計",
-    school = "琉球大学 大学院理工学研究科 情報工学専攻",
-    year   = "2016"
+@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},
 }
-
--- a/paper/xv6.tex	Fri Feb 08 14:39:46 2019 +0900
+++ b/paper/xv6.tex	Fri Feb 08 17:23:51 2019 +0900
@@ -1,15 +1,15 @@
 \chapter{xv6 の CbC への書き換え}
-Gears OS をハードウェア上で実装するために、ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry Pi\cite{rpi} 上で Gears OS 実装したい。
+Gears OS をハードウェア上で実装するために、ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry Pi 上で Gears OS 実装したい。
 ハードウェア上でのメタレベルの計算や並列実行を行うために、Linax 等に比べてシンプルである xv6 の機能の一部を Gears OS に置き換えることで実現させる。
 xv6 は UNIX V6 を x86 へ再実装したものであるが、
-ここでは xv6 を Raspberry pi 用に移植した xv6\_rpi\cite{xv6rpi} を用いて実装する。
+ここでは xv6 を Raspberry pi 用に移植した xv6-rpi を用いて実装する。

 Xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。
 Xv6 はプロセス、仮想メモリ、カーネルとユーザの分離、割り込み、ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、
 シンプルで学習しやすい。

 \section{Raspberry Pi}
-Raspberry Pi\cite{rpi} は ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである。
+Raspberry Pi は ARM プロセッサを搭載したシングルボードコンピュータである。
 教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。
 ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。
 HDMI 出力や USB ポートも備えており、開発に最適である。