Mercurial > hg > Papers > 2021 > okud-thesis

--- a/paper/chapter/chapter3.tex	Mon Feb 15 03:21:24 2021 +0900
+++ b/paper/chapter/chapter3.tex	Mon Feb 15 05:00:58 2021 +0900
@@ -3,7 +3,7 @@


 \section{GearsOS}
-GearsOS\cite{Gears}は当研究室で信頼性と拡張性をテーマに開発を行っているsOSである。
+GearsOS\cite{Gears}は当研究室で信頼性と拡張性をテーマに開発を行っているOSである。
 GearsOSはContinuation based C(CbC)によって記述されている。
 当研究室では、GearsOSの信頼性とCbCの有効性を示すために、基本的な機能を揃えたOSであるxv6をCbCで置き換えを行っている。
 これにより、OSの個々のシステムコールが持つ状態を明確にすることができると考えている。
--- a/paper/chapter/chapter4.tex	Mon Feb 15 03:21:24 2021 +0900
+++ b/paper/chapter/chapter4.tex	Mon Feb 15 05:00:58 2021 +0900
@@ -2,7 +2,7 @@


 \section{UEFI}
-UEFI\cite{uefi}とは、Unified Extensible Firmware Interfaceの略で
+UEFI\cite{uefi}は、Unified Extensible Firmware Interfaceの略で
 OSとプラットフォームファームウェアの間のソフトウェアインタフェースを定義する仕様である。
 1990年代半ばにIntelによってBIOSに変わるEFI仕様が開発された。
 2005年にIntel、AMD、Apple、Microsoftなどの企業からなるUnified EFI　Forumという業界団体のもとUEFIが開発された。
--- a/paper/chapter/chapter5.tex	Mon Feb 15 03:21:24 2021 +0900
+++ b/paper/chapter/chapter5.tex	Mon Feb 15 05:00:58 2021 +0900
@@ -28,4 +28,10 @@
     \end{center}
     \caption{OS boot 処理}
     \label{bootos}
-\end{figure}
\ No newline at end of file
+\end{figure}
+
+\section{xv6 bootloader}
+実装中
+
+
+
--- a/paper/chapter/introduction.tex	Mon Feb 15 03:21:24 2021 +0900
+++ b/paper/chapter/introduction.tex	Mon Feb 15 05:00:58 2021 +0900
@@ -11,16 +11,23 @@
 これらの問題を解決するためにUEFIが開発された。
 UEFIは、2TBを超える大きなディスクからブートでき、高速にブートできる。
 CPUに依存しないアーキテクチャとドライバを持ちネットワークも使用可能な柔軟なプレOS環境が利用できる。
-今後、Legacy BIOSからUEFIへの移行が急速に進むだろう。\\\
+今後、Legacy BIOSからUEFIへの移行が急速に進むだろう。
+また、UEFIはApplicationを持っていて、それはC言語などの高級言語で記述可能なので個人で開発がしやすい。
+
 当研究室では、信頼性と拡張性をテーマにGearsOSを開発している。
 GearsOSはContinuation based C(CbC)によってアプリケーションとOSそのものを記述している。
 現在、CbCで証明可能なOSを実装するために、xv6のCbCの書き換えを行っている。
 xv6は Legacy OSなため、UEFIから起動することができない。
 UEFIからxv6を起動させることができれば、拡張性が大きく広がる。
-本研究では、ARMで動くシングルコンピュータであるRaspberryPi上にUEFIからGearsOSをブートさせることを目指している。
+さらに、UEFIは接続されているデバイスの認識を持てるので、マウスやキーボードを使えるように
+UEFI Applicationを使い、デバイスドライバを作れる。
+これにより、利便性もよくなる。
+本研究では、ARMで動くシングルコンピュータであるRaspberryPi上にUEFIからGearsOSをブートさせることにより
+様々な組み込みシステムに対してGearsOSを応用できる様にすることである。


-\section{論文の構成}
+

+
Binary file prepaper/fig/CbC.png has changed
Binary file prepaper/pre.pdf has changed
--- a/prepaper/pre.tex	Mon Feb 15 03:21:24 2021 +0900
+++ b/prepaper/pre.tex	Mon Feb 15 05:00:58 2021 +0900
@@ -23,23 +23,88 @@

 \renewcommand{\abstractname}{Abstract}
 \begin{document}
-\title{タイトル}
-\author{175733E 氏名 {宮平 賢}\\ 指導教員 : {河野 真治} }
+\title{GearsOSのBootに関する研究}
+\author{175733E 氏名 {奥田光希}\\ 指導教員 : {河野 真治} }
 \date{}
 \twocolumn [
 \maketitle
 \begin{onecolabstract}
-
-abstract
-
+We are proposing GearsOS, which uses Meta-calculus to improve reliability in our lab.
+We are implementing GearsOS on Raspberry Pi based on x.v6.
+Currently, GearsOS is booted from BIOS, and we would like to migrate it to UEFI.
+If we can migrate to UEFI, we can avoid dependencies on CPU and other devices.
+GearsOS is written in CbC (Continuation based C), so it is not affected by CPU or device.
+This will make it possible to apply GearsOS to a variety of embedded systems.
 \end{onecolabstract}]
 \thispagestyle{fancy}

 \section{はじめ}
+2017年、Intel社は2020年までにLegacy BIOSとUEFIへの互換を非推奨とし、互換モジュールのCSMを削除すると発表した。\cite{IntelNews}
+Legacy BIOSはPCの進化に伴い、致命的な問題点が発生する。
+問題点の一つとして、拡張性がないことがあげられる。EthernetやUSBにつながるディスクなど、新たにブートデバイスが追加されるたびに,
+OSのブートローダを変更しなければならない。またマザーボードごとに、ファームウェアをアセンブラで開発する必要がある。
+また、1MBのメモリ制限により、セキュリティを含めたシステム機能の強化が困難であるためセキュリティにも問題がある。
+これらの問題を解決するためにUEFIが開発された。
+UEFIは、2TBを超える大きなディスクからブートでき、高速にブートできる。
+CPUに依存しないアーキテクチャとドライバを持ちネットワークも使用可能な柔軟なプレOS環境が利用できる。
+今後、Legacy BIOSからUEFIへの移行が急速に進むだろう。
+また、UEFIはApplicationを持っていて、それはC言語などの高級言語で記述可能なので個人で開発がしやすい。
+
+当研究室では、信頼性と拡張性をテーマにGearsOSを開発している。
+GearsOSはContinuation based C(CbC)によってアプリケーションとOSそのものを記述している。
+現在、CbCで証明可能なOSを実装するために、xv6のCbCの書き換えを行っている。
+xv6は Legacy OSなため、UEFIから起動することができない。
+UEFIからxv6を起動させることができれば、拡張性が大きく広がる。
+さらに、UEFIは接続されているデバイスの認識を持てるので、マウスやキーボードを使えるように
+UEFI Applicationを使い、デバイスドライバを作れる。
+これにより、利便性もよくなる。
+本研究では、ARMで動くシングルコンピュータであるRaspberryPi上にUEFIからGearsOSをブートさせることにより
+様々な組み込みシステムに対してGearsOSを応用できる様にすることである。
+
+\section{Continuation based C(CbC)}
+Continuation based C(CbC)\cite{CbC}は、当研究室で開発を行っているプログラミング言語である。
+CbCは、C言語の下位言語であり、関数呼び出しではなく継続を導入している。
+CbCでは、関数の代わりにCodeGearという単位でプログラミングを行う。
+CodeGearは入力と出力を持ち、CbCでは引数が入出力になっている。
+CodeGearから次のCodeGearへとgotoによる継続で遷移して処理を行い、引数として出力を与える。
+
+
+\subsection{CbC GCC ARM CrossCompile}
+GCC上で実装されたCbCのARM CrossCompile環境をSingularity\cite{singularity}で構築した。
+CrossCompileは、Compilerが動作している以外のプラットフォーム向けに
+実行ファイルを生成する機能を持ったCompile手法である。
+これにより、CbCで実装されたプログラムをRaspberry Pi上で実装ができる様になった。
+
+\section{GearsOS}
+GearsOS\cite{Gears}は当研究室で信頼性と拡張性をテーマに開発を行っているOSである。
+GearsOSはContinuation based C(CbC)によって記述されている。
+当研究室では、GearsOSの信頼性とCbCの有効性を示すために、基本的な機能を揃えたOSであるxv6\cite{xv6}をCbCで置き換えを行っている。
+これにより、OSの個々のシステムコールが持つ状態を明確にすることができると考えている。
+CbCで書き換えられたxv6をRaspberry Pi\cite{raspi}に搭載することでハードウェア上でのメタレベルの計算や並列実行を行える様になる。
+
+
+\section{UEFI}
+UEFI\cite{uefi}は、OSとプラットフォームファームウェアの間のソフトウェアインタフェースを定義する仕様である。
+UEFIは、インタフェース仕様であるため、特定のプロセッサに依存しない。
+C言語などの高級言語で実装することができ、個人でも開発の難易度が低い。
+
+
+UEFIにはApplicationがあり、UEFI Applicationは開発を行うマシンのOSやアーキテクチャに左右されることなく、
+高級言語から直接生成することができる。
+UEFI Applicationを自作することにより、xv6をUEFIでBootさせるBootLoaderを作ったり、xv6のデバイスドライバを作れる様になる。
+
+\section{BootLoader}
+


 \begin{thebibliography}{9}
-  \bibitem{sanko} 参考
+  \bibitem{IntelNews} Intel/Unified EFI Forum, https://www.uefi.org ,2017/11/3.
+  \bibitem{CbC} 清水隆博,河野慎治..xv6の構成要素の継続の分析.情報処理学会研究報告,2020.
+  \bibitem{singularity} https://sylabs.io/singularity
+  \bibitem{Gears} 東恩納 琢偉,河野真治.Gears OSでモデル検査を実現する手法について.情報処理学会研究報告2020
+  \bibitem{xv6} Russ Cox, M Frans Kaashoek, and Robert Morris. Xv6, a simple unix-like teaching operating system,2012.
+  \bibitem{raspi} https://www.raspberrypi.org
+  \bibitem{uefi} https://wiki.osdev.org/UEFI
 \end{thebibliography}